IT/Tutorial/logic.tex

1 \chapter{La logica di \HOL{}}\label{HOLlogic}
3 Il sistema \HOL{} supporta \emph{la logica di ordine superiore}.
9 \item Non c'� una categoria sintattica separata per le \emph{formule} (i termini di tipo \ml{bool} adempiono a questo ruolo).
12 In questo capitolo, daremo una breve panoramica della notazione usata per scrivere l'espressioni della logica di \HOL{} in \ML{}, e discuteremo anche alcune tecniche fondamentali di dimostrazione in \HOL{}.
14 La sintassi e la semantica del particolare sistema logico supportato da \HOL{} � descritta nei dettagli in \DESCRIPTION. I lettori che desiderano vedere \HOL{} in azione, senza l'introduzione ai dettagli pi� sottili dei fondamenti di \HOL, potrebbero preferire di saltare al Capitolo~\ref{chap:euclid}.
17 La tabella di sotto riassume un utile sottoinsieme della notazione (ASCII) usata in \HOL.
22 \multicolumn{4}{|c|}{\bf Termini della Logica di HOL} \\
24 {\it Genere di termine} & {\it Notazione \HOL{}} &
52 I termini della logica di \HOL{} sono rappresentati in \ML{} da un \emph{tipo astratto} chiamato {\small\verb|term|}.
53 Normalmente essi sono inseriti tra due segni di doppio accento grave.
56 Per esempio, la funzione \ML{} \ml{dest\_imp} con il tipo \ML{} \ml{term -> term * term} divide un'implicazione in una coppia di termini che consiste nel suo antecedente e nel suo conseguente, e la funzione \ML\ \ml{dest\_conj} di tipo \ml{term -> term * term} divide una congiunzione nei suoi due congiunti%
57 \footnote{Tutti gli esempi di sotto assumono che l'utente stia eseguendo \texttt{hol}, il cui eseguibile � nella directory \texttt{bin/}.
58 A seconda della configurazione del sistema, � anche possibile che la notazione ASCII utilizzata nelle sessioni di esempio che seguono sia sostituita da una notazione
75 I termini della logica di \HOL{} sono piuttosto simili a espressioni \ML{}, e questo all'inizio pu� confondere.
78 Il tipo \HOL{} di questo termine � \holtxt{num \# num}.
85 La funzione incorporata \ml{type_of} ha il tipo \ML{} \ml{term->hol_type} e restituisce il tipo logico di un termine.
103 Per tentare di minimizzare la confusione tra i tipi logici dei termini \HOL{} e i tipi \ML{} di espressioni \ML{}, ci si riferir� ai primi come a \emph{tipi del  linguaggio oggetto} e ai secondi come a \emph{tipi del meta-linguaggio}.
116 \paragraph{Costruttori di termine}
117 I termini \HOL{} possono essere inseriti, come di sopra, usando \emph{quotation} esplicite, o possono essere costruiti chiamando le funzioni costruttore \ML{}.
119 Nell'esempio di sotto, sono costruite tre variabili di tipo {\small\verb|bool|}.
134 E' disponibile un'ampia collezione di costruttori e distruttori di termini per le teorie core di \HOL.
143 \paragraph{Controllo di tipo}
145 Di fatto ci sono quattro generi differenti di termini in \HOL: variabili, costanti, applicazioni di funzione (\ml{``$t_1$ $t_2$``}), e lambda astrazioni (\ml{``\bs$x$.$t$``}).
146 Termini pi� complicati, come quelli che abbiamo gi� visto di sopra, sono soltanto composizioni di termini da questo semplice insieme.
147 Al fine di comprendere il comportamento del parser delle quotation, � necessario capire come il controllore dei tipi deduca i tipi per le quattro categorie base di termini.
149 Sia le variabili sia le costanti hanno un nome e un tipo; la differenza � che le costanti non possono essere legate da quantificatori, e il loro tipo � fissato quando sono dichiarate (si veda di sotto).
150 Quando una quotation � immessa in \HOL{}, l'algoritmo di controllo del tipo usa i tipi delle costanti per dedurre i tipi delle variabili nella stessa quotation.
151 Per esempio, nel caso seguente, il controllore di tipi di \HOL{} ha usato il tipo conosciuto \holtxt{bool->bool} della negazione booleana (\holtxt{\td}) per dedurre che la variabile \holtxt{x} deve avere il tipo \holtxt{bool}.
160 Nei prossimi due casi, il tipo di \ml{x} e \ml{y} non pu� essere
162 (Di default lo `scopo' dell'informazione di tipo per il controllore di tipo � una singola quotation, cos� un tipo in una quotation non pu� influenzare il controllo di tipo di un'altra.
183 Se non c'� abbastanza informazione di tipo determinata dal contesto per risolvere i tipi di tutte le variabili in una quotation, allora il sistema ipotizzer� variabili di tipo differenti per tutte le variabili non vincolate.
185 \paragraph{Vincoli di tipo}
187 In alternativa, � possibile indicare esplicitamente i tipi richiesti usando la notazione \ml{``$\mathit{term}$:$\mathit{type}$``}, come illustrato di sotto.
199 \paragraph{I tipi delle applicazioni di funzione}
244 Il simbolo di dollaro all'inizio di \holtxt{\td} indica che la costante di negazione booleana ha uno stato sintattico speciale (in questo caso una precedenza non standard).
274 La sessione di sotto illustra l'uso di queste costanti come infissi, illustra anche i tipi del linguaggio oggetto di contro a quelli del meta-linguaggio.
293 Il simbolo `\holtxt{\bs}' � usato come una approssimazione ASCII di $\lambda$.
307 Altri due simboli di binding nella logica sono i suoi due pi� importanti quantificatori: \ml{!} e \ml{?}, i quantificatori universale ed esistenziale.
312 mentre una versione del risultato di Euclide circa l'infinit� dei numeri primi �:
317 Simboli di binding come questi possono essere usati su pi� `parametri' cos�:
332 \section{Dimostrazioni di base in \HOL{}}
342 Per un logico, una\linebreak definizione di una dimostrazione formale � che � una sequenza, ciascuno dei cui elementi � o un \emph{assioma} o segue dai membri precedenti della sequenza da una \emph{regola d'inferenza}.
343 Un teorema � l'ultimo elemento di una dimostrazione.
345 I teoremi sono rappresentati in \HOL{} da valori di un tipo astratto \ml{thm}.
346 L'unico modo per creare teoremi � quello di generare una tale dimostrazione.
347 In \HOL, seguendo lo stile \LCF, questo consiste nell'applicazione di funzioni \ML{} che rappresentano \emph{regole d'inferenza} ad assiomi o teoremi generati in precedenza.
348 La sequenza di tali applicazioni corrisponde direttamente alla dimostrazione di un logico.
350 Ci sono cinque assiomi della logica di \HOL{} e otto regole primitive d'inferenza.
353 Si noti ora come il printer di termini rende le uguaglianze nel teorema con il simbolo \holtxt{<=>} piuttosto che \holtxt{=}.
355 Il parser accetta sia \holtxt{<=>} che \holtxt{=} con argomenti booleani; tentare di usare \holtxt{<=>} su valori che non sono di tipo booleano (diciamo numeri) risulter� in un errore di parsing.%
366 I teoremi sono stampati con un turnstile anteposto {\small\verb+|-+} come illustrato di sotto; il simbolo `{\small\verb|!|}' � il quantificatore universale `$\forall$'.
367 Le regole d'inferenza sono funzioni \ML{} che restituiscono valori di tipo \ml{thm}.
368 Un esempio di una regola d'inferenza � la {\it specializzazione\/} (o $\forall$-eliminazione).
374 \item $t[t'/x]$ denota il risultato della sostituzione di $t'$ per tutte le occorrenze libere di $x$ in $t$, con la restrizione che nessuna variabile libera in $t'$ venga legata dopo la sostituzione.
380 che prende come argomenti un termine \ml{``$a$``} e un teorema \holtxt{|-~!$x.\,t[x]$} e restituisce il teorema \holtxt{|-~$t[a]$}, il risultato della sostituzione di $a$ per $x$ in $t[x]$.
392 Questa sessione consiste di una dimostrazione di due passi: usando un assioma e applicando la regola \ml{SPEC}; essa esegue in modo interattivo la seguente dimostrazione:
402 Per esempio, $\ml{SPEC}\ t\ th$ fallir� se $th$ non � della forma $\ml{|-\ !}x\ml{.}\cdots$ o se � di questa forma ma il tipo di $t$ non � lo stesso del tipo di $x$, o se non � soddisfatta la restrizione della variabile libera.
405 Comunque, quando le viene passata un'eccezione \ml{HOL\_ERR}, stampa alcune utili informazioni prima di passare l'eccezione al livello successivo.}.
421 Comunque, come illustra questa sessione, il messaggio di fallimento non sempre indica la ragione esatta del fallimento.
422 In \REFERENCE\ sono date dettagliate condizioni di fallimento per le regole d'inferenza.
425 Dal momento che le dimostrazioni possono consistere di milioni di passi, � necessario fornire strumenti per rendere pi� facile la costruzione della dimostrazione da parte dell'utente.
426 Gli strumenti che generano dimostrazioni nel sistema \HOL{} sono soltanto quelli di \LCF, e sono descritti pi� avanti.
428 La forma generale di un teorema � $t_1,\ldots,t_n\;\ml{|-}\;t$, dove $t_1$, $\ldots$ , $t_n$ sono termini booleani chiamati le {\it assunzioni} e $t$ � un termine booleano chiamato la  {\it conclusione\/}.
430 Le sue condizioni di verit� sono cos� le stesse di quelle per il
434 I cinque assiomi e le otto regole primitive d'inferenza della logica di \HOL{} sono descritte nel dettaglio nel documento \DESCRIPTION.
435 Ogni valore di tipo \ml{thm} nel sistema \HOL{} si pu� ottenere applicando ripetutamente regole primitive d'inferenza agli assiomi.
438 Questa � una delle ragioni per cui la costruzione di \ml{hol} richiede cos� tanto tempo.
440 Nel resto di questa sezione, il processo di \emph{dimostrazione in avanti}, che � stato appena abbozzato, � descritto in maggior dettaglio.
441 Nella Sezione~\ref{tactics} � descritta la \emph{dimostrazione diretta dal goal}, incluse le importanti nozioni di \emph{tattiche} e \emph{tatticali}, dovute a Robin Milner.
447 \ml{ASSUME} (introduzione di un'assunzione), \ml{DISCH} (scaricamento o
448 eliminazione di un'assunzione) e \ml{MP} (Modus Ponens). Queste regole saranno
449 usate per illustrare la dimostrazione in avanti e la scrittura di regole derivate.
453 assunzione come un punto (ma questo default pu� essere cambiato; si veda di sotto). La
467 Una sorta di duale di \ml{ASSUME} � la regola primitiva d'inferenza
468 \ml{DISCH} (scaricamento, eliminazione di un'assunzione) che deduce da
502 di \ml{MP} e anche un errore comune, cio� il non fornire informazione sufficiente
503 al controllore di tipo logico di \HOL\ .
527 Le ipotesi di \ml{Th6} possono essere ispezionate con la funzione \ML{}
528 \ml{hyp}, che restituisce la lista delle assunzioni di un teorema (la
567 La sequenza di teoremi: \ml{Th3}, \ml{Th5}, \ml{Th6}, \ml{Th7}, \ml{Th8} costituisce una dimostrazione in \HOL{} del teorema \ml{|-\ t1 ==> (t1 ==> t2) ==> t2}.
572 [Introduzione di assunzione]
574 [Introduzione di assunzione]
586 Una \emph{dimostrazione dalle ipotesi} $th_1, \ldots, th_n$ � una sequenza ciascuno dei cui elementi � o un assioma, o una delle ipotesi $th_i$, o segue dagli elementi precedenti per mezzo di una regola d'inferenza.
588 Per esempio, una dimostrazione di $\Gamma,\ t'\turn t$ dalle ipotesi $\Gamma\turn t$ �:
591 \item $ t'\turn t'$ \hfill [Introduzione di assunzione]
598 e qualsiasi termine booleano $t'$ e mostra che il risultato di aggiungere un'ipotesi
600 linee di sopra possono essere aggiunte a qualsiasi dimostrazione di $\Gamma\turn t$ per ottenere una
601 dimostrazione di $\Gamma,\ t'\turn t$)\footnote{Questa propriet� della logica �
623 		svolge la dimostrazione di sopra. In notazione standard questo sarebbe
645 \noindent Il corpo di \ml{ADD\_ASSUM} � stato codificato per riflettere la dimostrazione fatta
646 nella sessione~10 di sopra, cos� da mostrare come una dimostrazione interattiva pu� essere
660 Un altro esempio di una regola d'inferenza derivata � \ml{UNDISCH}; questa sposta l'antecedente di un'implicazione nelle assunzioni.
684 \item $ t_1\turn t_1$ \hfill [Introduzione di assunzione]
695 Un'interessante regola derivata � \ml{REWRITE\_RULE}. Questa prende una lista di
701 e un teorema $\Delta\turn t$ e sostituisce ripetutamente istanze di $u_i$ in $t$ con l'istanza corrispondente di $v_i$ fino a quando non occorrono altri cambiamenti.
702 Il risultato � un teorema $\Gamma\cup\Delta\turn t'$ dove $t'$ � il risultato di riscrivere $t$ in questo modo.
703 La sessione di sotto illustra l'uso di \ml{REWRITE\_RULE}.
704 In essa la lista di equazioni � il valore \ml{rewrite\_list} che contiene i teoremi pre-dimostrati \ml{ADD\_CLAUSES} and \ml{MULT\_CLAUSES}.
753 Ci sono degli strumenti elaborati in \HOL{} per produrre riscritture personalizzate che eseguono la scansione dei termini in un ordine programmato dall'utente; \ml{REWRITE\_RULE} � la punta di un iceberg, si veda \DESCRIPTION\ per maggiori dettagli.
759 innaturale e troppo di `basso livello' per molte applicazioni. Un importante
760 passo in avanti nella metodologia di generazione delle dimostrazioni fu fatto da Robin Milner nei primi
768 \noindent Si consideri, per esempio, la regola di $\wedge$-introduzione\footnote{Nella
769   logica di ordine superiore questa � una regola derivata; nella logica del primo ordine essa
770 	di solito � primitiva. In HOL la regola � chiamata {\tt CONJ} e la sua
771 	derivazione � data in \DESCRIPTION.} mostrata di sotto:
785 seguente nuova sessione (si noti che il numero di sessione � stata reimpostato a
813 e $\turn B$ � la regola di $\wedge$-introduzione.
816 Un \emph{goal} in \HOL{} � una coppia \ml{([$t_1$,\ldots,$t_n$],$t$)} di tipo \ML{} \ml{term list~*~term}.
817 Una \emph{realizzazione} di un tale goal � un teorema \ml{$t_1$,$\ldots$,$t_n$\ |-\ $t$}.
818 Una tattica � una funzione \ML{} che quando applicata a un goal genera i subgoal insieme con una \emph{funzione di giustificazione} o di {\it validazione\/}, che sar� una regola d'inferenza derivata \ML{}, che pu� essere usata per inferire una realizzazione del goal originale dalla realizzazione dei subgoal.
820 Se $T$ � una tattica (cio� una funzione \ML{} di tipo\linebreak \ml{goal\,->\,(goal\,list\,*\,(thm\,list\,->\,thm))}) e $g$ � un goal, allora applicare $T$ a
822 oggetto che � una coppia il cui primo componente � una lista di goal e
823 il cui secondo componente � una funzione di giustificazione, cio� un valore con
826 Un esempio di tattica � \ml{CONJ\_TAC} che implementa (i) e (ii) di sopra.
827 Per esempio, si consideri il goal del tutto banale di mostrare \holtxt{T~/\bs{}~T}, dove \ml{T} � una costante che sta per $\top$ (verit�):
847 \noindent \ml{CONJ\_TAC} ha prodotto una lista di goal che consiste di due subgoal
848 identici di dimostrare soltanto \ml{([],"T")}. Ora, c'� un teorema
858 \noindent Applicare la funzione di giustificazione \ml{just\_fn} a una lista
859 di teoremi che ottengono i goal nella \ml{goal\_list} risulta
871 		speciali di dimostrazione di teoremi; esse sono solo funzioni \ML{}. Per
872 		esempio, la definizione di \ml{CONJ\_TAC} � semplicemente:
887 \ml{(asl,$t_1$)} e \ml{(asl,$t_2$)}. La funzione di giustificazione,
889 di teoremi \ml{[$th_1$,$th_2$]} e applica la regola \ml{CONJ} a
892 Riassumendo: se $T$ � una tattica e $g$ � un goal, allora l'applicazione di $T$
893 a $g$ risulter� in una coppia il cui primo componente � una lista di goal
894 e il cui secondo componente � una funzione di giustificazione, con tipo \ML{}
905 dall'applicazione di $T$ a $g$) � una funzione \ML{} che quando applicata alla
912 dimostrazione di teoremi non validi; il peggio che possono fare � risultare in
913 goal irrisolvibili o nella dimostrazione di teoremi diversi da quelli che si aveva l'intenzione di dimostrare. Se $T$ fosse
936 � un sottoinsieme di $\{u_1,\ldots,u_n\}$ e $t$ � uguale a $u$ (a meno
944 di subgoal. Cos� $T$ risolve $g$ se
999 � indicata nella notazione delle tattiche con le parentesi di insieme.
1038 Supponiamo di dover risolvere il goal $g$. Se $g$ � semplice potrebbe essere
1040 alla lista vuota di subgoal. Se questo � il caso allora eseguire:
1045 di teoremi restituisce un teorema $th$ che ottiene $g$. (La dichiarazione
1046 di sopra legher� anche $gl$ alla lista vuota di goal.) Cos� un teorema
1052 di equazioni (vuota nell'esempio che segue) e prover� a dimostrare un goal
1069 \noindent I teoremi dimostrati sono di solito archiviati nella teoria attuale
1073  \ml{store\_thm} di
1081 Se non si deve salvare il teorema, si pu� usare la funzione \ml{prove} di tipo\linebreak
1088 Quando si conduce una dimostrazione che coinvolge molti subgoal e tattiche, � necessario tenere traccia di tutte le funzioni di giustificazione e comporle nell'ordine corretto.
1090 \HOL{} fornisce un pacchetto per costruire e traversare l'albero dei subgoal, raccogliendo le funzioni di giustificazione e applicandole in modo appropriato; questo pacchetto fu inizialmente implementato per \LCF\ da Larry Paulson.
1091 Il suo utilizzo � dimostrato di sotto in alcune delle sessioni di esempio, e nel Capitolo~\ref{chap:euclid}.
1102 Alcuni tatticali importanti nel sistema \HOL{} sono elencati di sotto.
1109 \ml{THENL} pu� essere illustrata eseguendo la dimostrazione di $\vdash \uquant{m}m+0=m$ in
1148 dimostrazione di un solo passo persino pi� semplice di quella di sopra:
1246 \item Dove $x'$ � una variante di $x$
1278 Questa sezione contiene un sommario di alcune tattiche incorporate nel
1280 qui sono quelle che sono usate nell'esempio del bit di parit�.
1289 e varie regole di riscrittura incorporate.
1309 \item{\bf Altre tattiche di riscrittura}:
1315 \item {\small\verb|RW_TAC|} di tipo \ml{simpLib.simpset -> thm
1317   di teoremi di riscrittura e altre funzionalit� di dimostrazione di teoremi. I valori
1319   di base dei connettivi booleani, \ml{bossLib.arith\_ss} che
1323   argomento di \ml{RW\_TAC}.
1344 \ml{CONJ_TAC} � invocata da \ml{STRIP_TAC} (si veda di sotto).
1378 di un goal implicazione nelle assunzioni
1391 {\small\verb|STRIP_TAC|} (si veda sotto) invocher� {\small\verb|DISCH_TAC|} su goal con la forma di implicazioni.
1410 \noindent Dove $x'$ � una variante di $x$
1416 {\small\verb|STRIP_TAC|} (si veda di sotto) applica {\small\verb|GEN_TAC|} ai goal quantificati universalmente.
1427 	goal. Alla fine fallisce se la ricerca fallisce di trovare una dimostrazione pi� corta
1428 	di una profondit� ragionevole.
1470 � il tatticale che applica gli elementi rispettivi della lista di
1485 \item Scrivere tatticali (si veda la descrizione di {\small\verb|REPEAT|}