1\chapter{La Logica \HOL{} in ML}\label{HOLsyschapter} 2 3In questo capitolo, � descritta la concreta rappresentazione della logica 4\HOL{}. Questo implica descrivere le funzioni \ML\ che contengono 5l'interfaccia alla logica (fino alla 6Sezione~\ref{sec:system-terms} inclusa); le quotation, il parsing, e la stampa dei 7tipi e dei termini logici (Sezione~\ref{quotation}); la rappresentazione dei 8teoremi (Sezione~\ref{sec:theorems-in-ml}); la rappresentazione delle teorie 9(Sezione~\ref{theoryfns}); la fondamentale teoria \HOL{} \texttt{bool} 10(Sezione~\ref{boolfull}); le regole primitive d'inferenza 11(Sezione~\ref{rules}); e i metodi per estendere le teorie 12(nella Sezione~\ref{theoryfns} e anche pi� avanti nella 13Sezione~\ref{sec:bossLib}). Si assume che il lettore sia familiare 14con l'\ML. Se non lo �, dovrebbe leggere prima l'introduzione all'\ML\ in {\sl Getting Started 15with HOL\/} nel \TUTORIAL. 16 17Il sistema \HOL{} fornisce i tipi \ML\ \ml{hol\_type} e \ml{term} 18che implementano i tipi e i termini della logica \HOL{}, come definito in 19\LOGIC. Esso fornisce anche delle funzioni \ML\ primitive per creare e 20manipolare valori di questi tipi. Su questa base � implementata la logica 21\HOL{}. L'idea chiave del sistema \HOL{} dovuta a Robin 22Milner\index{Milner, R.}, e discussa in questo capitolo, � che 23i teoremi sono rappresentati da un tipo astratto \ML\ i cui unici 24valori predefiniti sono gli assiomi, e le cui sole operazioni sono regole 25d'inferenza. Questo significa che l'unico modo per costruire teoremi in 26\HOL{} � quello di applicare le regole d'inferenza ad assiomi o a teoremi esistenti; 27di conseguenza la coerenza della logica � preservata. 28 29Il proposito del meta-linguaggio \ML\ � di fornire un ambiente 30di programmazione in cui costruire strumenti di dimostrazione per assistere nella 31costruzione di dimostrazioni. Quando il build del sistema \HOL{} � eseguito, una variet� di 32utili teoremi � pre-dimostrato e un insieme di strumenti pre-definito. Il sistema 33di base cos� offre un ricco ambiente iniziale; gli utenti lo possono arricchire ulteriormente 34implementando i loro propri strumenti per applicazioni specifiche e costruire 35le loro teorie per applicazioni specifiche. 36 37 38\section{Questioni lessicali}\label{HOL-lex} 39 40\index{identificatori, nella logica HOL@identificatori, nella logica \HOL{}|(} Il nome 41di una variabile \HOL{} 42% 43\index{tokens|(} 44\index{variabili, nella logica HOL@variabili, nella logica \HOL{}!nomi di|(} 45% 46pu� essere qualsiasi stringa \ML{}, ma il meccanismo di quotation eseguir� il parsing solo 47di nomi che sono identificatori (si veda la Sezione~\ref{ident} di sotto). Usare dei non-identificatori come nomi di variabili � sconsigliato eccetto in circostanze 48speciali (per esempio, quando si scrivono delle regole derivate che generano 49variabili con nomi che sono garantiti essere differenti da nomi 50esistenti). Il nome di una variabile di tipo 51% 52\index{variabili di tipo, nella logica HOL@variabili di tipo, nella logica \HOL{}!nomi di} 53% 54nella logica \HOL{} � formato da un apice (\ml{'}) seguito da un 55alfanumerico che a sua volta non contiene apici (si veda la Sezione~\ref{tyvars} 56per degli esempi). Il nome di una costante di tipo o di un termine costante nella 57logica \HOL{} pu� essere qualsiasi identificatore, bench� alcuni nomi sono trattati 58in modo speciale dal parser e dal printer di HOL e dovrebbero quindi essere 59evitati. 60% 61\index{identificatori, nella logica HOL@identificatori, nella logica \HOL{}|)} 62 63\subsection{identificatori}\label{ident} 64 65In aggiunta a forme speciali gi� presenti nella grammatica rilevante, 66un identificatore \HOL{} pu� essere di due forme: 67\begin{myenumerate} 68\item Una sequenza finita di \emph{alfanumerici} che cominciano con una lettera. Il 69 carattere di underscore � considerato un carattere numerico, e cos� pu� 70 occorrere dopo la prima lettera di un identificatore. I caratteri greci (approssimativamente 71 caratteri Unicode che variano da \ml{U+0370} a \ml{U+03FF}) sono anch'essi lettere, eccetto per 72 $\lambda$~(\ml{U+03BB}), che � trattata come un simbolo. \HOL{} � 73 case-sensitive: le lettere maiuscole e minuscole sono considerate essere 74 differenti. 75 76 Le cifre sono i caratteri ASCII 0--9, il carattere di underscore, e i 77 sottoscritti e i soprascritti Unicode. Il carattere di apostrofo 78 � speciale.% 79 \index{apostrofo, gestione lessicale del} 80 % 81 Non � una lettera, ma pu� comparire come parte di un identificatore di termine 82 alfanumerico dopo la prima lettera. Esso deve apparire all'inizio del 83 nome di una variabile di tipo, e pu� anche apparire nel contesto di un termine come 84 una sequenza di apostrofi per conto proprio. 85 86\item Un identificatore \emph{simbolico}, cio�, una sequenza finita formata da 87 qualsiasi combinazione dei simboli ASCII e dei simboli Unicode. I 88 simboli ASCII di base sono 89\begin{verbatim} 90 # ? + * / \ = < > & % @ ! : | - ^ ` 91\end{verbatim} 92 L'uso del segno di omissione e del carattere di accento circonflesso � complicato dal fatto 93 che questi caratteri hanno un significato speciale nel meccanismo 94 di quotation; si veda la Sezione~\ref{sec:quotation-antiquotation}. I simboli 95 ASCII di raggruppamento (graffe, quadre, e parentesi tonde), e i caratteri 96 tilde~(\holtxt{\symbol{126}}), il punto~(\holtxt{.}), 97 la virgola~(\holtxt{,}), il punto-e-virgola~(\holtxt{;}) e il trattino~(\holtxt{-}) 98 sono chiamati caratteri \emph{non-aggreganti}. % 99% 100 \index{identificatori, nella logica HOL@identificatori, nella logica \HOL{}!caratteri non-aggreganti}% 101% 102 A meno che il token desiderato non sia gi� presente nella grammatica, questi 103 caratteri non si combinano tra di loro o con altri caratteri 104 simbolici. Cos�, la stringa \holtxt{"(("} � vista come \emph{due} 105 token, cos� come lo sono \holtxt{"+;"} e \holtxt{"-+"}. 106 107 \index{token!Caratteri unicode} 108 \index{Unicode} 109 I caratteri unicode che non sono n� lettere n� cifre sono considerati 110 come simboli. Nessuno di questi � non-aggregante. 111 112\item Un \emph{numero} � una stringa di una o pi� cifre. Se non � la 113 cifra iniziale, un underscore pu� essere usato all'interno della sequenza per 114 fornire una spaziatura. Al fine di distinguere differenti generi di numeri 115 si pu� usare un singolo carattere suffisso: per esempio \holtxt{3n} � un 116 numero naturale mentre \holtxt{3i} � un intero. I prefissi \holtxt{0x} e 117 \holtxt{0b} possono anche essere usati per cambiare la base del 118 numero. Se � usato il prefisso \holtxt{0x}, possono anche essere usate 119 le `cifre' esadecimali \holtxt{a}--\holtxt{f} e \holtxt{A}--\holtxt{F}. 120 Si veda anche la Sezione~\ref{sec:numerals}.% 121\end{myenumerate} 122\index{variabili, nella logica HOL@variabili, nella logica \HOL{}!names of|)} 123 124 125\paragraph{Separatori} 126 127I separatori usati dall'analizzatore lessicale \HOL{} sono (con i codici ASCII tra 128parentesi): 129 130\bigskip 131 132lo spazio (32), il carriage return (13), il line feed (10), il tab ({\verb+^+}I, 9), 133il form feed ({\verb+^+}L, 12) 134 135 136\paragraph{Identificatori speciali} 137 138I seguenti identificatori validi sono usati dalla grammatica nella teoria 139dei booleani, e di conseguenza anche in tutte le teorie discendenti. Essi non 140dovrebbero essere usati come il nome di una variabile o di una costante a meno che l'utente sia 141molto confidente della propria abilit� di perdere tempo con le grammatiche 142% 143\begin{verbatim} 144 let in and \ . ; => | : := with updated_by case of 145\end{verbatim} 146 147\paragraph {Nomi di variabili di tipo}\label{tyvars} 148 149Il nome di una variabile di tipo nella logica \HOL{} � una stringa 150che comincia con un apice (\ml{'}) seguito da un alfanumerico che a sua volta 151non contiene primi; per esempio tutti quelli che seguono sono nomi validi 152di variabili di tipo eccetto l'ultimo: 153% 154\begin{hol} 155\begin{verbatim} 156 'a 'b 'cat 'A11 'g_a_p 'f'oo 157\end{verbatim} 158\end{hol} 159 160\paragraph{Token utente} 161In generale, un utente \HOL{} ha una grande quantit� di libert� di creare la sua propria sintassi, richiedendo token speciali a prescindere dalle variabili e dai nomi per le costanti. 162Per esempio, la sintassi if-then-else per l'operatore condizionale % 163\index{condizionali, nella logica HOL@condizionali, nella logica \HOL{}!stampa dei}% 164ha token speciali (l'``if'', il ``then'' e l'``else'') che non sono nomi per le variabili, n� per le costanti (la costante sottostante � di fatto chiamata \holtxt{COND}). 165Per essere sicuro che le operazioni di stampa e parsing dei token siano appropriatamente l'una l'inverso dell'altra, gli utenti non dovrebbero creare token che includono spazi vuoti o le stringhe di commento (\ml{(*} and \ml{*)}). 166\index{token|)} 167 168\section{Tipi}\index{tipi, nella logica HOL@tipi, nella logica \HOL{}} 169 170I tipi ammessi dipendono da quali costanti di tipo 171% 172\index{costanti di tipo, nella logica HOL@costanti di tipo, nella logica \HOL{}} 173% 174sono state dichiarate nella teoria corrente. Si veda la Sezione~\ref{theoryfns} 175per i dettagli di come tali dichiarazioni sono fatte. Ci sono due funzioni 176primitive 177% 178\index{tipi, nella logica HOL@tipi, nella logica \HOL{}!costruttori per} 179\index{costruttori di tipo!nella logica HOL@nella logica \HOL{}} 180% 181che fungono da costruttori per valori di tipo \ml{hol\_type}: 182% 183\index{tipi funzioni, nella logica HOL@tipi funzioni, nella logica \HOL{}!costruttori per} 184\index{mk_vartype@\ml{mk\_vartype}|pin} 185\index{mk_type@\ml{mk\_type}|pin} 186\begin{holboxed} 187\begin{verbatim} 188 mk_vartype : string -> hol_type 189 mk_thy_type : {Tyop:string, Thy:string, Args:hol_type list} -> hol_type 190\end{verbatim} 191\end{holboxed} 192% 193La funzione \ml{mk\_vartype} costruisce una variabile di tipo 194% 195\index{variabili di tipo, nella logica HOL@variabili di tipo, nella logica \HOL{}!costruttori per} 196% 197con un nome dato; essa da un warning se il nome non � un nome ammissibile 198per una variabile di tipo (cio� non � un \ml{'} seguito da un alfanumerico). 199La funzione \ml{mk\_thy\_type} costruisce un tipo composto 200% 201\index{tipi composti, nella logica HOL@tipi composti, nella logica \HOL{}!costruttori per} 202% 203da un record \ml{\lb Tyop,Thy,Args\rb{}} dove \ml{Tyop} � una stringa 204che rappresenta il nome di un operatore di tipo, \ml{Thy} � una stringa 205che rappresenta la teoria in cui \ml{Tyop} � stato dichiarato, e \ml{Args} 206� una lista di tipi che rappresentano gli argomenti dell'operatore. 207I tipi funzione $\sigma_1\fun\sigma_2$ della logica sono rappresentati in 208\ML{} come se fossero tipi composti $(\sigma_1,\sigma_2)$\ml{fun} 209(in \LOGIC, tuttavia, i tipi funzioni non erano considerati come tipi 210composti). 211 212La valutazione di 213$\ml{mk\_thy\_type}\{\ml{Tyop} = \mathit{name},\ 214\ml{Thy} = \mathit{thyname},\ 215\ml{Args} = [\sigma_1, \cdots ,\sigma_n]\}$ 216fallisce se 217% 218\begin{myenumerate} 219\item $\mathit{name}$ non � un tipo operatore della teoria $\mathit{thyname}$ 220\item $\mathit{name}$ � un tipo operatore della teoria $\mathit{thyname}$, 221ma la sua ariet� non � $n$. 222\end{myenumerate} 223% 224Per esempio, \ml{mk\_thy\_type\lb{}Tyop="bool", Thy="bool", Args=[]\rb{}} 225\index{valori di verit�, nella logica HOL@valori di verit�, nella logica \HOL{}} 226\index{bool, il tipo nella logica HOL@\ml{bool}, il tipo nella logica \HOL{}} 227� valutato a un valore \ML{} di tipo \ml{hol\_type} che rappresenta il tipo 228\ty{bool}. 229% 230%\paragraph{Support for constructing types} 231 232Le costanti di tipo possono essere 233legate a valori \ML\ e non hanno bisogno di essere costruiti ripetutamente, ad esempio il tipo costruito da\linebreak 234\ml{mk\_thy\_type\lb{}Tyop="bool", Thy="bool", Args=[]\rb{}} � abbreviato 235dal valore \ML\ \ml{bool}. Analogamente, i tipi funzione possono essere costruiti 236con la funzione infissa \ML\ \ml{-->}. Alcune variabili di tipo comuni 237sono state costruite e legate a identificatori \ML{}, ad esempio, \ml{alpha} 238� la variabile di tipo \ml{'a} e \ml{beta} � la variabile di tipo 239\ml{'b}. Cos� il codice \ML\ \ml{alpha --> bool} � uguale a, ma molto pi� conciso di 240% 241\begin{hol} 242\begin{verbatim} 243 mk_thy_type{Tyop="fun", Thy="min", 244 Args=[mk_vartype "'a", 245 mk_thy_type{Tyop="bool", Thy="bool", Args=[]}} 246\end{verbatim} 247\end{hol} 248 249%\paragraph{Taking types apart} 250 251\noindent 252Ci sono due funzioni primitive 253% 254\index{tipi, nella logica HOL@tipi, nella logica \HOL{}!de-costruttori per} 255\index{de-costruttori di tipo, nella logica HOL@de-costruttori di tipo, nella logica \HOL{}} 256% 257che fungono da de-costruttori per valori di tipo \ml{hol\_type}: 258\begin{holboxed} 259\index{tipi funzione, nella logica HOL@tipi funzione, nella logica \HOL{}!de-costruttori per} 260\index{dest_vartype@\ml{dest\_vartype}|pin} 261\index{dest_thy_type@\ml{dest\_thy\_type}|pin} 262\begin{verbatim} 263 dest_vartype : hol_type -> string 264 dest_thy_type : hol_type -> {Tyop:string, Thy:string, Args:hol_type list} 265\end{verbatim} 266\end{holboxed} 267 268\noindent La funzione \ml{dest\_vartype} 269% 270\index{variabili di tipo, nella logica HOL@variabili di tipo, nella logica \HOL{}!de-costruttori per} 271\index{tipi composti, nella logica HOL@tipi composti, nella logica \HOL{}!de-costruttori per} 272% 273estrae il nome di una variabile di tipo. Un tipo composto � de-costruito 274dalla funzione \ml{dest\_thy\_type} nel nome dell'operatore 275di tipo, il nome della teoria in cui esso fu dichiarato, e una lista dei 276tipi argomento; \ml{dest\_vartype} e \ml{dest\_thy\_type} sono cos� 277le inverse di \ml{mk\_vartype} e \ml{mk\_thy\_type}, rispettivamente. 278I de-costruttori falliscono su argomenti della forma sbagliata. 279 280\section{Termini}\label{sec:system-terms} 281 282Le quattro specie primitive di termini della logica sono descritte in 283\LOGIC. Le funzioni \ML\ per manipolarle sono descritte in 284questa sezione. Ci sono anche termini \emph{derivati} che sono descritti 285nella Sezione~\ref{derived-terms}. 286 287In qualunque momento, i termini che possono essere costruiti dipendono da quali 288costanti sono state dichiarate nella teoria corrente. Si veda 289la Sezione~\ref{theoryfns} per i dettagli su come sono fatte queste dichiarazioni. 290 291Ci sono quattro funzioni primitive 292\index{variabili, nella logica HOL@variabili, nella logica \HOL{}!costruttori per} 293\index{termini, nella logica HOL@termini, nella logica \HOL{}!costruttori per} 294\index{costruttori di termini, nella logica HOL@costruttori di termini, nella logica \HOL{}} 295che fungono da costruttori per valori di tipo \ml{term}: 296 297\begin{holboxed} 298\index{mk_var@\ml{mk\_var}|pin} 299\begin{verbatim} 300 mk_var : (string * hol_type) -> term 301\end{verbatim} 302\end{holboxed} 303 304\noindent\ml{mk\_var($x$,$\sigma$)} � valutata a una variabile 305con nome $x$ e tipo $\sigma$; essa ha sempre successo. 306 307\begin{holboxed} 308\index{mk_thy_const@\ml{mk\_thy\_const}|pin} 309\begin{verbatim} 310 mk_thy_const : {Name:string, Thy:string, Ty:hol_type} -> term 311\end{verbatim} 312\end{holboxed} 313 314\noindent $\mathtt{mk\_thy\_const}\{\mathtt{Name} = \mathit{c},\ 315\mathtt{Thy} = \mathit{thyname},\ \mathtt{Ty} = \sigma\}$ 316 � valutata a un termine che rappresenta la costante 317\index{costanti, nella logica HOL@costanti, nella logica \HOL{}!costruttori per} 318con nome $c$ e tipo $\sigma$; essa fallisce se: 319\begin{myenumerate} 320% \item $c$ is not an allowable constant name; 321\item $c$ non � il nome di una costante nella teoria $\mathit{thyname}$; 322\item $\sigma$ non � un'istanza del tipo generico di $c$ 323(il tipo generico di una costante � stabilito quando la costante � definita; 324si veda la Sezione~\ref{theoryfns}). 325\end{myenumerate} 326 327\begin{holboxed}\index{mk_comb@\ml{mk\_comb}|pin} 328\begin{verbatim} 329 mk_comb : (term * term) -> term 330\end{verbatim} 331\end{holboxed} 332 333\noindent\ml{mk\_comb($t_1$,$t_2$)} 334% 335\index{applicazione di funzione, nella logica HOL@applicazione di funzione, nella logica \HOL{}!costruttore per} 336% 337� valutata a un termine che rappresenta la combinazione 338% 339\index{combinazioni, nella logica HOL@combinazioni, nella logica \HOL{}!costruttori per} 340% 341$t_1\ t_2$. Essa fallisce se: 342\begin{myenumerate} 343\item il tipo di $t_1$ non ha la forma \ml{$\sigma'$->$\sigma$}; 344\item il tipo di $t_1$ ha la forma \ml{$\sigma'$->$\sigma$}, ma il 345tipo di $t_2$ non � uguale a $\sigma'$. 346\end{myenumerate} 347 348\begin{holboxed} 349\index{mk_abs@\ml{mk\_abs}|pin} 350\begin{verbatim} 351 mk_abs : (term * term) -> term 352\end{verbatim} 353\end{holboxed} 354 355\noindent\ml{mk\_abs($x$,$t$)} � valutato a un termine che rappresenta 356l'astrazione 357% 358\index{astrazione di funzione, nella logica HOL@astrazione di funzione, nella logica \HOL{}!costruttore per} 359% 360$\lquant{x}t$; essa fallisce se $x$ non � una variabile. 361 362 363Le quattro funzioni primitive di de-costruzione sui termini sono: 364% 365\index{de-costruttori di termini, nella logica HOL@de-costruttori di termini, nella logica \HOL{}} 366\index{variabili, nella logica HOL@variabili, nella logica \HOL{}!de-costruttori per} 367\index{costanti, nella logica HOL@costanti, nella logica \HOL{}!de-costruttori per} 368\index{combinazioni, nella logica HOL@combinazioni, nella logica \HOL{}!de-costruttori per} 369\index{astrazione di funzione, nella logica HOL@astrazione di funzione, nella logica \HOL{}!de-costruttori per} 370\index{applicazione di funzione, nella logica HOL@applicazione di funzione, nella logica \HOL{}!de-costruttori per} 371% 372 373\begin{holboxed} 374 375\index{dest_var@\ml{dest\_var}|pin} 376\index{dest_thy_const@\ml{dest\_thy\_const}|pin} 377\index{dest_comb@\ml{dest\_comb}|pin} 378\index{dest_abs@\ml{dest\_abs}|pin} 379\begin{verbatim} 380 dest_var : term -> (string * hol_type) 381 dest_thy_const : term -> {Name:string, Thy:string, Ty:hol_type} 382 dest_comb : term -> (term * term) 383 dest_abs : term -> (term * term) 384\end{verbatim} 385\end{holboxed} 386 387Queste sono le inverse di \ml{mk\_var}, \ml{mk\_thy\_const}, 388\ml{mk\_comb} e \ml{mk\_abs}, rispettivamente. Esse falliscono quando applicate 389a termini della forma sbagliata. Altre utili funzioni di de-costruzione sono 390\ml{rator}\index{rator@\ml{rator}}, 391\ml{rand}\index{rand@\ml{rand}}, 392\ml{bvar}\index{bvar@\ml{bvar}}, 393\ml{body}\index{body@\ml{body}}, 394\ml{lhs}\index{lhs@\ml{lhs}} and 395\ml{rhs}\index{rhs@\ml{rhs}}. 396Si veda \REFERENCE\ per i dettagli. 397 398La funzione 399 400\begin{holboxed}\index{type_of@\ml{type\_of}|pin} 401\begin{verbatim} 402 type_of : term -> hol_type 403\end{verbatim} 404\end{holboxed} 405 406\noindent restituisce il tipo 407\index{tipi, nella logica HOL@tipi, nella logica \HOL{}!determinazione di} 408di un termine. La funzione 409 410\begin{holboxed}\index{aconv@\ml{aconv}|pin} 411\begin{verbatim} 412 aconv : term -> term -> bool 413\end{verbatim} 414\end{holboxed} 415 416\noindent implementa il test di $\alpha$-convertibil� per 417termini del $\lambda$-calcolo. 418% 419\index{$\alpha$-convertibil�, nella logica HOL@$\alpha$-convertibil�, nella logica \HOL{}!determinazione di} 420% 421Dal punto di vista della logica \HOL{}, i termini $\alpha$-convertibili 422sono identici. Una variet� di altre funzioni sono disponibili per 423eseguire la $\beta$-riduzione (\ml{beta\_conv}), l'$\eta$-riduzione 424(\ml{eta\_conv}), la sostituzione (\ml{subst}), l'istanziazione di tipo (\ml{inst}), la computazione delle variabili libere (\ml{free\_vars}) e 425altre operazioni comuni sui termini. Si veda \REFERENCE{} per maggiori dettagli. 426 427 428\section{Quotation} 429\label{quotation}\label{gen-abs}\label{let} 430\index{type checking, nella logica HOL@type checking, nella logica \HOL{}!della sintassi delle quotation|(} 431\index{quotation, nella logica HOL@quotation, nella logica \HOL{}|(} 432\index{ type quotes, in ML@\ml{\dq:$\cdots$\dq} (type quotes, in \ML)|(} 433\index{ term quotes, in ML@\ml{\dq$\cdots$\dq} (term quotes, in \ML)|(} 434 435Sarebbe noioso dover sempre immettere tipi e termini 436usando le funzioni costruttore. Il sistema \HOL{}, adattando 437l'approccio preso in \LCF\index{LCF@\LCF}, ha dei parser 438speciali per le quotation 439\index{quotation, nella logica HOL@quotation, nella logica \HOL{}!parser per} 440\index{parsing, della logica HOL@parsing, della logica \HOL{}!delle quotation di sintassi} 441per tipi e termini \HOL{} che permettono di immettere 442tipi e termini usando una sintassi abbastanza standard. Per esempio, 443l'espressione \ML{} $\holquote{\ml{:bool -> bool}}$ denota esattamente lo stesso 444valore (con tipo \ML\ \ml{hol\_type}) di 445 446\begin{hol} 447\index{bool, the type nella logica HOL@\ml{bool}, the type nella logica \HOL{}} 448\begin{verbatim} 449 mk_thy_type{Tyop = "fun",Thy = "min", 450 Args = [mk_thy_type{Tyop = "bool", Thy = "bool", Args = []}, 451 mk_thy_type{Tyop = "bool", Thy = "bool", Args = []}]} 452\end{verbatim} 453\end{hol} 454 455\noindent e l'espressione \holtxt{\holquote{\bs{}x.~x~+~1}} 456% 457\index{astrazione di funzione, nella logica HOL@astrazione di funzione, nella logica \HOL{}} 458% 459pu� essere usata al posto di\footnote{Per poter essere elaborata con successo 460 questa quotation richiede che la teoria dell'aritmetica sia gi� 461 stata caricata, il che si pu� ottenere nel sistema interattivo attraverso 462 \ml{load "arithmeticTheory"}.} 463 464\begin{hol} 465\begin{verbatim} 466 let val numty = mk_thy_type{Tyop="num",Thy="num",Args=[]} 467 in 468 mk_abs 469 (mk_var("x",numty), 470 mk_comb(mk_comb 471 (mk_thy_const 472 {Name="+",Thy="arithmetic",Ty=numty --> numty --> numty}, 473 mk_var("x", numty)), 474 mk_comb(mk_thy_const{Name="NUMERAL",Thy="arithmetic",Ty=numty-->numty}, 475 mk_comb(mk_thy_const{Name="BIT1",Thy="arithmetic",Ty=numty-->numty}, 476 mk_thy_const{Name="ZERO",Thy="arithmetic",Ty=numty})))) 477 end 478\end{verbatim} 479\end{hol} 480 481Il printer \HOL{}, che � integrato nel loop toplevel \ML{}, 482mostra in output anche i tipi e i termini usando questa sintassi. 483% 484\index{stampa, nella logica HOL@stampa, nella logica \HOL{}!della sintassi delle quotation} 485% 486I tipi sono stampati 487% 488\index{stampa, nella logica HOL@stampa, nella logica \HOL{}!dei tipi} 489% 490nella forma \holquote{\ml{:}\textit{type}}. Per esempio, il valore \ML\ 491di tipo \ml{hol\_type} che rappresenta 492$\alpha\fun(\ty{ind}\fun\ty{bool})$ sarebbe stampato 493come \ml{\holquote{:'a -> ind -> bool}}. 494Analogamente, i termini sono stampati nella forma \holquote{\textit{term}}. 495Cos�, il termine che rappresenta $\uquant{x\ y}x<y \imp\equant{z}x+z = y$ 496sarebbe stampato come: 497% 498\[ \holquote{\ml{!x y. x < y ==> ?z. x + z = y}} \] 499% 500Un segno iniziale di due punti � usato per distinguere una quotation di tipo da una quotation di termine: 501la prima ha la forma \holquote{\ml{:}~$\cdots$~} e il secondo ha 502la forma \holquote{~$\cdots$~}. 503\index{quotation, nella logica HOL@quotation, nella logica \HOL{}|)} 504 505La Sessione~\ref{sec:parsing-printing} ha informazioni pi� dettagliate circa 506le capacit� delle funzioni di parsing e stampa di termini e tipi 507nel sistema. Il resto di questa sezione fornisce una breve 508panoramica di ci� che � possibile. 509 510 511\subsection{Inferenza di tipo} 512\index{inferenza di tipo!nel parser HOL@nel parser \HOL{}|(} 513% 514Si noti che non c'� alcuna informazione esplicita di tipo in 515\holtxt{\bs{}x.x+1}. Il type checker \HOL{} sa che \ml{1} ha 516il tipo \holtxt{num} e \holtxt{+} ha il tipo \holtxt{num->(num->num)}. 517Da questa informazione esso pu� inferire che entrambe le occorrenze di \ml{x} in 518\holtxt{\bs{}x.x+1} potrebbero avere il tipo \holtxt{num}. Questa non � 519l'unica assegnazione di tipo possibile; per esempio, la prima occorrenza di 520\holtxt{x} potrebbe avere il tipo \holtxt{bool} e la seconda avere il tipo 521\holtxt{num}. In quel caso ci sarebbero due variabili 522\emph{differenti} con nome \holtxt{x}, cio� \holtxt{x}$_{\holtxt{bool}}$ e 523\holtxt{x}$_{\holtxt{num}}$, la seconda delle quali � libera. Tuttavia, 524l'unico modo di costruire in termine con questa seconda assegnazione di tipo � 525usando dei costruttori, dal momento che il type checker usa l'euristica che tutte 526le variabili in un termine con lo stesso nome hanno lo stesso tipo. Questo � 527illustrato nella sessione seguente. 528% 529\setcounter{sessioncount}{0} 530\begin{session} 531\begin{verbatim} 532- ``x = (x = 1)``; 533Type inference failure: unable to infer a type for the application of 534 535$= (x :num) 536 537which has type 538 539:num -> bool 540 541to 542 543(x :num) = (1 :num) 544 545which has type 546 547:bool 548 549unification failure message: unify failed 550\end{verbatim} 551\end{session} 552 553Il valore desiderato pu� essere costruito direttamente per mezzo delle funzioni costruttore 554primitive: 555 556\begin{session} 557\begin{verbatim} 558- mk_eq 559 (mk_var("x",bool), 560 mk_eq(mk_var("x",numty), 561 mk_numeral (Arbnum.fromString "1"))); 562> val it = ``x <=> (x = 1)`` : term 563\end{verbatim} 564\end{session} 565 566Il type checker delle quotation originario fu progettato e implementato da 567Robin milner\index{Milner, R.}. Esso sfrutta delle euristiche come quella 568di sopra per inferire un tipo sensato per tutte le variabili che occorrono in un termine. 569 570\index{vincoli di tipo!nella logica HOL@nella logica \HOL{}} A volte, 571l'utente pu� voler controllare il tipo esatto di un sottotermine. Per supportare tale 572funzionalit�, i tipo possono essere indicati esplicitamente facendo seguire a qualsiasi 573termine un simbolo di due punti e poi un tipo. Per esempio, dato 574\holtxt{\dq{}f(x:num):bool\dq} il type checker assegner� a \holtxt{f} il tipo 575\holtxt{num->bool} e a \holtxt{x} il tipo 576\holtxt{num}. Questo trattamento dei tipi all'interno delle quotation � ereditato 577da \LCF. 578% 579\index{LCF@\LCF} 580\index{ type quotes, in ML@\ml{\dq:$\cdots$\dq} (type quotes, in \ML)|)} 581\index{ term quotes, in ML@\ml{\dq$\cdots$\dq} (term quotes, in \ML)|)} 582\index{type inference!nel parser HOL@nel parser \HOL{}|)} 583 584\subsection{Visualizzare la grammatica} 585 586\index{parsing, della logica HOL@parsing, della logica \HOL{}!grammatiche per il} 587\index{stampa, nella logica HOL@stampa, nella logica \HOL{}!grammatiche per la} 588Il comportamento del parser e del printer di \HOL{} � determinato 589dalla grammatica corrente. Cos�, � importante una familiarit� con il vocabolario 590della collezione standard di teorie di \HOL{} se si vuole usare 591\HOL{} in modo efficace. Si pu� esaminare la grammatica attuale usata 592dal parser con le funzioni \verb+type_grammar+ e 593\verb+term_grammar+. 594 595Per esempio, nella seguente sessione, vediamo che la grammatica dei tipi 596usata nel contesto di avvio di \HOL{} ha gli operatori di tipo 597\verb+fun+, \verb+sum+, \verb+prod+, \verb+list+, \verb+recspace+, 598\verb+num+, \verb+option+, \verb+one+, \verb+label+, \verb+ind+, and 599\verb+bool+. 600 601\setcounter{sessioncount}{0} 602\begin{session} 603\begin{verbatim} 604- type_grammar(); 605> val it = 606 Rules: 607 (50) TY ::= TY -> TY [fun] (R-associative) 608 (60) TY ::= TY + TY [sum] (R-associative) 609 (70) TY ::= TY # TY [prod] (R-associative) 610 (100) TY ::= TY list | TY recspace | num | (TY, TY)prod | TY option | 611 one | (TY, TY)sum | label | (TY, TY)fun | ind | bool 612 : grammar 613\end{verbatim} 614\end{session} 615 616Inoltre, \verb+fun+, \verb+sum+, e \verb+prod+ hanno le notazioni 617infisse (\verb+->+), (\verb|+|), e (\verb+#+), rispettivamente, con 618differenti precedenze: \verb+#+ (con 70) lega in modo pi� forte di 619\verb|+| (60), che lega pi� forte di \verb+->+ (50). Tutti gli 620operatori di tipo suffissi (con 100) legano pi� fortemente di quelli infissi. 621 622La prossima sessione, nella Figura~\ref{fig:term-grammar}, mostra 623l'output (abbreviato) dell'invocazione della funzione \ml{term\_grammar} 624nell'ambiente di avvio di \HOL{}. L'output omesso include un elenco 625di tutte le costanti conosciute dal sistema, inclusi gli operatori prefissi, 626insieme con tutti gli overload attualmente attivi. La grammatica ritratta 627varia da operatori di binding con forza di binding molto bassa (0), 628fino all'applicazione di funzione (2000) e alla selezione di record (2500), 629che legano molto strettamente. 630 631\setcounter{sessioncount}{0} 632\begin{figure}[htbp] 633\begin{session} 634\begin{verbatim} 635- term_grammar(); 636> val it = 637 (0) TM ::= "LEAST" <..binders..> "." TM | 638 "?!" <..binders..> "." TM | "?" <..binders..> "." TM | 639 "!" <..binders..> "." TM | "@" <..binders..> "." TM | 640 "\" <..binders..> "." TM 641 (2) TM ::= "let" TM "in" TM [let] 642 (4) TM ::= TM "::" TM (restricted quantification operator) 643 (5) TM ::= TM TM (binder argument concatenation) 644 (7) TM ::= "case" TM "of" TM [case__magic] 645 (8) TM ::= TM "|" TM [case_split__magic] (R-associative) 646 (9) TM ::= TM "and" TM (L-associative) 647 (10) TM ::= TM "=>" TM [case_arrow__magic] (R-associative) 648 (50) TM ::= TM "##" TM | TM "," TM (R-associative) 649 (70) TM ::= "if" TM "then" TM "else" TM [COND] 650 (80) TM ::= TM ":-" TM (non-associative) 651 (100) TM ::= TM "=" TM (non-associative) 652 (200) TM ::= TM "==>" TM (R-associative) 653 (300) TM ::= TM "\/" TM (R-associative) 654 (400) TM ::= TM "/\" TM (R-associative) 655 (425) TM ::= TM "IN" TM (non-associative) 656 (440) TM ::= TM "++" TM (L-associative) 657 (450) TM ::= TM "::" TM [CONS] | TM ">=;" TM | TM "<=" TM | 658 TM ">" TM | TM "<;" TM | TM ">=" TM | TM "<=" TM | 659 TM ">" TM | TM "<" TM | TM "LEX" TM | TM "RSUBSET" TM | 660 TM ":=" TM [record field update] | 661 TM "updated_by" TM [functional record update] | 662 TM "with" TM [record update] 663 (R-associative) 664 (500) TM ::= TM "-" TM | TM "+" TM | TM "RUNION" TM (L-associative) 665 (600) TM ::= TM "DIV" TM | TM "*" TM | TM "RINTER" TM 666 (L-associative) 667 (650) TM ::= TM "MOD" TM (L-associative) 668 (700) TM ::= TM "**" TM | TM "EXP" TM (R-associative) 669 (800) TM ::= TM "O" TM | TM "o" TM (R-associative) 670 (900) TM ::= "~" TM 671 (1000) TM ::= TM ":" TY (type annotation) 672 (2000) TM ::= TM TM (function application) | (L-associative) 673 (2500) TM ::= TM "." TM [record field selection] (L-associative) 674 TM ::= "[" ... "]" (separator = ";") | 675 "<|" ... "|>" (separator = ";") 676 TM ::= "(" ")" [one] | 677 "(" TM ")" [just parentheses, no term produced] 678 ... <further output omitted> 679 : grammar 680\end{verbatim} 681\end{session} 682\caption{Risultato della chiamata a \ml{term\_grammar()}} 683\label{fig:term-grammar} 684\end{figure} 685 686\subsection{Controllo di namespace} 687 688Per convenienza, il parser tratta con l'overload e 689l'ambiguit�. L'overload di letterali numerici � discusso nella 690Sessione~\ref{arith-overloading}, bench� a qualunque simbolo si possa applicare 691l'overload, non solo i numerali. A volte una tale flessibilit� � piuttosto 692utile; comunque, pu� accadere che si voglia designare in modo esplicito 693una costante particolare. In quel caso, la notazione 694$\mathit{thy}\holtxt{\$}\mathit{const}$ pu� essere usata nel parser per 695designare la costante $\mathit{const}$ dichiarata nella teoria 696$\mathit{thy}$. Nell'esempio seguente, � esplicitamente specificato 697l'operatore minore-di. 698 699\setcounter{sessioncount}{0} 700\begin{session} 701\begin{verbatim} 702- ``prim_rec$< x y`` 703> val it = ``x < y`` : term 704\end{verbatim} 705\end{session} 706Si noti come il simbolo \holtxt{<} non sia trattato come un infisso dal 707parser quando fornito nella sua forma ``fully-qualified''. Dal punto di vista sintattico, a tali 708token non � mai dato un trattamento speciale dal parser della sintassi 709concreta di \HOL. 710% 711\index{costanti, nella logica HOL@costanti, nella logica \HOL{}!nomi di ... fully-qualified} 712 713\section{Modi di Costruire Tipi e Termini} 714 715\index{variabili di tipo, nella logica HOL@variabili di tipo, nella logica \HOL{}!costruttori per} 716\index{costruttori di tipo!nella logica HOL@nella logica \HOL{}} 717\index{costruttori di termine, nella logica HOL@costruttori di termine, nella logica \HOL{}|(} 718\index{termini, nella logica HOL@termini, nella logica \HOL{}!costruttori per|(} 719La tabella di sotto mostra l'espressioni \ML\ per varie specie di quotazioni 720di tipo\index{quotation, nella logica HOL@quotation, nella logica \HOL{}!di tipi}. 721L'espressioni nella stessa riga sono equivalenti. 722 723\bigskip 724 725\begin{center} 726\index{tipi composti, nella logica HOL@tipi composti, nella logica \HOL{}!costruttori per} 727\index{ variabili di tipo, nella logica HOL@\ml{'a,\,'b,\,}$\ldots$ (variabili di tipo, nella logica \HOL{})} 728\index{tipi, nella logica HOL@tipi, nella logica \HOL{}!costruttori per} 729\index{ operatore di tipo funzione, nella logica HOL@\ml{->} (operatore di tipo funzione, nella logica \HOL{})} 730\index{mk_vartype@\ml{mk\_vartype}} 731\index{mk_type@\ml{mk\_type}} 732\index{virgolette di tipo, in ML@\ml{`:$\cdots$`} (virgolette di tipo, in \ML)} 733\begin{tabular}{|l|l|l|} \hline 734\multicolumn{3}{|c|}{ } \\ 735\multicolumn{3}{|c|}{\bf Types} \\ 736\multicolumn{3}{|c|}{ } \\ 737{\it Specie di tipo} & {\it quotation \ML} & {\it Espressione costruttore} \\ \hline 738 & & \\ 739Variabile di tipo & 740{\small\verb+: '+}{\small $alphanum$} & {\small\verb+mk_vartype("'+$alphanum$\verb+")+} \\ \hline 741Costante di tipo & $:op$ & {\small\verb+mk_type("+}$op${\small\verb+",[])+} \\ \hline 742 & $:\mathit{thy}$\verb+$+$\mathit{op}$ 743 & \parbox{7cm} 744 {\small \holtxt{mk\_thy\_type\lb{}Thy="}$\mathit{thy}$\holtxt{",} \newline 745 \holtxt{\quad Tyop="}$\mathit{op}$\holtxt{", Args=[]\rb{}}} \\ \hline 746Tipo funzione & $: \sigma_1$ {\small\verb+->+} $\sigma_2$ & 747$\sigma_1$ {\small\verb+-->+} $\sigma_2$ \\ 748\hline 749Tipo composto & 750{\small\verb+:(+}$\sigma_1${\small\verb+,+} $\ldots$ {\small\verb+,+} $\sigma_n${\small\verb+)+}$op$ & 751{\small\verb+mk_type("+}$op${\small\verb+", [+} 752 $\sigma_1$ {\small\verb+,+} $\ldots$ {\small\verb+,+} $\sigma_n${\small\verb+])+} 753\\ 754\hline 755& {\small\verb+:(+}$\sigma_1${\small\verb+,+} $\ldots$ {\small\verb+,+} $\sigma_n${\small\verb+)+}$\mathit{thy}$\verb+$+$\mathit{op}$ 756& \parbox{7cm} 757 {\small \holtxt{mk\_thy\_type\lb{}Thy="}$\mathit{thy}$\holtxt{",} \newline 758 \holtxt{\quad Tyop="}$\mathit{op}$\holtxt{", Args=[} 759 $\sigma_1, \ldots, \sigma_n$ \holtxt{]\rb{}}} \\ \hline 760\end{tabular} 761\end{center} 762 763 764Modi equivalenti di immettere le quattro specie di termini primitivi sono mostrati nella 765prossima tabella. 766 767\bigskip 768 769\begin{center} 770\index{combinazioni, nella logica HOL@combinazioni, nella logica \HOL{}!quotation of} 771\index{termini, nella logica HOL@termini, nella logica \HOL{}!primitive} 772\index{termini, nella logica HOL@termini, nella logica \HOL{}!costruttori per} 773\index{quotation, nella logica HOL@quotation, nella logica \HOL{}!di termini primitivi} 774\index{astrazione di funzione, nella logica HOL@astrazione di funzione, nella logica \HOL{}!symbol for} 775\index{applicazione di funzione, nella logica HOL@applicazione di funzione, nella logica \HOL{}!costruttori per} 776\index{applicazione di funzione, nella logica HOL@applicazione di funzione, nella logica \HOL{}!sintassi delle} 777\index{variabili, nella logica HOL@variabili, nella logica \HOL{}!costruttori per} 778\index{variabili, nella logica HOL@variabili, nella logica \HOL{}!sintassi delle} 779\index{mk_var@\ml{mk\_var}} 780\index{mk_const@\ml{mk\_const}} 781\index{mk_comb@\ml{mk\_comb}} 782\index{mk_abs@\ml{mk\_abs}} 783\begin{tabular}{|l|l|l|} \hline 784\multicolumn{3}{|c|}{ } \\ 785\multicolumn{3}{|c|}{\bf Termini primitivi} \\ 786\multicolumn{3}{|c|}{ } \\ 787{\it Specie di termine} & {\it quotation \ML} & 788{\it Espressione costruttore} \\ \hline 789 & & \\ 790Variabile & $var${\small\verb+:+}$\sigma$ & 791{\small\verb+mk_var("+}$var${\small\verb+",+}$\sigma${\small\verb+)+} \\ \hline 792% 793Costante & $const${\small\verb+:+}$\sigma$ & 794{\small\verb+mk_const("+}$const${\small\verb+",+}$\sigma${\small\verb+)+} \\ \hline 795% 796Costante & $\mathit{thy}$\verb+$+$\mathit{const}${\small\verb+:+}$\sigma$ & 797{\small\verb+mk_thy_const{Name="+}$\mathit{const}${\small\verb+",Thy="+}$\mathit{thy}${\small\verb+",Ty=+}$\sigma${\small\verb+}+} \\ \hline 798% 799Combinazione & $t_1\ t_2$ & 800{\small\verb+mk_comb(+}$t_1${\small\verb+, +}$t_2${\small\verb+)+} \\ \hline 801% 802Atrazione & \holtxt{\bs$x$.$t$} & 803{\small\verb+mk_abs(+}$x${\small\verb+, +}$t${\small\verb+)$+} \\ \hline 804\end{tabular} 805\end{center} 806% 807\index{type checking, nella logica HOL@type checking, nella logica \HOL{}!delle quotation di sintassi|)} 808 809In aggiunta alle specie di termini nella tabella di sopra, il parser supporta 810anche le seguenti abbreviazioni sintattiche. 811 812 813\begin{center} 814 815\index{variabili, nella logica HOL@variabili, nella logica \HOL{}!legate in modo multiplo} 816\index{list_mk_comb@\ml{list\_mk\_comb}|pin} 817\index{list_mk_abs@\ml{list\_mk\_abs}|pin} 818\index{list_mk_forall@\ml{list\_mk\_forall}|pin} 819\index{list_mk_exists@\ml{list\_mk\_exists}|pin} 820\index{combinazioni, nella logica HOL@combinazioni, nella logica \HOL{}!abbreviazione per ... multiple} 821\index{quantificatore esistenziale, nella logica HOL@quantificatore esistenziale, nella logica \HOL{}!abbreviazione per ... multiplo} 822\index{quantificatore universale, nella logica HOL@quantificatore universale, nella logica \HOL{}!abbreviazione per ... multiplo} 823\begin{tabular}{|l|l|l|} \hline 824\multicolumn{3}{|c|}{ } \\ 825\multicolumn{3}{|c|}{\bf Operazioni sintattiche} \\ 826\multicolumn{3}{|c|}{ } \\ 827{\it Termine abbreviato} & {\it Significato} & 828{\it Espressione costruttore} \\ \hline 829 & & \\ 830$t\ t_1 \cdots t_n$ & 831{\small\verb+(+}$\cdots${\small\verb+(+}$t\ t_1${\small\verb+)+}$\cdots t_n${\small\verb+)+} & 832{\small\verb+list_mk_comb(+}$t${\small\verb+,[+}$t_1${\small\verb+, +}$\ldots${\small\verb+ ,+}$t_n${\small\verb+])+} \\ \hline 833{\small\verb+\+}$x_1\cdots x_n${\small\verb+.+}$t$ & 834\holtxt{\bs}$x_1${\small\verb+. +}$\cdots${\small\verb+ \+}$x_n${\small\verb+.+}$t$ & 835{\small\verb+list_mk_abs([+}$x_1${\small\verb+, +}$\ldots${\small\verb+ ,+}$x_n${\small\verb+],+}$t${\small\verb+)+} 836\\ \hline 837\end{tabular} 838\end{center} 839 840 841\section{Teoremi} 842\label{sec:theorems-in-ml} 843 844In \LOGIC, la nozione di deduzione � stata introdotta in termini di 845\textit{sequenti}, 846% 847\index{sequenti!nella deduzione naturale} 848% 849dove un sequente � una coppia il cui secondo componente � una formula che viene 850asserita (una conclusione), 851% 852\index{conclusioni!di sequenti} 853% 854e il cui primo componente � un insieme di formule 855(ipotesi). 856% 857\index{ipotesi!di sequenti} 858% 859Su questo era basata la nozione di un \textit{sistema 860 deduttivo}: 861\index{deduzione naturale} 862\index{sistemi deduttivi} 863% 864un insieme di coppie, il cui secondo componente � un sequente, e il cui primo 865componente � un insieme di sequenti\footnote{Si noti che questi sequenti formano 866 una lista, non un insieme; cio�, sono ordinati.}. Fu quindi definito il concetto di un sequente 867\textit{che segue da} 868% 869\index{segue da, nella deduzione naturale} 870% 871un insieme di sequenti attraverso un sistema deduttivo: un sequente 872segue da un insieme di sequenti se il sequente � l'ultimo elemento di 873qualche catena di sequenti, ognuno dei cui elementi o � nell'insieme, 874o esso stesso segue dall'insieme attraverso elementi precedenti della 875catena, attraverso il sistema deduttivo. 876 877\index{notazione turnstile|(} E' stata poi introdotta una notazione per `segue 878da'. Il fatto che un sequente\linebreak $(\{t_1,\ldots,t_n\},\ t)$ segua da un 879insieme di sequenti $\Delta$, attraverso un sistema deduttivo ${\cal D}$, � 880denotato da: $t_1,\ldots,t_n\vdash_{{\cal D},\Delta} t$. (E' stato notato 881che dove sia ${\cal D}$ sia $\Delta$ sono fossero chiari dal contesto, la loro 882menzione potrebbe essere omessa; e dove l'insieme delle ipotesi fosse vuoto, 883la sua menzione potrebbe essere omessa.) 884 885Un sequente che segue dall'insieme vuoto di sequenti attraverso un sistema 886deduttivo � chiamato un \textit{teorema} di quel sistema deduttivo. In altre 887parole, un teorema 888% 889\index{teoremi, nella deduzione naturale} 890% 891� l'ultimo elemento di una \textit{dimostrazione} 892% 893\index{dimostrazione!nella deduzione naturale} 894% 895(nel senso di \LOGIC) dall'insieme vuoto di sequenti. Quando una coppia 896$(L,(\Gamma,t))$ appartiene a un sistema deduttivo, e la lista $L$ � 897vuota, allora il sequente $(\Gamma,t)$ � chiamato un 898\textit{assioma}\index{assiomi!nella deduzione naturale}. Qualsiasi coppia 899$(L,(\Gamma,t))$ appartenente a un sistema deduttivo � chiamata una 900\textit{inferenza primitiva}\index{inferenza, nella deduzione 901 naturale}\index{inferenza primitiva, nella deduzione naturale} del 902sistema, con ipotesi\footnote{Si noti che `ipotesi' e 903 `conclusione' sono usate anche per le componenti dei sequenti.} $L$ e 904conclusione $(\Gamma,t)$. 905 906Una formula 907% 908\index{formule come termini, nella logica HOL@formule come termini, nella logica \HOL{}} 909% 910in astratto � rappresentata concretamente in \HOL{} da un termine il cui 911tipo \HOL{} � \holtxt{:bool}. Perci�, un termine 912% 913\index{termini, nella logica HOL@termini, nella logica \HOL{}!come formule logiche} 914% 915di tipo \holtxt{:bool} � usato per rappresentare un membro dell'insieme di 916ipotesi di un sequente; e allo stesso modo per rappresentare la conclusione di un 917sequente. Gli insiemi in questo contesto sono rappresentati da un'implementazione della 918firma \ML{} \ml{HOLset} che supporta operazioni come 919\ml{member} e \ml{union}. 920% 921\index{sequenti!rappresentazione dei, nella logica HOL@rappresentazione dei, nella logica \HOL{}} 922 923Un teorema in astratto � rappresentato concretamente nel sistema 924\HOL{} da un valore con il tipo \ML{} astratto \ml{thm}. 925% 926\index{thm (tipo ML)@\ml{thm} (tipo \ML{})} 927% 928Il tipo \ml{thm} ha una funzione de-costruttore 929 930\begin{holboxed} 931\index{dest_thm@\ml{dest\_thm}|pin} 932\begin{verbatim} 933 dest_thm : thm -> (term list * term) 934\end{verbatim} 935\end{holboxed} 936 937\noindent che restituisce una coppia che consiste, rispettivamente, di una lista delle 938ipotesi 939\index{ipotesi!di teoremi} 940e della conclusione, 941\index{conclusioni!di teoremi} 942% 943di un teorema. Non si dovrebbe fare affidamento sull'ordine delle assunzioni 944nella lista. Le ipotesi di un teorema sono disponibili anche nella forma 945di insieme con la funzione 946 947\begin{holboxed} 948\index{hyp_set@\ml{hyp\_set}} 949\begin{verbatim} 950 hyp_set : thm -> term HOLset.set 951\end{verbatim} 952\end{holboxed} 953 954Usando \ml{dest\_thm}, sono derivate ulteriori funzioni di 955\index{teoremi, nella logica HOL@teoremi, nella logica \HOL{}!de-costruttori per} 956de-costruzione 957 958\begin{holboxed} 959\index{hyp@\ml{hyp}|pin} 960\index{concl@\ml{concl}|pin} 961\begin{verbatim} 962 hyp : thm -> term list 963 concl : thm -> term 964\end{verbatim} 965\end{holboxed} 966 967\noindent per estrarre, rispettivamente, la lista delle ipotesi e la conclusione 968di un teorema. Il tipo \ML\ non ha 969una funzione costruttore primitiva. In questo modo, il sistema di tipi \ML{} protegge 970la logica \HOL{} 971dalla costruzione arbitraria e non tracciata 972di teoremi, che comprometterebbero 973la coerenza\index{coerenza, della logica HOL@coerenza, della logica \HOL{}} della logica. 974(Le funzioni che restituiscono teoremi come valori, ad esempio le funzioni che rappresentano inferenze primitive, 975sono discusse nella Sezione~\ref{rules}.) 976%% derived-rules reference is dead for the moment (until we 977%% resuscitate drules.tex) 978%, and further in Chapter\ref{derived-rules}.) 979 980In \LOGIC � stato menzionato che il sistema deduttivo di \HOL{} 981include quattro assiomi\footnote{Questa � una semplificazione: di fatto i 982 vari assiomi sono un'estensione della logica di base.}. In quel 983manuale, gli assiomi sono stati presentati in forma astratta. Concretamente, 984gli assiomi sono semplicemente valori teorema che sono introdotti attraverso l'uso della 985funzione \ML{} \ml{new\_axiom} (si veda la Sessione~\ref{theoryprims} 986di sotto). Per esempio, l'assioma \ml{BOOL\_CASES\_AX} menzionato in 987\LOGIC{} � stampato in \HOL{} come segue (dove \ml{T} e 988\ml{F} sono le costanti della logica \HOL{} che rappresentano la verit� e 989la falsit�, rispettivamente): 990 991\begin{hol} 992\index{F (falsity), the HOL constant@\holtxt{F} (falsity), the \HOL{} constant!axiom for} 993\begin{verbatim} 994 |- !t. (t = T) \/ (t = F) : thm 995\end{verbatim} 996\end{hol} 997 998\noindent 999Si noti lo speciale formato di stampa, 1000\index{stampa, nella logica HOL@stampa, nella logica \HOL{}!dei teoremi} 1001% 1002con l'approssimazione 1003alla notazione astratta $\vdash$, 1004% 1005\index{notazione dei teoremi, nella logica HOL@notazione dei teoremi, nella logica \HOL{}|(} 1006% 1007\ml{|-}, usata per indicare lo status di tipo \ML{} \ml{thm}; insieme con 1008l'assenza dei segni di quotation \HOL{} 1009% 1010\index{ segno di teorema, nella logica HOL@\ml{"|-} (segno di teorema, nella logica \HOL{})} 1011% 1012nel contesto \ml{|-}. La sessione di sotto illustra l'uso delle 1013funzioni di de-costruzione: 1014 1015\setcounter{sessioncount}{0} 1016\begin{session} 1017\begin{verbatim} 1018 - val th = BOOL_CASES_AX; 1019 > val th = |- !t. (t = T) \/ (t = F) : thm 1020 1021 - hyp th; 1022 > val it = [] : term list 1023 1024 - concl th; 1025 > val it = ``!t. (t = T) \/ (t = F)`` : term 1026 1027 - type_of it; 1028 > val it = ``:bool`` : hol_type 1029\end{verbatim} 1030\end{session} 1031\index{notazione turnstile|)} 1032 1033\noindent In aggiunta alle convenzioni di stampa menzionate di sopra, la 1034stampa di teoremi stampa le ipotesi 1035\index{stampa, nella logica HOL@stampa, nella logica \HOL{}!delle ipotesi dei teoremi} 1036come dei punti (cio� un singolo punto di conclusione o dei puntini). Il flag \ml{show\_assums} 1037\index{show_assums@\ml{show\_assums}} permette di stampare i teoremi 1038con le ipotesi mostrate in modo completo. Questi punti sono illustrati con un 1039teorema inferito, a scopo di esempio, da un altro assioma menzionato 1040in \LOGIC, \ml{SELECT\_AX}. 1041 1042\begin{session} 1043\begin{verbatim} 1044- val th = UNDISCH (SPEC_ALL SELECT_AX); 1045> val th = [.] |- P ($@ P) : thm 1046 1047- show_assums := true; 1048> val it = () : unit 1049 1050- th; 1051> val it = [P x] |- P ($@ P) : thm 1052\end{verbatim} 1053\end{session} 1054\index{notazione dei teoremi, nella logica HOL@notazione dei teoremi, nella logica \HOL{}|)} 1055 1056\section{Regole Primitive d'Inferenza della Logica \HOL{}} 1057\label{rules} 1058 1059\index{regole d'inferenza, della logica HOL@regole d'inferenza, della logica \HOL{}!primitive|(} 1060% 1061Le regole primitive d'inferenza della logica sono state descritte 1062in astratto in \LOGIC. Le descrizioni si basavano su meta-variabili $t$, 1063$t_1$, $t_2$, e cos� via. Nella logica \HOL{}, infinite famiglie di 1064inferenze primitive sono raggruppate insieme e pensate come singoli 1065schemi primitivi di inferenza. % 1066% 1067\index{famiglie d'inferenze, nella logica HOL@famiglie d'inferenze, nella logica \HOL{}} 1068% 1069Ciascuna famiglia contiene tutte le istanze concrete di un particolare 1070`pattern' d'inferenza. Queste possono essere prodotte, in astratto, 1071istanziando le meta-variabili delle regole in \LOGIC\ su termini 1072concreti. 1073 1074In \HOL, gli schemi primitivi d'inferenza sono rappresentati da funzioni \ML{} 1075che restituiscono teoremi come valori. Cio�, per particolari termini \HOL{}, 1076le funzioni \ML{} restituiscono l'istanza del teorema per quei termini. 1077Le funzioni \ML{} sono parte del tipo \ML{} astratto 1078\ml{thm}: 1079% 1080\index{thm (tipo ML)@\ml{thm} (tipo \ML{})} 1081% 1082bench� \ml{thm} non abbia dei costruttori primitivi, esso ha (otto) 1083operazioni che restituiscono teoremi come valori: \ml{ASSUME}, \ml{REFL}, 1084\ml{BETA\_CONV}, \ml{SUBST}, \ml{ABS}, \ml{INST\_TYPE}, \ml{DISCH} e 1085\ml{MP}. 1086% 1087\index{schemi d'inferenza, nella logica HOL@schemi d'inferenza, nella logica \HOL{}} 1088 1089Le funzioni \ML{} che implementano gli schemi primitivi d'inferenza nel 1090sistema \HOL{} sono descritte di sotto. E' usata qui la stessa notazione 1091% 1092\index{inferenze, nella logica HOL@inferenze, nella logica \HOL{}!notazione per le} 1093% 1094usata in \LOGIC: le ipotesi sono sopra una linea orizzontale e la 1095conclusione 1096% 1097\index{conclusioni!delle regole d'inferenza} di sotto. Per le costanti logiche � usata 1098la notazione {\small ASCII} leggibile dalla macchina. 1099 1100\subsection{Introduzione di assunzione} 1101% 1102\index{introduzione di assunzione, nella logica HOL@introduzione di assunzione, nella logica \HOL{}!funzione ML per@funzione \ML{} per} 1103 1104\begin{holboxed} 1105\index{ASSUME@\ml{ASSUME}|pin} 1106\begin{verbatim} 1107 ASSUME : term -> thm 1108\end{verbatim}\end{holboxed} 1109 1110\begin{center} 1111\begin{tabular}{c} 1112 \\ \hline 1113$t${\small\verb+ |- +}$t$ \\ 1114\end{tabular} 1115\end{center} 1116 1117\noindent 1118{\small\verb+ASSUME +}$t${\small\verb++} � valutata a $t${\small\verb+|- +}$t$. 1119Fallisce se $t$ non � di tipo \ml{bool}. 1120 1121\bigskip 1122 1123\subsection{Riflessivit�}\index{riflessivit�, nella logica HOL@riflessivit�, nella logica \HOL{}!funzione ML per@funzione \ML\ per} 1124 1125\begin{holboxed}\index{REFL@\ml{REFL}|pin} 1126\begin{verbatim} 1127 REFL : term -> thm 1128\end{verbatim} 1129\end{holboxed} 1130 1131\begin{center} 1132\begin{tabular}{c} 1133 \\ \hline 1134{\small\verb+ |- +}$t${\small\verb+ = +}$t$ \\ 1135\end{tabular} 1136\end{center} 1137 1138\noindent {\small\verb+REFL +}$t${\small\verb++} � valutata a 1139{\small\verb+|- +}$t${\small\verb+ = +}$t$. Una chiamata a \ml{REFL} non fallisce mai. 1140 1141\bigskip 1142 1143\subsection{Beta-conversione} 1144\index{beta-conversione, nella logica HOL@beta-conversione, nella logica \HOL{}!funzione ML per@funzione \ML\ per} 1145 1146\begin{holboxed}\index{BETA_CONV@\ml{BETA\_CONV}|pin} 1147\begin{verbatim} 1148 BETA_CONV : term -> thm 1149\end{verbatim} 1150\end{holboxed} 1151 1152\begin{center} 1153\begin{tabular}{c} 1154 \\ \hline 1155\holtxt{ |- (\bs$x$.$t_1$)$t_2$ = $t_1[t_2/x]$} 1156\end{tabular} 1157\end{center} 1158 1159\begin{itemize} 1160\item dove $t_1[t_2/x]$ denota il risultato di sostituire $t_2$ per $x$ 1161in $t_1$, con una rinomina appropriata delle variabili per evitare che variabili libere 1162in $t_2$ diventino legate dopo la sostituzione. La sostituzione 1163 $t_1[t_2/x]$ � sempre definita. 1164\end{itemize} 1165 1166%'' below makes latex font-locking cope with the "unbalanced" double 1167%back-tick quotations. 1168\noindent \ml{BETA\_CONV ``(\bs$x$.$t_1$)$t_2$``} %'' 1169� valutata al teorema \ml{|- (\bs$x$.$t_1$)$t_2$ = $t_1[t_2/x]$}. 1170Fallisce se l'argomento a \ml{BETA\_CONV} non � un $\beta$-redex 1171(cio� non � della forma \holtxt{(\bs$x$.$t_1$)$t_2$}. 1172 1173\bigskip 1174 1175\subsection{Sostituzione}\index{regola di sostituzione, nella logica HOL@regola di sostituzione, nella logica \HOL{}!funzione ML per@funzione \ML\ per|(}\index{SUBST@\ml{SUBST}|(} 1176 1177\begin{holboxed} 1178\begin{verbatim} 1179 SUBST : (thm * term)list -> term -> thm -> thm 1180\end{verbatim}\end{holboxed} 1181 1182\begin{center} 1183\begin{tabular}{c} 1184$\Gamma_1${\small\verb+ |- +} $t_1${\small\verb+=+}$t'_1$ {\small\verb+ +} $\cdots$ {\small\verb+ +} 1185$\Gamma_n${\small\verb+ |- +} $t_n${\small\verb+=+}$t'_n$ {\small\verb+ +} 1186$\Gamma${\small\verb+ |- +} $t[t_1,\ldots,t_n]$ \\ \hline 1187$\Gamma_1 \cup \cdots 1188\cup \Gamma_n \cup \Gamma${\small\verb+ |- +} $t[t'_1,\ldots,t'_n]$ \\ 1189\end{tabular} 1190\end{center} 1191 1192\bigskip 1193 1194\begin{itemize} 1195\item dove $t[t_1,\ldots,t_n]$ denota un termine $t$ con qualche occorrenza 1196libera dei termini $t_1$, $\dots$, $t_n$ scelti e 1197$t[t'_1,\ldots,t'_n]$ denota il risultato di sostituire simultaneamente ciascuna 1198di tali occorrenze di $t_i$ con $t'_i$ (per $1{\leq}i {\leq} n$), 1199con un'appropriata rinomina delle variabili per evitare che variabili libere 1200in $t_i'$ diventino legate dopo la sostituzione. 1201\end{itemize} 1202 1203\noindent 1204Il primo argomento a {\small\verb+SUBST+} � una lista 1205{\small\verb+[(|-+}$t_1${\small\verb+=+}$t'_1${\small\verb+, +}$x_1${\small\verb+);+}$\:\ldots\:${\small\verb+;(|-+}$t_n${\small\verb+=+} 1206$t'_n${\small\verb+, +}$x_n${\small\verb+)]+}. Il secondo argomento � 1207un template di termine $t[x_1,\ldots,x_n]$ in cui le occorrenze della variabile 1208$x_i$ (dove $1 \leq i\leq n$) sono usate per segnare gli spazi in cui 1209le sostituzioni con {\small\verb+|- +}$t_i${\small\verb+=+}$t'_i$ devono essere 1210fatte. Cos� 1211 1212\bigskip 1213 1214{\small\verb+SUBST [(|-+}$t_1${\small\verb+=+}$t'_1${\small\verb+, +}$x_1${\small\verb+);+}$\ldots${\small\verb+;(|-+}$t_n${\small\verb+=+} 1215$t'_n${\small\verb+, +}$x_n${\small\verb+)] +}$t[x_1,\ldots,x_n]${\small\verb+ +} 1216$\Gamma${\small\verb+ |- +}$t[t_1,\ldots,t_n]$ 1217 1218\bigskip 1219 1220\noindent restituisce $\Gamma${\small\verb+ |- +}$t[t'_1,\ldots,t'_n]$. 1221Fallisce se: 1222\begin{myenumerate} 1223\item qualcuno degli argomenti � della forma sbagliata; 1224\item il tipo di $x_i$ non � uguale al tipo di $t_i$ per qualche 1225$1\leq i\leq n$. 1226\end{myenumerate}\index{SUBST@\ml{SUBST}|)}\index{regola di sostituzione, nella logica HOL@regola di sostituzione, nella logica \HOL{}!funzione ML per@funzione \ML\ per|)} 1227 1228\subsection{Astrazione}\index{regola di astrazione, nella logica HOL@regola di astrazione, nella logica \HOL{}!funzione ML per@funzione \ML\ per} 1229\index{astrazione di funzione, nella logica HOL@astrazione di funzione, nella logica \HOL{}!regola d'inferenza per} 1230 1231 1232\begin{holboxed}\index{ABS@\ml{ABS}|pin} 1233\begin{verbatim} 1234 ABS : term -> thm -> thm 1235\end{verbatim}\end{holboxed} 1236 1237 1238\begin{center} 1239\begin{tabular}{c} 1240$\Gamma${\small\verb+ |- +}$t_1${\small\verb+ = +}$t_2$ \\ \hline 1241$\Gamma${\small\verb+ |- (\+}$x${\small\verb+.+}$t_1${\small\verb+) = (\+}$x${\small\verb+.+}$t_2${\small\verb+)+} \\ 1242\end{tabular} 1243\end{center} 1244 1245\begin{itemize} 1246\item dove $x$ non � libera in $\Gamma$. 1247\end{itemize} 1248 1249\noindent 1250{\small\verb+ABS +}$x${\small\verb+ +}$\Gamma${\small\verb+ |- +}$t_1${\small\verb+=+}$t_2$ restituisce il teorema 1251$\Gamma${\small\verb+ |- (\+}$x${\small\verb+.+}$t_1${\small\verb+) = (\+}$x${\small\verb+.+}$t_2${\small\verb+)+}. 1252Fallisce se $x$ non � una variabile, o $x$ 1253 occorre libera in qualcuna delle assunzioni in $\Gamma$. 1254 1255 1256\bigskip 1257 1258\subsection{Istanziazione di tipo} 1259\index{istanziazione di tipo, nella logica HOL@istanziazione di tipo, nella logica \HOL{}!funzione ML per@funzione \ML\ per} 1260\index{tipi, nella logica HOL@tipi, nella logica \HOL{}!istanziazione di} 1261 1262\begin{holboxed}\index{INST_TYPE@\ml{INST\_TYPE}|pin} 1263\begin{verbatim} 1264 INST_TYPE : {redex : hol_type, residue : hol_type} list -> thm -> thm 1265\end{verbatim} 1266\end{holboxed} 1267 1268\begin{center} 1269\begin{tabular}{c} 1270$\Gamma${\small\verb+ |- +}$t$ \\ \hline 1271$\Gamma[\sigma_1,\ \ldots\ ,\sigma_n/\alpha_1,\ \ldots\ ,\alpha_n]${\small\verb+ |- +}$t[\sigma_1,\ \ldots\ ,\sigma_n/\alpha_1,\ \ldots\ ,\alpha_n]$ 1272\end{tabular} 1273\end{center} 1274 1275\bigskip 1276 1277\begin{itemize} 1278\item dove $t[\sigma_1,\ \ldots\ ,\sigma_n/\alpha_1,\ \ldots\ ,\alpha_n]$ 1279denota il risultato di sostituire (in parallelo) i tipi $\sigma_1$, 1280$\ldots$\ , $\sigma_n$ per le variabili di tipo $\alpha_1$, $\ldots$\ , 1281$\alpha_n$ nel termine $t$. Analogamente, $\Gamma[\sigma_1,\ \ldots\ 1282,\sigma_n/\alpha_1,\ \ldots\ ,\alpha_n]$ denota il risultato di 1283eseguire la stessa sostituzione per tutte le ipotesi nell'insieme 1284$\Gamma$. 1285\end{itemize} 1286 1287\noindent 1288\ml{INST\_TYPE[$\alpha_1$~|->~$\sigma_1$% 1289 ,$\ldots$,$\alpha_n$~|->~$\sigma_n$]~$th$} restituisce il risultato di 1290sostituire ciascuna occorrenza di $\alpha_i$ nel teorema $th$ con 1291$\sigma_i$ (per $1 \leq i \leq n$). Si verifica un fallimento se un $\alpha_i$ non 1292� una variabile di tipo. 1293 1294La funzione \ML{} polimorfica infissa {\small\verb+|->+} � usata per 1295costruire valori del tipo record \ml{redex-residue}. Essa � definita 1296\begin{verbatim} 1297 fun ((x:'a) |-> (y:'b)) = {redex = x, residue = y} 1298\end{verbatim} 1299 1300\bigskip 1301 1302\subsection{Scaricamento di un'assunzione}\index{scaricamento di assunzioni, nella logica HOL@scaricamento di assunzioni, nella logica \HOL{}!funzione ML per@funzione \ML\ per} 1303 1304 1305\begin{holboxed}\index{DISCH@\ml{DISCH}|pin} 1306\begin{verbatim} 1307 DISCH : term -> thm -> thm 1308\end{verbatim}\end{holboxed} 1309 1310\begin{center} 1311\begin{tabular}{c} 1312$\Gamma${\small\verb+ |- +} $t_2$ \\ \hline 1313$\Gamma{-}\{t_1\}${\small\verb+ |- +} $t_1${\small\verb+ ==> +}$t_2$ 1314\end{tabular} 1315\end{center} 1316 1317\begin{itemize} 1318\item $\Gamma{-}\{t_1\}$ denota l'insieme ottenuto rimuovendo $t_1$ 1319da $\Gamma$ (si noti che non � necessario che $t_1$ occorra in $\Gamma$; in questo caso 1320$\Gamma{-}\{t_1\} = \Gamma$). 1321\end{itemize} 1322 1323\noindent 1324{\small\verb+DISCH +}$t_1${\small\verb+ +}$\Gamma${\small\verb+ |- +}$t_2$ 1325� valutata al teorema 1326$\Gamma{-}\{t_1\}${\small\verb+ |- +}$t_1${\small\verb+ ==> +}$t_2$. 1327\ml{DISCH} fallisce se il termine dato come suo primo argomento non � di 1328tipo \ml{bool}. 1329 1330 1331 1332\bigskip 1333 1334\subsection{Modus Ponens}\index{Modus Ponens, nella logica HOL@Modus Ponens, nella logica \HOL{}!funzione ML per@funzione \ML\ per} 1335 1336 1337\begin{holboxed}\index{MP@\ml{MP}|pin} 1338\begin{verbatim} 1339 MP : thm -> thm -> thm 1340\end{verbatim}\end{holboxed} 1341 1342\begin{center} 1343\begin{tabular}{c} 1344$\Gamma_1${\small\verb+ |- +}$t_1${\small\verb+ ==> +}$t_2$ {\small\verb+ +} $\Gamma_2${\small\verb+ |- +}$t_1$ \\ 1345\hline 1346$\Gamma_1 \cup \Gamma_2${\small\verb+ |- +}$t_2$ \\ 1347\end{tabular} 1348\end{center} 1349 1350\noindent 1351{\small\verb+MP+} prende due teoremi (nell'ordine mostrato di sopra) e restituisce 1352il risultato dell'applicazione del Modus Ponens; fallisce se gli argomenti non sono della 1353forma corretta. 1354\index{regole d'inferenza, della logica HOL@regole d'inferenza, della logica \HOL{}!primitive|)} 1355 1356\section{Oracoli} 1357 1358\HOL{} estende la tradizione \LCF\ permettendo l'uso di un 1359meccanismo di \emph{oracolo}, consentendo che formule arbitrarie diventino 1360elementi del tipo \ml{thm}. Per mezzo dell'uso di questo meccanismo, \HOL{} pu� 1361utilizzare i risultati di procedure di dimostrazione arbitrarie. Nonostante questa 1362liberalit�, si possono fare ancora forti asserzioni circa la sicurezza 1363degli oggetti ML di tipo \ml{thm}. 1364 1365Per evitare la non validit�, � attaccato un \emph{tag} a ogni teorema che deriva 1366da un oracolo. Questo tag � propagato attraverso ogni inferenza cui quel 1367teorema partecipa (un p� come le assunzioni ordinarie sono 1368propagate nella regola d'inferenza \ml{MP}). Se accade che la falsit� 1369sia derivata, l'oracolo incriminato pu� essere trovato esaminando i 1370tag componenti del teorema. Un teorema dimostrato senza l'uso di 1371oracoli avr� un tag vuoto, e pu� essere cos� considerato essere stato dimostrato 1372soltanto attraverso passi deduttivi nella logica HOL. 1373 1374Un teorema taggato pu� essere creato attraverso 1375 1376\begin{holboxed} 1377\index{mk_oracle_thm@\ml{mk\_oracle\_thm}!type of} 1378\begin{verbatim} 1379 mk_oracle_thm : string -> term list * term -> thm 1380\end{verbatim} 1381\end{holboxed} 1382 1383che crea direttamente il teorema richiesto e attacca ad esso il tag 1384dato. Il tag � creato attraverso una chiamata a 1385 1386\begin{holboxed} 1387\index{Tag.read@\ml{Tag.read}!making tags} 1388\begin{verbatim} 1389 Tag.read : string -> tag 1390\end{verbatim} 1391\end{holboxed} 1392 1393Oltre a fornire un accesso di principio ai risultati di ragionatori 1394esterni, i tag sono usati per implementare alcune utili operazioni di `sistema' 1395sui teoremi. Per esempio, si pu� creare direttamente un teorema attraverso la 1396funzione \ml{mk\_thm}. Il tag \verb+MK_THM+ viene attaccato ad ogni 1397teorema creato con questa chiamata. Questo permette agli utenti di creare direttamente 1398utili teoremi, ad esempio, da usare come dati di test per regole d'inferenza 1399derivate. Un altro tag � usato per implementare il cosiddetto `check 1400di validit�' per le tattiche. 1401 1402I tag in un teorema possono essere visualizzati impostando \verb+Globals.show_tags+ a 1403vero. 1404 1405\setcounter{sessioncount}{0} 1406\begin{session} 1407\begin{verbatim} 1408 - Globals.show_tags := true; 1409 > val it = () : unit 1410 1411 - mk_thm([], Term `F`);; 1412 > val it = [oracles: MK_THM] [axioms: ] [] |- F : thm 1413\end{verbatim} 1414\end{session}\index{mk_thm@\ml{mk\_thm}} 1415 1416Ci sono tre elementi alla sinistra del turnstile nella rappresentazioni completamente 1417stampata di un teorema: i primi due\footnote{I tag sono usati anche per 1418tenere traccia dell'uso di assiomi nelle dimostrazioni.} comprendono i tag componenti e il 1419terzo � la lista standard di assunzioni. Il tag componente di un teorema 1420pu� essere estratto da 1421 1422\begin{holboxed} 1423\begin{verbatim} 1424 Thm.tag : thm -> tag 1425\end{verbatim} 1426\end{holboxed} 1427 1428\noindent e stampato a video con 1429 1430\begin{holboxed} 1431\begin{verbatim} 1432 Tag.pp : ppstream -> tag -> unit. 1433\end{verbatim} 1434\end{holboxed} 1435 1436 1437\section{Teorie} 1438\label{theoryfns} 1439 1440\index{teorie, nella logica HOL@teorie, nella logica \HOL{}!rappresentazione di|(} 1441% 1442In \LOGIC{} una teoria � descritta come una $4$-upla 1443 1444\[ {\cal T}\ =\ \langle{\sf Struc}_{\cal T},\ 1445 {\sf Sig}_{\cal T},\ 1446 {\sf Axioms}_{\cal T},\ 1447 {\sf Theorems}_{\cal T}\rangle \] 1448 1449\noindent dove 1450\begin{myenumerate} 1451\item ${\sf Struc}_{\cal T}$ � 1452la struttura di tipo di ${\cal T}$; 1453\item ${\sf Sig}_{\cal T}$ � 1454la firma di ${\cal T}$; 1455\item ${\sf Axioms}_{\cal T}$ � 1456l'insieme di assiomi di ${\cal T}$; 1457\item ${\sf Theorems}_{\cal T}$ � l'insieme di 1458teoremi di ${\cal T}$. 1459\end{myenumerate} 1460 1461Nell'implementazione di \HOL, le teorie sono strutturate in modo gerarchico 1462per rappresentare sequenze di estensioni chiamate 1463\emph{segmenti} 1464% 1465\index{segmenti di teoria} 1466% 1467di una teoria iniziale chiamata \ml{min}\index{min@\ml{min}}. Un segmento di 1468teoria non � realmente un concetto logico, ma piuttosto un mezzo per 1469rappresentare teorie nel sistema \HOL{}. Ciascun segmento registra 1470alcuni tipi, costanti, assiomi e teoremi, insieme con dei puntatori ad 1471altri segmenti chiamati i suoi \emph{genitori} 1472% 1473\index{genitori, di teorie HOL@genitori, di teorie \HOL{}} 1474% 1475La teoria rappresentata da un segmento � ottenuta prendendo l'unione di 1476tutti i tipi, le costanti, gli assiomi e i teoremi nel segmento, insieme 1477con i tipi, le costanti, gli assiomi e i teoremi in tutti i segmenti 1478raggiungibili seguendo i puntatori ai genitori. Questa collezione di 1479segmenti raggiungibili � chiamata la \emph{stirpe} 1480% 1481\index{stirpe, delle teorie del sistema HOL@stirpe, delle teorie del sistema \HOL{}} 1482\index{teorie, nella logica HOL@teorie, nella logica \HOL{}!gerarchie di} 1483% 1484del segmento. 1485 1486\index{teorie, nella logica HOL@teorie, nella logica \HOL{}!rappresentazione di|)} 1487 1488\subsection{Funzioni ML per le operazioni sulle teorie} 1489\label{theoryprims} 1490 1491Un tipico\index{sistema HOL@sistema \HOL{}!lavoro tipico in} pezzo di lavoro 1492con il sistema \HOL{} consiste in un numero di sessioni\index{sessioni 1493con il sistema HOL@sessioni, con il sistema \HOL{}}. Nella prima di queste, � creata 1494una nuova teoria, diciamo ${\cal T}$, importando qualche segmento di teoria 1495esistente, facendo una serie di definizioni, e magari dimostrando e 1496archiviando alcuni teoremi nell'attuale segmento. Poi il segmento corrente 1497(nominato $name$ diciamo) � esportato. Il risultato concreto sar� un modulo \ML\ 1498$name$\ml{Theory} il cui contenuto � il segmento di teoria attuale 1499creato durante la sessione e la cui stirpe rappresenta la teoria logica 1500desiderata ${\cal T}$. Le sessioni di lavoro successive possono accedere alle 1501definizioni e ai teoremi di ${\cal T}$ importando $name$\ml{Theory}; 1502questo evita di dover caricare gli strumenti e rieseguire 1503le dimostrazioni che $name$\ml{Theory} ha creato in precedenza. 1504 1505Il nome dato ai dati nelle teorie � basato sul nome dato ai segmenti. 1506In modo specifico si accede\index{teorie, nella logica HOL@teorie, nella logica \HOL{}!nomina delle} a un assioma, 1507una definizione, una specifica o a un teorema 1508attraverso un identificatore lungo \ML\ $thy${\small\verb+Theory.+}$name$, dove 1509$thy$ � il nome dell'attuale segmento di teoria quando l'elemento fu 1510dichiarato e $name$ � un nome specifico fornito dall'utente (si vedano le 1511funzioni \ml{new\_axiom}, \ml{new\_definition}, di sotto). Elementi differenti 1512possono avere lo stesso nome specifico se il segmento associato � differente. 1513Cos� ciascun segmento di teoria fornisce un namespace separato di binding ML di 1514elementi \HOL{}. 1515 1516Vari pezzi aggiuntivi d'informazione sono archiviati in un segmento 1517di teoria, incluso lo status di parsing delle costanti (ad esempio se 1518esse sono degli infissi o dei binder). 1519 1520\paragraph {Determinare il contesto} 1521 1522C'� sempre una \emph{teoria attuale} che � la teoria 1523rappresentata dal segmento di teoria attuale insieme con la sua 1524stirpe. Il nome del segmento di teoria attuale � restituito dalla funzione 1525\ML: 1526 1527\begin{holboxed}\index{current_theory@\ml{current\_theory}|pin} 1528\begin{verbatim} 1529 current_theory : unit -> string 1530\end{verbatim} 1531\end{holboxed} 1532 1533 Quando una sessione interattiva \HOL{} inizia, alcune teorie saranno 1534 gi� nel contesto logico. L'insieme esatto di teorie nel 1535 contesto varier�. Se l'eseguibile usato � \texttt{hol.bare}, 1536 allora saranno caricate solo \theoryimp{min} e \theoryimp{bool}. Quando 1537 � usato l'eseguibile \texttt{hol}, � caricato un conteso logico pi� ricco. 1538 1539L'esatto insieme di teorie caricate pu� essere determinato con il 1540comando \ml{ancestry}. 1541% 1542\begin{holboxed} 1543\index{ancestry@\ml{ancestry}|pin} 1544\begin{verbatim} 1545 ancestry : string -> string list 1546\end{verbatim} 1547\end{holboxed} 1548 1549Questa funzione fornisce un meccanismo generale per esaminare la struttura 1550della gerarchia delle teorie. L'argomento � il nome di una teoria (o 1551\texttt{"-"} come abbreviazione per la teoria attuale), al quale 1552\texttt{ancestry} risponder� con una lista degli antenati dell'argomento 1553nella gerarchia delle teorie. 1554 1555\begin{holboxed} 1556{\small 1557\begin{verbatim} 1558 - ancestry "-"; 1559 > val it = 1560 ["num", "prim_rec", "normalForms", "relation", "pair", 1561 "arithmetic", "while", "numeral", "label", "combin", "sum", "min", 1562 "bool", "marker", "one", "option", "ind_type", "list"] : string list 1563\end{verbatim} 1564} 1565\end{holboxed} 1566 1567 1568\paragraph{Creare un segmento di teoria} 1569 1570\index{teorie, nella logica HOL@teorie, nella logica \HOL{}!creazione di|(} 1571% 1572Nuovi segmenti di teoria sono creati con una chiamata a \ml{new\_theory}. 1573% 1574\begin{holboxed} 1575\index{new_theory@\ml{new\_theory}|pin} 1576\begin{verbatim} 1577 new_theory : string -> unit 1578\end{verbatim} 1579\end{holboxed} 1580% 1581Questo alloca una nuova `area' dove le successive operazioni 1582di teoria hanno effetto. Se la teoria attuale (diciamo $thy_1$) al momento 1583di una chiamata a {\small\verb+new_theory +}$thy_2$ non � vuota, cio�, � stato 1584archiviato in essa un assioma, una definizione, o un teorema, allora $thy_1$ � 1585esportata prima che $thy_2$ sia allocata. Inoltre, $thy_2$ otterr� 1586$thy_1$ come genitore. Se {\small\verb+new_theory +}$thy$ � chiamato quando 1587il segmento attuale di teoria � gi� chiamato $thy$, allora questo � 1588interpretato semplicemente come una richiesta di ripulire l'attuale segmento di teoria 1589(nulla sar� esportato). 1590 1591Una chiamata a \ml{new\_theory "$\mathit{name}$"} fallisce se: 1592\begin{itemize} 1593\item $name$ non � un alfanumerico che inizia con una lettera. 1594 1595\item c'� gi� una teoria chiamata $name$ nella stirpe del 1596segmento attuale. 1597 1598\item se � necessario esportare il segmento attuale prima di creare 1599il nuovo e il tentativo di export fallisce. 1600\end{itemize} 1601 1602All'avvio, il segmento di teoria attuale di \HOL{} � chiamato \ml{scratch}, 1603che � una teoria vuota, che ha un'utile collezione di teorie nella 1604sua stirpe. Tipicamente, un utente inizierebbe caricando qualunque contesto 1605logico extra sia richiesto per il lavoro da fare. 1606 1607Il segmento attuale di teoria agisce come una sorta di blocco di appunti. Gli elementi archiviati 1608nel segmento attuale possono essere sovrascritti da aggiunte successive, o 1609cancellati completamente. Ogni elemento di teoria che fosse stato sovrascritto 1610o cancellato sarebbe quindi considerato {\it scaduto}, e non sarebbe 1611incluso nella teoria nel momento cui essa fosse in fine esportata. Le costanti 1612e i tipi scaduti sono individuati dal printer \HOL{}, che li stamper� 1613inclusi in una sintassi strana-alla-vista per avvertire l'utente. 1614 1615Contrariamente al segmento attuale, i segmenti antenati (propri) non possono 1616essere alterati. 1617% 1618\index{teorie, nella logica HOL@teorie, nella logica \HOL{}!creazione di|)} 1619 1620 1621\paragraph{Caricare teorie pre-costruite} 1622 1623Dal momento che le teorie \HOL{} sono rappresentate da moduli \ML, si importa 1624un segmento di teoria esistente semplicemente importando il modulo corrispondente. 1625 1626\begin{holboxed} 1627\index{load (funzione ML)@\ml{load} (funzione \ML{})|pin} 1628\begin{verbatim} 1629 load : string -> unit 1630\end{verbatim}\end{holboxed} 1631 1632\noindent 1633Eseguire {\small\verb+load +}$name${\small\verb+Theory+} importa nella sessione il 1634primo file chiamato $name${\small\verb+Theory.uo+} trovato lungo il 1635{\small\verb+loadPath+}. Qualunque antenato di 1636$name$ sar� caricato prima che il caricamento di $name${\small\verb+Theory+} 1637continui. Si noti che {\small\verb+load+} non pu� essere usato in file ML 1638che non sono stati compilati; pu� essere usato solo nel sistema 1639interattivo. 1640 1641\paragraph{Aggiungere alla teoria attuale} 1642 1643Le seguenti funzioni \ML{} aggiungono tipi e termini al segmento di teoria 1644attuale. Nell'uso tipico, queste funzioni non saranno 1645necessarie dal momento che funzionalit� di definizione di pi� alto livello invocheranno queste 1646in caso di necessit�. Tuttavia, queste funzioni possono essere utili per coloro che scrivono 1647strumenti di dimostrazione e principi derivati di definizione. 1648 1649\begin{holboxed} 1650\index{new_type@\ml{new\_type}|pin} 1651\begin{verbatim} 1652 new_type : int -> string -> unit 1653\end{verbatim} 1654\end{holboxed} 1655 1656 1657\noindent Eseguire \ml{new\_type}$\ n\ \ml{"\ty{op}"}$ rende \ty{op} 1658un nuovo operatore di tipo\index{operatori di tipo, nella logica HOL@operatori di 1659tipo, nella logica \HOL{}!dichiarazione di} $n$-ario nella teoria attuale. Se 1660\ty{op} non � un nome permesso per un tipo, sar� emesso un warning. 1661 1662 1663\begin{holboxed} 1664\index{new_constant@\ml{new\_constant}|pin} 1665\begin{verbatim} 1666 new_constant : (string * type) -> unit 1667\end{verbatim} 1668\end{holboxed} 1669 1670\noindent Eseguire {\small\verb+new_constant("+}$c${\small\verb+",+}$\sigma${\small\verb+)+} rende 1671$c_{\sigma'}$ una nuova costante\index{costanti, nella logica HOL@costanti, nella logica \HOL{}!dichiarazione di} della teoria attuale, 1672per ogni $c_{\sigma'}$ dove $\sigma'$ � un'istanza di $\sigma$. 1673Il tipo $\sigma$ � 1674chiamato il {\it tipo generico\/}\index{tipi generici, nella logica 1675 HOL@tipi generici, nella logica \HOL{}} di $c$. 1676Se $c$ non � un nome permesso per una costante, sar� emesso un warning. 1677 1678\begin{holboxed} 1679\index{new_axiom@\ml{new\_axiom}|pin} 1680\begin{verbatim} 1681 new_axiom : (string * term) -> thm 1682\end{verbatim} 1683\end{holboxed} 1684 1685\noindent Eseguire \ml{new\_axiom("}$name$\ml{",}$t$\ml{)} dichiara il 1686sequente 1687\ml{(\lb\rb{},$t$)} essere un assioma\index{assiomi!dichiarazione di, nella logica HOL@dichiarazione di, nella logica \HOL{}} della teoria attuale con nome $name$. 1688Fallisce se: 1689\begin{myenumerate} 1690\item il tipo di $t$ non � \verb+bool+. 1691 1692\item $t$ contiene costanti o tipi scaduti, cio�, costanti o 1693 tipi che sono stati ri-dichiarati dopo che � stato eseguito il build di $t$. 1694\end{myenumerate} 1695 1696Una volta che un teorema � stato dimostrato, esso pu� essere salvato con la funzione 1697 1698\begin{holboxed} 1699\index{save_thm@\ml{save\_thm}|pin} 1700\begin{verbatim} 1701 save_thm : (string * thm) -> thm 1702\end{verbatim} 1703\end{holboxed} 1704 1705\noindent 1706Valutare \ml{save\_thm("}$\mathit{name}$\ml{",}$\mathit{th}$\ml{)} 1707salver� il teorema 1708% 1709\index{teoremi, nella logica HOL@teoremi, nella logica \HOL{}!salvataggio di} 1710\index{salvare teoremi} 1711% 1712$\mathit{th}$ con nome $\mathit{name}$ nel segmento di teoria 1713attuale. 1714 1715\paragraph{Esportare una teoria} 1716 1717Una volta che un segmento di teoria � stato costruito, pu� essere scritto su un 1718file, che, dopo la compilazione, pu� essere importato in sessioni future. 1719 1720\begin{holboxed} 1721\index{export_theory@\ml{export\_theory}|pin} 1722\begin{verbatim} 1723 export_theory : unit -> unit 1724\end{verbatim} 1725\end{holboxed} 1726 1727Quando � chiamato {\small\verb+export_theory+}, tutte le entit� scadute 1728sono rimosse dal segmento attuale. Inoltre, � calcolata la paternit� della 1729teoria. Il segmento di teoria attuale � scritto sul file 1730$name${\small{\tt Theory.sml}} nell'attuale directory di lavoro. Anche il 1731file $name${\small{\tt Theory.sig}}, che documenta il contenuto di 1732$name$, � scritto nell'attuale directory di lavoro. Si noti che 1733la teoria esportata non � compilata da \HOL. Questo � lasciato a uno 1734strumento esterno, \holmake{} (si veda la sezione~\ref{Holmake}), che mantiene 1735le dipendenze tra collezioni di segmenti di teoria \HOL{}. 1736 1737 1738\subsection{Funzioni ML per accedere alle teorie} 1739 1740\index{teorie, nella logica HOL@teorie, nella logica \HOL{}!funzioni per accedere alle|(} 1741\index{assiomi!recupero degli, nel sistema HOL@recupero degli, nel sistema \HOL{}|(} 1742% 1743Gli argomenti di tipo \ML{} \ml{string} a \ml{new\_axiom}, 1744\ml{new\_definition}, ecc., sono i nomi degli assiomi e delle 1745definizioni corrispondenti. Questi nomi sono usati quando si accede alle teorie con le 1746funzioni \ml{axiom}, \ml{definition}, ecc., descritte di sotto. 1747 1748La teoria attuale 1749% 1750\index{teorie, nella logica HOL@teorie, nella logica \HOL{}!gerarchia delle} 1751% 1752pu� essere estesa aggiungendo nuovi genitori, tipi, costanti, assiomi e 1753definizioni. Le teorie che sono nella stirpe della teoria attuale 1754non possono essere estese in questo modo; esse possono essere pensate come 1755\emph{congelate}. 1756 1757Ci sono varie funzioni per caricare il contenuto dei file di teoria: 1758 1759\begin{holboxed} 1760\index{genitori@\ml{genitori}|pin} 1761\index{tipi@\ml{tipi}|pin} 1762\index{costanti@\ml{costanti}|pin} 1763\begin{verbatim} 1764 parents : string -> string list 1765 types : string -> (int * string) list 1766 constants : string -> term list 1767\end{verbatim} 1768\end{holboxed} 1769 1770\noindent Il primo argomento � il nome di una teoria (che deve essere nella 1771stirpe dell'attuale segmento di teoria); il risultato � una lista delle 1772componenti della teoria. Il nome della teoria attuale pu� essere 1773abbreviato da \ml{"-"}. 1774% 1775\index{ abbreviazione, di parte dei nomi di teoria HOL@\ml{-} (abbreviazione, di parte dei nomi di teoria \HOL{})} 1776% 1777Per esempio, \ml{parents "-"} restituisce i genitori della teoria 1778attuale. 1779 1780Nel caso di \ml{types} � restituita una lista di coppie ariet�-nome. 1781Gli assiomi, le definizioni e i teoremi individuali possono essere letti dalla 1782teoria attuale usando le seguenti funzioni \ML: 1783 1784\begin{holboxed} 1785\index{assioma@\ml{assioma}|pin} 1786\index{definizione@\ml{definizione}|pin} 1787\index{teorema@\ml{teorema}|pin} 1788\begin{verbatim} 1789 axiom : string -> thm 1790 definition : string -> thm 1791 theorem : string -> thm 1792\end{verbatim} 1793\end{holboxed} 1794 1795\noindent Il primo argomento � il nome dell'assioma, definizione o teorema 1796fornito dall'utente nella teoria attuale. Inoltre, pu� essere estratta 1797una lista di tutti gli assiomi, definizioni e teoremi della teoria con 1798le funzioni \ML{}: 1799 1800\begin{holboxed} 1801\index{assiomi@\ml{assiomi}|pin} 1802\index{teoremi@\ml{teoremi}|pin} 1803\index{definizioni@\ml{definizioni}|pin} 1804\begin{verbatim} 1805 axioms : string -> (string * thm) list 1806 definitions : string -> (string * thm) list 1807 theorems : string -> (string * thm) list 1808\end{verbatim} 1809\end{holboxed} 1810 1811Il contenuto della teoria attuale pu� essere stampato in un formato leggibile 1812usando la funzione \ml{print\_theory}. 1813% 1814\index{stampa, nella logica HOL@stampa, nella logica \HOL{}!di teorie} 1815\index{print_theory@\ml{print\_theory}} 1816\index{assiomi!estrazione degli, nel sistema HOL@estrazione degli, nel sistema \HOL{}|)} 1817\index{teorie, nella logica HOL@teorie, nella logica \HOL{}!funzioni per accedere alle|)} 1818 1819\subsection{Funzioni per creare estensioni definizionali} 1820\index{estensione, della logica HOL@estensione, della logica \HOL{}!definzionale} 1821\index{estensione definizionale, della logica HOL@estensione definizionale, della logica \HOL{}} 1822\index{teorie, nella logica HOL@teorie, nella logica \HOL{}!estensione di|(} 1823\label{avra_definitional} 1824 1825Ci sono tre specie di estensioni definizionali: 1826definizioni di costante, specifiche di costane e definizioni di tipo. 1827 1828\subsubsection{Definizioni di costante} 1829\label{sec:constant-definitions} 1830 1831In \LOGIC{} una definizione di costante 1832% 1833\index{estensione, della logica HOL@estensione, della logica \HOL{}!per definizione di costante} 1834\index{estensione per definizione di costante, della logica HOL@estensione per definizione di costante, della logica \HOL{}!funzione ML per@funzione \ML\ per} 1835% 1836su una firma $\Sigma_{\Omega}$ � definita essere un'equazione, cio� 1837una formula della forma $c_{\sigma}=t_{\sigma}$, tale che: 1838\begin{myenumerate} 1839\item $c$ non � il nome di alcuna costante in $\Sigma_{\Omega}$; 1840\item $t_{\sigma}$ � un termine chiuso in ${\sf Terms}_{\Sigma_{\Omega}}$; 1841\item tutte le variabili di tipo che occorrono in $t_{\sigma}$ occorrono in $\sigma$. 1842\end{myenumerate} 1843 1844In \HOL, le definizioni possono essere leggermente pi� generali di questo, nel senso che 1845� permesso che un'equazione: 1846 1847\[ c\ v_1\ \cdots\ v_n\ =\ t \] 1848 1849\noindent sia una definizione dove $v_1$, $\dots$, $v_n$ sono 1850strutture variabili (cio� tuple di variabili distinte). Una tale equazione � 1851logicamente equivalente a: 1852 1853\[ c\ =\ \lambda v_1\ \cdots\ v_n.\ t \] 1854 1855\noindent che � una definizione nel senso di \LOGIC{} se valgono (i), 1856(ii) e (iii). 1857 1858La seguente funzione \ML\ crea\index{meccanismi di definizione, per la logica HOL@meccanismi di definizione, per la logica \HOL{}} una nuova definizione nella 1859teoria attuale. 1860 1861\begin{holboxed} 1862\index{new_definition@\ml{new\_definition}|pin} 1863\begin{verbatim} 1864 new_definition : (string * term) -> thm 1865\end{verbatim} 1866\end{holboxed} 1867 1868 1869\noindent Valutare 1870 \ml{new\_definition("$name$", \holquote{$c\ v_1\ \cdots\ v_n\ =\ t$})}, 1871dichiara il sequente\linebreak 1872\ml{(\lb\rb{},$c = \lambda v_1\ \cdots\ v_n.\ t$)} essere una definizione di costante 1873\index{definizioni, aggiungere ... alla logica HOLc@definizioni, aggiungere ... alla logica \HOL{}} 1874della teoria attuale. Il nome associato con la definizione in 1875questa teoria � $name$. 1876Si verifica un fallimento se: 1877\begin{myenumerate} 1878\item $t$ contiene delle variabili libere che non sono in nessuna delle 1879strutture variabili $v_1$, $\dots$, $v_n$ (questo equivale 1880a richiedere che $\lambda v_1\ \cdots\ v_n.\ t$ sia un termine chiuso); 1881\item c'� una variabile di tipo in $v_1$, $\dots$, $v_n$ o $t$ 1882che non occorre nel tipo di $c$. 1883\end{myenumerate} 1884 1885\subsubsection{Specifiche di costante} 1886\label{conspec} 1887 1888\index{specifica di costanti, nella logica HOL@specifica di costanti, nella logica \HOL{}|(} 1889% 1890\index{estensione, della logica HOL@estensione, della logica \HOL{}!per specifica di costante} 1891% 1892In \LOGIC{} una specifica di costante\index{estensione per specifica di costante, della logica HOL@estensione per specifica di costante, della logica \HOL{}!funzione ML per@funzione \ML\ per} per una teoria ${\cal T}$ 1893� definita essere una coppia: 1894 1895\[ 1896\langle(c_1,\ldots,c_n),\ \lquant{{x_1}_{\sigma_1} 1897\cdots {x_n}_{\sigma_n}}t_{\ty{bool}}\rangle 1898\] 1899tale che: 1900 1901\begin{myenumerate} 1902\item $c_1$, $\dots$, $c_n$ sono nomi distinti. 1903\item $\lquant{{x_1}_{\sigma_1} 1904\cdots {x_n}_{\sigma_n}}t_{\ty{bool}}\ \in\ {\sf Terms}_{\cal T}$. 1905\item $tyvars(\lquant{{x_1}_{\sigma_1} 1906\cdots {x_n}_{\sigma_n}}t_{\ty{bool}})\ \subseteq\ tyvars(\sigma_i)$ per 1907$1\leq i\leq n$. 1908\item $\equant{{x_1}_{\sigma_1}\ \cdots\ {x_n}_{\sigma_n}}t 1909\ \in\ {\sf Theorems}_{\cal T}$. 1910\end{myenumerate} 1911La seguente funzione \ML\ � usata per fare specifiche di costante nel 1912sistema \HOL{}. 1913 1914\begin{holboxed} 1915\index{new_specification@\ml{new\_specification}|pin} 1916\begin{verbatim} 1917 new_specification : string * string list * thm -> thm 1918\end{verbatim} 1919\end{holboxed} 1920% 1921Valutando: 1922{ 1923\newcommand{\cone}{\ensuremath{c_1}} 1924\newcommand{\cn}{\ensuremath{c_n}} 1925\newcommand{\xone}{\ensuremath{x_1}} 1926\newcommand{\xn}{\ensuremath{x_n}} 1927\begin{alltt} 1928 new_specification("\(\mathit{name}\)", ["\cone", ..., "\cn"], 1929 |- ?\xone ... \xn. \(t\)[\xone, ..., \xn]) 1930\end{alltt} 1931} 1932sono introdotte simultaneamente nuove costanti chiamate $c_1$, $\dots$, 1933$c_n$ che soddisfano la propriet�: 1934 1935\[ \ml{|- }t\ml{[}c_1\ml{,}\ \ldots\ \ml{,}c_n\ml{]} \] 1936 1937\noindent Questo teorema � archiviato, 1938con nome $name$, come una definizione nell'attuale segmento di teoria. Una chiamata a 1939\ml{new\_specification} fallisce se: 1940 1941\begin{myenumerate} 1942\item il teorema argomento non ha una lista vuota di assunzioni; 1943\item ci sono variabili libere nel teorema argomento; 1944\item $c_1$, $\dots$, $c_n$ non sono variabili distinte; 1945\item il tipo di qualche $c_i$ non contiene tutte le variabili 1946di tipo che occorrono nel termine 1947\holtxt{\bs$x_1\ \cdots\ x_n$. $t$[$x_1$, $\ldots$, $x_n$]}. 1948\end{myenumerate} 1949% 1950\index{specifica di costanti, nella logica HOL@specifica di costanti, nella logica \HOL{}|)} 1951 1952\subsubsection{Definizioni di tipo} 1953\label{type-defs} 1954 1955\index{estensione, della logica HOL@estensione, della logica \HOL{}!per definizione di tipo|(} 1956% 1957\index{definizioni di tipo, nella logica HOL@definizioni di tipo, nella logica \HOL{}|(} 1958% 1959In \LOGIC{} � spiegato che 1960definire 1961% 1962\index{definizioni di tipo, nella logica HOL@definizioni di tipo, nella logica \HOL{}!introduzione di} 1963\index{estensione per definizione di tipo, nella logica HOL@estensione per definizione di tipo, nella logica \HOL{}!funzione ML per@funzione \ML\ per|(} 1964% 1965un nuovo tipo $(\alpha_1,\ldots,\alpha_n)\ty{op}$ in una teoria ${\cal T}$ 1966consiste nell'introdurre $\ty{op}$ come un nuovo operatore di tipo $n$-ario e 1967 1968\[\turn \equant{f_{(\alpha_1,\ldots,\alpha_n)\ty{op}\fun\sigma}}\TyDef\ p\ f\] 1969 1970\noindent come un nuovo assioma, dove $p$ � un predicato 1971che caratterizza\index{predicato caratteristico, di definizioni di tipo} un 1972sottoinsieme non vuoto di un tipo esistente $\sigma$. Formalmente, una definizione di tipo 1973per una teoria ${\cal T}$ � una tripla 1974 1975\[ \langle \sigma,\ (\alpha_1,\ldots,\alpha_n)\ty{op}, 1976 \ p_{\sigma\fun\ty{bool}}\rangle \] 1977 1978\noindent dove: 1979 1980\begin{myenumerate} 1981\item $\sigma\in{\sf Types}_{\cal T}$ e 1982$tyvars(\sigma)\in\{\alpha_1, \ldots , \alpha_n\}$. 1983\item \ty{op} � il nome di una costante di tipo in ${\sf Struc}_{\cal T}$. 1984\item $p\in{\sf Terms}_{\cal T}$ � un termine chiuso di 1985tipo $\sigma\fun\ty{bool}$ e 1986$tyvars(p)\subseteq\{\alpha_1, \ldots , \alpha_n\}$. 1987\item $\equant{x_{\sigma}}p\ x \ \subseteq\ {\sf Theorems}_{\cal T}$. 1988\end{myenumerate} 1989 1990La seguente funzione \ML\ esegue una definizione di tipo nel sistema \HOL{}. 1991 1992\begin{holboxed} 1993\index{new_type_definition@\ml{new\_type\_definition}|pin} 1994\begin{verbatim} 1995 new_type_definition : (string * thm) -> thm 1996\end{verbatim}\end{holboxed} 1997 1998\noindent Se $t$ � un termine di tipo 1999$\sigma$\ml{->bool} contenente $n$ distinte variabili di tipo, allora 2000valutare: 2001 2002{\def\op{{\normalsize\sl op}} 2003\begin{hol} 2004\begin{alltt} 2005 new_type_definition("{\op}", |- ?\(x\). \(t\) \(x\)) 2006\end{alltt} 2007\end{hol}} 2008 2009\noindent risulta nella dichiarazione di \ty{op} come un nuovo operatore di tipo $n$-ario 2010caratterizzato dall'assioma 2011definizionale\index{operatori di tipo, nella logica HOL@operatori di tipo, nella logica \HOL{}!assiomi definizionali per}: 2012\begin{hol} 2013\begin{alltt} 2014 |- ?rep. TYPE\_DEFINITION \m{t} rep 2015\end{alltt} 2016\end{hol} 2017 2018\noindent che � archiviato come una definizione con il nome generato 2019automaticamente 2020\ty{op}\ml{\_TY\_DEF}.\index{TY_DEF@$\ldots$\ml{\_TY\_DEF}}. La costante 2021\ml{TYPE\_DEFINITION}\index{TYPE_DEFINITION@\ml{TYPE\_DEFINITION}} 2022� definita nella teoria \ml{bool} da: 2023 2024\begin{hol} 2025\begin{verbatim} 2026 |- TYPE_DEFINITION (P:'a->bool) (rep:'b->'a) = 2027 (!x' x''. (rep x' = rep x'') ==> (x' = x'')) /\ 2028 (!x. P x = (?x'. x = rep x')) 2029\end{verbatim} 2030\end{hol} 2031 2032\noindent Eseguire \ml{new\_type\_definition("\ty{op}", |- ?}$x$\ml{.}\ $t\ x$\ml{)} fallisce se: 2033\begin{myenumerate} 2034\item $t$ non ha un tipo della forma $\sigma$\ml{->bool}. 2035\end{myenumerate} 2036\index{estensione, della logica HOL@estensione, della logica \HOL{}!per definizione di tipo|)} 2037\index{teorie, nella logica HOL@teorie, nella logica \HOL{}!estensione di|)} 2038\index{estensione per definizione di tipo, nella logica HOL@estensione per definizione di tipo, nella logica \HOL{}!funzione ML per@funzione \ML\ per|)} 2039\index{definizioni di tipo, nella logica HOL@definizioni di tipo, nella logica \HOL{}|)} 2040 2041\paragraph{Definire le biezioni} 2042\index{definizioni di tipo, nella logica HOL@definizioni di tipo, nella logica \HOL{}!definire le biezioni per|(} 2043 2044Il risultato di una definizione di tipo usando \ml{new\_type\_definition} � un teorema 2045che asserisce solo l'{\it esistenza\/} di una 2046biezione\index{biezione di tipi, nella logica HOL@biezione di tipi, nella logica \HOL{}} 2047dal tipo che esso definisce al corrispondente sottoinsieme di un tipo esistente. Per 2048introdurre costanti che di fatto denotano una tale biezione e la sua inversa, � 2049fornita la seguente funzione \ML: 2050 2051\begin{holboxed} 2052\index{define_new_type_bijections@\ml{define\_new\_type\_bijections}|pin} 2053\begin{verbatim} 2054 define_new_type_bijections 2055 : {name:string, ABS:string, REP:string, tyax:thm} -> thm 2056\end{verbatim}\end{holboxed} 2057 2058\noindent Questa funzione prende un record {\small\verb+{ABS, REP, name, tyax}+}. 2059L'argomento {\verb+tyax+} deve essere un assioma definizionale della forma restituita da 2060\ml{new\_type\_definition}.\linebreak L'argomento {\verb+name+} � il nome sotto cui 2061la definizione di costante (di fatto, una specifica di costante) fatta da 2062{\small\verb!define_new_type_bijections!} sar� archiviata nel segmento di teoria 2063attuale, e gli argomenti {\small\verb+ABS+} e {\small\verb+REP+} 2064sono nomi specificati dall'utente per le due costanti che devono essere 2065definite. Queste costanti sono definite in modo da denotare biezioni mutuamente 2066inverse tra il tipo definito, la cui definizione � data dal 2067teorema fornito, e il tipo rappresentante di questo tipo 2068definito. 2069 2070Valutare: 2071 2072\medskip 2073{\def\op{{\normalsize\sl op}} 2074\begin{hol}\begin{alltt} 2075 define\_new\_type\_bijections 2076 \lb{}name="\m{name}", ABS="\m{abs}", REP="\m{rep}", 2077 tyax = |- ?rep:newty->ty. TYPE\_DEFINITION \m{P} rep\rb{} 2078\end{alltt}\end{hol}} 2079 2080\medskip 2081 2082\noindent definisce automaticamente due nuove costanti 2083\m{abs}{\small\verb!:ty->newty!} e \m{rep}{\small\verb!:ty->newty!} 2084tali che: 2085 2086{\def\bk{\char'134} 2087\begin{hol}\begin{alltt} 2088 |- (!a. \m{abs}(\m{rep} a) = a) /\bk (!r. \m{P} r = (\m{rep}(\m{abs} r) = r)) 2089\end{alltt}\end{hol}} 2090 2091\noindent Questo teorema, che � la propriet� di definizione per le costanti 2092\m{abs} e \m{rep}, � archiviato sotto il nome "\m{name}" nell'attuale segmento 2093di teoria. Esso � anche il valore restituito da \ml{define\_new\_type\_bijections}. 2094Il teorema dichiara che \m{abs} � l'inversa sinistra di \m{rep} e---per 2095valori che soddisfano \ml{P}---che \ml{rep} � l'inversa sinistra di \m{abs}. 2096 2097Una chiamata a 2098\ml{define\_new\_type\_bijections \m{name} \m{abs} \m{rep} \m{th}} 2099fallisce se: 2100 2101\begin{myenumerate} 2102\item $th$ non � un teorema della forma restituita da 2103\ml{new\_type\_definition}. 2104\end{myenumerate}% 2105\index{definizioni di tipo, nella logica HOL@definizioni di tipo, nella logica \HOL{}!definire biezioni per|)} 2106 2107\paragraph{Propriet� delle biezioni di tipo} 2108 2109\index{definizioni di tipo, nella logica HOL@definizioni di tipo, nella logica \HOL{}!propriet� delle biezioni per|(} 2110 2111Le seguenti funzioni \ML\ sono fornite per dimostrare che le biezioni 2112introdotte da \ml{define\_new\_type\_bijections} sono iniettive\linebreak \ml{define\_new\_type\_bijections} 2113e suriettive (onto): 2114 2115\begin{holboxed} 2116\index{prove_rep_fn_one_one@\ml{prove\_rep\_fn\_one\_one}|pin} 2117\index{prove_rep_fn_onto@\ml{prove\_rep\_fn\_onto}|pin} 2118\index{prove_abs_fn_one_one@\ml{prove\_abs\_fn\_one\_one}|pin} 2119\index{prove_abs_fn_onto@\ml{prove\_abs\_fn\_onto}|pin} 2120\begin{verbatim} 2121 prove_rep_fn_one_one : thm -> thm 2122 prove_rep_fn_onto : thm -> thm 2123 prove_abs_fn_one_one : thm -> thm 2124 prove_abs_fn_onto : thm -> thm 2125\end{verbatim}\end{holboxed} 2126 2127\noindent Il teorema argomento a ciascuna di queste funzioni deve essere un teorema 2128della forma restituita da \ml{define\_new\_type\_bijections}: 2129 2130{\def\bk{\char'134} 2131\begin{hol}\begin{alltt} 2132 |- (!a. \m{abs}(\m{rep} a) = a) /\bk (!r. \m{P} r = (\m{rep}(\m{abs} r) = r)) 2133\end{alltt}\end{hol}} 2134 2135\noindent Se \m{th} � un teorema di questa forma, allora valutare 2136\ml{prove\_rep\_fn\_one\_one \m{th}} dimostra che la funzione \m{rep} � 2137uno-a-uno, e restituisce il teorema: 2138 2139\begin{hol}\begin{alltt} 2140 |- !a a'. (\m{rep} a = \m{rep} a') = (a = a') 2141\end{alltt}\end{hol} 2142 2143\noindent Allo stesso modo, \ml{prove\_rep\_fn\_onto \m{th}} dimostra che \m{rep} � 2144sopra (onto [n.d.t]) l'insieme di valori che soddisfano \m{P}: 2145 2146{\def\bk{\char'134} 2147\begin{hol}\begin{alltt} 2148 |- !r. \m{P} r = (?a. r = \m{rep} a) 2149\end{alltt}\end{hol}} 2150 2151\noindent Valutare \ml{prove\_abs\_fn\_one\_one \m{th}} dimostra che \m{abs} 2152� uno-a-uno per valori che soddisfano \m{P}, e restituisce il teorema: 2153 2154{\def\bk{\char'134} 2155\begin{hol}\begin{alltt} 2156 |- !r r'. \m{P} r ==> \m{P} r' ==> ((\m{abs} r = \m{abs} r') = (r = r')) 2157\end{alltt}\end{hol}} 2158 2159\noindent E valutare \ml{prove\_abs\_fn\_onto \m{th}} dimostra che \m{abs} 2160� suriettiva, restituendo il teorema: 2161 2162{\def\bk{\char'134} 2163\begin{hol} 2164\begin{alltt} 2165 |- !a. ?r. (a = \m{abs} r) /\bk \m{P} r 2166\end{alltt} 2167\end{hol}} 2168 2169\noindent Tutte e quattro le funzioni falliranno se applicate a qualunque teorema che non 2170abbia la forma di un teorema restituito da \ml{define\_new\_type\_bijections}. 2171Nessuna di queste funzioni salva alcunch� nella teoria attuale. 2172 2173\index{definizioni di tipo, nella logica HOL@definizioni di tipo, nella logica \HOL{}!propriet� delle biezioni per|)} 2174 2175 2176%\subsection{Type abbreviations}\label{typeabbrev}\index{types, nella logica HOL@types, nella logica \HOL{}!abbreviation of}\index{type abbreviations!nella logica HOL@nella logica \HOL{}}\index{abbreviation of types, nella logica HOL@abbreviation of types, nella logica \HOL{}|(} 2177%It is possible to introduce an abbreviation for a monomorphic type using the 2178%function: 2179% 2180%\begin{holboxed}\index{new_type_abbrev@\ml{new\_type\_abbrev}|pin} 2181%\begin{verbatim} 2182% new_type_abbrev : (string * type) -> unit 2183%\end{verbatim}\end{holboxed} 2184% 2185%\noindent Evaluating \ml{new\_type\_abbrev(`}$name$\ml{`,":}$\sigma$\ml{")} 2186%enables $name$ to be used in quotations instead of $\sigma$. The evaluation 2187%fails 2188%if $\sigma$ is polymorphic. Type abbreviations 2189%are recorded in theory files, so that 2190%when a theory is loaded, any type abbreviations made are 2191%activated. The list of currently active abbreviations in a theory 2192%is given by the function: 2193% 2194%\begin{holboxed}\index{type_abbrevs@\ml{type\_abbrevs}|pin} 2195%\begin{verbatim} 2196% type_abbrevs : string -> (string * type) list 2197%\end{verbatim}\end{holboxed} 2198% 2199% 2200%Note that abbreviation can also be made using antiquotation\index{antiquotation, nella logica HOL terms@antiquotation, nella logica \HOL{} terms}, without the 2201%restriction to monomorphic types. Such \ML\ abbreviations are not, of course, 2202%stored in theory files and so do not persist beyond a single session. 2203%The following session illustrates various ways of 2204%abbreviating types: 2205% 2206%\setcounter{sessioncount}{1} 2207%\begin{session}\begin{verbatim} 2208%*new_theory `numpair`;; 2209%() : unit 2210% 2211%#new_type_abbrev(`numpair`, ":num*num");; 2212%() : unit 2213% 2214%#let t1 = "x:numpair";; 2215%t1 = "x" : term 2216% 2217%#type_of t1;; 2218%":num * num" : type 2219% 2220%#":numpair" = ":num*num";; 2221%true : bool 2222%\end{verbatim}\end{session} 2223% 2224%\noindent The alternative to introducing a type abbreviation is 2225%to give an \ML\ name to the type, and then to use this name via antiquotation. 2226%Continuing the session:\index{abbreviation of types, nella logica HOL@abbreviation of types, nella logica \HOL{}|)} 2227% 2228%\begin{session}\begin{verbatim} 2229%#let ty = ":num*num";; 2230%ty = ":num * num" : type 2231% 2232%#let t2 = "x:^ty";; 2233%t2 = "x" : term 2234% 2235%#t1 = t2;; 2236%true : bool 2237%\end{verbatim}\end{session} 2238% 2239%\pagebreak[2] 2240% 2241%\noindent The type abbreviation is stored in the theory file and so 2242%persists across sessions. This can be seen by the result of printing 2243%the theory \ml{numpair}: 2244% 2245%\begin{session}\begin{verbatim} 2246%#print_theory`numpair`;; 2247%The Theory numpair 2248%Parents -- HOL 2249%Type Abbreviations -- numpair ":num * num" 2250%******************** numpair ******************** 2251% 2252%() : unit 2253%\end{verbatim}\end{session} 2254% 2255%\noindent If the session is then ended: 2256% 2257%\begin{session}\begin{verbatim} 2258%#close_theory();; 2259%() : unit 2260% 2261%#quit();; 2262%\end{verbatim}\end{session} 2263% 2264%\noindent and a new session is started in which the theory \ml{numpair} is 2265%loaded: 2266% 2267%\setcounter{sessioncount}{1} 2268%\begin{session}\begin{verbatim} 2269%#load_theory`numpair`;; 2270%Theory numpair loaded 2271%() : unit 2272% 2273%#"x:numpair";; 2274%"x" : term 2275% 2276%#type_abbrevs `-`;; 2277%[(`numpair`, ":num * num")] : (string * type) list 2278%\end{verbatim}\end{session} 2279% 2280%\noindent then the type abbreviation persists. 2281% 2282%Type abbreviations tend to be little used in practice; the antiquotation 2283%method is usually sufficient. 2284 2285 2286%%% Local Variables: 2287%%% mode: latex 2288%%% TeX-master: "description" 2289%%% End: 2290