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