1% Revised version of Part II, Chapter 9 of HOL DESCRIPTION 2% Incorporates material from both of chapters 9 and 10 of the old 3% version of DESCRIPTION 4% Written by Andrew Pitts 5% 8 March 1991 6% revised August 1991 7\chapter{Sintassi e Semantica}\label{logic} 8 9\section{Introduzione} 10\label{introduction} 11 12Questo capitolo descrive la sintassi e la semantica a modelli della 13logica supportata dal sistema \HOL{}, che � una variante della 14teoria dei tipi semplici di Church\index{Church, A.} \cite{Church} e 15che sar� d'ora in poi chiamata la logica \HOL{}, o semplicemente \HOL. Il 16meta-linguaggio per questa descrizione sar� l'Italiano, arricchito con 17varie notazioni e convenzioni matematiche. Il liguaggio oggetto 18di questa descrizione � la logica \HOL{}. Si noti che c'� un 19`meta-linguaggio', in un senso differente, associato con la logica 20\HOL\, cio� il linguaggio di programmazione \ML. Questo � il linguaggio usato 21per manipolare la logica \HOL{} da parte degli utenti del sistema. Si spera 22che in base al contesto, non risulti alcuna confusione da questi due usi della 23parola `meta-linguaggio'. Quando l'oggetto dello studio � l'\ML\ (come in 24\cite{sml}), l'\ML\ � il linguaggio oggetto considerato---e 25l'Italiano � di nuovo il meta-linguaggio! 26 27La sintassi di \HOL{} contiene categorie sintattiche di tipi e termini i cui 28elementi sono intesi denotare rispettivamente certi insiemi e elementi 29di insiemi. Questa interpretazione insiemistica sar� sviluppata accanto alla 30descrizione della sintassi di \HOL{}, e nel prossimo capitolo il sistema di dimostrazione 31di \HOL\ sar� mostrato essere valido per il ragionamento circa propriet� 32del modello insiemistico\footnote{Ci sono altri, modelli 33`non standard' di \HOL, che non ci riguarderanno qui.}. Questo modello � dato in 34termini di un insieme di insiemi fisso $\cal U$, che sar� chiamato l'{\em 35universo\/}\index{universo, nella semantica della logica HOL@universo, nella 36semantica della logica \HOL{}\/} e che si assume avere le seguenti 37propriet�. 38\begin{description} 39 40\item[Inhab] Ogni elemento di $\cal U$ � un insieme non vuoto. 41 42\item[Sub] Se $X\in{\cal U}$ e $\emptyset\not=Y\subseteq X$, allora 43$Y\in{\cal U}$. 44 45\item[Prod] Se $X\in{\cal U}$ e $Y\in{\cal U}$, allora $X\times 46Y\in{\cal U}$. L'insieme $X\times Y$ � il prodotto cartesiano, 47consistente di coppie ordinate $(x,y)$ con $x\in X$ e $y\in Y$, con 48l'usuale notazione insiemistica delle coppie ordinate, cio� 49$(x,y)=\{\{x\},\{x,y\}\}$. 50 51\item[Pow] Se $X\in{\cal U}$, allora anche l'insieme potenza 52$P(X)=\{Y:Y\subseteq X\}$ � un elemento di $\cal U$. 53 54\item[Infty] $\cal U$ contiene un distinto insieme infinito $\inds$. 55 56\item[Choice] C'� un elemento distinto $\ch\in\prod_{X\in{\cal 57U}}X$. Gli elementi del prodotto $\prod_{X\in{\cal U}}X$ sono 58funzioni (dipendentemente tipizzate): cos� per tutti gli $X\in{\cal U}$, $X$ � 59non vuoto per {\bf Inhab} e $\ch(X)\in X$ testimonia questo\footnote{[ndt] Il prodotto cartesiano generalizzato $\prod_{X\in{\cal 60U}}X$ � definito come l'insieme di tutte le funzioni che mandano ciascun elemento $X\in{\cal U}$ in 61un qualche elemento di $X$. Queste funzioni si possono, dunque, considerare come se scegliessero per ogni elemento 62$X\in{\cal U}$ un elemento di $X$ rappresentativo di tutto l'insieme $X$ e per 63questo si parla di funzioni di scelta. {\bf Choice} isola una di queste funzioni: $\ch$.}. 64 65\end{description} 66Ci sono alcune conseguenze di queste assunzioni che saranno necessarie. 67Nella teoria degli insiemi le funzioni sono identificate dai loro grafi, che sono 68certi insiemi di coppie ordinate. Cos� l'insieme $X\fun Y$ di tutte le funzioni 69da un insieme $X$ a un insieme $Y$ � un sottoinsieme di $P(X\times Y)$; ed � un 70insieme non vuoto quando $Y$ non � vuoto. Cos� {\bf Sub}, {\bf Prod} e {\bf 71Pow} insieme implicano che $\cal U$ soddisfa anche 72\begin{description} 73 74\item[Fun] Se $X\in{\cal U}$ e $Y\in{\cal U}$, allora $X\fun Y\in{\cal U}$. 75 76\end{description} 77Iterando {\bf Prod}, si ottiene che il prodotto cartesiano di qualsiasi 78numero finito, diverso da zero, di insiemi in $\cal U$ � ancora in $\cal U$. 79$\cal U$ contiene anche il prodotto cartesiano di nessun insieme, il che equivale a 80dire che contiene un insieme di un unico elemento (in virt� di {\bf Sub} applicato 81a qualsiasi insieme in ${\cal U}$---{\bf Infty} garantisce che ce n'� uno); per 82precisione, sar� isolato un particolare insieme di un solo elemento. 83\begin{description} 84 85\item[Unit] $\cal U$ contiene un distinto insieme di un solo elemento $1=\{0\}$. 86 87\end{description} 88Analogamente, a causa di {\bf Sub} e {\bf Infty}, $\cal U$ contiene 89insiemi di due elementi, uno dei quali sar� isolato. 90\begin{description} 91 92\item[Bool] $\cal U$ contiene un distinto insieme di due elementi 93$\two=\{0,1\}$. 94 95\end{description} 96 97Le assunzioni di sopra circa $\cal U$ sono pi� deboli di quelle imposte su un 98universo di insiemi dagli assiomi della 99teoria degli insiemi di Zermelo-Fraenkel\index{teoria degli insiemi Zermelo-Fraenkel} con 100l'Assioma di Scelta (\theory{ZFC})\index{assioma di scelta}\index{ZFC@\ml{ZFC}}, 101principalmente perch� a $\cal U$ non � 102richiesto di soddisfare alcuna forma dell'Assioma di 103Rimpiazzamento\index{assioma di rimpiazzamento}. 104Di fatto, � possibile dimostrare l'esistenza di un insieme 105$\cal U$ con le propriet� di sopra dagli assiomi di \theory{ZFC}. 106(Per esempio si potrebbe considerare $\cal U$ consistere di tutti gli insiemi non vuoti 107nella gerarchia cumulativa di von~Neumann formata prima della fase 108$\omega+\omega$.) Cos�, come per altri pezzi della matematica, � 109possibile in linea di principio dare una versione completamente formale all'interno 110della teoria degli insiemi \theory{ZFC} della semantica della logica \HOL{} che sar� fornita 111di sotto. 112 113\section{Tipi} 114\label{types} 115 116I tipi\index{vincolo di tipo!nella logica HOL@nella logica \HOL{}} della 117logica \HOL{} sono espressioni che denotano insiemi (nell'universo $\cal U$). 118Seguendo la tradizione, 119$\sigma$, possibilmente decorato con sottoscritti o primi, � usato per 120variare su tipi arbitrari. 121 122Ci sono quattro specie di tipi nella logica \HOL{}. Questi possono essere descritti 123informalmente dalla seguente grammatica {\small BNF}, 124in cui $\alpha$ varia 125su variabili di tipo, \textsl{c} varia su tipi atomici e \textsl{op} varia su 126operatori di tipo. 127 128\newlength{\ttX} 129\settowidth{\ttX}{\tt X} 130\newcommand{\tyvar}{\setlength{\unitlength}{\ttX}\begin{picture}(1,6) 131\put(.5,0){\makebox(0,0)[b]{\footnotesize variabili di tipo}} 132\put(0,1.5){\vector(0,1){4.5}} 133\end{picture}} 134\newcommand{\tyatom}{\setlength{\unitlength}{\ttX}\begin{picture}(1,6) 135\put(.5,2.3){\makebox(0,0)[b]{\footnotesize tipi atomici}} 136\put(.5,3.3){\vector(0,1){2.6}} 137\end{picture}} 138\newcommand{\funty}{\setlength{\unitlength}{\ttX}\begin{picture}(1,6) 139\put(.5,1.5){\makebox(0,0)[b]{\footnotesize tipi funzione}} 140\put(.5,0){\makebox(0,0)[b]{\footnotesize (dominio $\sigma_1$, rango $\sigma_2$)}} 141\put(1,2.5){\vector(0,1){3.5}} 142\end{picture}} 143\newcommand{\cmpty}{\setlength{\unitlength}{\ttX}\begin{picture}(1,6) 144\put(2,3.3){\makebox(0,0)[b]{\footnotesize tipi composti}} 145\put(1.9,4.5){\vector(0,1){1.5}} 146\end{picture}} 147% 148$$\sigma\quad ::=\quad {\mathord{\mathop{\alpha}\limits_{\tyvar}}} 149 \quad\mid\quad{\mathord{\mathop{c}\limits_{\tyatom}}} 150 \quad\mid\quad\underbrace{(\sigma_1, \ldots , \sigma_n){op}}_{\cmpty} 151 \quad\mid\quad\underbrace{\sigma_1\fun\sigma_2}_{\funty}$$ 152 153\noindent In maggiore dettaglio, le quattro specie di tipi sono come segue. 154 155\begin{enumerate} 156 157\item {\bf Variabili di tipo:}\index{variabili di tipo, nella logica HOL@variabili di tipo, nella logica \HOL{} logic!forma astratta di} queste stanno per insiemi 158arbitrari nell'universo. Nella formulazione originale di Church della teoria dei tipi 159semplici, le variabili di tipo sono parte del meta-linguaggio e sono usate per 160variare su tipi del linguaggio oggetto. Le dimostrazioni contenenti variabili di tipo 161erano concepite come schemi di dimostrazione (cio� famiglie di dimostrazioni). Per supportare 162tali schemi di dimostrazione {\it all'interno} della logica \HOL{}, le variabili di tipo sono 163state aggiunte al sistema di tipi del linguaggio oggetto\footnote{Questa tecnica 164fu inventata da Robin Milner per la logica oggetto \PPL\ del suo sistema 165\LCF.}. 166 167\item {\bf Tipi atomici:}\index{tipi atomici} questi denotano insiemi fissati nell'universo. Ogni 168teoria determina una particolare collezione di tipi atomici. Per 169esempio, i tipi atomici standard \ty{bool} e \ty{ind} denotano, 170rispettivamente, l'insieme distinto di due elementi $\two$ e 171l'insieme distinto infinito $\inds$. 172 173\item {\bf Tipi composti:}\index{tipi composti, nella logica HOL@tipi composti, nella logica \HOL{}!forma astratta di} questi hanno la 174forma $(\sigma_1,\ldots,\sigma_n)\ty{op}$, dove $\sigma_1$, $\dots$, 175$\sigma_n$ sono i tipi argomento e $op$ � un {\it operatore di tipo\/} 176di ariet� $n$. Gli operatori di tipo denotano operazioni per costruire insiemi. 177Il tipo $(\sigma_1,\ldots,\sigma_n)\ty{op}$ denota l'insieme che risulta 178dall'applicare l'operazione denotata da $op$ agli insiemi denotati da 179$\sigma_1$, $\dots$, $\sigma_n$. Per esempio, 180\ty{list} � un operatore di tipo con ariet� 1. Esso denota l'operazione 181di formare tutte le liste finite di elementi da un dato insieme. Un altro 182esempio � l'operatore \ty{prod} di ariet� 2 che denota 183l'operazione di prodotto cartesiano. Il tipo $(\sigma_1,\sigma_2)\ty{prod}$ 184� scritto come $\sigma_1\times\sigma_2$. 185 186\item {\bf Tipi funzione:}\index{tipi funzione, nella logica HOL@tipi funzione, nella logica \HOL{}!forma astratta di} Se $\sigma_1$ 187e $\sigma_2$ sono tipi, allora $\sigma_1\fun\sigma_2$ � il tipo 188funzione con {\it dominio\/} $\sigma_1$ e {\it rango} $\sigma_2$. Esso 189denota l'insieme di tutte le funzioni (totali) dall'insieme denotato dal suo 190dominio all'insieme denotato dal suo rango. (Nella letteratura 191$\sigma_1\fun\sigma_2$ � scritto senza la freccia e 192alla rovescia--cio� come $\sigma_2\sigma_1$.) Si noti che sintatticamente 193$\fun$ � semplicemente un distinto operatore di tipo di ariet� 2 scritto con 194notazione infissa. E' isolato nella definizione dei tipi \HOL{} 195perch� denoter� sempre la stessa operazione in qualsiasi 196modello di una teoria \HOL{}---contrariamente agli altri operatori di tipo che 197possono essere interpretati in modo differente in modelli differenti. (Si veda 198la Sezione~\ref{semantics of types}.) 199 200\end{enumerate} 201 202Risulta conveniente identificare i tipi atomici con 203tipi composto costruiti con operatori di tipo $0$-ari. Per esempio, 204il tipo atomico \ty{bool} dei valori di verit� pu� essere considerato come 205un'abbreviazione per $()\ty{bool}$. Questa identificazione sar� fatta nei 206dettagli tecnici che seguono, ma nella presentazione informale 207i tipi atomici continueranno ad essere distinti dai tipi composti, 208e $()c$ sar� scritto come $c$. 209 210\subsection{Strutture di tipo} 211\label{type structures} 212\index{struttura di tipo, nella logica HOL@struttura di tipo, nella logica \HOL{}} 213 214Il termine `costante di tipo' � usato per comprendere sia i tipi atomici sia gli operatori 215di tipo. Si assume che sia dato un insieme infinito {\sf 216TyNames} dei {\em nomi delle costanti di tipo\/}. La lettera 217greca $\nu$ � usata per variare su membri arbitrari di {\sf TyNames}, 218si continuer� ad usare \textsl{c} per variare sui nomi dei tipi 219atomici (cio� costanti di tipo $0$-ari), e \textsl{op} � usato per variare 220sui nomi degli operatori di tipo (cio� costanti di tipo $n$-arie, dove 221$n>0$). 222 223Si assume che sia dato un insieme infinito {\sf TyVars} di {\em variabili 224di tipo\/}\index{variabili di tipo, nella logica HOL@variabili di tipo, nella logica \HOL{}}. 225Le lettere greche $\alpha,\beta,\ldots$, possibilmente con indici 226sottoscritti o apici, sono usate per variare su {\sf Tyvars}. Gli insiemi 227{\sf TyNames} e {\sf TyVars} sono assunti disgiunti. 228 229Una {\it struttura di tipo\/} � un insieme $\Omega$ di costanti di tipo. Una {\it costante 230di tipo\/}\index{costanti di tipo, nella logica HOL@costanti di tipo, nella logica \HOL{}} � una coppia $(\nu,n)$ dove $\nu\in{\sf TyNames}$ � il 231nome della costante e $n$ � la sua ariet�. Cos� $\Omega\subseteq{\sf 232TyNames}\times\natnums$ (dove $\natnums$ � l'insieme dei numeri 233naturali). Si assume che non esistano due distinte costanti di tipo che hanno lo 234stesso nome 235cio� ogni volta che $(\nu, n_1)\in\Omega$ e 236$(\nu, n_2)\in\Omega$, allora $n_1 = n_2$. 237 238L'insieme {\sf Types}$_{\Omega}$ dei tipi su una struttura ${\Omega}$ 239pu� ora essere definito come il pi� piccolo insieme tale che: 240 241\begin{itemize} 242 243\item {\sf TyVars}$\ \subseteq\ ${\sf Types}$_{\Omega}$. 244 245\item Se $(\nu,0)\in\Omega$ allora $()\nu\in{\sf Types}_{\Omega}$. 246 247\item Se $(\nu,n)\in\Omega$ e $\sigma_i\in{\sf Types}_{\Omega}$ per 248$1\leq i\leq n$, allora $(\sigma_1,\ \ldots\ ,\sigma_n)\nu\in{\sf 249Types}_{\Omega}$. 250 251\item Se $\sigma_1\in{\sf Types}_{\Omega}$ e $\sigma_2\in{\sf 252Types}_{\Omega}$ allora $\sigma_1\fun\sigma_2\in{\sf Types}_{\Omega}$. 253 254 255\end{itemize} 256Si assume che l'operatore di tipo $\fun$ associ\index{operatori di tipo, nella logica HOL@operatori di tipo, nella logica \HOL{}!associativit� degli} a 257destra, cos� che 258\[ 259\sigma_1\fun\sigma_2\fun\ldots\fun \sigma_n\fun\sigma 260\] 261abbrevia 262\[ 263\sigma_1\fun(\sigma_2\fun\ldots\fun (\sigma_n\fun\sigma)\ldots) 264\] 265La notazione $tyvars(\sigma)$ � usata per denotare l'insieme delle variabili 266di tipo che occorrono in $\sigma$. 267 268\subsection{Semantica dei tipi} 269\label{semantics of types} 270 271 272Un {\em modello} $M$ di una struttura di tipo $\Omega$ � specificato dando 273per ogni costante di tipo $(\nu,n)$ una funzione $n$-aria 274\[ 275M(\nu):{\cal U}^{n}\longrightarrow{\cal U} 276\] 277Cos� dati gli insiemi $X_1,\ldots,X_n$ nell'universo $\cal U$, 278$M(\nu)(X_1,\ldots,X_n)$ � anche un insieme nell'universo. Nel caso $n=0$, 279questo equivale a specificare un elemento $M(\nu)\in{\cal U}$ per il 280tipo atomico $\nu$. 281 282I tipi che non contengono alcuna variabile di tipo sono chiamati {\it monomorfici}, 283mentre quelli che contengono variabili di tipo sono chiamati {\it 284polimorfici}\index{tipi polimorfici, nella logica HOL@tipi polimorfici, nella logica \HOL{}}\index{tipo, nella logica HOL@tipo, nella logica \HOL{}!polimorfico}. Qual � il 285significato di un tipo polimorfico? Si pu� 286dire quale insieme denota un tipo polimorfico solo una volta che si sono istanziate 287le sue variabili di tipo su insiemi particolari. Cos� il suo significato complessivo non � un 288singolo insieme, ma � piuttosto una funzione con valori su insiemi ${\cal 289U}^{n}\longrightarrow{\cal U}$, che assegna un insieme per ogni particolare 290assegnazione di insiemi alle variabili di tipo rilevanti. L'ariet� $n$ 291corrisponde al numero di variabili di tipo coinvolte. E' conveniente 292in tale contesto essere in grado di considerare che una variabile di tipo sia 293coinvolta nella semantica di un tipo $\sigma$ sia che occorra effettivamente 294in $\sigma$ sia che non occorra in esso, portando alla nozione di un 295tipo-in-contesto. 296 297Un {\em contesto di tipo}\index{contesto di tipo}, $\alpha\!s$, � semplicemente una 298lista finita (possibilmente vuota) di variabili di tipo {\em distinte\/} 299$\alpha_{1},\ldots,\alpha_{n}$. Un {\em 300tipo-in-contesto\/}\index{tipo-in-contesto} � una coppia, scritta 301$\alpha\!s.\sigma$, dove $\alpha\!s$ � un contesto di tipo, $\sigma$ � un 302tipo (su una data struttura di tipo) e tutte le variabili di tipo 303che occorrono in $\sigma$ appaiono da qualche parte nella lista $\alpha\!s$. La 304lista $\alpha\!s$ pu� anche contenere variabili di tipo che non occorrono in 305$\sigma$. 306 307Per ogni $\sigma$ ci sono dei contesti minimi $\alpha\!s$ per cui 308$\alpha\!s.\sigma$ � un tipo-in-contesto, che differiscono solo per l'ordine 309in cui le variabili di tipo di $\sigma$ sono elencate in $\alpha\!s$. Al 310fine di selezionare uno di tali contesti, assumiamo che {\sf TyVars} 311venga con un fissato ordine totale e definiamo il contesto {\em 312canonico}\index{contesti canonici, nella logica HOL@contesti canonici, nella logica \HOL{}!dei tipi} del tipo $\sigma$ in modo che esso consista esattamente 313delle variabili di tipo che esso contiene, elencate in ordine\footnote{E' 314possibile lavorare con contesti non ordinati, specificati da insiemi finiti 315piuttosto che liste, ma scegliamo di non fare questo dal momento che complica 316moderatamente la definizione della semantica che sar� data di 317sotto}. 318 319Sia $M$ un modello di una struttura di tipo $\Omega$. Per ogni 320tipo-in-contesto 321$\alpha\!s.\sigma$ su $\Omega$, definiamo una funzione 322\[ 323\den{\alpha\!s.\sigma}_{M}:{\cal U}^{n}\longrightarrow{\cal U} 324\] 325(dove $n$ � la lunghezza del contesto) per induzione sulla struttura 326di $\sigma$ come segue. 327\begin{itemize} 328 329\item Se $\sigma$ � una variabile di tipo, essa deve essere $\alpha_{i}$ per qualche unico 330$i=1,\ldots,n$ e allora $\den{\alpha\!s.\sigma}_{M}$ � la $i$\/esima 331funzione di proiezione, che manda $(X_{1},\ldots,X_{n})\in{\cal U}^{n}$ 332a $X_{i}\in{\cal U}$. 333 334\item Se $\sigma$ � un tipo funzione\index{tipi funzione, nella logica HOL@tipi funzione, nella logica \HOL{}!semantica formale dei} 335$\sigma_{1}\fun\sigma_{2}$, allora $\den{\alpha\!s.\sigma}_M$ manda 336$X\!s\in{\cal U}^n$ all'insieme di tutte le funzioni 337da $\den{\alpha\!s.\sigma_1}_M(X\!s)$ a 338$\den{\alpha\!s.\sigma_2}_M(X\!s)$. (Questo fa 339uso della propriet� {\bf Fun} di $\cal U$.) 340 341\item Se $\sigma$ � un 342tipo composto $(\sigma_{1},\ldots,\sigma_{m})\nu$, allora 343$\den{\alpha\!s.\sigma}_{M}$ manda $X\!s$ a 344$M(\nu)(S_{1},\ldots,S_{m})$ dove ogni $S_{j}$ � 345$\den{\alpha\!s.\sigma_{j}}_{M}(X\!s)$. 346\end{itemize} 347Si pu� ora definire che il significato di un tipo $\sigma$ in un modello $M$ � 348la funzione 349\[ 350\den{\sigma}_{M}:{\cal U}^{n}\longrightarrow{\cal U} 351\] 352data da $\den{\alpha\!s.\sigma}_{M}$, dove $\alpha\!s$ � il 353contesto canonico di $\sigma$. Se $\sigma$ � monomorfico, allora $n=0$ 354e $\den{\sigma}_{M}$ pu� essere identificato con l'elemento 355$\den{\sigma}_{M}()$ di $\cal U$. Quando il particolare modello $M$ � 356chiaro dal contesto, $\den{\_}_{M}$ sar� scritto $\den{\_}$. 357 358Per riassumere, dato un modello in $\cal U$ di una struttura di tipo $\Omega$, 359la semantica interpreta i tipi monomorfici su $\Omega$ come gli insiemi in 360$\cal U$ e pi� in generale, interpreta i tipi polimorfici\index{tipi, nella logica HOL@tipi, nella logica \HOL{}!polimorfici}\index{tipi polimorfici, nella logica HOL@tipi polimorfici, nella logica \HOL{}!semantica formale dei} che coinvolgono $n$ variabili di tipo come funzioni $n$-arie ${\cal 361U}^{n}\longrightarrow{\cal U}$ sull'universo. I tipi funzione sono 362interpretati da insiemi di funzioni complete. 363 364\medskip 365 366\noindent{\bf Esempi\ } 367Supponiamo che $\Omega$ contenga una costante di tipo $(\textsl{b},0)$ e che 368il modello $M$ assegni l'insieme $\two$ a $\textsl{b}$. Allora: 369\begin{enumerate} 370 371\item $\den{\textsl{b}\fun\textsl{b}\fun\textsl{b}}=\two\fun\two\fun\two\in{\cal U}$. 372 373\item $\den{(\alpha\fun\textsl{b})\fun\alpha}:{\cal U}\longrightarrow{\cal U}$ 374� la funzione che manda $X\in{\cal U}$ a $(X\fun\two)\fun X\in{\cal U}$. 375 376\item $\den{\alpha,\beta . (\alpha\fun\textsl{b})\fun\alpha}:{\cal 377U}^{2}\longrightarrow{\cal U}$ � la funzione che manda $(X,Y)\in{\cal 378U}^{2}$ a $(X\fun\two)\fun X\in{\cal U}$. 379 380\end{enumerate} 381 382\medskip 383 384\noindent{\bf Nota\ } 385Un approccio pi� tradizionale alla semantica implicherebbe dare 386dei significati ai tipi in presenza di `ambienti' che assegnano insiemi in 387$\cal U$ a tutte le variabili di tipo. L'uso di tipi-in-contesti � quasi 388la stessa cosa di usare ambienti parziali con domini finiti---� 389solo che il contesto vincola il dominio ammissibile a un particolare 390insieme finito (ordinato) di variabili di tipo. Al livello dei tipi non c'� 391molto da scegliere tra i due approcci. Tuttavia per la sintassi 392e la semantica dei termini che sar� data di sotto, dove c'� una dipendenza 393sia dalle variabili di tipo sia dalle variabili individuali, l'approccio usato 394qui sembra migliore. 395 396\subsection{Istanze e sostituzione} 397\label{instances-and-substitution} 398 399Se $\sigma$ e $\tau_1,\ldots,\tau_n$ sono tipi su una struttura di tipo 400$\Omega$, 401\[ 402\sigma[\tau_{1},\ldots,\tau_{p}/\beta_{1},\ldots,\beta_{p}] 403\] 404denoter� il tipo risultante dalle sostituzioni simultanee per 405ogni $i=1,\ldots,p$ di 406$\tau_i$ per la variabile di tipo $\beta_i$ in $\sigma$. 407Il tipo risultante � chiamato una {\it istanza\/}\index{tipi, nella logica HOL@tipi, nella logica \HOL{}!istanziazione di} di $\sigma$. Il 408seguente lemma circa le istanze sar� utile pi� avanti; esso � dimostrato per 409induzione sulla struttura di $\sigma$. 410 411\medskip 412 413\noindent{\bf Lemma 1\ }{\it 414Supponiamo che $\sigma$ sia un tipo che contiene le variabili di tipo distinte 415$\beta_1,\ldots,\beta_p$ e che 416$\sigma'=\sigma[\tau_{1},\ldots,\tau_{n}/\beta_1,\ldots,\beta_p]$ sia 417un'istanza di $\sigma$. Allora i tipi $\tau_1,\ldots,\tau_p$ sono 418determinati univocamente da $\sigma$ e $\sigma'$. 419} 420 421\medskip 422 423Abbiamo anche bisogno di sapere come la semantica dei tipi si comporta rispetto 424alla sostituzione: 425 426\medskip 427 428\noindent{\bf Lemma 2\ }{\it Dati i tipi-in-contesto $\beta\!s.\sigma$ e 429$\alpha\!s.\tau_i$ ($i=1,\ldots,p$, dove $p$ � la 430lunghezza di $\beta\!s$), sia $\sigma'$ l'istanza 431$\sigma[\tau\!s/\beta\!s]$. Allora anche $\alpha\!s.\sigma'$ � un 432tipo-in-contesto e il suo significato in qualsiasi modello $M$ � collegato a quello di 433$\beta\!s.\sigma$ come segue. Per tutti gli $X\!s\in{\cal U}^n$ (dove $n$ 434� la lunghezza di $\alpha\!s$) 435\[ 436\den{\alpha\!s.\sigma'}(X\!s) = 437\den{\beta\!s.\sigma}(\den{\alpha\!s.\tau_{1}}(X\!s), 438 \ldots ,\den{\alpha\!s.\tau_{p}}(X\!s)) 439\] 440} 441Ancora una volta, il lemma pu� essere dimostrato per induzione sulla struttura di 442$\sigma$. 443 444\section{Termini} 445\label{terms} 446 447I termini della logica \HOL{} sono espressioni che denotano elementi degli insiemi 448denotati dai tipi. La meta-variabile $t$ 449� usata per variare su termini arbitrari, possibilmente decorata 450con indici sottoscritti o apici. 451 452Ci sono quattro specie di termini nella logica \HOL{}. Queste possono essere 453descritte approssimativamente nella seguente grammatica {\small BNF}, in 454cui $x$ varia su variabili e $c$ varia su costanti. 455\index{combinazioni, nella logica HOL@combinazioni, nella logica \HOL{}!forma astratta di} 456 457\settowidth{\ttX}{\tt X} 458\newcommand{\var}{\setlength{\unitlength}{\ttX}\begin{picture}(1,6) 459\put(.5,0){\makebox(0,0)[b]{\footnotesize variabili}} 460\put(0,1.5){\vector(0,1){4.5}} 461\end{picture}} 462\newcommand{\const}{\setlength{\unitlength}{\ttX}\begin{picture}(1,6) 463\put(.5,2.3){\makebox(0,0)[b]{\footnotesize costanti}} 464\put(.5,3.5){\vector(0,1){2.4}} 465\end{picture}} 466\newcommand{\app}{\setlength{\unitlength}{\ttX}\begin{picture}(1,6) 467\put(.5,1.5){\makebox(0,0)[b]{\footnotesize applicazioni di funzione}} 468\put(.5,0){\makebox(0,0)[b]{\footnotesize (funzione $t$, argomento $t'$)}} 469\put(0.5,2.5){\vector(0,1){3.5}} 470\end{picture}} 471\newcommand{\abs}{\setlength{\unitlength}{\ttX}\begin{picture}(1,6) 472\put(1,3.3){\makebox(0,0)[b]{\footnotesize $\lambda$-astrazioni}} 473\put(0.7,4.5){\vector(0,1){1.5}} 474\end{picture}} 475% 476$$ t \quad ::=\quad {\mathord{\mathop{x}\limits_{\var}}} 477 \quad\mid\quad{\mathord{\mathop{\con{c}}\limits_{\const}}} 478 \quad\mid\quad\underbrace{t\ t'}_{\app} 479 \quad\mid\quad\underbrace{\lambda x .\ t}_{\abs}$$ 480 481Informalmente, un $\lambda$-termine\index{lambda termini, nella logica HOL@lambda termini, nella logica \HOL{}}\index{astrazione di funzione, nella logica HOL@astrazione di funzione, nella logica \HOL{}!forma astratta di} $\lambda x.\ t$ denota 482una funzione $v\mapsto t[v/x]$, dove $t[v/x]$ denota il risultato di 483sostituire $v$ per $x$ in $t$. Un'applicazione\index{applicazione di funzione, nella logica HOL@applicazione di funzione, nella logica \HOL{}!forma astratta di} $t\ t'$ denota il 484risultato di applicare la 485funzione denotata da $t$ al valore denotato da $t'$. Questo sar� 486reso pi� preciso di sotto. 487 488La grammatica {\small BNF} appena data omette di menzionare i tipi. Di fatto, ogni 489termine nella 490logica \HOL{} � associato con un unico tipo. 491La notazione $t_{\sigma}$ � 492tradizionalmente usata per variare su termini di tipo $\sigma$. Una 493grammatica pi� accurata dei 494termini �: 495 496$$ t_{\sigma} \quad ::=\quad {\mathord{\mathop{x_{\sigma}}\limits_{}}} 497\quad\mid\quad 498{\mathord{\mathop{\con{c}_{\sigma}}\limits_{}}} 499\quad\mid\quad (t_{\sigma'\fun\sigma}\ t'_{\sigma'})_{\sigma} 500\quad\mid\quad(\lambda x_{\sigma_1} .\ t_{\sigma_2}) 501_{\sigma_1\fun\sigma_2}$$\index{costanti, nella logica HOL@costanti, nella logica \HOL{}!forma astratta di} 502 503Di fatto, esattamente come la definizione dei tipi era relativa a una particolare 504struttura di tipo $\Omega$, la definizione formale dei termini � relativa a 505una data collezione di costanti tipizzate su $\Omega$. Assumiamo che sia dato 506un insieme infinito {\sf Names} di nomi. Una {\em costante\/} su 507$\Omega$ � una coppia $(\con{c}, \sigma)$, dove $\con{c}\in{\sf Names}$ 508e $\sigma\in{\sf Types}_{\Omega}$. Una {\em firma} su $\Omega$ 509� semplicemente un insieme $\Sigma_\Omega$ di tali costanti. 510 511L'insieme {\sf Terms}$_{\Sigma_{\Omega}}$ di termini su 512$\Sigma_{\Omega}$ � definito essere il pi� piccolo insieme chiuso sotto le 513seguenti regole di formazione: 514\begin{enumerate} 515 516\item {\bf Costanti:} Se $(\con{c},\sigma)\in{\Sigma_{\Omega}}$ e 517$\sigma'\in{\sf Types}_{\Omega}$ 518� un'istanza di $\sigma$, allora $(\con{c},{\sigma'})\in{\sf 519Terms}_{\Sigma_{\Omega}}$. I termini formati in questo modo sono chiamati {\it 520costanti\/}\index{costanti, nella logica HOL@costanti, nella logica \HOL{}!forma astratta di} e sono scritti $\con{c}_{\sigma'}$. 521 522\item {\bf Variabili:} Se $x\in{\sf Names}$ e $\sigma\in{\sf 523Types}_{\Omega}$, allora ${\tt var}\ x_{\sigma}\in{\sf 524Terms}_{\Sigma_{\Omega}}$. I termini formati in questo modo sono chiamati {\it 525variabili}\index{variabili, nella logica HOL@variabili, nella logica \HOL{}!forma astratta di}. Il marcatore {\tt var}\ � semplicemente un accorgimento per 526distinguere le variabili da costanti con lo stesso nome. Una variabile 527${\tt var}\ x_{\sigma}$ sar� di solito scritta come $x_{\sigma}$, se 528� chiaro dal contesto che $x$ � una variabile piuttosto che una 529costante 530 531\item {\bf Applicazioni di funzione:} Se $t_{\sigma'{\fun}\sigma}\in{\sf 532Terms}_{\Sigma_{\Omega}}$ e $t'_{\sigma'}\in{\sf 533Terms}_{\Sigma_{\Omega}}$, allora $(t_{\sigma'\fun\sigma}\ 534t'_{\sigma'})_{\sigma}\in {\sf Terms}_{\Sigma_{\Omega}}$. 535(I termini formati in questo modo sono chiamati {\it combinazioni}.) 536 537\item {\bf $\lambda$-Astrazioni:} Se ${\tt var}\ x_{\sigma_1} 538\in{\sf Terms}_{\Sigma_{\Omega}}$ e $t_{\sigma_2}\in{\sf 539Terms}_{\Sigma_{\Omega}}$, allora $(\lambda x_{\sigma_1}.\ 540t_{\sigma_2})_{\sigma_1\fun\sigma_2} 541\in{\sf Terms}_{\Sigma_{\Omega}}$. 542 543\end{enumerate} 544 545Si noti che � possibile avere costanti e variabili\index{variabili, nella logica HOL@variabili, nella logica \HOL{}!con gli stessi nomi} 546con lo stesso nome. E' anche possibile avere variabili differenti con 547lo stesso nome, se esse hanno tipi differenti. 548 549Il tipo sottoscritto a un termine pu� essere omesso se � chiaro dalla 550struttura del termine o dal contesto in cui occorre quale deve essere il 551suo tipo. 552 553L'applicazione di funzione\index{applicazione di funzione, nella logica HOL@applicazione di funzione, nella logica \HOL{}!associativit� della} � assunta associare 554a sinistra, cos� che $t\ t_1\ t_2\ \ldots\ t_n$ abbrevia $(\ 555\ldots\ ((t\ t_1)\ t_2)\ \ldots\ t_n)$. 556 557La notazione $\lambda x_1\ x_2\ \cdots\ x_n.\ t$ abbrevia $\lambda 558x_1.\ (\lambda x_2.\ \cdots\ (\lambda x_n.\ t)\ \cdots\ )$. 559 560Un termine � chiamato polimorfico\index{termini polimorfici, nella logica HOL@termini polimorfici, nella logica \HOL{}} se contiene una variabile 561di tipo. Altrimenti � chiamato monomorfico. Si noti che un termine 562$t_{\sigma}$ pu� essere polimorfico anche se $\sigma$ � 563monomorfico -- per esempio, 564$(f_{\alpha\fun\textsl{b}}\ x_{\alpha})_{\textsl{b}}$, dove $\textsl{b}$ � un tipo atomico. L'espressione 565$tyvars(t_{\sigma})$ denota l'insieme di variabili di tipo che occorrono in 566$t_{\sigma}$. 567 568L'occorrenza di una variabile $x_{\sigma}$ � chiamata {\it 569legata\/}\index{variabili legate, nella logica HOL@variabili legate, nella logica \HOL{}}\index{variabili, nella logica HOL@variabili, nella logica \HOL{}!forma astratta di} 570 se essa occorre all'interno dello scopo di una $\lambda x_{\sigma}$ 571che chiude dal punto di vista testuale, altrimenti l'occorrenza � chiamata {\it 572libera\/}\index{variabili libere, nella logica HOL@variabili libere, nella logica \HOL{}!forma astratta di}. Si noti che $\lambda x_{\sigma}$ non lega 573$x_{\sigma'}$ se $\sigma\neq \sigma'$. Un termine in cui tutte le occorrenze 574delle variabili sono legate � chiamato {\it chiuso\/}. 575 576\subsection{Termini-in-contesto} 577\label{terms-in-context} 578 579Un {\em contesto\/}\index{contesti, nella semantica della logica HOL@contesti, nella semantica della logica \HOL{}} $\alpha\!s,\!x\!s$ consiste di un contesto 580di tipo $\alpha\!s$ insieme con una lista $x\!s=x_{1},\ldots,x_{m}$ di 581variabili distinte i cui tipi contengono solo variabili di tipo dalla 582lista $\alpha\!s$. 583 584La condizione che $x\!s$ contenga variabili {\em distinte\/} necessita 585di qualche commento. Dal momento che una variabile � specificata sia da un nome sia da un 586tipo, � permesso che $x\!s$ contenga 587nomi\index{variabili, nella logica HOL@variabili, nella logica \HOL{}!con gli stessi nomi} ripetuti, 588 purch� ai nomi siano attaccati tipi 589differenti. Questo aspetto della sintassi significa che si deve procedere con 590cautela quando si definisce il significato dell'istanziazione delle variabili di tipo, 591dal momento che l'istanziazione pu� far s� che delle variabili diventino uguali 592`accidentalmente'. Si veda la Sezione~\ref{term-substitution}. 593 594Un {\em termine-in-contesto\/}\index{term-in-context} 595$\:\;\alpha\!s,\!x\!s.t\;\:$ consiste di un contesto insieme con un termine 596$t$ che soddisfa le seguenti condizioni: 597\begin{itemize} 598 599\item $\alpha\!s$ contiene qualsiasi variabile di tipo che occorre in $x\!s$ e $t$. 600 601\item $x\!s$ contiene qualsiasi variabile che occorre libera in $t$. 602 603\item $x\!s$ non contiene alcuna variabile che occorre 604legata in $t$. 605 606\end{itemize} 607Il contesto $\alpha\!s,\!x\!s$ pu� contenere variabili (di tipo) che 608non appaiono in $t$. Si noti che la combinazione della seconda e della terza 609condizione implica che una variabile non pu� avere occorrenze sia libere sia 610legate in $t$. Per un termine arbitrario, c'� sempre un 611termine $\alpha$-equivalente che soddisfa questa condizione, ottenuto 612rinominando le variabili legate in caso di necessit�\footnote{Si ricordi che due 613termini sono detti essere $\alpha$-equivalenti se differiscono soltanto nei 614nomi delle loro variabili legate.}. Nella semantica dei termini che sar� 615data di seguito restringeremo l'attenzione a tali termini. Quindi il significato di un 616termine arbitrario � considerato essere il significato di qualche $\alpha$-variante di 617esso non avente variabili sia libere sia legate. (La semantica uguaglier� 618le $\alpha$-varianti, cos� che non importa quale � scelta.) Evidentemente 619per un tale termine c'� un contesto minimale $\alpha\!s,\!x\!s$, unico 620a meno dell'ordine in cui le variabili sono elencate, per il quale 621$\alpha\!s,\!x\!s.t$ � un termine-in-contesto. Come per le variabili di tipo, 622assumeremo dato un fissato ordine totale sulle variabili. Quindi l'unico 623contesto minimo con le variabili elencate in ordine sar� chiamato il contesto {\em 624canonico}\index{contesti canonici, nella logica HOL@contesti canonici, nella logica \HOL{}!di termini} del termine $t$. 625 626\subsection{Semantica dei termini} 627\label{semantics of terms} 628 629Sia $\Sigma_{\Omega}$ una firma\index{firme, della logica HOL@firme, della logica \HOL{}!semantica formale delle} su una struttura 630di tipo $\Omega$ (si veda la Sezione~\ref{terms}). Un {\em modello\/} $M$ di 631$\Sigma_{\Omega}$ � specificato da un modello della struttura di tipo pi� 632per ogni costante\index{costanti primitive, della logica HOL@costanti primitive, della logica \HOL{}} $(\con{c},\sigma)\in\Sigma_{\Omega}$ un 633elemento 634\[ 635M(\con{c},\sigma) \in 636\prod_{X\!s\in{\cal U}^{n}}\den{\sigma}_{M}(X\!s) 637\] 638del prodotto cartesiano indicato, dove $n$ � il numero delle variabili 639di tipo che occorrono in $\sigma$. In altre parole 640$M(\con{c},\sigma)$ � una funzione (dipendentemente tipizzata) 641che assegna ad ogni $X\!s\in{\cal U}^{n}$ un elemento di 642$\den{\sigma}_{M}(X\!s)$. Nel caso che $n=0$ (cos� che 643$\sigma$ � monomorfico), $\den{\sigma}_{M}$ era identificato 644con un insieme in $\cal U$ e quindi $M(c,\sigma)$ pu� essere 645identificato con un elemento di quell'insieme. 646 647Il significato dei termini \HOL{} in un tale modello sar� ora descritto. La 648semantica interpreta termini chiusi che non coinvolgono variabili di tipo come 649elementi di insiemi in $\cal U$ (il particolare insieme coinvolto essendo derivato 650dal tipo del termine come nella Sezione~\ref{semantics of types}). Pi� 651in generale, se il termine chiuso coinvolge $n$ variabili di tipo allora � 652interpretato come un elemento di un prodotto $\prod_{X\!s\in{\cal 653U}^{n}}Y(X\!s)$, dove la funzione $Y:{\cal U}^{n}\longrightarrow{\cal 654U}$ � derivata dal tipo del termine (in un contesto di tipo derivato 655dal termine). Cos� il significato del termine � una funzione (dipendentemente tipizzata) 656che, quando applicata a qualsiasi significato scelto per le variabili 657di tipo nel termine, d� un significato per il termine come un elemento di un 658insieme in $\cal U$. Dall'altro lato, se il termine coinvolge $m$ variabili 659libere ma nessuna variabile di tipo, allora � interpretato come una funzione 660$Y_1\times\cdots\times Y_m\fun Y$ dove gli insiemi $Y_1,\ldots,Y_m$ in 661$\cal U$ sono interpretazioni dei tipi delle variabili libere nel 662termine e l'insieme $Y\in{\cal U}$ � l'interpretazione del tipo del 663termine; cos� il significato del termine � una funzione che, quando 664applicata a qualsiasi significato scelto per le variabili libere nel termine, 665d� un significato per il termine. Infine, il caso pi� generale � quello di un 666termine che coinvolge $n$ variabili di tipo e $m$ variabili libere: esso � 667interpretato come un elemento di un prodotto 668\[ 669\prod_{X\!s\in{\cal 670U}^{n}}Y_{1}(X\!s)\times\cdots\times Y_{m}(X\!s) \;\fun\; Y(X\!s) 671\] 672dove le funzioni $Y_{1},\ldots,Y_{m},Y:{\cal 673U}^{n}\longrightarrow{\cal U}$ sono determinati dai tipi delle variabili 674libere e dal tipo del termine (in un conteso di tipo derivato dal 675termine). 676 677Pi� precisamente, dato un termine-in-contesto $\alpha\!s,\!x\!s.t$ 678su $\Sigma_{\Omega}$ supponiamo che 679\begin{itemize} 680 681\item $t$ abbia il tipo $\tau$ 682 683\item $x\!s=x_{1},\ldots,x_{m}$ ed ogni $x_{j}$ abbia il tipo $\sigma_{j}$ 684 685\item $\alpha\!s=\alpha_{1},\ldots,\alpha_{n}$. 686 687\end{itemize} 688Allora dal momento che $\alpha\!s,\!x\!s.t$ � un termine-in-contesto, $\alpha\!s.\tau$ 689e $\alpha\!s.\sigma_{j}$ sono tipi-in-contesto, e quindi danno origine 690a funzioni $\den{\alpha\!s.\tau}_{M}$ e 691$\den{\alpha\!s.\sigma_{j}}_{M}$ da ${\cal U}^{n}$ a $\cal U$ come nella 692sezione~\ref{semantics of types}. Il significato di $\alpha\!s,\!x\!s.t$ 693nel modello $M$ sar� dato da un elemento 694\[ 695\den{\alpha\!s,\!x\!s.t}_{M} \in \prod_{X\!s\in{\cal U}^{n}} 696\left(\prod_{j=1}^{m}\den{\alpha\!s.\sigma_{j}}_{M}(X\!s)\right) 697\fun \den{\alpha\!s.\tau}_{M}(X\!s) . 698\] 699In altre parole, dato 700\begin{eqnarray*} 701X\!s & = & (X_{1},\ldots,X_{n})\in{\cal U}^{n} \\ 702y\!s & = & (y_{1},\ldots,y_{m})\in\den{\alpha\!s.\sigma_{1}}_{M}(X\!s) 703 \times\cdots\times \den{\alpha\!s.\sigma_{m}}_{M}(X\!s) 704\end{eqnarray*} 705si ottiene un elemento $\den{\alpha\!s,\!x\!s.t}_{M}(X\!s)(y\!s)$ di 706$\den{\alpha\!s.\tau}_{M}(X\!s)$. La definizione di 707$\den{\alpha\!s,\!x\!s.t}_{M}$ procede per induzione sulla struttura del 708termine $t$ come segue. (Come prima, il sottoscritto $M$ sar� omesso dalle 709parentesi semantiche $\den{ \_ }$ quando il particolare modello coinvolto � 710chiaro dal contesto.) 711\begin{itemize} 712 713\item 714Se $t$ � una variabile\index{variabili, nella logica HOL@variabili, nella logica \HOL{}!semantica formale delle}, deve essere $x_{j}$ per qualche unico 715$j=1,\ldots,m$, so $\tau=\sigma_{j}$ e allora 716$\den{\alpha\!s,\!x\!s.t}(X\!s)(y\!s)$ � definito essere $y_{j}$. 717 718\item 719Supponiamo che $t$ sia una costante\index{costanti, nella logica HOL@costanti, nella logica \HOL{}!semantica formale delle} $\con{c}_{\sigma'}$, dove 720$(\con{c},\sigma)\in\Sigma_{\Omega}$ e $\sigma'$ � un'istanza di 721$\sigma$. Allora per il Lemma~1 di \ref{instances-and-substitution}, 722$\sigma'=\sigma[\tau_{1},\ldots,\tau_{p}/\beta_{1},\ldots,\beta_{p}]$ 723per tipi univocamente determinati $\tau_{1},\ldots,\tau_{p}$ (dove 724$\beta_{1},\ldots,\beta_{p}$ sono le variabili di tipo che occorronoin 725$\sigma$). Allora definiamo $\den{\alpha\!s,\!x\!s.t}(X\!s)(y\!s)$ essere 726$M(\con{c},\sigma)(\den{\alpha\!s.\tau_{1}}(X\!s), 727\ldots,\den{\alpha\!s.\tau_{p}}(X\!s))$, 728che � un elemento di $\den{\alpha\!s.\tau}(X\!s)$ per il Lemma~2 di 729\ref{instances-and-substitution} (dal momento che $\tau$ � $\sigma'$). 730 731\item 732Supponiamo che $t$ sia un termine applicazione di funzione\index{combinazioni, nella logica HOL@combinazioni, nella logica \HOL{}!semantica formale delle} $(t_{1}\ 733t_{2})$\index{applicazione di funzione, nella logica HOL@applicazione di funzione, nella logica \HOL{}!semantica formale delle} dove $t_{1}$ � di tipo 734$\tau'\fun\tau$ e $t_{2}$ � di tipo $\tau'$. Allora 735$f=\den{\alpha\!s,\!x\!s.t_{1}}(X\!s)(y\!s)$, essendo un elemento di 736$\den{\alpha\!s.\tau'\fun\tau}(X\!s)$, � una funzione dall'insieme 737$\den{\alpha\!s.\tau'}(X\!s)$ all'insieme $\den{\alpha\!s.\tau}(X\!s)$ 738che si pu� applicare all'elemento 739$y=\den{\alpha\!s,\!x\!s.t_{2}}(X\!s)(y\!s)$. Definiamo 740$\den{\alpha\!s,\!x\!s.t}(X\!s)(y\!s)$ essere $f(y)$. 741 742\item Supponiamo che $t$ sia il termine astrazione\index{astrazione di funzione, nella logica HOL@astrazione di funzione, nella logica \HOL{}!semantica formale della} 743$\lambda x.t_{2}$ dove $x$ � di tipo $\tau_{1}$ e $t_{2}$ di 744tipo $\tau_{2}$. Cos� $\tau=\tau_{1}\fun\tau_{2}$ e 745$\den{\alpha\!s.\tau}(X\!s)$ � l'insieme di funzioni 746$\den{\alpha\!s.\tau_{1}}(X\!s)\fun\den{\alpha\!s.\tau_{2}}(X\!s)$. 747Definiamo $\den{\alpha\!s,\!x\!s.t}(X\!s)(y\!s)$ essere l'elemento di 748questo insieme che � la funzione che manda 749$y\in\den{\alpha\!s.\tau_{1}}(X\!s)$ a 750$\den{\alpha\!s,\!x\!s,\!x.t_{2}}(X\!s)(y\!s,y)$. (Si noti che dal momento che 751$\alpha\!s,\!x\!s.t$ � un termine in contesto, per convenzione la variabile 752legata $x$ non occorre in $x\!s$ e cos� anche 753$\alpha\!s,\!x\!s,\!x.t_{2}$ � un termine in contesto.) 754\end{itemize} 755Ora definiamo il significato di un termine $t_{\tau}$ in un modello $M$ essere la 756funzione dipendentemente tipizzata 757\[ \den{t_{\tau}} \in \prod_{X\!s\in{\cal U}^{n}} 758 \left(\prod_{j=1}^{m}\den{\alpha\!s.\sigma_{j}}(X\!s)\right) 759 \fun \den{\alpha\!s.\tau}(X\!s) 760\] 761data da $\den{\alpha\!s,\!x\!s.t_{\tau}}$, dove $\alpha\!s,\!x\!s$ � il 762contesto canonico di $t_{\tau}$. Cos� $n$ � il numero di variabili di tipi in 763$t_{\tau}$, $\alpha\!s$ � una lista di quelle variabili di tipo, $m$ � il 764numero di variabili ordinarie che occorrono libere in $t_{\tau}$ (assunte essere 765distinte dalle variabili legate di $t_{\tau}$) e i $\sigma_{j}$ sono 766i tipi di quelle variabili. (E' importante notare che la lista 767$\alpha\!s$, che � parte del contesto canonico di $t$, pu� essere strettamente 768pi� grande dei contesti di tipo canonici di $\sigma_{j}$ o $\tau$. Cos� 769non avrebbe senso scrivere semplicemente $\den{\sigma_{j}}$ o $\den{\tau}$ nella 770definizione di sopra.) 771 772Se $t_{\tau}$ � un termine chiuso, allora $m=0$ e per ogni $X\!s\in{\cal 773U}^{n}$ si pu� identificare $\den{t_{\tau}}$ con l'elemento 774$\den{t_{\tau}}(X\!s)()\in\den{\alpha\!s.\tau}(X\!s)$. Cos� per termini chiusi 775si ottiene 776\[ \den{t_{\tau}} \in \prod_{X\!s\in{\cal U}^{n}} 777\den{\alpha\!s.\tau}(X\!s) 778\] 779dove $\alpha\!s$ � la lista delle variabili di tipo che occorrono in $t_{\tau}$ e 780$n$ � la lunghezza di quella lista. Se inoltre, nessuna variabile di tipo occorre in 781$t_{\tau}$, allora $n=0$ e $\den{t_{\tau}}$ pu� essere identificato con 782l'elemento $\den{t_{\tau}}()$ dell'insieme $\den{\tau}\in{\cal U}$. 783 784La semantica dei termini appare qualcosa di complicato a casua della 785possibile dipendenza di un termine sia dalle variabili di tipo sia dalle variabili 786ordinarie. Esempi di come la definizione della semantica 787funziona in pratica si pu� trovare nella Sezione~\ref{LOG}, dove � dato il significato 788di alcuni termini che denotano costanti logiche. 789 790\subsection{Sostituzione} 791\label{term-substitution} 792 793Dal momento che i termini possono coinvolgere sia variabili di tipo sia 794variabili ordinarie, ci sono due differenti operazioni di sostituzione 795sui termini che bisogna considerare---sostituzione di tipi per variabili 796di tipo e sostituzione di termini per variabili. 797 798\subsubsection*{Sostituire tipi per variabili di tipo nei termini} 799\index{regola di sostituzione, nella logica HOL@regola di sostituzione, nella logica \HOL{}!semantica formale della} 800 801Supponiamo che $t$ sia un termine, con contesto canonico $\alpha\!s,\!x\!s$ diciamo, 802dove $\alpha\!s = \alpha_1,\ldots,\alpha_n$, $x\!s = x_1,\ldots,x_m$ 803e dove per $j=1,\ldots,m$ il tipo della variabile $x_j$ � 804$\sigma_j$. Se $\alpha\!s'.\tau_{i}$ ($i=1,\ldots,n$) sono 805tipi-in-contesto, allora sostituendo\index{sostituzione di tipo, nella logica HOL@sostituzione di tipo, nella logica \HOL{}!semantica formale della} i tipi 806$\tau_{i}$ per le variabili di tipo $\alpha_{i}$ nella lista $x\!s$, si 807ottiene una nuova lista di variabili $x\!s'$. Cos� il $j$\/esimo elemento di 808$x\!s'$ ha il tipo $\sigma'_{j} = \sigma_{j}[\tau\!s/\alpha\!s]$. Saranno considerate solo 809sostituzioni con la seguente propriet�. 810\begin{quote} 811Nell'istanziare\index{tipi, nella logica HOL@tipi, nella logica \HOL{}!istanziazione di} le variabili di tipo $\alpha\!s$ con i tipi 812$\tau\!s$, nessuna coppia di due variabili distinte nella lista $x\!s$ diventano uguali 813nella lista $x\!s'$\footnote{Una tale identificazione di variabili potrebbe 814accadere se le variabili avessero lo stesso nome componente e i loro tipi 815diventassero uguali in seguito all'istanziazione.}. 816\end{quote} 817Questa condizione assicura che $\alpha\!s',x\!s'$ sia davvero un contesto. Allora 818si ottiene un nuovo termine-in-contesto $\alpha\!s',\!x\!s'.t'$ 819sostituendo i tipi $\tau\!s=\tau_{1},\ldots,\tau_{n}$ per le variabili 820di tipo $\alpha\!s$ in $t$ (con un'adatta rinomina delle occorrenze 821legate delle variabili per renderle distinte dalle variabili in 822$x\!s'$). La notazione 823\[ 824t[\tau\!s/\alpha\!s] 825\] 826� usata per il termine $t'$. 827 828\medskip 829 830\noindent{\bf Lemma 3\ }{\it 831Il significato di $\alpha\!s',\!x\!s'.t'$ in un modello � collegato a quello 832di $t$ come segue. Per tutti $X\!s'\in{\cal U}^{n'}$ (dove $n'$ � la 833lunghezza di $\alpha\!s'$) 834} 835\[ 836\den{\alpha\!s',\!x\!s'.t'}(X\!s') = 837 \den{t}(\den{\alpha\!s'.\tau_{1}}(X\!s'),\ldots, 838 \den{\alpha\!s'.\tau_{n}}(X\!s')). 839\] 840 841\medskip 842 843Il lemma~2 in \ref{instances-and-substitution} � necessario per vedere che entrambi 844i lati dell'equazione di sopra sono elementi dello stesso insieme di funzioni. 845La validit� dell'equazione � dimostrata per induzione sulla struttura 846del termine $t$. 847 848\subsubsection*{Sostituire termini per variabili nei termini} 849\index{regola di sostituzione, nella logica HOL@regola di sostituzione, nella logica \HOL{}!semantica formale della} 850 851Supponiamo che $t$ sia un termine, con contesto canonico $\alpha\!s,\!x\!s$ diciamo, 852dove $\alpha\!s = \alpha_1,\ldots,\alpha_n$, $x\!s = x_1,\ldots,x_m$ 853e dove per $j=1,\ldots,m$ il tipo della variabile $x_j$ � 854$\sigma_j$. Se si hanno termini-in-contesto $\alpha\!s,\!x\!s'.t_{j}$ per 855$j=1,\ldots,m$ con $t_{j}$ dello stesso tipo di $x_{j}$, diciamo 856$\sigma_{j}$, allora si ottiene un nuovo termine-in-contesto 857$\alpha\!s,\!x\!s'.t''$ sostituendo i termini 858$t\!s=t_1,\ldots,t_m$ per le variabili $x\!s$ in $t$ (con la rinomina 859adatta delle occorrenze legate delle variabili per prevenire che le variabili 860libere delle $t_{j}$ diventino legate dopo la sostituzione). La 861notazione 862\[ 863t[t\!s/x\!s] 864\] 865� usata per il termine $t''$. 866 867\medskip 868 869\noindent{\bf Lemma 4\ }{\it 870Il significato di $\alpha\!s,\!x\!s'.t''$ in un modello � collegato con quello di 871$t$ come segue. Per tutti $X\!s\in{\cal U}^{n}$ e tutti 872$y\!s'\in\den{\alpha\!s.\sigma'_{1}} \times\cdots\times 873\den{\alpha\!s.\sigma'_{m'}}$ (dove $\sigma'_{j}$ � il tipo di 874$x'_{j}$)} 875\[ 876\den{\alpha\!s,\!x\!s'.t''}(X\!s)(y\!s') = \den{t}(X\!s)( 877\den{\alpha\!s,\!x\!s'.t_{1}}(X\!s)(y\!s'),\ldots, 878\den{\alpha\!s,\!x\!s'.t_{m}}(X\!s)(y\!s')) 879\] 880 881\medskip 882 883Di nuovo, questo risultato � dimostrato per induzione sulla struttura del 884termine $t$. 885 886 887\section{Nozioni standard} 888 889Fino ad ora la sintassi dei tipi e dei termini � stata molto generale. Per 890rappresentare le formule standard della logica � necessario 891imporre qualche struttura specifica. In particolare, ogni struttura di tipo 892deve contenere un tipo atomico \ty{bool} che � inteso denotare 893l'insieme distinto di due elementi $\two\in{\cal U}$, considerato come un insieme 894di valori di verit�. Le formule logiche sono allora identificate con 895i termini\index{variabili di tipo, nella logica HOL@variabili di tipo, nella logica \HOL{}!forma astratta di}\index{termini, nella logica HOL@termini, nella logica \HOL{}!as logical formulas} di 896tipo \ty{bool}. In aggiunta, varie 897costanti logiche sono assunte essere in tutte le firme. Questi 898requisiti sono formalizzati definendo la nozione di una 899firma standard. 900 901\subsection{Strutture di tipo standard} 902\label{standard-type-structures} 903 904Una struttura di tipo $\Omega$ � {\em standard\/} se contiene i 905tipi atomici \ty{bool} (dei booleani o valori di verit�) e \ty{ind} (degli 906individui). (Nella letteratura, � spesso utilizzato il simbolo $o$ 907al posto di \ty{bool} e $\iota$ al posto di \ty{ind}.) 908 909Un modello $M$ di $\Omega$ � {\em standard\/} se $M(\bool)$ e $M(\ind)$ sono 910rispettivamente gli insiemi distinti $\two$ e $\ind$ nell'universo 911$\cal U$. 912 913Si assumer� d'ora in avanti che le strutture di tipo e i loro modelli 914sono standard. 915 916\subsection{Firme standard} 917\label{standard-signatures} 918\index{firme, della logica HOL@firme, della logica \HOL{}!standard}\index{firme standard, della logica HOL@firme standard, della logica \HOL{}} 919 920Una firma $\Sigma_{\Omega}$ � {\em standard\/} se contiene le 921seguenti tre costanti primitive\index{costanti primitive, della logica HOL@costanti primitive, della logica \HOL{}}\index{costanti, nella logica HOL@costanti, nella logica \HOL{}!primitive, forma astratta di}: 922\[ 923{\imp}_{\ty{bool}\fun\ty{bool}\fun\ty{bool}} 924\] 925\[ 926{=}_{\alpha\fun\alpha\fun\ty{bool}} 927\] 928\[ 929\hilbert_{(\alpha\fun\ty{bool})\fun\alpha} 930\] 931L'interpretazione intesa di queste costanti � che $\imp$ denota 932l'implicazione, $=_{\sigma\fun\sigma\fun\ty{bool}}$ denota l'uguaglianza 933sull'insieme denotato da $\sigma$, e 934$\hilbert_{(\sigma\fun\ty{bool})\fun\sigma}$ denota una funzione di scelta 935sull'insieme denotato da $\sigma$. Pi� precisamente, un modello $M$ di 936$\Sigma_{\Omega}$ sar� chiamato {\em standard\/}\index{modelli standard, della logica HOL@modelli standard, della logica \HOL{}} se 937\begin{itemize} 938 939\item 940$M({\imp},\bool\fun\bool\fun\bool)\in(\two\fun\two\fun\two)$ � 941la funzione d'implicazione standard\index{implicazione, nella logica HOL@implicazione, nella logica \HOL{}!semantica formale della}, che manda $b,b'\in\two$ su 942\[ 943(b\imp b') = \left\{ \begin{array}{ll} 944 0 & \mbox{se $b=1$ e $b'=0$} \\ 945 1 & \mbox{altrimenti} 946 \end{array} 947 \right.%} 948\] 949 950\item 951$M({=},\alpha\fun\alpha\fun\bool)\in\prod_{X\in{\cal U}}.X\fun 952X\fun\two$ � la funzione che assegna ad ogni $X\in{\cal U}$ 953la funzione di test dell'uguaglianza\index{uguaglianza, nella logica HOL@uguaglianza, nella logica \HOL{}!semantica formale della}, che manda $x,x'\in X$ a 954\[ 955(x=_{X}x') = \left\{ \begin{array}{ll} 956 1 & \mbox{se $x=x'$} \\ 957 0 & \mbox{altrimenti} 958 \end{array} 959 \right.%} 960\] 961 962\item 963\index{operatore epsilon}$M(\hilbert,(\alpha\fun\bool)\fun\alpha)\in\prod_{X\in{\cal 964U}}.(X\fun\two)\fun X$ � la funzione cha assegna ad ogni $X\in{\cal 965U}$ la funzione di scelta\index{operatore di scelta, nella logica HOL@operatore di scelta, nella logica \HOL{}!semantica formale del} che manda $f\in(X\fun\two)$ a 966\[ 967\ch_{X}(f) = \left\{ \begin{array}{ll} 968 \ch(f^{-1}\{1\}) 969 & \mbox{se $f^{-1}\{1\}\not=\emptyset$}\\ 970 \ch(X) & \mbox{altrimenti} 971 \end{array} 972 \right.%} 973\] 974dove $f^{-1}\{1\}=\{x\in X : f(x)=1\}$. (Si noti che $f^{-1}\{1\}$ � in 975$\cal U$ quando non � vuota, per la propriet� {\bf Sub} 976dell'universo $\cal U$ data nella Sezione~\ref{introduction}. La funzione 977$\ch$ � data dalla propriet� {\bf Choice}.) 978 979\end{itemize} 980 981Si assumer� da qui in avanti che le firme e i loro modelli sono 982standard. 983 984\medskip 985 986\noindent{\bf Nota\ } 987Questa particolare scelta delle costanti primitive � arbitraria. La 988collezione standard delle costanti logiche include $\T$ (`vero'), $\F$ 989(`falso')\index{valori di verit�, nella logica HOL@valori di verit�, nella logica \HOL{}!forma astratta di}, $\imp$ (`implica'), $\wedge$ (`e'), $\vee$ 990(`o'), $\neg$ (`non'), $\forall$ (`per tutti'), $\exists$ (`esiste'), 991$=$ (`� uguale'), $\iota$ (`il'), e $\hilbert$ (`un'). Questo 992insieme � ridondante, dal momento che pu� essere definito (in un senso spiegato nella 993Sezione~\ref{defs}) da vari sottoinsiemi. In pratica, � 994necessario lavorare con l'insieme completo delle costanti logiche, e il 995particolare sottoinsieme preso come primitivo non � importante. il lettore 996interessato pu� esplorare ulteriormente questo argomento leggendo il libro 997di Andrews~\cite{Andrews} e i riferimenti che esso contiene. 998 999\medskip 1000 1001I termini di tipo \ty{bool} sono chiamati {\it formule\/}\index{formule come termini, nella logica HOL@formule come termini, nella logica \HOL{}}. 1002 1003Sono usate le seguenti abbreviazioni notazionali: 1004 1005\begin{center} 1006\index{uguaglianza, nella logica HOL@uguaglianza, nella logica \HOL{}!forma astratta di} 1007\index{implicazione, nella logica HOL@implicazione, nella logica \HOL{}!forma astratta di} 1008\index{operatore di scelta, nella logica HOL@operatore di scelta, nella logica \HOL{}!forma astratta di} 1009\index{quantificatore esistenziale, nella logica HOL@quantificatore esistenziale, nella logica \HOL{}!forma astratta di} 1010\index{quantificatore universale, nella logica HOL@quantificatore universale, nella logica \HOL{}!forma astratta di} 1011\index{operatore epsilon} 1012\begin{tabular}{|l|l|}\hline 1013{\rm Notazione} & {\rm Significato}\\ \hline 1014$t_{\sigma}=t'_{\sigma}$ & 1015 $=_{\sigma\fun\sigma\fun\ty{bool}}\ t_{\sigma}\ t'_{\sigma}$\\ \hline 1016$t\imp t'$ & 1017 $\imp_{\ty{bool}\fun\ty{bool}\fun\ty{bool}}\ t_\ty{bool}\ 1018t'_\ty{bool}$\\ \hline 1019$\hilbert x_{\sigma}.\ t$ & 1020 $ \hilbert_{(\sigma\fun\ty{bool})\fun\sigma} 1021(\lambda x_{\sigma}.\ t)$\\ \hline 1022\end{tabular} 1023\end{center} 1024Queste notazioni sono casi speciali di convenzioni generali di abbreviazione 1025supportate dal sistema \HOL{}. Le prime due sono infissi e la 1026terza � un binder (si vedano le sezioni di \DESCRIPTION\/ sul parsing e 1027il pretty-printing). 1028 1029 1030 1031%%% Local Variables: 1032%%% mode: latex 1033%%% TeX-master: "logic" 1034%%% End: 1035