1\chapter{Librerie}\label{HOLlibraries} 2 3% LaTeX macros in HOL manuals 4% 5% \holtxt{..} for typewriter text that is HOL types or terms. To 6% produce backslashes, for /\, \/ and \x. x + 1, use \bs 7% \ml{..} for typewriter text that is ML input, including the 8% names of HOL API functions, such as mk_const 9% \theoryimp{..} for names of HOL theories. 10 11% text inside \begin{verbatim} should be indented three spaces, unless 12% the verbatim is in turn inside a \begin{session}, in which case it 13% should be flush with the left margin. 14 15 16\newcommand{\simpset}{simpset} 17\newcommand{\Simpset}{Simpset} 18 19 \newcommand{\term} {\mbox{\it term}} 20 \newcommand{\vstr} {\mbox{\it vstr}} 21 22Una \emph{libreria} � un'astrazione intesa fornire un livello pi� alto 23di organizzazione per applicazioni \HOL{}. In generale, una libreria pu� 24contenere una collezione di teorie, procedure di dimostrazione, e materiale 25di supporto, come la documentazione. Alcune librerie forniscono semplicemente 26procedure di dimostrazione, come \ml{simpLib}, mentre altre forniscono teorie e 27procedure di dimostrazioni, tale che \ml{intLib}. Le librerie possono includere altre 28librerie. 29 30Nel sistema \HOL{}, le librerie sono tipicamente rappresentate da strutture 31\ML{} nominate seguendo la convenzione che la libreria \emph{x} 32si trover� nella struttura \ML{} \ml{xLib}. Caricare questa struttura 33dovrebbe caricare tutte le sotto-componenti rilevanti della libreria e settare 34qualunque parametro di sistema che sia appropriato per l'uso della libreria. 35 36Quando il sistema \HOL{} � invocato nella sua configurazione normale, alcune 37utili librerie sono caricate automaticamente. La libreria \HOL{} 38pi� di base � \ml{boolLib}, che supporta le definizioni della logica 39\HOL{}, che si trova nella teoria \theoryimp{bool}, e fornisce un'utile 40suite di strumenti di definizione e ragionamento. 41 42Un'altra libreria usata in modo pervasivo si trova nella struttura \ml{Parse} 43(il lettore pu� vedere che non siamo strettamente fedeli alla nostra 44convenzione circa le denominazioni delle librerie). La libreria parser fornisce supporto 45per il parsing e il `pretty-printing' dei tipi, i termini, e 46i teoremi \HOL{}. 47 48La libreria \ml{boss} fornisce una collezione base di teorie 49standard e di procedure di dimostrazione di alto livello, e serve come una piattaforma 50standard su cui lavorare. Essa � pre-caricata e aperta quando il sistema 51\HOL{} si avvia. Essa include \ml{boolLib} e 52\ml{Parse}. Le teorie fornite includono \theoryimp{pair}, 53\theoryimp{sum}, \theoryimp{option}; le teorie aritmetiche 54\theoryimp{num}, \theoryimp{prim\_rec}, \theoryimp{arithmetic}, 55e \theoryimp{numeral}; e \theoryimp{list}. Altre librerie 56incluse in \ml{bossLib} sono \ml{goalstackLib}, che fornisce 57un gestore di dimostrazione per dimostrazioni basate su tattiche; \ml{simpLib}, che fornisce 58una variet� di semplificatori; \ml{numLib}, che fornisce una procedura 59di decisione per l'aritmetica; \ml{Datatype}, che fornisce 60supporto di alto-livello per definire tipi di dato algebrici; e \ml{tflLib}, 61che fornisce supporto per definire funzioni ricorsive. 62 63 64\section{Parsing e Prettyprinting} 65\label{sec:parsing-printing} 66 67Ogni tipo e termine in \HOL{} � in definitiva costruito per applicazione dei 68costruttori (astratti) primitivi per i tipi e i termini. Tuttavia, al 69fine di ospitare un'ampia variet� di espressioni matematiche, \HOL{} 70fornisce un'infrastruttura flessibile per il parsing e il prettyprinting dei tipi 71e dei termini attraverso la struttura \ml{Parse}. 72 73Il parser dei termini supporta l'inferenza di tipo, l'overloading, i binders, e 74varie dichiarazioni di fixity (infisso, prefisso, suffisso, e 75combinazioni). Ci sono anche dei flag per controllare il comportamento 76del parser. Inoltre, la struttura del parser � esposta cos� che 77possano essere costruiti rapidamente nuovi parser per supportare applicazioni utente. 78 79Il parser � parametrizzato da grammatiche per tipi e termini. Il 80comportamento del parser e del prettyprinter di conseguenza � di solito alterato 81da manipolazioni di grammatica. 82% 83\index{parsing, della logica HOL@parsing, della logica \HOL{}!grammatiche per} 84% 85Queste possono essere di due generi: \emph{temporanee} o \emph{permanenti}. 86I cambiamenti temporanei dovrebbero essere usati nelle implementazioni di librerie, o nei 87file di script per quei cambiamenti che l'utente non vuole far 88persistere nelle teorie discendenti da quella attuale. I cambiamenti permanenti 89sono appropriati per l'uso in file di script, e saranno forzati in tutte 90le teorie discendenti. Le funzioni che fanno cambiamenti temporanei sono denotate 91da un prefisso \ml{temp\_} nei loro nomi. 92 93\subsection{Parsing dei tipi} 94\index{types, nella logica HOL@types, nella logica \HOL{}!parsing of|(} 95 96Il linguaggio dei tipi � semplice. Una grammatica astratta per il 97linguaggio � presentata nella Figura~\ref{fig:abstract-type-grammar}. La 98grammatica attuale (con i valori concreti per i simboli infissi e gli operatori 99di tipo) pu� essere ispezionata usando la funzione \ml{type\_grammar}. 100\begin{figure}[tbhp] 101\newcommand{\nt}[1]{\mathit{#1}} 102\newcommand{\tok}[1]{\texttt{\bfseries #1}} 103\renewcommand{\bar}{\;\;|\;\;} 104\[ 105\begin{array}{lcl} 106\tau &::=& \tau \odot \tau \bar \nt{vtype} \bar \nt{tyop} \bar 107 \tok{(} \;\nt{tylist}\;\tok{)} \;\nt{tyop}\bar \tau \;\nt{tyop} 108 \bar \tok{(}\;\tau\;\tok{)} \bar \tau\tok{[}\tau\tok{]}\\ 109\odot &::=& \tok{->} \bar \tok{\#} \bar \tok{+} \bar \cdots\\ 110\nt{vtype} &::=& \tok{'a} \bar \tok{'b} \bar \tok{'c} \bar \cdots\\ 111\nt{tylist} &::=& \tau \bar \tau \;\tok{,}\;\nt{tylist}\\ 112\nt{tyop} &::=& \tok{bool} \bar \tok{list} \bar \tok{num} \bar 113 \tok{fun} \bar \cdots 114\end{array} 115\] 116\caption{Una grammatica astratta per i tipi \HOL{} ($\tau$). Gli infissi ($\odot$) 117 legano sempre pi� debolmente dei gli operatori di tipo~($\nt{tyop}$) (e 118 e dei sottoscritti di tipo~($\tau\tok{[}\tau\tok{]}$)), cos� che 119 $\tau_1 \,\odot\, \tau_2 \,\nt{tyop}$ � sempre parsato come $\tau_1\, \odot\, 120 (\tau_2 \,\nt{tyop})$. Infissi differenti possono avere priorit� 121 differenti, e gli infissi a diversi livelli di priorit� possono associare 122 in modo differente (alla sinistra, alla destra, o non associare del tutto). Gli utenti possono 123 estendere le categorie $\odot$ e $\nt{tyop}$ facendo nuove definizioni 124 di tipo, e manipolando la grammatica direttamente.} 125\label{fig:abstract-type-grammar} 126\end{figure} 127 128\paragraph{Infissi di tipo} 129Gli infissi possono essere introdotti con la funzione \ml{add\_infix\_type}. 130Questa imposta un mapping da un simbolo infisso (come \texttt{->}) al 131nome di un operatore di tipo esistente (come \texttt{fun}). E' necessario 132dare al simbolo binario un livello di precedenza e 133un'associativit�. Si veda \REFERENCE{} per maggiori dettagli. 134 135\paragraph{Abbreviazioni di tipo} 136\index{abbreviazioni di tipo} 137 138Gli utenti possono abbreviare pattern di tipo comuni con delle \emph{abbreviazioni}. 139Questo � fatto con la funzione \ML{} \ml{type\_abbrev}: 140\begin{hol} 141\begin{verbatim} 142 type_abbrev : string * hol_type -> unit 143\end{verbatim} 144\end{hol} 145Un'abbreviazione � un nuovo operatore di tipo, di qualsiasi numero di argomenti, 146che espande in un tipo esistente. Per esempio, si potrebbe sviluppare una 147teoria leggera di numeri estesi con un infinito, in cui 148tipo rappresentante fosse \holtxt{num option} (\holtxt{NONE} 149rappresenterebbe il valore infinito). Si potrebbe impostare un'abbreviazione 150\holtxt{infnum} che si espanderebbe a questo tipo sottostante. 151Sono supportati anche i pattern polimorfici. Per esempio, come descritto 152nella Sezione~\ref{sec:theory-of-sets}, l'abbreviazione \holtxt{set}, di 153un unico argomento, � tale che \holtxt{:'a set} espande nel tipo 154\holtxt{:'a -> bool}, per qualsiasi tipo \holtxt{:'a}. 155 156Quando i tipi devono essere stampati, l'espansione delle abbreviazioni fatta dal parser � invertita. 157Per maggiori informazioni, si veda la voce \ml{type\_abbrev} in \REFERENCE. 158\index{tipi, nella logica HOL@tipi, nella logica \HOL{}!parsing dei|)} 159 160\subsection{Parsing dei termini} 161 162Il parser dei termini fornisce un'infrastruttura basata sulla grammatica per supportare 163la sintassi concreta per le formalizzazioni. Di solito, la grammatica \HOL{} viene 164estesa quando viene fatta una nuova definizione o una specifica di costante. (L'introduzione 165di una nuova costante � discussa 166nelle Sezioni~\ref{sec:constant-definitions} e \ref{conspec}.) Tuttavia, 167qualsiasi identificatore pu� avere assegnato ad esso in ogni momento uno stato di parsing. 168In quello che segue, esploriamo alcune delle capacit� del 169parser dei termini \HOL{}. 170 171 172\subsubsection{Architettura del parser} 173\label{sec:parser:architecture} 174 175Il parser trasforma le stringhe in termini. Fa questo nella seguente 176serie di fasi, ciascuna delle quali � influenzata dalla grammatica fornita. 177Di solito questa grammatica � la grammatica globale di default, ma gli utenti possono 178organizzarsi per usare grammatiche differenti se lo desiderano. % 179\index{parsing, della logica HOL@parsing, della logica \HOL{}!grammatiche per} 180% 181Correttamente, il parsing avviene dopo che il lexing ha diviso l'input in una 182serie di token. Per maggiori informazioni sul lexing, si veda la Sezione~\ref{HOL-lex}. 183\begin{description} 184\item[Sintassi Concreta:] Caratteristiche come gli infissi, i binder e le forme 185 mix-fix sono tradotte, creando una forma di ``sintassi 186 astratta'' intermedia (tipo ML \ml{Absyn}). Le fixity possibili sono 187 discusse nella Sezione~\ref{sec:parseprint:fixities} di sotto. Le forme 188 di sintassi concreta sono aggiunte alla grammatica con funzioni come 189 \ml{add\_rule} e \ml{set\_fixity} (per le quali, si veda \REFERENCE). 190 L'azione di questa fase di parsing � incarnata nella funzione 191 \ml{Absyn}. 192 193 Il data type \ml{Absyn} � costruito usando i costruttori \ml{AQ} 194 (un antiquote, si veda la Sezione~\ref{sec:quotation-antiquotation}); % 195% 196 \index{antiquotation, nei termini della logica HOL@antiquotation, nei termini della logica \HOL{}}% 197% 198 \ml{IDENT} (un identificatore); \ml{QIDENT} (un identificatore qualificato, 199 dato come \holtxt{thy\$ident}); \ml{APP} (un'applicazione di una forma 200 a un'altra); \ml{LA} (un'astrazione di una variabile su un corpo), 201 e \ml{TYPED} (una forma accompagnata da un vincolo di tipo\footnote{I 202 tipi nei vincoli \ml{Absyn} non sono tipi HOL completi, ma valori 203 da un'altro tipo intermedio \ml{Pretype}.}, si veda 204 la Sezione~\ref{sec:parseprint-type-constraints}). A questo stadio della 205 traduzione, non viene fatta alcuna distinzione tra costanti e 206 variabili: bench� le forme \ml{QIDENT} debbano essere delle costanti, gli utente sono 207 anche in grado di riferirsi alle costanti dando loro dei nomi nudi. 208 209 E' possibile che i nomi che occorrono nel valore \ml{Absyn} siano 210 differenti da qualsiasi token che appariva nell'input 211 originale. Per esempio, l'input 212\begin{verbatim} 213 ``if P then Q else R`` 214\end{verbatim} si trasformer� in 215\begin{verbatim} 216 APP (APP (APP (IDENT "COND", IDENT "P"), IDENT "Q"), IDENT "R") 217\end{verbatim} 218 (Questo � un output leggermente semplificato: i vari costruttori per 219 \ml{Absyn}, incluso \ml{APP}, prendono anche parametri di localizzazione.) 220 221 La grammatica standard include una regola che associa la speciale 222 forma miz-fix per l'espressioni if-then-else con il sottostante 223 ``nome'' \holtxt{COND}. E' \holtxt{COND}. che sar� alla fine 224 risolto come la costante \holtxt{bool\dol{}COND}. 225 226 Se si usa la sintassi di ``quotation'' con un dollaro nudo,% 227% 228\index{ escape, nel parser della logica HOL@\ml{\$} (escape, nel parser della logica \HOL{})}% 229\index{token!sopprimere il comportamento di parsing dei|(} 230% 231allora questa fase del parser non tratter� le stringhe come parte di una 232forma speciale. Per esempio, \holtxt{\holquote{\dol{}if~P}} si trasforma 233nella forma \ml{Absyn} 234\begin{verbatim} 235 APP(IDENT "if", IDENT "P") 236\end{verbatim} 237 \emph{non} in una forma che coinvolge \holtxt{COND}. 238 239 Pi� tipicamente, spesso si scrive qualcosa come 240 \holtxt{\holquote{\$+~x}}, che genera la sintassi astratta 241\begin{verbatim} 242 APP(IDENT "+", IDENT "x") 243\end{verbatim} 244 Senza il segno di dollaro, il parser della sintassi concreta si lamenterebbe 245 del fatto che l'infisso pi� non ha un argomento 246 sinistro. Quando il risultato di successo del parsing � passato alla 247 fase successiva, il fatto che ci sia una costante chiamata \holtxt{+} 248 dar� all'input il suo significato desiderato. 249 250 Si pu� eseguire l'``escape'' dei simboli racchiudendoli in parentesi. 251 Cos�, quello di sopra si potrebbe scrivere \holtxt{\holquote{(+)~x}} per avere 252 lo stesso effetto. 253\index{token!sopprimere il comportamento di parsing dei|)} 254 255 L'utente pu� inserire a questo punto nel processo di parsing delle funzioni 256 di trasformazione intermedia sviluppate per proprio conto . Questo � fatto 257 con la funzione 258\begin{verbatim} 259 add_absyn_postprocessor 260\end{verbatim} 261 La funzione dell'utente sar� di tipo \ml{Absyn~->~Absyn} e potr� 262 eseguire qualunque cambiamento sia appropriato. Come tutti gli altri aspetti del 263 parsing, queste funzioni sono parte di una grammatica: se l'utente non vuole 264 vedere usata una particolare funzione, pu� organizzarsi in modo che il parsing 265 sia fatto rispetto a una grammatica differente. 266 267\item[Risoluzione dei Nomi:] Le forme nude \ml{IDENT} nel valore \ml{Absyn} 268 sono risolte come variabili libere, nomi legati o costanti. 269 Questo processo risulta in un valore del tipo di dati \ml{Preterm}, che 270 ha costruttori simili a quelli in \ml{Absyn} eccetto che con le forme 271 per le costanti. % 272 \index{parsing, della logica HOL@parsing, della logica \HOL{}!preterms}% 273 Una stringa pu� essere convertita direttamente in un \ml{Preterm} per mezzo della 274 funzione \ml{Preterm}. 275 276 Un nome legato � il primo argomento a un costruttore \ml{LAM}, un 277 identificatore che occorro sul lato sinistro di una freccia di 278 una espressione case, o un identificatore che occorre all'interno di un pattern 279 di comprensione d'insieme. Una costante � una stringa che � presente nel dominio 280 dell'``overload map'' della grammatica. Le variabili libere sono tutti gli altri identificatori. 281 Variabili libere dello stesso nome in un termine avranno lo stesso 282 tipo. Gli identificatori sono testati per vedere se sono legati, e poi per 283 vedere se sono costanti. Cos� � possibile scrivere 284\begin{verbatim} 285 \SUC. SUC + 3 286\end{verbatim} 287 ed avere la stringa \holtxt{SUC} trattata come un numero nel 288 contesto dell'astrazione data, piuttosto che come la costante 289 successore. 290 291\index{parsing, della logica HOL@parsing, della logica \HOL{}!overloading} 292\index{overloading|see{parsing, of \HOL{} logic, overloading}} 293 L'``overloap map'' � una mappa da stringhe a liste di termini. I 294 termini di solito sono solo costanti, ma possono essere termini arbitrari (dando 295 origine a ``macro sintattiche'' o ``pattern'').\index{macro sintattiche} 296 Questa infrastruttura � usata per permettere ad un nome come \holtxt{+} di mappare a 297 costanti di addizione differenti in teorie come 298 \theoryimp{arithmetic}, \theoryimp{integer}, e 299 \theoryimp{words}. In questo modo i nomi ``reali'' delle costanti si possono 300 slegare da ci� che l'utente digita. Nel caso dell'addizione, il 301 pi� sui numeri naturali � di fatto chiamato \holtxt{+} (strettamente, 302 \holtxt{arithmetic\$+}); ma sugli interi, � 303 \holtxt{int\_add}, e su word � \holtxt{word\_add}. (Si noti 304 che poich� ciascuna costante arriva da una teoria differente e cos� da un 305 namespace differenti, esse potrebbero avere tutte il nome \holtxt{+}.) 306 307 \index{inferenza di tipo!nel parser HOL@nel parser \HOL{}} 308 Quando la risoluzione dei nomi determina che un identificatore dovrebbe essere trattato 309 come una costante, esso � mappato a una forma pretermine che elenca tutte le 310 possibilit� per quella stringa. Successivamente, poich� i termini nel 311 range della mappa di overload tipicamente avranno tipi differenti, 312 l'inferenza di tipo spesso eliminer� le possibilit� dalla lista. Se 313 rimangono pi� possibilit� dopo che l'inferenza di tipo � stata 314 eseguita, allora sar� stampato un warning, e sar� scelta una 315 delle possibilit�. (Gli utenti possono controllare quali termini sono 316 selezionati quando si presenta questa situazione.) 317 318 Quando un termine nella mappa di overload � scelto come l'opzione migliore, � 319 sostituito nel termini alla posizione appropriata. Se il termine � una 320 lambda astrazione, allora sono fatte tante $\beta$-riduzioni quante 321 possibili, usando qualsiasi argomento a cui il termine sia stato applicato. E' 322 in questo modo che un pattern sintattico pu� elaborare gli argomenti. (Si veda 323 anche la Sezione~\ref{sec:parser:syntactic-patterns} per maggiori informazioni sui 324 pattern sintattici.) 325\item[Inferenza di Tipo:] % 326 \index{inferenza di tipo!nel parser HOL@nel parser \HOL{}}% 327 Tutti i termini nella logica \HOL{} sono ben tipizzati. Il kernel rafforza 328 questo attraverso le API per il tipo di dato \ml{term}. (In particolare, 329 la funzione \ml{mk\_comb} % 330 \index{mk_comb@\ml{mk\_comb}}% 331 controlla che il tipo del primo argomento sia una funzione il cui 332 dominio � uguale al tipo del secondo argomento.) Il lavoro del 333 parser � di trasformare le stringhe fornite dall'utente in termini. Per convenienza, 334 � vitale che l'utente non debba fornire tipi per tutti gli 335 identificatori che digita. (Si veda la Sezione~\ref{sec:parser:type-inference} 336 di sotto.) 337 338 In presenza di identificatori sottoposti a overload, l'inferenza di tipo pu� non essere 339 in grado di assegnare un tipo unico a tutte le costanti. Se esistono 340 pi� possibilit�, ne sar� scelto uno quando il \ml{Preterm} � infine 341 convertito in un termine genuino. 342\item[Conversione a un Termine:]% 343 Quando � stato completato il controllo di tipo di un \ml{Preterm}, la conversione finale da 344 quel tipo al tipo del \ml{term} � per lo pi� semplice. L'utente 345 pu� pure inserire ulteriore elaborazione a questo punto, cos� che una 346 funzione fornita dall'utente modifichi il risultato prima che il parser 347 lo restituisca. 348\end{description} 349 350\subsubsection{Caratteri unicode} 351\label{sec:parser:unicode-characters} 352 353\index{Unicode}\index{UTF-8} 354\index{parsing, della logica HOL@parsing, della logica \HOL{}!Caratteri unicode|(} 355E' possibile fare in modo che l'infrastruttura \HOL{} di parsing e stampa 356utilizzi caratteri Unicode (scritti nella codifica UTF-8). Questo rende 357possibile scrivere e leggere termini come 358\begin{alltt} 359 \(\forall\)x. P x \(\land\) Q x 360\end{alltt} 361piuttosto che 362\begin{alltt} 363 !x. P x /\bs{} Q x 364\end{alltt} 365Se lo desiderano, gli utenti possono semplicemente definire costanti che hanno caratteri 366Unicode nei loro nomi, e lasciare le cose come stanno. Il problema con 367questo approccio � che gli strumenti standard probabilmente creeranno file 368di teoria che includono binding \ML{} (illegali) come \ml{val $\rightarrow$\_def = 369 \dots}. Il risultato saranno file \ml{...Theory.sig} e 370\ml{...Theory.sml} che falliranno di compilare, anche se la chiamata a 371\ml{export\_theory} pu� avere successo. Questo problema pu� essere manovrato attraverso 372l'uso di funzioni come \ml{set\_MLname}, probabilmente � una pratica 373migliore usare solamente caratteri alfanumerici nei nomi delle costanti, e 374usare poi funzioni come \ml{overload\_on} e \ml{add\_rule} per creare 375la sintassi unicode per la costante sottostante. 376 377Se gli utenti hanno a disposizione dei font con il repertorio di caratteri appropriati per 378mostrare la loro sintassi, e confidano nel fatto che anche ognuno degli utenti delle loro 379teorie li hanno, allora questo � perfettamente ragionevole. Tuttavia, se 380gli utenti vogliono mantenere la retro-compatibilit� con la pura sintassi 381ASCII, possono farlo definendo prima una sintassi ASCII pura. Dopo aver fatto 382questo, possono creare una versione Unicode della sintassi con la 383funzione \ml{Unicode.unicode\_version}. Quindi, quando la variabile 384di traccia \ml{"Unicode"} � $0$, la sintassi ASCII sar� usata per 385il parsing e la stampa. Se la traccia � impostata a $1$, allora funzioner� 386anche la sintassi unicode nel parse, e il pretty-priunter 387la preferir� quando i termini sono stampati. 388 389Per esempio, in \ml{boolScript.sml}, il carattere Unicode per l'and 390logico (\texttt{$\land$}), � impostato come un'alternativa unicode per 391\texttt{/\bs} con la chiamata 392\begin{verbatim} 393 val _ = unicode_version {u = UChar.conj, tmnm = "/\\"}; 394\end{verbatim} 395(In questo contesto, � stata aperta la struttura \ml{Unicode}, 396dando accesso anche alla struttura \ml{UChar} che contiene i binding 397per l'alfabeto Greco, e alcuni altri simboli matematici.) 398 399L'argomento a \ml{unicode\_version} � un record con campi \ml{u} 400e \ml{tmnm}. Entrambe sono stringhe. Il campo \ml{tmnm} pu� essere o 401il nome di una costante, o un token che appare in una regola di sintassi concreta 402(che possibilmente mappa a qualche altro nome). Se il \ml{tmnm} � solo il 403nome di una costante, allora, con la variabili di traccia abilitata, la stringa 404\ml{u} sar� sottoposta a overloading con lo stesso nome. Se il \ml{tmnm} � lo 405stesso di un token di una regola di sintassi concreta, allora il comportamento � di 406creare una nuova regola che mappa allo stesso nome, ma con la stringa \ml{u} 407usata come il token. 408 409\paragraph{Regole di lexing con caratteri Unicode} 410% 411\index{token!Caratteri unicode} 412\index{identificatori, nella logica HOL@identificatori, nella logica \HOL{}!caratteri che non associano} 413% 414In parole povere, \HOL{} considera i caratteri divisi in tre 415classi: alfanumerici, simboli che non associano e simboli. Questo 416influenza il comportamento del lexer quando incontra delle stringhe di 417caratteri. A meno che ci sia gi� nella grammatica uno specifico token ``misto'', 418i token si dividono quando la classe di caratteri cambia. Cos�, nella 419stringa 420\begin{verbatim} 421 ++a 422\end{verbatim} 423il lexer vedr� due token, \holtxt{++} e \holtxt{a}, perch� 424\holtxt{+} � un simbolo e \holtxt{a} � un alfanumerico. La 425classificazione dei caratteri Unicode extra � molto 426semplicistica: tutt le lettere greche eccetto \holtxt{$\lambda$} sono alfanumerici; 427il simbolo di negazione logica \holtxt{$\neg$} non associa; e 428ogni altra cosa � simbolica. (L'eccezzione per \holtxt{$\lambda$} � per 429permettere a stringhe come \holtxt{$\lambda$x.x} di essere divise dal lexer in \emph{quattro} token.) 430 431\index{parsing, della logica HOL@parsing, della logica \HOL{}!Caratteri unicode|)} 432 433\subsubsection{Pattern sintattici (``macro'')} 434\label{sec:parser:syntactic-patterns} 435\index{parsing, della logica HOL@parsing, della logica \HOL{}!overloading} 436\index{parsing, della logica HOL@parsing, della logica \HOL{}!pattern sintattici|(} 437 438La ``mappa di overload'' menzionata in precedenza � di fatto una combinazione di 439mappe, una per il parsing, e una per la stampa. La mappa di parsing � da 440nomi a liste di termini, e determina come i nomi che appaiono in un 441\ml{Preterm} saranno tradotti in termini. In sostanza, i nomi legati sono tradotti 442in variabili legate, nomi non legati che non sono nel dominio della mappa sono tradotti 443in variabili libere, e nomi non legati nel dominio della mappa sono tradotti 444in uno degli elementi dell'insieme associato con il nome dato. 445Ogni termine nell'insieme delle possibilit� pu� avere un tipo differente, cos� 446l'inferenza di tipo sceglier� da quelli che hanno tipi coerenti con 447il resto del termine dato. Se la lista risultante contiene pi� di 448un elemento, allora il termine che appare prima nella lista sar� 449scelto. 450 451Il caso d'uso pi� comune per la mappa di overload � di avere nomi mappati a 452costanti. In questo modo, per esempio, le varie teorie aritmetiche possono 453mappare la stringa \ml{"+"} alla nozione rilevante di addizione, ognuna delle 454quali � una costante differente. Tuttavia, il sistema ha una flessibilit� 455extra perch� i nomi possono mappare termini arbitrari. Per esempio, � 456possibile mappare a istanze di costanti con specifici tipi. Cos�, la 457stringa \ml{"<=>"} mappa l'eguaglianza, ma dove gli argomenti sono forzati 458essere di tipo \holquote{:bool}. 459 460Inoltre, se il termine mappato � una lambda-astrazione (cio�, della 461forma $\lambda x.\;M$), allora il parser eseguir� tutte le $\beta$-riduzioni 462possibili per quel termine e gli argomenti che lo accompagnano. per 463esempio, in \theoryimp{boolTheory} e nei suoi discendenti, la stringa 464\ml{"<>"} � sottoposta a overload rispetto al termine \holquote{\bs{}x~y.~\td{}(x~=~y)}. 465Inoltre, \ml{"<>"} � impostato come un infisso al livello della sintassi 466concreta. Quando l'utente inserisce \holquote{x~\lt\gt~y}, il valore 467\ml{Absyn} risultante � 468\begin{verbatim} 469 APP(APP(IDENT "<>", IDENT "x"), IDENT "x") 470\end{verbatim} 471The \ml{"x"} and \ml{"y"} identifiers will map to free variables, but 472the \ml{"<>"} identifier maps to a list containing 473\holquote{\bs{}x~y.~\td(x~=~y)}. This term has type 474\begin{verbatim} 475 :'a -> 'a -> bool 476\end{verbatim} 477e le variabili polimorfiche sono generalizzabili, permettendo all'inferenza 478di tipo di dare i tipi (identici) appropriati a \ml{x} e \ml{y}. 479Assumendo che questa opzione sia l'unico oveloading per il \ml{"<>"} lasciato 480dopo l'inferenza di tipo, allora il termine risultante sar� 481\holtxt{\td(x~=~y)}. Meglio, bench� questa sar� la struttura 482sottostante del termine in memoria, esso sar� di fatto stampato come 483\holquote{x~\lt\gt~y}. 484 485Se il termine mappato nella mappa di overload contiene qualsiasi variabili libere, 486queste variabili non saranno istanziate in alcun modo. In particolare, 487se queste variabili hanno tipi polimorfici, allora le variabili di tipo in 488questi tipi saranno costanti: non soggette a istanziazione dall'inferenza 489di tipo. 490 491\paragraph{Il pretty-printing e i pattern sintattici} La seconda parte della ``mappa di overload'' � una mappa da termini a stringhe, che specifica come 492i termini dovrebbero essere trasformati indietro in identificatori. (Bench� di fatto 493non costruisca un valore \ml{Absyn}, questo processo inverte la fase del parsing 494di risoluzione dei nomi, producendo qualcosa che � poi stampato 495secondo la parte di sintassi concreta della grammatica data.) 496 497Poich� il parsing pu� mappare nomi singoli in complicate strutture di termine, 498la stampa deve essere in grado di ricondurre una complicata struttura di termine a 499un nome singolo. Esso fa questo eseguendo 500un term matching.% 501\index{matching!nel pretty-printing dei termini}% 502% 503\footnote{Il matching eseguito � del primo ordine; per contro il matching di ordine superiore 504 � fatto nel semplificatore.} 505Se pi� pattern matchano con lo stesso termine, allora il printer sceglie il 506match pi� specifico (quello che richiede l'istanziazione minima delle 507variabili del pattern.) Se questo risulta ancora in pi� possibilit�, ugualmente 508specifiche, ha la precedenza il pattern aggiunto 509pi� recentemente. (Gli utenti possono cos� manipolare le preferenze del printer 510eseguendo delle chiamate altrimenti ridondanti alla funzione \ml{overload\_on}.) 511 512Nell'esempio di sopra dell'operatore non-uguale-a, il pattern sar� 513\holtxt{\~{}(?x = ?y)}, dove i punti interrogativi, indicano variabili del pattern 514istanziabili. Se un pattern include delle variabili libere (si ricordi che 515la \ml{x} e la \ml{y} in questo esempio erano legate da un'astrazione), 516allora queste non saranno istanziabili. 517 518Non c'� alcun'altra finezza nell'uso di questa infrastruttura: matching 519``pi� grandi'', che coprono pi� di un termine hanno la precedenza. La difficolt� 520che questo pu� causare � illustrata nel pattern \holtxt{IS\_PREFIX} dalla teoria 521\theoryimp{rich\_listTheory}. Per questioni di retro-compatibilit� 522questo identificatore mappa a 523\begin{verbatim} 524 \x y. isPREFIX y x 525\end{verbatim} 526dove \holtxt{isPREFIX} � una costante da \theoryimp{listTheory}. 527(La questione � che \holtxt{IS\_PREFIX} si aspetta i suoi argomenti in 528ordine inverso a quello che si aspetta \holtxt{isPREFIX}.) Ora, quando questa 529macro � impostata la mappa di overload contiene gi� un mapping dalla 530stringa \holtxt{"isPREFIX"} alla costante \holtxt{isPREFIX} (questo 531accade con ogni definizione di costante). Ma dopo la chiamata 532che stabilisce il nuovo pattern per \holtxt{IS\_PREFIX}, la 533forma \holtxt{isPREFIX} non sar� pi� stampata. N� � sufficiente, 534ripetere la chiamata 535\begin{verbatim} 536 overload_on("isPREFIX", ``isPREFIX``) 537\end{verbatim} 538Piuttosto (supponendo che \holtxt{isPREFIX} sia di fatto la forma 539di stampa preferita), la chiamata deve essere 540\begin{verbatim} 541 overload_on("isPREFIX", ``\x y. isPREFIX x y``) 542\end{verbatim} 543cos� che il pattern di \ml{isPREFIX} � lungo quanto quella di \ml{IS\_PREFIX}. 544\index{parsing, della logica HOL@parsing, della logica \HOL{}!pattern sintattici|)} 545 546 547\subsubsection{Vincoli di tipo} 548\label{sec:parseprint-type-constraints} 549 550\index{vincoli di tipo!nel parser HOL@nel parser \HOL{}} 551Un termine pu� essere vincolato ad essere un certo tipo. Per esempio, 552\holtxt{X:bool} vincola la variabile \holtxt{X} ad avere il tipo 553\holtxt{bool}. Un tentativo di vincolare un 554termine in modo inappropriato sollever� un'eccezione: per esempio, 555\begin{hol} 556\begin{verbatim} 557 if T then (X:ind) else (Y:bool) 558\end{verbatim} 559\end{hol} 560fallir� perch� entrambi i rami di un condizionale dovono essere dello stesso 561tipo. I vincoli di tipo possono essere visti come un suffisso che lega pi� 562strettamente di qualunque altra cosa eccetto l'applicazione di funzione. Cos� $\term\ 563\ldots\ \term \ : \type$ � uguale a $(\term\ \ldots\ \term)\ : 564\type$, ma $x < y:\holtxt{num}$ � un vincolo legittimo sulla sola 565variabile $y$. 566 567 568L'inclusione di \holtxt{:} negli identificatori simbolici significa che pu� 569essere necessario separare qualche vincolo con degli spazi vuoti. Per esempio, 570\begin{hol} 571\begin{verbatim} 572 $=:bool->bool->bool 573\end{verbatim} 574\end{hol} 575sar� suddiviso dal lexer \HOL{} come 576\begin{hol} 577\begin{verbatim} 578 $=: bool -> bool -> bool 579\end{verbatim} 580\end{hol} 581ed elaborato dal parser come un'applicazione del'identificatore simbolico \holtxt{\$=:} alla 582lista di termini argomento [\holtxt{bool}, \holtxt{->}, \holtxt{bool}, 583\holtxt{->}, \holtxt{bool}]. Uno spazio messo al punto giusto eviter� questo problema: 584\begin{hol} 585\begin{verbatim} 586 $= :bool->bool->bool 587\end{verbatim} 588\end{hol} 589� elaborato da parser come l'identificatore simbolico ``='' vincolato a un tipo. 590Al posto del \holtxt{\$}, si possono anche usare le parentesi per rimuovere dai lessemi 591un comportamento di parsing speciale: 592\begin{hol} 593\begin{verbatim} 594 (=):bool->bool->bool 595\end{verbatim} 596\end{hol} 597 598\subsubsection{Inferenza di tipo} 599\label{sec:parser:type-inference} 600 601\index{inferenza di tipo!nel parser HOL@nel parser \HOL{}|(} 602Si consideri il termine \holtxt{x = T}: esso (e tutti i suoi sottotermini) 603ha un tipo nella logica \HOL{}. Ora, \holtxt{T} ha il tipo \holtxt{bool}. Questo 604significa che la costante \holtxt{=} ha tipo \holtxt{xty -> bool -> bool}, 605per qualche tipo \holtxt{xty}. Dal momento che lo schema di tipo per \holtxt{=} � 606\holtxt{'a -> 'a -> bool}, sappiamo che \holtxt{xty} di fatto deve essere 607\holtxt{bool} perch� l'istanza di tipo sia ben formata. Sapendo 608questo, possiamo dedurre che il tipo di \holtxt{x} deve essere \holtxt{bool}. 609 610Trascurando il gergo (``schema'' e ``istanza'') nel precedente 611paragrafo, abbiamo condotto un assegnamento di tipo alla struttura di termine, 612finendo con un termine ben formato. Sarebbe molto noioso per gli utenti 613condurre un tale assegnamento a mano per ciascun termine immesso ad \HOL{}. 614Cos�, \HOL{} usa un adattamento dell'algoritmo d'inferenza di tipo di Milner 615per l'\ML{} quando si costruiscono dei termini attraverso il parsing. Alla fine dell'inferenza 616di tipo, alle variabili di tipo non vincolate sono assegnati dei nomi da parte del sistema. 617Di solito, questa assegnazione fa la cosa giusta. Tuttavia, a volte, il 618tipo pi� generale non � ci� che si desidera e l'utente deve aggiungere dei vincoli 619di tipo ai sotto termini rilevanti. Per situazioni complicate, si pu� assegnare la 620variabili globale \ml{show\_types}. Quando � impostato questo flag, 621i prettyprinter per i termini e i teoremi mostreranno come i tipi 622sono stati assegnati ai sottotermini. Se non si vuole che il sistema assegni 623delle variabili di tipo per proprio conto, si pu� impostare la variabile globale 624\ml{guessing\_tyvars} a \ml{false}, nel qual caso 625l'esistenza delle variabili di tipo non assegnate alla fine dell'inferenza di tipo 626solleveranno un'eccezzione. 627\index{type inference!nel parser HOL@nel parser \HOL{}|)} 628 629 630\subsubsection{Overloading} 631\label{sec:parsing:overloading} 632 633\index{parsing, della logica HOL@parsing, della logica \HOL{}!overloading|(} 634Una misura limitata di risoluzione di overloading � eseguita dal parser 635del termine. Per esempio, il simbolo `tilde' (\holtxt{\~{}}) 636denota la negazione booleana nella teoria iniziale di \HOL, e denota anche 637l'invero additivo nelle teorie \ml{integer} e 638\ml{real}. Se carichiamo la teoria \ml{integer} 639e immettiamo un termine ambiguo con \holtxt{\~{}}, il 640sistema ci informer� che � stata eseguita la risoluzione dell'overloading. 641 642\setcounter{sessioncount}{0} 643\begin{session} 644\begin{verbatim} 645- load "integerTheory"; 646> val it = () : unit 647 648- Term `~~x`; 649<<HOL message: more than one resolution of overloading was possible.>> 650> val it = `~~x` : term 651 652- type_of it; 653> val it = `:bool` : hol_type 654\end{verbatim} 655\end{session} 656 657Per risolvere pi� scelte possibili � usato un meccanismo di priorit�. 658Nell'esempio, \holtxt{\~{}} potrebbe essere coerentemente scelto avere il tipo 659\holtxt{:bool -> bool} o \holtxt{:int -> int}, e il 660meccanismo ha scelto il primo. Per un controllo pi� fine, si possono usare dei 661vincoli di tipo espliciti. Nella seguente sessione, il 662\holtxt{\~{}\~{}x} nella prima quotation ha il tipo \holtxt{:bool}, 663mentre nella seconda, un vincolo di tipo assicura che \holtxt{\~{}\~{}x} ha 664il tipo \holtxt{:int}. 665 666\begin{session} 667\begin{verbatim} 668- show_types := true; 669> val it = () : unit 670 671- Term `~(x = ~~x)`; 672<<HOL message: more than one resolution of overloading was possible.>> 673> val it = `~((x :bool) = ~~x)` : term 674 675- Term `~(x:int = ~~x)`; 676> val it = `~((x :int) = ~~x)` : term 677\end{verbatim} 678\end{session} 679 680Si noti che il simbolo \holtxt{\~{}} sta per due costanti differenti nella 681seconda quotation; la sua prima occorrenza � la negazione booleana, mentre 682le altre due occorrenze sono l'operazione d'inverso additivo per 683gli interi. 684\index{parsing, della logica HOL@parsing, della logica \HOL{}!overloading|)} 685 686\subsubsection{Le fixity} 687\label{sec:parseprint:fixities} 688 689Al fine di fornire qualche flessibilit� notazionale, le costanti sono disponibili in varie forme o {\it fixity}: oltre a essere costanti ordinarie (senza alcuna fixity), le costanti possono essere anche dei {\it binder}, {\it prefissi}, {\it suffissi}, {\it infissi}, o {\it closefix}. 690Pi� in generale, i termini possono anche essere rappresentati usando specifiche {\it mixfix} ragionevolmente arbitrarie. 691Il grado in cui i termini legano i loro argomenti associati � conosciuto come precedenza. 692Pi� grande � questo numero, pi� stretto il binding. 693Per esempio, nel momento in cui � introdotto, \verb-+- ha una precedenza di 500, mentre il pi� stretto binder moltiplicazione (\verb+*+) ha una precedenza di 600. 694 695\paragraph{I binder} 696 697Un binder � un costrutto che lega una variabile; per esempio, il 698quantificatore universale. In \HOL, questo � rappresentato usando un trucco che 699risale ad Alnozo Church: un binder � una costante che prende una lambda 700astrazione come suo argomento. Il binding lambda � usato per implementare 701il binding del costrutto. Questa � una soluzione elegante ed uniforme. 702Cos� la sintassi concreta \verb+!v. M+ � rappresentata 703dall'applicazione della costante \verb+!+ all'astrazione \verb+(\v. M)+. 704 705I binder pi� comuni sono \verb+!+, \verb+?+, \verb+?!+, e 706\verb+@+. A volte si vogliono iterare applicazione dello stesso 707binder, ad esempio, 708\begin{alltt} 709 !x. !y. ?p. ?q. ?r. \term. 710\end{alltt} 711Questo pu� invece essere reso come 712\begin{alltt} 713 !x y. ?p q r. \term. 714\end{alltt} 715 716\paragraph{Infissi} 717 718Le costanti infisse possono associare in tre modi differenti: a destra, 719a sinistra o non associare del tutto. (Se \holtxt{+} fosse non-associativo, allora 720il parser non riuscirebbe ad elaborare \holtxt{3 + 4 + 5}; si dovrebbe scrivere 721\holtxt{(3 + 4) + 5} o \holtxt{3 + (4 + 5)} a seconda del significato 722desiderato.) L'ordine di precedenza per l'insieme iniziale di infissi � 723\holtxt{/\bs}, \holtxt{\bs/}, \holtxt{==>}, \holtxt{=}, 724\begin{Large}\holtxt{,}\end{Large} (la virgola\footnote{Quando 725 � stata caricata \theoryimp{pairTheory}.}). Inoltre, tutte queste 726costanti sono associative a destra. Cos� 727\begin{hol} 728\begin{verbatim} 729 X /\ Y ==> C \/ D, P = E, Q 730\end{verbatim} 731\end{hol} 732% 733� uguale a 734% 735\begin{hol} 736\begin{verbatim} 737 ((X /\ Y) ==> (C \/ D)), ((P = E), Q). 738\end{verbatim} 739\end{hol} 740% 741\noindent Un'espressione 742\[ 743\term \; \holtxt{<infix>}\; \term 744\] 745� rappresentata internamente come 746\[ 747((\holtxt{<infix>}\; \term)\; \term) 748\] 749 750\paragraph{Prefissi} 751 752Mentre gli infissi appaiono tra i loro argomenti, i prefissi appaiono prima di essi. 753Questo potrebbe inizialmente apparire la stessa cosa di quanto accade con la normale applicazione di funzione dove il simbolo alla sinistra semplicemente non ha alcuna fixity: $f$ in $f(x)$ non si comporta forse come un prefisso? 754Di fatto tuttavia, in un termine come $f(x)$, dove $f$ e $x$ non hanno fixity, la sintassi � trattata come se ci fosse una invisibile applicazione di funzione infissa tra i due token: $f\cdot{}x$. 755Questo operatore infisso lega pi� strettamente, cos� che quando si scrive $f\,x + y$, il risultato del parser � $(f\cdot{}x) + y$\footnote{Ci sono operatori infissi che legano pi� strettamente, il punto nella selezione di campo fa s� che $f\,x.fld$ sia elaborato dal parser come $f\cdot(x.fld)$.\index{tipi record!notazione di selezione del campo}}. 756E' quindi utile permettere dei prefissi genuini cos� che gli operatori possano vivere a livelli di precedenza differenti rispetto all'applicazione di funzione. 757Un esempio di questo � \verb+~+, la negazione logica. 758Questo � un prefisso con una precedenza pi� bassa dell'applicazione di funzione. 759Normalmente 760\[ 761 f\;x\; y\qquad \mbox{� elaborata dal parser come}\qquad (f\; x)\; y 762\] ma \[ 763 \holtxt{\~{}}\; x\; y\qquad\mbox{� elaborata dal parser come}\qquad 764 \holtxt{\~{}}\; (x\; y) 765\] 766poich� la precedenza di \verb+~+ � pi� bassa di quella dell'applicazione di funzione. 767Il simbolo unario di negazione sarebbe anche tipicamente definito come un prefisso, se non altro per permettere di scrivere \[ 768 {\it negop}\,{\it negop}\,3 769\] 770(qualunque cosa sia {\it negop}) senza bisogno di parentesi extra. 771 772Dall'altro lato, la sintassi \holtxt{univ} per l'insieme universale (si veda la Sezione~\ref{sec:theory-of-sets}\index{universal set}) � un esempio di un operatore prefisso che lega pi� strettamente dell'applicazione. 773Questo significa che \holtxt{f\,univ(:'a)} � elaborato dal parser come \holtxt{f(univ(:'a))}, non come \holtxt{(f univ)(:'a)} (su cui il parser fallirebbe il controllo di tipo). 774 775\paragraph{Suffissi} 776 777I suffissi appaiono dopo il loro argomenti. Non ci sono suffissi 778introdotti nelle teorie standard disponibili in \HOL{}, ma gli utenti 779sono sempre in grado di introdurli per loro conto se lo scelgono. I suffissi sono 780associati con una precedenza esattamente come lo sono gli infissi e i prefissi. 781Se \holtxt{p} � un prefisso, \holtxt{i} un infisso, e \holtxt{s} un 782suffisso, allora ci sono sei ordinamenti possibili per i tre differenti 783operatori, sulla base delle loro precedenze, dando cinque risultati per il parsing di 784$\holtxt{p}\; t_1\; \holtxt{i}\; t_2\; \holtxt{s}$ a seconda delle 785relative precedenze: 786\[ 787\begin{array}{cl} 788\mbox{\begin{tabular}{c}Precedenze\\(dalla pi� bassa alla pi� alta)\end{tabular}} & 789\multicolumn{1}{c}{\mbox{Risultato del parsing}}\\ 790\hline 791p,\;i,\;s & \holtxt{p}\;(t_1\;\holtxt{i}\;(t_2\;\holtxt{s}))\\ 792p,\;s,\;i & \holtxt{p}\;((t_1\;\holtxt{i}\;t_2)\;\holtxt{s})\\ 793i,\;p,\;s & (\holtxt{p}\;t_1)\;\holtxt{i}\;(t_2\;\holtxt{s})\\ 794i,\;s,\;p & (\holtxt{p}\;t_1)\;\holtxt{i}\;(t_2\;\holtxt{s})\\ 795s,\;p,\;i & (\holtxt{p}\;(t_1\;\holtxt{i}\;t_2))\;\holtxt{s}\\ 796s,\;i,\;p & ((\holtxt{p}\;t_1)\;\holtxt{i}\;t_2)\;\holtxt{s}\\ 797\end{array} 798\] 799 800\paragraph{I closefix} 801 802I termini closefix sono operatori che racchiudono completamente gli argomenti. 803Un esempio che si potrebbe usare nello sviluppo di una teoria della 804semantica denotazionale sono le parentesi semantiche. Cos�, le infrastrutture di parsing 805di \HOL{} possono essere configurate in modo da permettere di scrivere \holtxt{denotation x} 806come \holtxt{[| x |]}. I closefix non sono associati con delle precedenze 807perch� non possono competere per gli argomenti con altri operatori. 808 809 810\subsubsection{Trucchi e magia del parser} 811 812Qui descriviamo come ottenere alcuni effetti utili con il 813parser in \HOL{}. 814 815\begin{description} 816 817\item[Aliasing] Se si vuole che una sintassi speciale sia un ``alias'' per una 818 forma \HOL{} normale, questo � facile da ottenere; entrambi gli esempi fatti finora 819 di fatto hanno fatto proprio questo. Tuttavia, se si vuole avere soltanto una 820 normale sostituzione uno-a-uno di una stringa per un'altra, non si pu� 821 usare la fase grammatica/sintassi per parsing per fare questo. Piuttosto, si 822 pu� usare il meccanismo di overloading. Per esempio, sia 823 \texttt{MEM} un alias per \texttt{IS\_EL}. Abbiamo bisogno della funzione 824 \texttt{overload\_on} per impostare l'overload della constante originale sul nuovo 825 nome: 826\begin{verbatim} 827 val _ = overload_on ("MEM", Term`IS_EL`); 828\end{verbatim} 829 830\item[Rendere l'addizione associativa a destra] Se si ha un numero di vecchi 831 script che assumono che l'addizione sia associativa a destra perch� questo � 832 come era una volta \HOL{}, potrebbe essere troppo penoso convertire tutto. Il trucco 833 � di rimuovere tutte le regole al livello dato della grammatica, e 834 rimetterle come infissi che associano sulla destra. il modo pi� semplice per riconoscere 835 quali regole sono nella grammatica � per ispezione (usando 836 \ml{term\_grammar()}). Con la sola \ml{arithmeticTheory} 837 caricata, gli unici infissi al livello 500 sono \holtxt{+} and 838 \holtxt{-}. Cos�, rimuoviamo le loro regole: 839\begin{verbatim} 840 val _ = app temp_remove_rules_for_term ["+", "-"]; 841\end{verbatim} 842 \noindent E poi le rimettiamo con l'associativit� 843 appropriata: 844\begin{verbatim} 845 val _ = app (fn s => temp_add_infix(s, 500, RIGHT)) ["+", "-"]; 846\end{verbatim} 847\noindent Si noti che usiamo le versioni \ml{temp\_} di queste due 848funzioni cos� che altre teorie che dipendono da questa non saranno 849influenzate. Si noti inoltre che non possiamo avere due infissi allo stesso 850livello di precedenza con differenti associativit�, cos� dobbiamo 851rimuovere entrambi gli operatori, non solo l'addizione. 852 853\item[Sintassi mix-fix per {\it if-then-else}:] 854\index{condizionali, nella logica HOL@condizionali, nella logica \HOL{}!stampa dei} 855% 856Il primo passo per andare in questa direzione � di guardare all'aspetto generale 857delle espressioni di questa forma. In questo caso, sar�: 858% 859\[ 860 \holtxt{if}\;\; \dots \;\;\holtxt{then}\;\;\dots\;\; 861 \holtxt{else}\;\;\dots 862 \] 863% 864 Dal momento che ci deve essere un termine ``a penzoloni'' sulla destra, la 865 fixity appropriata � \ml{Prefix}. Sapendo che il termine costante 866 sottostante � chiamato \holtxt{COND}, il modo pi� semplice per ottenere 867 la sintassi desiderata �: 868\begin{verbatim} 869val _ = add_rule 870 {term_name = "COND", fixity = Prefix 70, 871 pp_elements = [TOK "if", BreakSpace(1,0), TM, BreakSpace(1,0), 872 TOK "then", BreakSpace(1,0), TM, BreakSpace(1,0), 873 TOK "else", BreakSpace(1,0)], 874 paren_style = Always, 875 block_style = (AroundEachPhrase, (PP.CONSISTENT, 0))}; 876\end{verbatim} 877\noindent La regola effettiva � leggermente un p� pi� complicata, e 878si pu� trovare nei sorgenti della teoria \theoryimp{bool}. 879 880\item[Sintassi mix-fix sintassi per la sostituzione di termini:] 881 882Qui ci� che si desidera � di essere in grado di scrivere qualcosa come: 883\[ 884 \mbox{\texttt{[}}\,t_1\,\mbox{\texttt{/}}\,t_2\,\mbox{\texttt{]}}\,t_3 885\] 886denotando la sostituzione di $t_1$ per $t_2$ in $t_3$, magari 887traducendolo in \holtxt{SUB $t_1$ $t_2$ $t_3$}. Questo sembra 888come ci dovesse essere un altro \ml{Prefix}, ma la scelta delle 889parentesi quadre (\holtxt{[} e \holtxt{]}) come delimitatori sarebbe 890in conflitto con la sintassi concreta per i letterali lista se si facesse questo. 891Dato che i letterali lista sono di fatto della classe 892\ml{CloseFix}, la nuova sintassi deve essere della stessa classe. Questo � abbastanza semplice 893da fare: impostiamo la sintassi 894\[ 895\holtxt{[}\,t_1\,\holtxt{/}\,t_2\,\holtxt{]} 896\] 897in modo che mappi a \holtxt{SUB $t_1$ $t_2$}, un valore di un tipo 898funzionale, che quando applicato a un terzo argomento apparir� 899corretto\footnote{Si noti che facendo la stessa cosa per 900 l'esempio \textit{if-then-else} di sopra sarebbe 901 inappropriato, dal momento che permetterebbe di scrivere 902\[ \holtxt{if}\;P\;\holtxt{then}\;Q\;\holtxt{else} \] 903senza l'argomento finale}. 904La regola per questo � cos�: 905\begin{verbatim} 906 val _ = add_rule 907 {term_name = "SUB", fixity = Closefix, 908 pp_elements = [TOK "[", TM, TOK "/", TM, TOK "]"], 909 paren_style = OnlyIfNecessary, 910 block_style = (AroundEachPhrase, (PP.INCONSISTENT, 2))}; 911\end{verbatim} 912 913\end{description} 914 915\subsubsection{Nascondere le costanti} 916\label{hidden} 917 918\index{parsing, della logica HOL@parsing, della logica \HOL{}!nascondere lo status di costante|(} 919\index{sistema HOL@sistema \HOL{}!nascondere le costanti nel|(} 920\index{costanti, nella logica HOL@costanti, nella logica \HOL{}!nascondere lo status delle} 921\index{parsing, della logica HOL@parsing, della logica \HOL{}!overloading} 922% 923La seguente funzione pu� essere usata per nascondere lo status di costante di un 924nome dal parser delle quotation. 925 926\begin{holboxed} 927\index{hide@\ml{hide}|pin} 928\begin{verbatim} 929 val hide : string -> ({Name : string, Thy : string} list * 930 {Name : string, Thy : string} list) 931\end{verbatim} 932\end{holboxed} 933 934\noindent La valutazione di \ml{hide "$x$"} 935fa s� che il parser delle quotation tratti $x$ come una variabile (purch� le regole 936lessicali lo permettano), anche se $x$ � il nome di una costante nella teoria attuale 937(le costanti e le variabili possono avere lo stesso nome). 938Questo � utile se si vogliono usare delle variabili 939% 940\index{variabili, nella logica HOL@variabili, nella logica \HOL{}!con nomi di costante} 941% 942con lo stesso nome di costanti dichiarate in precedenza (o incorporate) 943(ad esempio \ml{o}, \ml{I}, \ml{S} \etc). Il nome $x$ � ancora una costante 944per i costruttori, le teorie, ecc; \ml{hide} influisce solo sul parsing e 945la stampa rimuovendo il nome dato dalla ``mappa di overload'' descritta 946di sopra nella Sezione~\ref{sec:parser:architecture}. Si noti che l'effetto 947di \ml{hide} � \emph{temporaneo}; i suoi effetti non persistono nelle 948teorie discendenti da quella attuale. Si veda la voce \ml{hide} in 949\REFERENCE{} per maggiori dettagli, inclusa una spiegazione del tipo 950restituito. 951 952La funzione 953 954\begin{holboxed} 955\index{reveal@\ml{reveal}|pin} 956\begin{verbatim} 957 reveal : string -> unit 958\end{verbatim} 959\end{holboxed} 960 961\noindent annulla il nascondimento. 962 963La funzione 964 965\begin{holboxed} 966\index{hidden@\ml{hidden}|pin} 967\begin{verbatim} 968 hidden : string -> bool 969\end{verbatim} 970\end{holboxed} 971 972\noindent controlla se una stringa � il nome di una costante nascosta. 973\index{sistema HOL@sistema \HOL{}!adattamento dell'interfaccia utente del} 974\index{sistema HOL@sistema \HOL{}!nascondere le costanti nel|)} 975\index{parsing, della logica HOL@parsing, della logica \HOL{}!nascondere lo status di costante nel|)} 976 977\subsubsection{Adattare la profondit� del pretty-print} 978\index{stampa, nella logica HOL@stampa, nella logica \HOL{}!adattamento della profondit� strutturale nella} 979 980La seguente reference \ML{} pu� essere usata per impostare la profondit� massima 981della stampa 982 983\begin{holboxed} 984\index{max_print_depth@\ml{max\_print\_depth}|pin} 985\begin{verbatim} 986 max_print_depth : int ref 987\end{verbatim} 988\end{holboxed} 989 990\index{profondit� di stampa di default, per la logica HOL@profondit� di stampa di default, per la logica \HOL{}|(} 991 992\noindent La profondit� di default della stampa � $-1$ che � intesa significare 993nessun massimo. I sotto termini annidati pi� profondamente della profondit� 994massima di stampa sono stampati come \holtxt{...}. Per esempio: 995 996\setcounter{sessioncount}{0} 997\begin{session} 998\begin{verbatim} 999- ADD_CLAUSES; 1000> val it = 1001 |- (0 + m = m) /\ (m + 0 = m) /\ (SUC m + n = SUC (m + n)) /\ 1002 (m + SUC n = SUC (m + n)) : thm 1003 1004- max_print_depth := 3; 1005> val it = () : unit 1006- ADD_CLAUSES; 1007> val it = |- (... + ... = m) /\ (... = ...) /\ ... /\ ... : thm 1008\end{verbatim} 1009\end{session} 1010\index{profondit� di stampa di default, per la logica HOL@profondit� di stampa di default, per la logica \HOL{}|)} 1011 1012\subsection{Quotation e antiquotation} 1013\label{sec:quotation-antiquotation} 1014 1015\index{quotation, nella logica HOL@quotation, nella logica \HOL{}!parser per} 1016\index{parsing, della logica HOL@parsing, della logica \HOL{}!della sintassi di quotation|(} 1017La sintassi correlata alla logica nel sistema HOL � tipicamente passato al 1018parser in forme speciali conosciute come \emph{quotation}. Una quotation di base 1019� delimitata da singoli accenti grave (cio�, \ml{`}, carattere ASCII~96). Quando 1020i valori quotation sono stampati dal loop interattivo ML, appaiono 1021piuttosto brutti a causa dello speciale filtro che � fatto di questi 1022valori ancor prima che l'interprete li veda: 1023\setcounter{sessioncount}{0} 1024\begin{session} 1025\begin{verbatim} 1026- val q = `f x = 3`; 1027> val 'a q = [QUOTE " (*#loc 1 11*)f x = 3"] : 'a frag list 1028\end{verbatim} 1029\end{session} 1030Quotations (Moscow ML prints the type as \ml{'a frag list}) are the 1031raw input form expected by the various HOL parsers. They are also 1032polymorphic (to be explained below). Thus the function 1033\ml{Parse.Term} function takes a (term) quotation and returns a term, 1034and is thus of type \[ \ml{term quotation -> term} 1035\] 1036 1037I parser dei termini e dei tipi possono essere chiamati anche implicitamente usando 1038i doppi accenti acuti come delimitatori. Per il parser dei tipi, il primo 1039carattere non spazio dopo il delimitatore principale deve essere un segno di deu punti. 1040Cos�: 1041\begin{session} 1042\begin{verbatim} 1043- val t = ``p /\ q``; 1044> val t = ``p /\ q`` : term 1045 1046- val ty = ``:'a -> bool``; 1047> val ty = ``:'a -> bool`` : hol_type 1048\end{verbatim} 1049\end{session} 1050 1051L'espressione legata alla variabile ML \ml{t} di sopra di fatto � espansa 1052a un'applicazione della funzione \ml{Parse.Term} alla quotation 1053argomento \ml{`p /\bs{} q`}. Analogamente, la seconda espressione si espande 1054in un'applicazione di \ml{Parse.Type} alla quotation \ml{`:'a -> bool`}. 1055 1056Il vantaggio importante delle quotation rispetto a normali stringhe \ML{} � 1057che esse possono includere caratteri di nuova riga e backslash senza 1058richiedere caratteri speciali di escape. Le nuove righe occorrono ogni volta che i termini vanno oltre 1059una dimensione banale, mentre i backslash occorrono non solo nella 1060rappresentazione di $\lambda$, ma anche nella sintassi per la congiunzione e 1061la disgiunzione. 1062 1063Se una quotation deve includere un carattere di accento grave, allora questo dovrebbe 1064essere fatto usando il carattere di escape proprio della sintassi della quotation, il 1065caret (\ml{\^}, carattere ASCII~94). Per avere un semplice caret, le cose diventano 1066leggermente pi� complicate. Se una sequenza di caret � seguita dallo 1067spazio vuoto (incluso un carattere di nuova riga), allora quella sequenza di caret � 1068passata al parser di HOL senza modifiche. Altrimenti, un singolo caret si pu� 1069ottenere scrivendone due in una riga. (L'ultima regola � analoga al 1070modo in cui in \ML{} la sintassi delle stringhe tratta il backslash.) Cos�: 1071\begin{session} 1072\begin{verbatim} 1073- ``f ^` x ``; 1074<<HOL message: inventing new type variable names: 'a, 'b, 'c>> 1075> val it = ``f ` x`` : term 1076 1077- ``f ^ x``; 1078<<HOL message: inventing new type variable names: 'a, 'b, 'c>> 1079> val it = ``f ^ x`` : term 1080\end{verbatim} 1081\end{session} 1082 1083La regola per i caret non seguiti da uno spazio vuoto � illustrata qui, 1084includendo un esempio che accade quando non si segue la regola 1085per il quoting: 1086\begin{session} 1087\begin{verbatim} 1088- ``f ^^+ x``; 1089<<HOL message: inventing new type variable names: 'a, 'b, 'c>> 1090> val it = ``f ^+ x`` : term 1091 1092- ``f ^+ x``; 1093! Toplevel input: 1094! (Parse.Term [QUOTE " (*#loc 2 3*)f ", ANTIQUOTE (+), 1095! QUOTE " (*#loc 2 7*) x"]); 1096! ^ 1097! Ill-formed infix expression 1098\end{verbatim} 1099\end{session} 1100 1101L'uso principale del caret � d'introdurre le \emph{quntiquotation} (come 1102suggerito nell'ultimo esempio di sopra). All'interno di una quotation, l'espressioni 1103della forma {\small\verb+^(+}$t${\small\verb+)+} 1104% 1105\index{ antiquotation, nella logica HOL@{\small\verb+^+} (antiquotation, nella logica \HOL{})} 1106% 1107(dove $t$ � un'espressione \ML\ di tipo 1108% 1109\index{controllo di tipo, nella logica HOL@controllo di tipo, nella logica \HOL{}!antiquotation nel} 1110% 1111\ml{term} o \ml{type}) sono chiamate antiquotation. 1112% 1113\index{termini, nella logica HOL@termini, nella logica \HOL{}!antiquotation} 1114\index{antiquotation, nei termini della logica HOL@antiquotation, nei termini della logica \HOL{}} 1115% 1116Una quotation \holtxt{\^{}($t$)} � valutata al 1117valore \ML{} di $t$. Per esempio, {\small\verb+``x \/ ^(mk_conj(``y:bool``, ``z:bool``))``+} 1118� valutata allo stesso termine di {\small\verb+``x \/ (y /\ z)``+}. L'uso 1119pi� comune dell'antiquotation � quando il termine $t$ � legato a una variabile 1120\ML\ $x$. In questo caso {\small\verb+^(+}$x${\small\verb+)+} pu� essere 1121abbreviato da {\small\verb+^+}$x$. 1122 1123La seguente sessione illustra l'antiquotation. 1124 1125\setcounter{sessioncount}{0} 1126\begin{session} 1127\begin{verbatim} 1128- val y = ``x+1``; 1129> val y = ``x + 1`` : term 1130 1131val z = ``y = ^y``; 1132> val z = ``y = x + 1`` : term 1133 1134- ``!x:num.?y:num.^z``; 1135> val it = ``!x. ?y. y = x + 1`` : term 1136\end{verbatim} 1137\end{session} 1138 1139\noindent Anche i tipi possono essere sottoposti all'antiquotation: 1140 1141\begin{session} 1142\begin{verbatim} 1143- val pred = ``:'a -> bool``; 1144> val pred = ``:'a -> bool`` : hol_type 1145 1146- ``:^pred -> bool``; 1147> val it = ``:('a -> bool) -> bool`` : hol_type 1148\end{verbatim} 1149\end{session} 1150 1151\noindent Le quotation sono polimorfiche, e la variabile di tipo di una 1152quotation corrisponde al tipo dell'entit� che pu� essere sottoposta all'antiquotation 1153in quella quotation. Dal moemnto che il parser dei termini si aspetta solo termini 1154sottoposti ad antiquotation, l'antiquotation di un tipo all'interno di una quotation di termine richiede l'uso di 1155\holtxt{ty\_antiq}. Per esempio,% 1156% 1157\index{ty_antiq@\ml{ty\_antiq}} 1158 1159\begin{session} 1160\begin{verbatim} 1161- ``!P:^pred. P x ==> Q x``; 1162 1163! Toplevel input: 1164! Term `!P:^pred. P x ==> Q x`; 1165! ^^^^ 1166! Type clash: expression of type 1167! hol_type 1168! cannot have type 1169! term 1170 1171- ``!P:^(ty_antiq pred). P x ==> Q x``; 1172> val it = `!P. P x ==> Q x` : term 1173\end{verbatim} 1174\end{session} 1175% 1176\index{parsing, della logica HOL@parsing, della logica \HOL{}!della sintassi delle quotation|)} 1177 1178 1179 1180\subsection{Retro-compatibilit� della sintassi} 1181 1182Questa sezione del manuale documenta il cambiamento (esteso) fatto al 1183parsing di \HOL{} dei termini e dei tipi nella release Taupo (una delle 1184release HOL3) e al di l� del punto di vista di un utente che non 1185vuole sapere come usare le nuove strutture, ma vuole essere sicuro 1186che il proprio vecchio codice continui a funzionare in modo pulito. 1187 1188I cambiamenti che possono far s� che i vecchi termini falliscano il parsing sono: 1189\begin{itemize} 1190\newcommand\condexp{\holtxt{$p$ => $q$ | $r$}} 1191\item La precedenza delle annotazioni di tipo � completamente cambiata. Ora 1192 � un suffisso molto stretto (bench� con una precedenza pi� debole di quella 1193 associata con l'applicazione di funzione), invece di uno debole. 1194 Questo significa che \mbox{\tt (x,y:bool \# bool)} ora dovrebbe essere scritto 1195 come \mbox{\tt (x,y):bool \# bool}. La forma precedente sar� ora 1196 parsata come un'annotazione di tipo che si applica solo a \verb+y+. Questo 1197 cambiamento porta la sintassi delle logica pi� vicina a quella dell'SML e 1198 dovrebbe rendere in genere pi� facile annotare le tuple, dal momento che ora 1199 si pu� scrivere \[ (x\,:\,\tau_1,\;y\,:\,\tau_2,\dots z\,:\,\tau_n) 1200 \] al posto di \[ 1201 (x\,:\,\tau_1, \;(y\,:\,\tau_2, \dots (z\,:\,\tau_n))) 1202 \] dove le parentesi extra si sono dovute aggiungere solo per permettere di 1203 scrivere una forma di vincolo che occorre frequentemente. 1204\item La maggior parte degli operatori aritmetici ora sono associativi a sinistra piuttosto che 1205 a destra. In particolare, $+$, $-$, $*$ e {\tt DIV} sono 1206 associativi a sinistra. In modo simile, gli analoghi operatori nelle altre 1207 teoria aritmetiche come {\tt integer} e {\tt real} sono anche associativi 1208 a sinistra. Questo porta il parser di \HOL{} in linea con la pratica 1209 matematica standard. 1210\item Il binding dell'eguaglianza nell'espressioni {\tt let} � trattata esattamente 1211 nello stesso modo dell'eguaglianze negli altri contesti. Nelle versioni precedenti 1212 di \HOL, l'eguaglianze in questo contesto hanno una precedenza di bindig differente 1213 pi� debole. 1214\item La vecchia sintassi per l'espressioni condizionali � stata 1215 rimossa. Cos� la stringa \holquote{\condexp} ora deve essere 1216 scritta 1217 $\holquote{\texttt{if}\;p\;\texttt{then}\;q\;\texttt{else}\;r}$. 1218\item Alcune categorie lessicali sono sorvegliate pi� strettamente. I letterali 1219 stringa (le stringhe all'interno dei doppi apici) e quelli numerici non possono essere usati 1220 a meno che le teorie rilevanti non siano state caricate. Inoltre questi 1221 letterali non possono essere usati come variabili all'interno di scopi di binding. 1222\end{itemize} 1223 1224 1225\section{Un Semplice Gestore di Dimostrazione Interattivo}\label{sec:goalstack} 1226 1227Il \emph{goal stack} fornisce una semplice interfaccia di dimostrazione interattiva 1228basata sulle tattiche. Quando si vogliono usare le tattiche per decomporre una dimostrazione, sorgono 1229molti stati intermedi; il goalstack si prende cura del necessario mantenimento 1230di queste informazioni. L'implementazione dei goalstack qui riportati � un 1231ridisegno della concezione originale di Larry Paulson. 1232 1233La libreria goalstack � caricata automaticamente quando \HOL{} si avvia. 1234 1235I tipi astratti \ml{goalstack} e \ml{proofs} sono il 1236punto focale delle operazioni di dimostrazione all'indietro. il tipo \ml{proofs} pu� essere 1237considerato come una lista di goalstack indipendenti. La maggior parte delle operazioni agiscono sulla 1238testa della lista dei goalstack; ci sono anche operazioni cos� che il 1239punto focale pu� essere cambiato. 1240 1241\subsection{Avviare un goalstack di dimostrazione} 1242 1243\begin{hol} 1244\begin{verbatim} 1245 g : term quotation -> proofs 1246 set_goal : goal -> proofs 1247\end{verbatim} 1248\end{hol} 1249 1250Si ricordi che il tipo \ml{goal} � un'abbreviazione per 1251\ml{term list * term}. Per partire su un nuovo goal, si da a 1252\ml{set\_goal} un goal. Questa crea un nuovo goalstack e lo rende il 1253punto focale di ulteriori operazioni. 1254 1255Un'abbreviazione per \ml{set\_goal} � la funzione \ml{g}: essa 1256invoca il parser automaticamente, e non permette al goal di 1257avere alcuna assunzione. 1258 1259La chiamata a \ml{set\_goal}, o \ml{g}, aggiunge un nuovo tentativo di dimostrazione a 1260quelli esistenti, \textit{cio�}, al posto di sovrascrivere il tentativo 1261di dimostrazione attuale, il nuovo tentativo � impilato in cima. 1262 1263\subsection{Applicare una tattica a un goal} 1264 1265\begin{hol} 1266\begin{verbatim} 1267 expandf : tactic -> goalstack 1268 expand : tactic -> goalstack 1269 e : tactic -> goalstack 1270\end{verbatim} 1271\end{hol} 1272 1273Come si fa dunque di fatto a fare una dimostrazione goalstack? Nella maggior parte dei casi, 1274l'applicazione delle tattiche al goal attuale � fatto con la funzione 1275\verb+expand+. Nel raro caso in cui si voglia applicare una 1276tattica {\it invalida\/}, allora � usata \verb+expandf+. (Per una 1277spiegazione delle tattiche invalide, si veda il Capitolo 24 di \& Melham.) 1278Per espandere una tattica si pu� anche usare l'abbreviazione \verb+e+. 1279 1280 1281\subsection{Undo} 1282 1283\begin{hol} 1284\begin{verbatim} 1285 b : unit -> goalstack 1286 drop : unit -> proofs 1287 dropn : int -> proofs 1288 backup : unit -> goalstack 1289 restart : unit -> goalstack 1290 set_backup : int -> unit 1291\end{verbatim} 1292\end{hol} 1293 1294Spesso (siamo tentati di dire {\it di solito}!) si prende una strada sbagliata 1295nel fare una dimostrazione, o si fa un errore nell'impostare un goal. Per annullare un passo 1296nel goalstack, sono usate la funzione \ml{backup} e la sua abbreviazione 1297\ml{b}. Questo ripristiner� il goalstack al suo stato 1298precedente. 1299 1300 1301Per eseguire il backup completo al goal originale, pu� essere usata 1302la funzione \ml{restart}. Ovviamente, � anche importante liberarsi 1303dei tentativi di dimostrazione che sono sbagliati; per questo c'� \ml{drop}, 1304che si sbarazza del tentativo di dimostrazione corrente, e \ml{dropn}, che 1305elimina i primi $n$ tentativi di dimostrazione. 1306 1307 1308Ogni tentativo di dimostrazione ha la sua \emph{lista-di-annullamento} degli stati 1309precedenti. La lista di annullamento per ciascun tentativo � di dimensione fissata (inzialmente 131012). Se si vuole impostare questo valore per il tentativo corrente di dimostrazione, si pu� 1311usare la funzione \ml{set\_backup}. Se la dimensione della lista di 1312backup � impostata essere pi� piccola di quanto sia attualmente, la lista di annullamente sar� 1313immediatamente troncata. Non si pu� annullare un'operazione ``proofs-level'', come 1314\ml{set\_goal} o \ml{drop}. 1315 1316\subsection{Visualizzare lo stato del proof manager} 1317 1318\begin{hol} 1319\begin{verbatim} 1320 p : unit -> goalstack 1321 status : unit -> proofs 1322 top_goal : unit -> goal 1323 top_goals : unit -> goal list 1324 initial_goal : unit -> goal 1325 top_thm : unit -> thm 1326\end{verbatim} 1327\end{hol} 1328 1329Per visualizzare lo stato del proof manager in qualsiasi momento, si possono 1330usare le funzioni \ml{p} e \ml{status}. La prima mostra solo 1331i subgoal in cima al goalstack corrente, mentre la seconda da una 1332sintesi di ogni tentativo di dimostrazione. 1333 1334To get the top goal or goals of a proof attempt, use \ml{top\_goal} 1335and \ml{top\_goals}. To get the original goal of a proof attempt, 1336use \ml{initial\_goal}. 1337 1338Per ottenere il o i top goal di un tentativo di dimostrazione, si usi \ml{top\_goal} 1339e \ml{top\_goals}. Per ottenere il goal originale di un tentativo di dimostrazione, 1340si usi \ml{initial\_goal}. 1341 1342Una volta che un teorema � stato dimostrato il goalstack che � stato usato per derivarlo 1343continua ad esistere (e anche la sua lista-di-annullamento): il suo compito principale ora � quello di 1344mantenere il teorema. Questo teorema pu� essere estratto con 1345\ml{top\_thm}. 1346 1347\subsection{Spostare il fuoco su un differente subgoal o tentativo di dimostrazione} 1348 1349\begin{hol} 1350\begin{verbatim} 1351 r : int -> goalstack 1352 R : int -> proofs 1353 rotate : int -> goalstack 1354 rotate_proofs : int -> proofs 1355\end{verbatim} 1356\end{hol} 1357 1358Spesso vogliamo spostare la nostra attenzione a un differente goal nella dimostrazione 1359attuale, o a una dimostrazione differente. Le funzioni che fanno questo sono 1360\ml{rotate} e \ml{rotate\_proofs}, rispettivamente. Le abbreviazioni 1361\ml{r} e \ml{R} sono pi� semplici da digitare. 1362 1363\section{Dimostrazione di Alto Livello---\texttt{bossLib}} 1364% would use \ml{boss} above but it puts LaTeX into fits 1365\label{sec:bossLib} 1366\newcommand\bossLib{\ml{bossLib}} 1367 1368\index{bossLib@\ml{bossLib}} 1369La libreria \bossLib\ introduce alcuni degli strumenti di dimostrazione di teoremi 1370pi� ampiamente utilizzati in \HOL{} e li fornisce di un'interfaccia conveniente 1371per l'interazione. La libreria attualmente si concentra su tre cose: 1372definizione di datatype e funzioni; operazioni interattive di dimostrazione 1373di alto livello, e composizione di ragionatori automatici. Il caricamento di \bossLib\ 1374impegna a lavorare in un contesto che fornisce gi� le teorie 1375dei booleani, le coppie, le somme, il tipo option, l'aritmetica, e le liste. 1376 1377 1378\subsection{Supporto per passi di dimostrazione di alto livello} 1379\label{sec:high-level-proof-steps} 1380 1381Le seguenti funzioni usano informazione nel database per facilitare 1382l'applicazione delle funzionalit� di \HOL{} sottostanti. 1383 1384\index{Induct_on (tattica ML d'induzione)@\ml{Induct\_on} (tattica \ML{} d'induzione)} 1385\index{Cases_on (tattica ML di case-split)@\ml{Cases\_on} (tattica \ML{} di case-split)} 1386\begin{verbatim} 1387 type_rws : hol_type -> thm list 1388 Induct : tactic 1389 Cases : tactic 1390 Cases_on : term quotation -> tactic 1391 Induct_on : term quotation -> tactic 1392\end{verbatim} 1393 1394\index{type_rws@\ml{type\_rws}} 1395\index{TypeBase@\ml{TypeBase}} 1396% 1397La funzione \ml{type\_rws} cercher� per il tipo dato nel 1398database sottostante \ml{TypeBase} e restituir� utili regole di riscrittura per 1399quel tipo. Le regole di riscrittura del datatype sono costruite a partire dai 1400teoremi di iniettivit� e distinzione, insieme con la definizione di costante 1401case. Le tattiche di semplificazione \ml{RW\_TAC}, \ml{SRW\_TAC}, 1402e il \simpset{} \ml{(srw\_ss())} includono automaticamente questi 1403teoremi. Altre tattiche usate con altri \simpset{} avranno bisogno di questi 1404teoremi per essere aggiunte manualmente. 1405 1406\index{teoremi d'induzione, nella logica HOL@teoremi d'induzione, nella logica \HOL{}!per tipi di dato algebrici} 1407% 1408La tattica \ml{Induct} rende conveniente invocare l'induzione. Quando 1409� applicata a un goal, � esaminato il quantificatore universale principale; 1410se il suo tipo � quello di un datatype conosciuto, � estratta e applicata 1411l'appropriata tattica d'induzione strutturale. 1412 1413The \ml{Cases} tactic makes it convenient to invoke case 1414analysis. The leading universal quantifier in the goal is examined; if 1415its type is that of a known datatype, the appropriate structural 1416case analysis theorem is extracted and applied. 1417 1418La tattica \ml{Cases\_on} prende una quotation, che � 1419parsata a un termine $M$, e poi in $M$ viene effettuata una ricerca per il goal. Se $M$ 1420� una variabile, allora si cerca per una variabile con lo stesso nome. Una volta 1421che si conosce il termine su cui effettuare lo split, il suo tipo e i fatti associati sono 1422ottenuti dal database sottostante e usati per eseguire il case 1423split. Se alcune delle variabili libere di $M$ sono legate nel goal, � fatto un tentativo 1424per rimuovere i quantificatori (universali) cos� che il case split abbia 1425vigore. Infine, $M$ non ha bisogno di apparire nel goal, bench� dovrebbe almeno 1426contenere alcune delle variabili libere che compaiono gi� nel goal. Si noti 1427che la tattica \ml{Cases\_on} � pi� generale di \ml{Cases}, ma 1428richiede che gli sia dato un termine esplicito. 1429 1430\index{Induct_on (tattica ML d'induzione)@\ml{Induct\_on} (tattica \ML{} d'induzione)} 1431La tattica \ml{Induct\_on} prende una quotation, che � parsata in un 1432termine $M$, e poi si cerca in $M$ il goal. Se $M$ � una 1433variabile, allora si cerca per una variabile con lo stesso nome. Una volta che il 1434termine su cui effettuare l'induzione � conosciuto, il suo tipo e i fatti associati sono 1435ottenuti dal database sottostante e usati per eseguire 1436l'induzione. Se $M$ non � una variabile, � creato una nuova variabile $v$ 1437che non occorre gi� nel goal, ed � usata per costruire un termine $v = M$ 1438a cui viene subordinato il goal prima che sia eseguita 1439l'induzione. Prima tuttavia, tutti i termini che contengono variabili libere da $M$ 1440sono spostate dalle assunzioni alla conclusione del goal, e tutte 1441le variabili libere dei $M$ sono quantificate universalmente. \ml{Induct\_on} � 1442pi� generale di \ml{Induct}, ma richiede che le venga dato un termine 1443esplicito. 1444 1445Sono stati forniti tre entry-point supplementari per induzioni pi� 1446esotiche: 1447\begin{description} 1448\item [\ml{completeInduct\_on}] esegue un'induzione completa sul 1449 termine denotato dalla quotazione data. L'induzione completa permette 1450 un'ipotesi d'induzione apparentemente\footnote{L'induzione completa e l'induzione 1451 matematica ordinaria sono entrambe derivabili l'una dall'altra.} pi� forte 1452 rispetto all'induzione matematica ordinaria: vale a dire, quando 1453 si esegue l'induzione su $n$, � permesso assumere che la propriet� valga per 1454 \emph{tutti} gli $m$ pi� piccoli di $n$. Formalmente: $\forall P.\ (\forall x.\ 1455 (\forall y.\ y < x \supset P\, y) \supset P\,x) \supset \forall x.\ 1456 P\,x$. Questo permette di usare l'ipotesi d'induzione pi� di 1457 una volta, e permette anche d'istanziare l'ipotesi d'induzione 1458 in modo diverso dal predecessore. 1459 1460\item [\ml{measureInduct\_on}] prende una quotation, e la suddivide 1461 per trovare un termine e una funzione misura con cui indurre. 1462 Per esempio, se si volesse fare un'induzione sulla lunghezza di una lista 1463 \holtxt{L}, l'invocazione \ml{measureInduct\_on~`LENGTH L`} 1464 sarebbe appropriata. 1465 1466\item [\ml{recInduct}] prende un teorema d'induzione generato da 1467 \ml{Define} o \ml{Hol\_defn} e lo applica al goal attuale. 1468 1469\end{description} 1470 1471 1472\subsection{Ragionatori Automatici} 1473\label{sec:automated-reasoners} 1474 1475\ml{bossLib} riunisce i pi� potenti ragionatori in \HOL{} e 1476prova a rendere facile comporli in un modo semplice. Prendiamo i nostri ragionatori 1477base da \ml{mesonLib}, \ml{simpLib}, e \ml{numLib}, 1478ma il punto di \ml{bossLib} � di fornire un livello di astrazione cos� 1479che l'utente debba sapere solo pochi entry-point\footnote{Nella met� degli anni 1980 1480 Graham Birtwistle ha sostenuto un tale approccio, chiamandolo `HOL in Dieci 1481 Tattiche}. (Quest librerie sottostanti, e altre che forniscono strumenti analogamente 1482potenti sono descritte nel dettaglio nelle sezioni di sotto.) 1483\begin{hol} 1484\begin{verbatim} 1485 PROVE : thm list -> term -> thm 1486 PROVE_TAC : thm list -> tactic 1487 1488 METIS_TAC : thm list -> tactic 1489 METIS_PROVE: thm list -> term -> thm 1490 1491 DECIDE : term quotation -> thm 1492 DECIDE_TAC : tactic 1493\end{verbatim} 1494\end{hol} 1495La regola d'inferenza \texttt{PROVE} (e la tattica corrispondente 1496\texttt{PROVE\_TAC}) prende una lista di teoremi e un termine, e tenta 1497di dimostrare il termine usando un ragionatore al primo ordine. Le due funzioni 1498\ml{METIS} eseguono la stessa funzionalit� ma usano un metodo di dimostrazione 1499sottostante differente. Gli entry-point \texttt{PROVE} si riferiscono alla 1500libreria \texttt{meson}, che � ulteriormente descritta nella 1501Sezione~\ref{sec:mesonLib} di sotto. Il sistema \ml{METIS} � descritto 1502nella Sezione~\ref{sec:metisLib}. La regola d'inferenza \texttt{DECIDE} 1503(e la tattica corrispondente \texttt{DECIDE\_TAC}) applica una procedura 1504di decisione che (al meno) gestisce enunciati dell'aritmetica lineare. 1505 1506\begin{hol} 1507\begin{verbatim} 1508 RW_TAC : simpset -> thm list -> tactic 1509 SRW_TAC : ssfrag list -> thm list -> tactic 1510 && : simpset * thm list -> simpset (* infix *) 1511 std_ss : simpset 1512 arith_ss : simpset 1513 list_ss : simpset 1514 srw_ss : unit -> simpset 1515\end{verbatim} 1516\end{hol} 1517% 1518\index{RW_TAC@\ml{RW\_TAC}} La tattica di riscrittura \ml{RW\_TAC} lavora 1519prima aggiungendo i teoremi dati nel \simpset dato; poi 1520semplifica il goal quanto pi� possibile; quindi esegue dei case split 1521sull'espressioni condizionali nel goal; poi ripetutamente (1) 1522elimina tutte le ipotesi della forma $v = M$ o $M = v$ dove $v$ � 1523una variabile che non occorre in $M$, (2) rompe qualsiasi equazione tra 1524termini costruttore ovunque nel goal. Infine, 1525\ml{RW\_TAC} solleva le espressioni-\holtxt{let} all'interno del goal cos� che 1526l'equazioni binding appaiono come 1527abbreviazioni\index{abbreviazioni!dimostrazione basata-su-tattche} nelle 1528assunzioni. 1529 1530\index{SRW_TAC@\ml{SRW\_TAC}} La tattica \ml{SRW\_TAC} � analoga a 1531\ml{RW\_TAC}, ma lavora rispetto a un \simpset{} sottostante 1532(accessibile attraverso la funzione \ml{srw\_ss}) che viene aggiornato ogni volta che viene caricato 1533un nuovo contesto. Questo \simpset{} pu� essere aumentato attraverso 1534l'aggiornamento di ``frammenti \simpset{} '' (valori \ml{ssfrag}) e 1535teoremi. Nelle situazioni in cui ci sono grandi tipi archiviati nel 1536sistema, le performance di \ml{RW\_TAC} ne possono risentire perch� 1537aggiunge ripetutamente tutti i teoremi di riscrittura per i tipi conosciuti in un 1538\simpset{} prima di attaccare il goal. Dall'altro lato, 1539\ml{SRW\_TAC} carica le riscritture nel \simpset{} al di sotto di 1540\ml{srw\_ss()} una volta sola, rendendo l'operazione pi� veloce in questa 1541situazione. 1542 1543\ml{bossLib} fornisce un numero d'insiemi di semplificazione. Il 1544simpset per la logica pura, le somme, le coppie e il tipo \ml{option} � 1545chiamato \ml{std\_ss}. Il simpset per l'aritmetica � chiamato 1546\ml{arith\_ss}, e il simpset per le liste � chiamato \ml{list\_ss}. 1547I simpset forniti da \bossLib{} aumentano strettamente di forza: 1548\ml{std\_ss} � contenuto in \ml{arith\_ss}, e \ml{arith\_ss} � 1549contenuto in \ml{list\_ss}. Il combinatore infisso \ml{\&\&} � usato 1550per costruire un nuovo \simpset{} da un \simpset{} e una lista di 1551teoremi dati. La tecnologia di semplificazione di \HOL{} � ulteriormente descritta nella 1552Sezione~\ref{sec:simpLib} di sotto e nelle \REFERENCE. 1553 1554\begin{hol} 1555\begin{verbatim} 1556 by : term quotation * tactic -> tactic (* infix 8 *) 1557 SPOSE_NOT_THEN : (thm -> tactic) -> tactic 1558\end{verbatim} 1559\end{hol} 1560La funzione \ml{by} � un operatore infisso che prende una quotation 1561e una tattica $tac$. La quotation � parsata in un termine $M$. Quando 1562l'invocazione ``\ml{$M$ by $\mathit{tac}$}'' � applicata a un goal 1563$(A,g)$, � creato un nuovo subgoal $(A,M)$ e ad esso � applicata la tattica $tac$. 1564Se il goal � dimostrato, il teorema risultante � de-costruito e aggiunto 1565alle assunzioni del goal originale; cos� la dimostrazione procede con 1566il goal $((M::A), g)$. (Si noti tuttavia, che avverr� uno split dei casi 1567se la de-costruzione di $\ \vdash M$ espone delle disgiunzioni.) Cos� 1568\ml{by} permette di mischiare un utile stile di ragionamento `asserzionale' o `Mizar-like' 1569all'ordinaria dimostrazione basata sulle tattiche\footnote{Le dimostrazioni nel 1570 sistema Mizar sono documenti leggibili, diversamente dalla maggior parte 1571 delle dimostrazioni basate su tattiche.} 1572 1573L'entry-point \ml{SPOSE\_NOT\_THEN} inizia una dimostrazione per 1574contraddizione assumendo la negazione del goal e spostando la 1575negazione all'interno dei quantificatori. Essa fornisce il teorema 1576risultante come un argomento della funzione fornite, che user� il 1577teorema per costruire e applicare una tattica. 1578 1579\section{Dimostrazione al Primo Ordine---\texttt{mesonLib} e \texttt{metisLib}} 1580\label{sec:first-order-proof} 1581\index{procedure di decisione!logica del primo ordine} 1582 1583La dimostrazione del primo ordine � una potente tecnica di dimostrazione di teoremi che pu� 1584sbrigare goal complicati. Diversamente da strumenti come il semplificatore, o 1585dimostra un goal completamente, o fallisce. Non pu� trasformare un goal 1586in una forma differente (e pi� utile). 1587 1588\subsection{Model elimination---\texttt{mesonLib}} 1589\label{sec:mesonLib} 1590 1591\index{meson (model elimination) procedura@\ml{meson} (model elimination) procedura} 1592\index{metodo model elimination per la logica del primo ordine} 1593 1594La libreria \ml{meson} � un'implementazione del 1595metodo model-elimination per trovare dimostrazioni di goal nella logica 1596del primo ordine. Ci sono tre entry-point principali: 1597\begin{hol} 1598\begin{verbatim} 1599 MESON_TAC : thm list -> tactic 1600 ASM_MESON_TAC : thm list -> tactic 1601 GEN_MESON_TAC : int -> int -> int -> thm list -> tactic 1602\end{verbatim} 1603\end{hol} 1604 1605Ciascuna di quest tattiche tenta di dimostrare il goal. Esse o avranno 1606successo nel fare questo, o falliranno con un eccezione ``depth exceeded''. Se 1607il fattore di ramificazione nello spazio di ricerca � alto, le tattiche 1608\texttt{meson} possono richiedere anche molto tempo per raggiungere la profondit� massima. 1609 1610Tutte le tattiche \texttt{meson} prendono una lista di teoremi. Questi 1611fatti extra sono usati dalla procedura di decisione per aiutare a dimostrare il goal. 1612\texttt{MESON\_TAC} ignora le assunzioni del goal; gli altri due 1613entry-point includono le assunzioni come pare del sequente da 1614dimostrare. 1615 1616I parametri extra a \ml{GEN\_MESON\_TAC} forniscono un controllo extra del 1617comportamento dell'aumentare iterativo della profondit� che � al centro della 1618ricerca per una dimostrazione. In ogni iterazione data, l'algoritmo ricerca 1619per una dimostrazione di profondit� non pi� alta di un parametro $d$. Il 1620comportamento di default per \ml{MESON\_TAC} e \ml{ASM\_MESON\_TAC} � di iniziare $d$ 1621a 0, incrementarlo di uno ogni volta che una ricerca fallisce, e di fallire se 1622$d$ eccede il valore archiviato nel valore della reference 1623\ml{mesonLib.max\_depth}. Per contro, 1624\ml{GEN\_MESON\_TAC~min~max~step} inizia $d$ a \ml{min}, lo incrementa 1625di \ml{step}, e rinuncia quando $d$ eccede \ml{max}. 1626 1627La funzione \ml{PROVE\_TAC} da \ml{bossLib} esegue qualche 1628normalizzazione, prima di passare un goal e le sue assunzioni a 1629\ml{ASM\_MESON\_TAC}. A causa di questa normalizzazione, nella maggior parte 1630delle circostanze, si dovrebbe preferire \ml{PROVE\_TAC} 1631a \ml{ASM\_MESON\_TAC}. 1632 1633\subsection{Risoluzione---\texttt{metisLib}} 1634\label{sec:metisLib} 1635 1636\index{procedura metis (risoluzione)@procedura \ml{metis} (risoluzione)} 1637\index{metodo di risoluzione per la logica del primo ordine} 1638 1639La libreria \ml{metis} � un'implementazione del metodo di risoluzione 1640per trovare dimostrazioni di goal nella logica del primo ordine. Ci sono due 1641entry-point principali: 1642 1643\begin{hol} 1644\begin{verbatim} 1645 METIS_TAC : thm list -> tactic 1646 METIS_PROVE : thm list -> term -> thm 1647\end{verbatim} 1648\end{hol} 1649 1650Entrambe le funzioni prendono una lista di teoremi, e questi sono usati come lemmi 1651nella dimostrazione. \texttt{METIS\_TAC} � una tattica, e o avr� successo 1652nel dimostrare il goal, o se non ha successo o fallir� o continuer� a ciclare 1653all'infinito. \texttt{METIS\_PROVE} prende un termine $t$ e prova a dimostrare un 1654teorema con conclusione $t$: se ha successo, � restituito il teorema 1655$\vdash t$. Come per \texttt{METIS\_TAC}, potrebbe fallire o ciclare all'infinito se 1656la ricerca della dimostrazione non ha successo. 1657 1658La famiglia \texttt{metisLib} di strumenti di dimostrazione implementano la risoluzione 1659ordinata e il calcolo di paramodulazione ordinata per la logica del primo ordine, 1660che di solito li rende pi� adatti a goal che richiedono ragionamenti di eguaglianza 1661non banali rispetto alle tattiche in \texttt{mesonLib}. 1662 1663 1664\section{Semplificazione---\texttt{simpLib}} 1665\label{sec:simpLib} 1666\index{semplificazione|(} 1667 1668Il semplificatore � il motore di riscrittura pi� sofisticato in \HOL{}. E' 1669raccomandato come un cavallo di battaglia di scopo generale durante la dimostrazione di teoremi 1670interattiva. Come strumenti di riscrittura, il ruolo generale del semplificatore 1671� di applicare teoremi della forma generale 1672\[ 1673\vdash l = r 1674\] 1675a termini, rimpiazzando le istanze di $l$ nel termine con $r$. Cos�, la 1676ruotine base di semplificazione � una \emph{conversione}, che prende un termine 1677$t$, e restituisce un teorema $\vdash t = t'$, o l'eccezione 1678\ml{UNCHANGED}. 1679 1680La conversione di base � 1681\begin{hol} 1682\begin{verbatim} 1683 simpLib.SIMP_CONV : simpLib.simpset -> thm list -> term -> thm 1684\end{verbatim} 1685\end{hol} 1686Il primo argomento, un \simpset, � il modo standard di fornire una 1687collezione di regole di (e altri dati, che saranno spiegati di sotto) al 1688semplificatore. Ci sono dei \simpset{} che accompagnano le teorie principali 1689di \HOL{}. Per esempio, il \simpset{} \ml{bool\_ss} 1690in \ml{boolSimps} incorpora tutti i teoremi di riscrittura usuali desiderabili su formule 1691booleane: 1692\setcounter{sessioncount}{0} 1693\begin{session} 1694\begin{verbatim} 1695- SIMP_CONV bool_ss [] ``p /\ T \/ ~(q /\ r)``; 1696> val it = |- p /\ T \/ ~(q /\ r) = p \/ ~q \/ ~r : thm 1697\end{verbatim} 1698\end{session} 1699Oltre alla riscrittura con i teoremi ovvi, \ml{bool\_ss} � 1700anche capace di eseguire semplificazioni che non sono esprimibili come 1701teoremi semplici: 1702\begin{session} 1703\begin{verbatim} 1704- SIMP_CONV bool_ss [] ``?x. (\y. P (f y)) x /\ (x = z)``; 1705> val it = |- (?x. (\y. P (f y)) x /\ (x = z)) = P (f z) : thm 1706\end{verbatim} 1707\end{session} 1708In questo esempio, il semplificatore ha eseguito una $\beta$-riduzione nel 1709primo congiunto sotto il quantificatore esistenziale, e poi ha fatto una 1710riduzione ``unwinding'' o ``one-point'', riconoscendo che l'unico 1711valore possibile per la variabile quantificata \holtxt{x} era il valore 1712\holtxt{z}. 1713 1714Il secondo argomento a \ml{SIMP\_CONV} � una lista di teoremi da 1715aggiungere al \simpset fornito, e da aggiungere come regole di riscrittura addizionali. 1716In questo modo, gli utenti possono aumentare temporaneamente i \simpset{} con 1717le loro proprie riscritture. Se un particolare insieme di teoremi � usato spesso come 1718un tale argomento, allora � possibile costruire un valore \simpset{} per 1719incorporare queste nuove riscritture. 1720 1721Per esempio, la riscrittura \ml{arithmeticTheory.LEFT\_ADD\_DISTRIB}, che 1722afferma che $p(m + n) = pm + pn$, non fa parte di alcun \simpset{} standard 1723di \HOL{}. Questo perch� pu� causare un aumento poco attraente nella 1724dimensione del termine (ci sono due occorrenze di $p$ al lato destro 1725del teorema). Ci� nonostante, � chiaro che questo teorema pu� pu� 1726essere appropriato occasionalmente: 1727\begin{session} 1728\begin{verbatim} 1729- SIMP_CONV bossLib.arith_ss [LEFT_ADD_DISTRIB] ``p * (n + 1)``; 1730> val it = |- p * (n + 1) = p + n * p : thm 1731\end{verbatim} 1732\end{session} 1733Si noti come il \simpset{} \ml{arith\_ss} non ha solamente semplificato il 1734termine intermedio \ml{(p * 1)}, ma ha anche riordinato l'addizione per 1735mettere il termine pi� semplice sulla sinistra, e ordinato gli argomenti 1736della moltiplicazione. 1737 1738 1739\subsection{Tattiche di semplificazione} 1740\label{sec:simplification-tactics} 1741\index{semplificazione!tattiche} 1742 1743Il semplificatore � implementato intorno alla conversione \ml{SIMP\_CONV}, 1744che � una funzione per `convertire' i termini in teoremi. Per applicare 1745il semplificatore ai goal (alternativamente, per eseguire dimostrazioni basate su tattiche 1746con il semplificatore), \HOL{} fornisce cinque tattiche, ognuna delle quali � 1747disponibile in \ml{bossLib}. 1748 1749\subsubsection{\ml{SIMP\_TAC : simpset -> thm list -> tactic}} 1750\index{SIMP_TAC@\ml{SIMP\_TAC}} 1751 1752\ml{SIMP\_TAC} � la tattica di semplificazione pi� semplice: essa tenta di 1753semplificare il goal attuale (ignorando le assunzioni) usando il \simpset{} 1754dato e i teoremi aggiuntivi. Non � niente di pi� che il 1755sollevamento della sottostante conversione \ml{SIMP\_CONV} al livello 1756di tattica attraverso l'uso della funzione standard \ml{CONV\_TAC}. 1757 1758\subsubsection{\ml{ASM\_SIMP\_TAC : simpset -> thm list -> tactic}} 1759\index{ASM_SIMP_TAC@\ml{ASM\_SIMP\_TAC}} 1760 1761Come \ml{SIMP\_TAC}, \ml{ASM\_SIMP\_TAC} semplifica il goal attuale 1762(lasciando le assunzioni intatte), ma include le assunzioni 1763del goal come regole di riscrittura extra. Cos�: 1764\begin{session} 1765\begin{verbatim} 17661 subgoal: 1767> val it = 1768 P x 1769 ------------------------------------ 1770 x = 3 1771 : goalstack 1772 1773- e (ASM_SIMP_TAC bool_ss []); 1774OK.. 17751 subgoal: 1776> val it = 1777 P 3 1778 ------------------------------------ 1779 x = 3 1780 : goalstack 1781\end{verbatim} 1782\end{session} 1783\noindent 1784In questo esempio, \ml{ASM\_SIMP\_TAC} ha usato \holtxt{x = 3} come una 1785regola di riscrittura addizionale, e ha sostituito la \holtxt{x} di \holtxt{P x} 1786con \holtxt{3}. Quando un'assunzione � usata da \ml{ASM\_SIMP\_TAC} essa 1787� convertita in regole di riscrittura nello stesso modo dei teoremi passati nella 1788lista data come secondo argomento della tattica. Per esempio, 1789un'assunzione \holtxt{\~{}P} sar� trattata come la riscrittura \holtxt{|- P = F}. 1790 1791\subsubsection{\ml{FULL\_SIMP\_TAC : simpset -> thm list -> tactic}} 1792\index{FULL_SIMP_TAC@\ml{FULL\_SIMP\_TAC}} 1793 1794\noindent 1795La tattica \ml{FULL\_SIMP\_TAC} semplifica non solo la conclusione di 1796un goal ma anche le sue assunzioni. Essa procede semplificando 1797ciascuna assunzione una alla volta, usando inoltre le assunzioni precedenti nella 1798semplificazione delle assunzioni successive. Dopo essere stata semplificata, ciascuna 1799assunzione � ri-aggiunta alla lista di assunzioni del goal con la 1800tattica \ml{STRIP\_ASSUME\_TAC}. Questo significa che le assunzioni che 1801diventano congiunzioni avranno ciascuno dei congiunti assunti separatamente. 1802Le assunzioni che diventano disgiunzioni faranno s� che un nuovo sotto goal sia 1803creato per ciascun disgiunto. Se un'assunzione � semplificata a falso, 1804questo risolver� il goal. 1805 1806\ml{FULL\_SIMP\_TAC} attacca le assunzioni nell'ordine in cui 1807appaiono nella lista dei termini che rappresentano le assunzioni 1808del goal. Tipicamente quindi, la prima assunzione da semplificare 1809sar� l'assunzione aggiunta pi� di recente. Vista alla luce della 1810stampa dei goal di \ml{goalstackLib}, \ml{FULL\_SIMP\_TAC} si fa 1811strada lungo l'elenco delle assunzioni, dal basso verso l'alto. 1812 1813La seguente sessione dimostra un uso semplice di \ml{FULL\_SIMP\_TAC}: 1814\begin{session} 1815\begin{verbatim} 1816 x + y < z 1817 ------------------------------------ 1818 0. f x < 10 1819 1. x = 4 1820 : goalstack 1821 1822- e (FULL_SIMP_TAC bool_ss []); 1823OK.. 18241 subgoal: 1825> val it = 1826 4 + y < z 1827 ------------------------------------ 1828 0. f 4 < 10 1829 1. x = 4 1830 : goalstack 1831\end{verbatim} 1832\end{session} 1833In questo esempio, l'assunzione \holtxt{x = 4} ha fatto s� che la \holtxt{x} 1834nell'assunzione \holtxt{f x < 10} sia stata rimpiazzata da \holtxt{4}. La 1835\holtxt{x} nel goal � stata sostituita in modo analogo. Se le assunzioni fossero 1836apparse nell'ordine opposto, solo la \holtxt{x} del goal sarebbe 1837cambiata. 1838 1839La prossima sessione dimostra un comportamento ancora pi� interessante. 1840\begin{session} 1841\begin{verbatim} 1842> val it = 1843 f x + 1 < 10 1844 ------------------------------------ 1845 x <= 4 1846 : goalstack 1847 1848- e (FULL_SIMP_TAC bool_ss [arithmeticTheory.LESS_OR_EQ]); 1849OK.. 18502 subgoals: 1851> val it = 1852 f 4 + 1 < 10 1853 ------------------------------------ 1854 x = 4 1855 1856 f x + 1 < 10 1857 ------------------------------------ 1858 x < 4 1859 : goalstack 1860\end{verbatim} 1861\end{session} 1862In questo esempio, il goal � stato riscritto con il teorema che afferma 1863\[ 1864\vdash x \leq y \equiv x < y \lor x = y 1865\] 1866Sostituendo l'assunzione con una disgiunzione che risulta in due sotto goal. 1867Nel secondo di questi, l'assunzione \holtxt{x = 4} ha ulteriormente 1868semplificato il resto del goal. 1869 1870\subsubsection{\ml{RW\_TAC : simpset -> thm list -> tactic}} 1871\index{RW_TAC@\ml{RW\_TAC}} 1872 1873Nonostante il suo tipo sia lo stesso delle tattiche di semplificazioni gi� 1874descritte, \ml{RW\_TAC} � una tattica ``aumentata''. Essa � aumentata in 1875due modi: 1876\begin{itemize} 1877\item Quando si semplifica il goal, il \simpset{} fornito � aumentato 1878 non solo con i teoremi passati esplicitamente nel secondo argomento, 1879 ma anche con tutte le regole di riscrittura dalla \ml{TypeBase}, e 1880 anche con le assunzioni del goal. 1881% 1882 \index{TypeBase@\ml{TypeBase}} 1883\item \ml{RW\_TAC} also does more than just perform simplification. 1884 It also repeatedly ``strips'' the goal. For example, it moves the 1885 antecedents of implications into the assumptions, splits 1886 conjunctions, and case-splits on conditional expressions. This 1887 behaviour can rapidly remove a lot of syntactic complexity from 1888 goals, revealing the kernel of the problem. On the other hand, this 1889 aggressive splitting can also result in a large number of 1890 sub-goals. \ml{RW\_TAC}'s augmented behaviours are intertwined with 1891 phases of simplification in a way that is difficult to describe. 1892\end{itemize} 1893 1894\subsubsection{\ml{SRW\_TAC : ssfrag list -> thm list -> tactic}} 1895\index{SRW_TAC@\ml{SRW\_TAC}} 1896 1897La tattica \ml{SRW\_TAC} ha un tipo differente dalle altre 1898tattiche di semplificazione. Non prende un \simpset{} come un argomento. 1899Piuttosto la sua operazione si fonda sempre sul \simpset{} incorporato 1900\ml{srw\_ss()} (ulteriormente descritto nella Sezione~\ref{sec:srw_ss}). I 1901teoremi forniti come il secondo argomento di \ml{SRW\_TAC} sono trattati nello 1902stesso modo delle altre tattiche di semplificazione. Infine, la 1903lista dei frammenti \simpset{} sono incorporati nel \simpset{} 1904sottostante, permettendo all'utente di fondere capacit� di semplificazione 1905aggiuntive se lo desidera. 1906 1907Per esempio, per includere la procedura di decisione Presburger, si potrebbe 1908scrivere 1909\begin{hol} 1910\begin{verbatim} 1911 SRW_TAC [ARITH_ss][] 1912\end{verbatim} 1913\end{hol} 1914I frammenti \Simpset{} sono descritti di sotto nella 1915Sezione~\ref{sec:simpset-fragments}. 1916 1917La tattica \ml{SRW\_TAC} esegue la stessa combinazione di semplificazione e 1918goal-splitting che fa \ml{RW\_TAC}. Le principali differenze tra le 1919due tattiche risiedono nel fatto che la seconda pu� essere inefficiente quando 1920si lavora con una grande \ml{TypeBase}, e nel fatto che lavorare con 1921\ml{SRW\_TAC} risparmia dal dover costruire esplicitamente 1922dei \simpset{} che includano tutte le riscritture ``appropriate'' del contesto 1923attuale. Il secondo ``vantaggio'' � basato sull'assunzione che 1924\ml{(srw\_ss())} non include mai riscritture inappropriate. La presenza 1925di riscritture non utilizzate non � mai un problema: la presenza di riscritture che 1926fanno la cosa sbagliata pu� essere causa di maggiore irritazione. 1927 1928\subsection{I \simpset{} standard} 1929\label{sec:standard-simpsets} 1930 1931\HOL{} � fornito con un numero di \simpset{} standard. Ognuno di questi � 1932accessibile dall'interno di \ml{bossLib}, bench� alcuni si originano in altre 1933strutture. 1934 1935\subsubsection{\ml{pure\_ss} and \ml{bool\_ss}} 1936\label{sec:purebool-ss} 1937% 1938\index{pure_ss@\ml{pure\_ss}} 1939% 1940Il \simpset{} \ml{pure\_ss} (definito nella struttura \ml{pureSimps}) 1941non contiene del tutto teoremi di riscrittura, e gioca il ruolo di una tabula 1942rasa all'interno dello spazio dei \simpset{} possibili. Quando si costruisce un 1943\simpset{} completamente nuovo, \ml{pure\_ss} � un punto di partenza possibile. 1944Il \simpset{} \ml{pure\_ss} ha solo due componenti: regole di congruenza 1945per specificare come traversare i termini. e una funzione che trasforma 1946i teoremi in regole di riscrittura. Le regole di congruenza sono ulteriormente descritte 1947nella Sezione~\ref{sec:advanced-simplifier}; la generazione di regole 1948di riscrittura da teoremi � descritta nella 1949Sezione~\ref{sec:simplifier-rewriting}. 1950 1951\index{bool_ss (insieme di semplificazione)@\ml{bool\_ss} (insieme di semplificazione)} 1952% 1953Il \simpset{} \ml{bool\_ss} (definito nella struttura \ml{boolSimps}) � 1954spesso usato quando altri \simpset{} potrebbero essere troppo. Esso contiene 1955regole di riscritture per i connettivi booleani, e poco altro. Esso 1956contiene tutti i teoremi di de~Morgan per spostare le negazioni tra i 1957connettivi (congiunzione, disgiunzione, implicazione e espressioni 1958condizionali), incluse le regole dei quantificatori che hanno $\neg(\forall 1959x.\,P(x))$ e $\neg(\exists x.\,P (x))$ sui loro lati sinistri. Esso 1960contiene anche le regole che specificano il comportamento dei connettivi 1961quando le costanti \holtxt{T} e \holtxt{F} appaiono come loro 1962argomenti. (Una di queste regole � \holtxt{|- T /\bs{} p = p}.) 1963 1964Come nell'esempio di sopra, \ml{bool\_ss} esegue anche 1965delle $\beta$-riduzioni e svolgimenti di un solo punto. Questi ultimi trasformano termini 1966della forma \[ 1967\exists x.\;P(x)\land\dots (x = e) \dots\land Q(x) 1968\] 1969in 1970\[ 1971P(e) \land \dots \land Q(e) 1972\] 1973Analogamente, lo svolgimento trasformer� $\forall x.\;(x = e) 1974\Rightarrow P(x)$ in $P(e)$. 1975 1976Infine, \ml{bool\_ss} include anche regole di congruenza che permettono 1977al semplificatore di fare delle assunzioni aggiuntive quando sono semplificate 1978implicazioni ed espressioni condizionali. Questa caratteristica � spiegata 1979ulteriormente nella Sezione~\ref{sec:simplifier-rewriting} di sotto, ma pu� essere 1980illustrata da qualche esempio (il primo dimostra anche lo svolgimento 1981sotto un quantificatore universale): 1982\begin{session} 1983\begin{verbatim} 1984- SIMP_CONV bool_ss [] ``!x. (x = 3) /\ P x ==> Q x /\ P 3``; 1985> val it = |- (!x. (x = 3) /\ P x ==> Q x /\ P 3) = P 3 ==> Q 3 : thm 1986 1987- SIMP_CONV bool_ss [] ``if ~(x = 3) then P x else Q x``; 1988> val it = |- (if ~(x = 3) then P x else Q x) = 1989 (if ~(x = 3) then P x else Q 3) : thm 1990\end{verbatim} 1991\end{session} 1992 1993\subsubsection{\ml{std\_ss}} 1994% 1995\index{std_ss (insieme di semplificazione)@\ml{std\_ss} (insieme di semplificazione)} 1996% 1997Il \simpset{} \ml{std\_ss} � definito in \ml{bossLib}, e aggiunge 1998regole di riscrittura pertinenti ai tipi di somme, coppie, option e 1999numeri naturali a \ml{bool\_ss}. 2000\begin{session} 2001\begin{verbatim} 2002- SIMP_CONV std_ss [] ``FST (x,y) + OUTR (INR z)``; 2003<<HOL message: inventing new type variable names: 'a, 'b>> 2004> val it = |- FST (x,y) + OUTR (INR z) = x + z : thm 2005 2006- SIMP_CONV std_ss [] ``case SOME x of NONE => P | SOME y => f y``; 2007> val it = |- (case SOME x of NONE => P | SOME v => f v) = f x : thm 2008\end{verbatim} 2009\end{session} 2010 2011Con i numeri naturali, il \simpset{} \ml{std\_ss} pu� calcolare 2012con valori ground, e anche includere una suite di ``riscritture ovvie'' 2013per formule che includono variabili. 2014\begin{session} 2015\begin{verbatim} 2016- SIMP_CONV std_ss [] ``P (0 <= x) /\ Q (y + x - y)``; 2017> val it = |- P (0 <= x) /\ Q (y + x - y) = P T /\ Q x : thm 2018 2019- SIMP_CONV std_ss [] ``23 * 6 + 7 ** 2 - 31 DIV 3``; 2020> val it = |- 23 * 6 + 7 ** 2 - 31 DIV 3 = 177 : thm 2021\end{verbatim} 2022\end{session} 2023 2024\subsubsection{\ml{arith\_ss}} 2025% 2026\index{arith_ss (insieme di semplificazione)@\ml{arith\_ss} (insieme di semplificazione)} 2027% 2028Il \simpset{} \ml{arith\_ss} (definito in \ml{bossLib}) estende 2029\ml{std\_ss} aggiungendo la capacit� di decidere formule dell'aritmetica 2030Presburger, e per normalizzare espressioni aritmetiche (raccogliendo 2031coefficienti , e ri-ordinazione di addendi). La sottostante procedura di decisione 2032per i numeri naturali � quella descritta nella 2033Sezione~\ref{sec:numLib} di sotto. 2034 2035Questi due aspetti del \simpset{} \ml{arith\_ss} sono dimostrati 2036qui: 2037\begin{session} 2038\begin{verbatim} 2039- SIMP_CONV arith_ss [] ``x < 3 /\ P x ==> x < 20 DIV 2``; 2040> val it = |- x < 3 /\ P x ==> x < 20 DIV 2 = T : thm 2041 2042- SIMP_CONV arith_ss [] ``2 * x + y - x + y``; 2043> val it = |- 2 * x + y - x + y = x + 2 * y : thm 2044\end{verbatim} 2045\end{session} 2046Si noti che la sottrazione su numeri naturali funziona in modi che possono 2047sembrare non intuitivi. In particolare, la normalizzazione del coefficiente non pu� 2048occorrere quando atteso prima: 2049\begin{session} 2050\begin{verbatim} 2051- SIMP_CONV arith_ss [] ``2 * x + y - z + y``; 2052! Uncaught exception: 2053! UNCHANGED 2054\end{verbatim} 2055\end{session} 2056Sui numeri naturali, l'espressione $2 x + y - z + y$ non � 2057uguale a $2 x + 2 y - z$. In particolare, queste espressioni non sono 2058uguali quando $2x + y < z$. 2059 2060\subsubsection{\ml{list\_ss}} 2061% 2062\index{list_ss (insieme di semplificazione)@\ml{list\_ss} (insieme di semplificazione)} 2063% 2064L'ultimo valore \simpset{} puro in \ml{bossLib}, \ml{list\_ss} aggiunge 2065teoremi di riscrittura circa il tipo delle liste a \ml{arith\_ss}. Queste 2066riscritture includono i fatti ovvi circa i costruttori del tipo lista 2067\holtxt{NIL} e \holtxt{CONS}, come il fatto che \holtxt{CONS} � 2068iniettivo: 2069\begin{hol} 2070\begin{verbatim} 2071 (h1 :: t1 = h2 :: t2) = (h1 = h2) /\ (t1 = t2) 2072\end{verbatim} 2073\end{hol} 2074Opportunamente, \ml{list\_ss} include anche delle riscritture per le funzioni 2075definite per ricorsione primitiva sulle liste. Esempi includono 2076\holtxt{MAP}, \holtxt{FILTER} e \holtxt{LENGTH}. Cos�: 2077\begin{session} 2078\begin{verbatim} 2079- SIMP_CONV list_ss [] ``MAP (\x. x + 1) [1;2;3;4]``; 2080> val it = |- MAP (\x. x + 1) [1; 2; 3; 4] = [2; 3; 4; 5] : thm 2081 2082- SIMP_CONV list_ss [] ``FILTER (\x. x < 4) [1;2;y + 4]``; 2083> val it = |- FILTER (\x. x < 4) [1; 2; y + 4] = [1; 2] : thm 2084 2085- SIMP_CONV list_ss [] ``LENGTH (FILTER ODD [1;2;3;4;5])``; 2086> val it = |- LENGTH (FILTER ODD [1; 2; 3; 4; 5]) = 3 : thm 2087\end{verbatim} 2088\end{session} 2089Questi esempi dimostrano come il semplificatore pu� essere usato come un valutatore 2090simbolico di scopo generale per termini che assomigliano in grande misura a quelli 2091che appaiono in un linguaggio di programmazione funzionale. Si noti che 2092questa funzionalit� � fornita anche da \ml{computeLib} (si veda 2093la Sezione~\ref{sec:computeLib} di sotto); \ml{computeLib} � pi� 2094efficiente, ma meno generale del semplificatore. Per esempio: 2095\begin{session} 2096\begin{verbatim} 2097- EVAL ``FILTER (\x. x < 4) [1;2;y + 4]``; 2098> val it = 2099 |- FILTER (\x. x < 4) [1; 2; y + 4] = 2100 1::2::(if y + 4 < 4 then [y + 4] else []) : thm 2101\end{verbatim} 2102\end{session} 2103 2104\subsubsection{Il \simpset{} ``stateful''---\ml{srw\_ss()}} 2105\label{sec:srw_ss} 2106\index{srw_ss (insieme di semplificazione)@\ml{srw\_ss} (insieme di semplificazione)} 2107 2108L'ultimo \simpset{} esportato da \ml{bossLib} � nascosto dietro una 2109funzione. Il valore \ml{srw\_ss} ha il tipo \ml{unit -> simpset}, cos� 2110che si deve digitare \ml{srw\_ss()} per ottenere un valore \simpset{}. 2111Questo uso di un tipo funzione permette al \simpset{} sottostante di essere 2112archiviato in una reference \ML{}, e permette ad esso di essere aggiornato 2113dinamicamente. In questo modo, la trasparenza referenziale � deliberatamente 2114spezzata. Tutti gli altri \simpset{} si comporteranno sempre in modo identico: 2115\ml{SIMP\_CONV~bool\_ss} � la stessa routine di semplificazione ovunque 2116e ogni volta che � chiamata. 2117 2118Per contro, \ml{srw\_ss} � progettata per essere aggiornata. Quando una teoria � 2119caricata, quando un nuovo tipo � definito. il valore dietro \ml{srw\_ss()} 2120cambia, e il comportamento di \ml{SIMP\_CONV} applicato a 2121\ml{(srw\_ss())} cambia con esso. La filosofia di sviluppo dietro 2122\ml{srw\_ss} � che essa dovrebbe essere sempre una ragionevole prima scelta in 2123tutte le situazioni dove il semplificatore � utilizzato. 2124 2125Questa versatilit� � illustrata nel seguente esempio: 2126\begin{session} 2127\begin{verbatim} 2128- Hol_datatype `tree = Leaf | Node of num => tree => tree`; 2129<<HOL message: Defined type: "tree">> 2130> val it = () : unit 2131 2132- SIMP_CONV (srw_ss()) [] ``Node x Leaf Leaf = Node 3 t1 t2``; 2133<<HOL message: Initialising SRW simpset ... done>> 2134> val it = 2135 |- (Node x Leaf Leaf = Node 3 t1 t2) = 2136 (x = 3) /\ (Leaf = t1) /\ (Leaf = t2) : thm 2137 2138- load "pred_setTheory"; 2139> val it = () : unit 2140 2141- SIMP_CONV (srw_ss()) [] ``x IN { y | y < 6}``; 2142> val it = |- x IN {y | y < 6} = x < 6 : thm 2143\end{verbatim} 2144\end{session} 2145% 2146Gli utenti possono aumentare il \simpset{} stateful da soli con la funzione 2147% 2148\begin{holboxed} 2149\index{export_rewrites@\ml{export\_rewrites}} 2150\begin{verbatim} 2151 BasicProvers.export_rewrites : string list -> unit 2152\end{verbatim} 2153\end{holboxed} 2154Le stringhe passate a \ml{export\_rewrites} sono i nomi di teoremi 2155nell'attuale segmento di teoria (quelli che saranno esportati quando 2156\ml{export\_theory} � chiamata). Non solo questi teoremi sono aggiunti 2157al \simpset{} sottostante nella sessione attuale, ma essi saranno 2158aggiunti nelle sessioni future quando la teoria � ricaricata. 2159\begin{session} 2160\begin{verbatim} 2161- val tsize_def = Define` 2162 (tsize Leaf = 0) /\ 2163 (tsize (Node n t1 t2) = n + tsize t1 + tsize t2) 2164`; 2165Definition has been stored under "tsize_def". 2166> val tsize_def = 2167 |- (tsize Leaf = 0) /\ 2168 !n t1 t2. tsize (Node n t1 t2) = n + tsize t1 + tsize t2 : thm 2169 2170- val _ = BasicProvers.export_rewrites ["tsize_def"]; 2171 2172- SIMP_CONV (srw_ss()) [] ``tsize (Node 4 (Node 6 Leaf Leaf) Leaf)``; 2173> val it = |- tsize (Node 4 (Node 6 Leaf Leaf) Leaf) = 10 : thm 2174\end{verbatim} 2175\end{session} 2176 2177Come regola generale, \ml{(srw\_ss())} include tutte le ``riscritture ovvie'' 2178del suo contesto, cos� come codice per fare calcoli standard 2179(come l'aritmetica esegita nell'esempio di sopra). Non 2180include procedure di decisione che possono esibire performance occasionalmente 2181povere, cos� i frammenti \simpset{} che contengono queste procedure 2182dovrebbero essere aggiunte manualmente a quelle invocazioni di semplificazione che ne 2183hanno bisogno. 2184 2185\subsection{Frammenti \simpset{}} 2186\label{sec:simpset-fragments} 2187\index{semplificazione!frammenti simpset} 2188 2189Il frammento \simpset{} � il blocco base di costruzione usato per 2190costruire valori \simpset{}. C'� una funzione base che 2191esegue questa costruzione: 2192\begin{hol} 2193\begin{verbatim} 2194 op ++ : simpset * ssfrag -> simpset 2195\end{verbatim} 2196\end{hol} 2197dove \ml{++} � un infisso. In generale, � meglio costruire sopra 2198il \simpset{} \ml{pure\_ss} o uno dei sui discendenti al fine di 2199selezionare la funzione ``filtro'' di default per convertire teoremi in 2200regole di riscrittura. (Questo processo di filtro � descritto di sotto nella 2201Sezione~\ref{sec:generating-rewrite-rules}.) 2202 2203Per le teorie principali (o gruppi di esse), una collezione di 2204frammenti \simpset{} rilevanti si trova di solito nel modulo \ml{<thy>Simps}, 2205dove \ml{<thy>} � il nome della teoria. Per esempio, i frammenti 2206\simpset{} per la teoria dei numeri naturali si trovano in 2207\ml{numSimps}, e i frammenti per le liste si trovano in \ml{listSimps}. 2208 2209Alcuni frammenti \simpset{} standard della distribuzione sono descritti 2210nella Tabella~\ref{table:ssfrags}. Questi ed altri frammenti \simpset{} 2211sono descritti in maggior dettaglio nelle \REFERENCE. 2212 2213\begin{table}[htbp] 2214\begin{center} 2215\renewcommand{\arraystretch}{1.2} 2216\begin{tabular}{lp{0.65\textwidth}} 2217\ml{BOOL\_ss} & 2218Riscritture standard per gli operatori booleani 2219(congiunzione, negazione \&c), cos� come una conversione per eseguire 2220$\beta$-riduzioni. (In \ml{boolSimps}.) 2221\\ 2222\ml{CONG\_ss} & Regole di congruenza per l'implicazione e le espressioni 2223condizionali. (In \ml{boolSimps}.) 2224\\ 2225\ml{ARITH\_ss} & 2226La procedura di decisione sui numeri naturali 2227per l'aritmetica universale Presburger. (In \ml{numSimps}.) 2228\\ 2229\ml{PRED\_SET\_AC\_ss} & Normalizzazione-AC per unioni e intersezioni 2230su insiemi. (In \ml{pred\_setSimps}.) 2231\end{tabular} 2232\end{center} 2233\caption{Alcuni dei frammenti \simpset{} standard di \HOL{}} 2234\label{table:ssfrags} 2235\end{table} 2236 2237I frammenti \simpset{} in definitiva sono costruiti con il costruttore 2238\ml{SSFRAG}: 2239\begin{hol} 2240\begin{verbatim} 2241 SSFRAG : { 2242 convs : convdata list, 2243 rewrs : thm list, 2244 ac : (thm * thm) list, 2245 filter : (controlled_thm -> controlled_thm list) option, 2246 dprocs : Traverse.reducer list, 2247 congs : thm list, 2248 name : string option 2249 } -> ssfrag 2250\end{verbatim} 2251\end{hol} 2252Una descrizione completa per i vari campi del record passato a 2253\ml{SSFRAG}, e il loro significato � dato in \REFERENCE. La 2254funzione \ml{rewrites} fornisce una strada semplice per costruire un 2255frammento che include solo una lista di riscritture: 2256\begin{hol} 2257\begin{verbatim} 2258 rewrites : thm list -> ssfrag 2259\end{verbatim} 2260\end{hol} 2261 2262\subsection{Riscrittura con il semplificatore} 2263\label{sec:simplifier-rewriting} 2264 2265La riscrittura � l'``operazione core'' del semplificatore. Questa sezione 2266descrive l'azione di riscrittura in maggior dettaglio. 2267 2268 2269\subsubsection{Riscrittura di base} 2270\label{sec:basic-rewriting} 2271 2272Data una regola di riscrittura della forma \[ 2273\vdash \ell = r 2274\] 2275il semplificatore eseguir� una scansione dall'alto verso il basso del termine di input $t$, 2276cercando per dei \emph{match}~(si veda la Sezione~\ref{sec:simp-homatch} di sotto) 2277di $\ell$ all'interno di $t$. Questo match occorrer� in un sotto termine di $t$ 2278(chiamiamolo $t_0$) e restituir� un'istanziazione. Quando questa 2279istanziazione � applicata alla regola di riscrittura, il risultato sar� una nuova 2280equazione della forma \[ 2281\vdash t_0 = r' 2282\] 2283Poich� il sistema a quel punto ha un teorema che esprime un'equivalenza per 2284$t_0$ pu� creare la nuova equazione \[ 2285 \vdash \underbrace{(\dots t_0\dots)}_t = (\dots r' \dots) 2286\] 2287L'attraversamento del termine da semplificare � ripetuto fino a quando non si trova 2288alcun match ulteriore per le regole di riscrittura del semplificatore. La 2289strategia di attraversamento � 2290\begin{enumerate} 2291\item \label{enum:simp-traverse-toplevel}% 2292 Mentre c'� un qualsiasi match per le regole di riscrittura archiviate a questo livello, 2293 si continui ad applicarle. \emph{Non} si pu� fare affidamento sull'ordine in cui le regole 2294 di riscrittura sono applicate, eccetto quando un \simpset{} 2295 include due riscritture con esattamente gli stessi lati sinistri. la 2296 riscrittura aggiunta per ultima sar� quella preferita per match. (Questo permette una 2297 certa misura di overloading della riscrittura nella costruzione dei 2298 \simpset{}.) 2299%% may not wish to own up to above detail 2300\item \label{enum:simp-traverse-recurse}% 2301 Eseguire una ricorsione sui sotto termini del termine. Il modo in cui i termini sono 2302 attraversati a questo passo pu� essere controllato da \emph{regole di 2303 congruenza}~(una caratteristica avanzata, si veda la Sezione~\ref{sec:simp-congruences} 2304 di sotto) 2305\item Se il passo~\ref{enum:simp-traverse-recurse} ha cambiato il termine 2306 completamente, si provi un'altra fase di riscrittura a questo livello. Se questo fallisce, 2307 o se non c'� stato alcun cambiamento dall'attraversamento dei sotto-termin, si provi 2308 qualsiasi procedura di decisione incorporata (si veda 2309 la Sezione~\ref{sec:simp-embedding-code}). Se la fase di riscrittura o 2310 qualsiasi delle procedure di decisione ha alterato il termine, ri ritorni al 2311 passo~\ref{enum:simp-traverse-toplevel}. Altrimenti di termini. 2312\end{enumerate} 2313 2314\subsubsection{Riscrittura condizionale} 2315\index{semplificazione!riscrittura condizionale} 2316 2317La descrizione di sopra � una leggera semplificazione dello stato reale delle 2318cose. Una caratteristica particolarmente potente del semplificatore � che 2319essa realmente usa regole di riscrittura \emph{condizionali}. Questi sono teoremi 2320della forma 2321\[ 2322\vdash P \Rightarrow (\ell = r) 2323\] 2324Quando il semplificatore trova un match per il termine $\ell$ durante il suo attraversamento 2325del termine, tenta di scaricare la condizione $P$. Se il 2326semplificatore pu� semplificare il termine $P$ a vero, allora l'istanza di 2327$\ell$ nel termine attraversato pu� essereo sostituito dall'appropriata 2328istanziazione di $r$. 2329 2330Quando si semplifica $P$ (un termine che non necessariamente nemmeno occorre 2331nell'originale), il semplificatore si pu� trovare ad applicare un'altra 2332regola di riscrittura condizionale. Per fermare eccessive applicazioni 2333ricorsive, il semplificatore tiene traccia di uno stack di tutte le 2334condizioni collaterali su cui sta lavorando. Il semplificatore smette la dimostrazione 2335su una condizione collaterale se nota una ripetizione in questo stack. 2336C'� anche una variabile accessibile dall'utente, \ml{Cond\_rewr.stack\_limit} 2337che specifica la dimensione massima dello stack che il semplificatore pu� 2338di usare. 2339 2340Le riscritture condizionali possono essere estremamente utili. Per esempio, i teoremi 2341circa la divisione e il modulo sono spesso accompagnate da condizioni 2342che richiedono che il divisore non sia zero. Il semplificatore pu� spesso 2343scaricare queste, in particolare se include una procedura di decisione 2344aritmetica. Per esempio, il teorema \ml{MOD\_MOD} dalla teoria 2345\ml{arithmetic} afferma 2346\[ 2347\vdash 0 < n \;\Rightarrow \; (k\,\textsf{MOD}\,n)\,\textsf{MOD}\,n = k 2348\,\textsf{MOD}\,n 2349\] 2350Il semplificatore (in modo specifico, \ml{SIMP\_CONV~arith\_ss~[MOD\_MOD]}) 2351pu� usare questo teorema per semplificare il termine 2352\holtxt{(k~MOD~(x~+~1))~MOD~(x~+~1)}: la procedura di decisione 2353aritmetica pu� dimostrare che \holtxt{0 < x + 1}, giustificando la riscrittura. 2354 2355Bench� le regole riscrittura condizionali siano potenti, non ogni teorema della 2356forma descritta di sopra � una scelta appropriata. Una riscrittura scelta male 2357pu� causare un considerevole degrado delle performance del semplificatore, dal momento 2358che perde tempo nel tentare di dimostrare condizioni collaterali impossibili. Per 2359esempio, il semplificatore non � molto bravo a trovare testimoni 2360esistenziali. Questo significa che la riscrittura condizionale \[ 2361\vdash x < y \land y < z \Rightarrow (x < z = \top) 2362\] 2363non funzioner� come si potrebbe sperare. In generale, il semplificatore non � un 2364buon strumento per eseguire ragionamenti di transitivit�. (Si provi invece uno strumento 2365al primo ordine come \ml{PROVE\_TAC}) 2366 2367\subsubsection{Generare regole di riscrittura per i teoremi} 2368\label{sec:generating-rewrite-rules} 2369\index{teoremi equazionali, nella logica HOL@teoremi equazionali, nella logica \HOL{}!uso dei ... nel semplificatore} 2370 2371Ci sono due strade per cui un teorema per la riscrittura pu� essere passato al 2372semplificatore: o come un argomento esplicito a una delle funzioni 2373\ML{} (\ml{SIMP\_CONV}, \ml{ASM\_SIMP\_TAC} ecc) che prendono liste di 2374teoremi come argomenti, o includendoli in un frammento \simpset{} 2375che � incorporato in un \simpset. In entrambi i casi, questi teoremi sono 2376trasformati prima di essere usati. Le trasformazioni applicate sono 2377progettate per rendere l'uso interattivo quanto pi� conveniente possibile. 2378 2379In particolare, non � necessario passare al semplificatore teoremi 2380che sono esattamente della forma 2381\[ 2382\vdash P \Rightarrow (\ell = r) 2383\] 2384Piuttosto, il semplificatore trasformer� i suoi teoremi di input per estrarre 2385le riscritture di questa stessa forma. L'esatta trasformazione eseguita � 2386dipendente dal \simpset{} utilizzato: ciascun \simpset{} contiene la sua 2387propriat funzione ``filtro'' che � applicata ai teoremi che sono aggiunti ad 2388esso. La maggior parte dei \simpset{} usano la funzione filtro dal \simpset{} 2389\ml{pure\_ss} (si veda la Sezione~\ref{sec:purebool-ss}). Tuttavia, quando un 2390frammento \simpset{} � aggiunto a un simpset completo, il frammento pu� 2391specificare un componente filtro addizionale. Se specificata, questa funzione 2392� di tipo \ml{controlled\_thm~->~controlled\_thm~list}, ed � applicata 2393ad ognuno dei teoremi prodotti dal filtro del \simpset{} esistente. 2394% 2395\index{semplificazione!garantire la terminazione} 2396(Un teorema ``controllato'' � uno che � accompagnato da un pezzo di 2397dati di ``controllo'' che esprimono il limite (se ne esiste uno) sul numero di volte 2398che pu� essere applicato. Si veda la Sezione~\ref{sec:simp-special-rewrite-forms} 2399per come gli utenti possono introdurre questi limiti. Il tipo di ``controllo'' 2400appare nel modulo \ML{} \ml{BoundedRewrites}.) 2401 2402Il filtro che produce riscritture in \ml{pure\_ss} elimina 2403le congiunzioni, le implicazioni e le quantificazioni universali fino a quando o ha 2404un teorema di eguaglianza, o qualche altra forma booleana. Per esempio, 2405il teorema \ml{ADD\_MODULUS} afferma 2406\[ 2407\vdash 2408\begin{array}[t]{l} 2409(\forall n\;x.\;\;0 < n \Rightarrow ((x + n)\,\textsf{MOD}\,n = 2410 x\,\textsf{MOD}\,n)) \;\;\land\\ 2411(\forall n\;x.\;\;0 < n \Rightarrow ((n + x)\,\textsf{MOD}\,n = 2412 x\,\textsf{MOD}\,n)) 2413\end{array} 2414\] 2415Questo teorema si trasforma in due regole di riscrittura \[ 2416\begin{array}{l} 2417\vdash 0 < n \Rightarrow ((x + n)\,\textsf{MOD}\,n = x\,\textsf{MOD}\,n)\\ 2418\vdash 0 < n \Rightarrow ((n + x)\,\textsf{MOD}\,n = x\,\textsf{MOD}\,n) 2419\end{array} 2420\] 2421 2422Se guardando a un'eguaglianza dove ci sono delle variabili sul 2423lato destro che non occorrono sul lato sinistro, il 2424semplificatore trasforma questo nella regola \[ 2425\vdash (\ell = r) = \top 2426\] 2427Analogamente, se � una negazione booleana $\neg P$, diventa la regola \[ 2428\vdash P = \bot 2429\] 2430e altre formule booleane $P$ diventano \[ 2431\vdash P = \top 2432\] 2433 2434Infine, se guardando a un'eguaglianza il cui lato sinistro � esso stesso 2435un'eguaglianza, e dove il lato destro non � a sua volta un'eguaglianza, 2436il semplificatore trasforma $(x = y) = P$ nelle due regole 2437\[ 2438\begin{array}{l} 2439\vdash (x = y) = P\\ 2440\vdash (y = x) = P 2441\end{array} 2442\] 2443Questo � generalmente utile. Per esempio, un teorema come 2444\[ 2445\vdash \neg(\textsf{SUC}\,n = 0) 2446\] 2447far� s� che il semplificatore riscriva entrambi $(\textsf{SUC}\,n = 0)$ e 2448$(0 = \textsf{SUC}\,n)$ a falso. 2449 2450La restrizione che il lato destro di una tale regola non sia esso stesso 2451un'eguaglianza � una semplifice euristica che previene alcune forme di looping. 2452 2453 2454\subsubsection{Regole di riscrittura di matching} 2455\label{sec:simp-homatch} 2456 2457Dato un teorema di riscrittura $\vdash \ell = r$, il primo passo di 2458esecuzione di una riscrittura � determinare se $\ell$ pu� o meno essere 2459istanziata cos� da renderla uguale al termine che � 2460riscritto. Questo processo � conosciuto come matching. Per esempio, se $\ell$ 2461� il termine $\textsf{SUC}(n)$, allora farne il matching verso il termine 2462$\textsf{SUC}(3)$ avr� successo, e trover� l'istanziazione $n\mapsto 24633$. Contrariamente all'unificazione, il matching non � simmetrico: un 2464pattern $\textsf{SUC}(3)$ non matcher� il termine $\textsf{SUC}(n)$. 2465 2466\index{matching di ordine superiore} \index{matching!di ordine superiore} Il semplificatore 2467usa una speciale forma di matching di ordine superiore. Se un pattern 2468include una variabile di qualche tipo funzione (diciamo $f$), e quella variabile 2469� applicata a un argomento $a$ che non include alcuna variabile eccetto quelle 2470che sono legate da un'atrazione ad uno spopo pi� alto. allora il termine 2471combinato $f(a)$ matcher� qualsiasi termine del tipo appropriato fino a quando le 2472sole occorrenze delle variabili legate in $a$ sono in sotto-termini 2473che matchano $a$. 2474 2475Assumiamo per i seguenti esempi che la variabile $x$ sia legata a uno 2476scopo pi� alto. Allora, se $f(x)$ deve matchare $x + 4$, la variabile $f$ 2477sar� istanziata a $(\lambda x.\; x + 4)$. Se $f(x)$ deve matchare 2478$3 + z$, allora $f$ sar� istanziata a $(\lambda x.\;3 + z)$. 2479Inoltre $f(x + 1)$ matcha $x + 1 < 7$, ma non matcha $x + 2 < 24807$. 2481 2482Un matching di ordine superiore di questo genere rende pi� facile esprimere i risultati 2483dei movimenti dei quantificatori come regole di riscrittura, e avere queste regole applicate dal 2484semplificatore. Per esempio, il teorema 2485\[ 2486\vdash (\exists x. \;P(x)\lor Q(x)) = (\exists x.\;P(x)) \lor (\exists 2487x.\;Q(x)) 2488\] 2489ha due variabili di un tipo funzione ($P$ e $Q$), ed entrambe sono 2490applicate alla variabile legata $x$. Questo significa che quando applicato 2491all'input \[ 2492\exists z. \;z < 4 \lor z + x = 5 * z 2493\] 2494il matcher trover� l'istanziazione \[ 2495\begin{array}{l} 2496P \mapsto (\lambda z.\;z < 4)\\ 2497Q \mapsto (\lambda z.\;z + x = 5 * z) 2498\end{array} 2499\] 2500 2501Eseguendo questa istanziazione, e poi facendo qualche $\beta$-riduzione 2502sulla regola di riscrittura, si produce il teorema \[ 2503\vdash (\exists z. \;z < 4 \lor z + x = 5 * z) = 2504(\exists z. \;z < 4) \lor (\exists z.\;z + x = 5 * z) 2505\] 2506come richiesto. 2507 2508Un altro esempio di una regola che il semplificatore user� con successo � 2509\[ 2510\vdash f \circ (\lambda x.\; g(x)) = (\lambda x.\;f(g(x))) 2511\] 2512La presenza dell'astrazione sul lato sinistro della regola 2513richiede che un'astrazione appaia nel termine da matchare, cos� questa 2514regola pu� essere vista come un'implementazione di un metodo per muovere le astrazioni 2515al di sopra delle composizioni di funzione. 2516 2517Un esempio di un possibile lato sinistro che \emph{non} matchare come 2518in generale si potrebbe desiderare � $(\exists x.\;P(x + y))$. Questo � 2519perch� il predicato $P$ � applicato a un argomento che include la 2520variabile libera $y$. 2521 2522\subsection{Caratteristiche avanzate} 2523\label{sec:advanced-simplifier} 2524 2525Questa sezione descrive alcune delle caratteristiche avanzate del semplificatore. 2526 2527\subsubsection{Regole di congruenza} 2528\label{sec:simp-congruences} 2529\index{semplificazione!regole di congruenza} 2530\index{regole di congruenza!nella semplificazione} 2531Le regole di congruenza controllano il modo in cui il semplificatore traversa un termine. 2532Esse forniscono anche un meccanismo per mezzo del quale possono essere 2533aggiunte al contesto del semplificatore assunzioni aggiuntive, che rappresentano informazione circa il 2534contesto contenitore. Le regole di congruenza pi� semplici sono incorporate nel 2535simpset \ml{pure\_ss}. Esse specificano come traversare termini applicazione e 2536astrazione. A questo livello fondamentale, queste regole di congruenza 2537sono poco di pi� che le regole d'inferenza \ml{ABS} 2538\[ 2539\frac{\Gamma \turn t_1 = t_2} 2540{\Gamma \turn (\lquant{x}t_1) = (\lquant{x}t_2)} 2541\] 2542(dove $x\not\in\Gamma$) e \ml{MK\_COMB} 2543\[ 2544\frac{\Gamma \turn f = g \qquad \qquad \Delta \turn x = y} 2545{\Gamma \cup \Delta \turn f(x) = g(y)} 2546\] 2547Quando si specifica l'azione del semplificatore, queste regole dovrebbero essere 2548lette verso l'alto. Con \ml{ABS}, per esempio, la regola dice ``quando 2549si semplifica un'astrazione, si semplifichi il corpo $t_1$ a qualche nuovo $t_2$, 2550e poi il risultato � formato ri-astraendo con la variabile 2551legata~$x$.'' 2552 2553Ulteriori regole di congruenza dovrebbero essere aggiunte al semplificatore nella forma 2554di teoremi, attraverso il campo \ml{congs} dei record passati al 2555costruttore \ml{SSFRAG}. Tali regole di congruenza dovrebbero essere della forma 2556\[ 2557\mathit{cond_1} \Rightarrow \mathit{cond_2} \Rightarrow \dots (E_1 = 2558E_2) 2559\] 2560dove $E_1$ � la forma da riscrivere. Ciascun $\mathit{cond}_i$ pu� 2561essere o una formula booleana arbitraria (nel qual caso � trattata come 2562una condizione collaterale da scaricare) o un'equazione della forma generale 2563\[ 2564\forall \vec{v}. \;\mathit{ctxt}_1 \Rightarrow \mathit{ctxt}_2 2565\Rightarrow \dots (V_1(\vec{v}) = V_2(\vec{v})) 2566\] 2567dove la variabile $V_2$ deve occorrere libera in $E_2$. 2568 2569Per esempio, la forma teorema di \ml{MK\_COMB} sarebbe 2570\[ 2571\vdash (f = g) \Rightarrow (x = y) \Rightarrow (f(x) = g(y)) 2572\] 2573e la forma teorema di \ml{ABS} sarebbe 2574\[ 2575\vdash (\forall x. \;f (x) = g (x)) \Rightarrow (\lambda x. \;f(x)) = (\lambda 2576x.\;g(x)) 2577\] 2578La forma per \ml{ABS} dimostra come � possibile per le regole 2579di congruenza gestire variabili legate. Dal momento che le regole di congruenza sono 2580matchate con il match di ordine superiore della Sezione~\ref{sec:simp-homatch}, 2581questa regola matcher� tutti i possibili termini astrazione. 2582 2583Questi semplici esempi non hanno ancora dimostrato l'uso delle 2584condizioni $\mathit{ctxt}$ su sotto-equazioni. Un esempio di questo � 2585la regola di congruenza (che si trova in \ml{CONG\_ss}) per le implicazioni. Questa 2586afferma 2587\[ 2588\vdash (P = P') \Rightarrow (P' \Rightarrow (Q = Q')) \Rightarrow 2589(P \Rightarrow Q = P' \Rightarrow Q') 2590\] 2591Questa regola dovrebbe essere letta: ``Quando si semplifica $P\Rightarrow Q$, prima 2592si semplifichi $P$ a $P'$. Poi si assuma $P'$, e si semplifichi $Q$ a $Q'$. 2593Poi il risultato � $P' \Rightarrow Q'$.'' 2594 2595La regola per espressioni condizionali � 2596\[ 2597\vdash \begin{array}[t]{l} 2598 (P = P') \Rightarrow (P' \Rightarrow (x = x')) \Rightarrow 2599 (\neg P' \Rightarrow (y = y')) \;\Rightarrow\\ 2600 (\textsf{if}\;P\;\textsf{then}\;x\;\textsf{else}\;y = 2601 \textsf{if}\;P'\;\textsf{then}\;x'\;\textsf{else}\;y') 2602\end{array} 2603\] 2604Questa regola permette di assumere la guardia quando si semplifica il 2605ramo-vero del condizionale, e di assumere la sua negazione quando si 2606semplifica il ramo-falso. 2607 2608Le assunzioni contestuali da regole di congruenza sono trasformate in 2609riscritture usando il meccanismo descritto nella 2610Sezione~\ref{sec:generating-rewrite-rules}. 2611 2612Le regole di congruenza possono essere usate per ottenere un numero di interessanti 2613effetti. Per esempio, una congruenza pu� specificare che i sotto-termini 2614\emph{non} siano semplificati se lo si desidera. Questo potrebbe essere usato per impedire 2615la semplificazione dei rami delle espressioni condizionali: 2616\[ 2617\vdash (P = P') \Rightarrow 2618 (\textsf{if}\;P\;\textsf{then}\;x\;\textsf{else}\;y = 2619 \textsf{if}\;P'\;\textsf{then}\;x\;\textsf{else}\;y) 2620\] 2621Se aggiunta al semplificatore, questa regola prender� la precedenza su qualsiasi 2622altra regola per le espressioni condizionali (mascherando quella sopra 2623\ml{CONG\_ss}, diciamo) e far� s� che il semplificatore di scendere solo 2624nella guardia. Con le riscritture standard (da \ml{BOOL\_ss}): 2625\[ 2626\begin{array}{l} 2627\vdash \;\textsf{if}\;\top\;\textsf{then}\;x\;\textsf{else}\;y \,\;=\,\; x\\ 2628\vdash \;\textsf{if}\;\bot\;\textsf{then}\;x\;\textsf{else}\;y \,\;=\,\; y 2629\end{array} 2630\] 2631gli utenti possono scegliere che il semplificatore ignori 2632i rami di un condizionali fino a quando la guarda di quel condizionale � semplificata 2633o a vero o a falso. 2634 2635 2636\subsubsection{Normalizzazione-AC} 2637\index{simplification!AC-normalisation} 2638 2639The simplifier can be used to normalise terms involving associative 2640and commutative constants. This process is known as 2641\emph{AC-normalisation}. The simplifier will perform AC-normalisation 2642for those constants which have their associativity and commutativity 2643theorems provided in a constituent \simpset{} fragment's \ml{ac} 2644field. 2645 2646For example, the following \simpset{} fragment will cause 2647AC-normalisation of disjunctions 2648\begin{hol} 2649\begin{verbatim} 2650 SSFRAG {ac = [(DISJ_ASSOC, DISJ_COMM)], 2651 rewrs = [], filter = NONE, convs = [], 2652 dprocs = [], congs = []} 2653\end{verbatim} 2654\end{hol} 2655The pair of provided theorems must state 2656\begin{eqnarray*} 2657x \oplus y &=& y \oplus x\\ 2658x \oplus (y \oplus z) &=& (x \oplus y) \oplus z 2659\end{eqnarray*} 2660for a constant $\oplus$. The theorems may be universally quantified, 2661and the associativity theorem may be oriented either way. Further, 2662either the associativity theorem or the commutativity theorem may be 2663the first component of the pair. Assuming the \simpset{} fragment 2664above is bound to the \ML{} identifier \ml{DISJ\_ss}, its behaviour is 2665demonstrated in the following example: 2666\begin{session} 2667\begin{verbatim} 2668- SIMP_CONV (bool_ss ++ DISJ_ss) [] ``p /\ q \/ r \/ P z``; 2669<<HOL message: inventing new type variable names: 'a>> 2670> val it = |- p /\ q \/ r \/ P z = r \/ P z \/ p /\ q : thm 2671\end{verbatim} 2672\end{session} 2673 2674\index{arith_ss (insieme di semplificazione)@\ml{arith\_ss} (insieme di semplificazione)} 2675L'ordine degli operandi nella forma normale-AC in cui lavora la normalizzazione-AC 2676del semplificatore non � specificato. Tuttavia, la forma 2677normale � sempre associata a destra. Si noti inoltre che il \simpset{} 2678\ml{arith\_ss}, e il frammento \ml{ARITH\_ss} che ne � la base, ha 2679le sue procedure di normalizzazione su misura per l'addizione sui 2680numeri naturali. Combinare la normalizzazione-AC, come descritta qui, con 2681\ml{arith\_ss} pu� far s� che il semplificatore entri in un loop infinito. 2682 2683I teoremi AC possono essere aggiunti ai \simpset{} anche attraverso la lista di teoremi parte 2684dell'interfaccia della tattica e della conversione, usando la forma speciale di riscrittura 2685\ml{AC}: 2686\begin{session} 2687\begin{verbatim} 2688- SIMP_CONV bool_ss [AC DISJ_ASSOC DISJ_COMM] ``p /\ q \/ r \/ P z``; 2689<<HOL message: inventing new type variable names: 'a>> 2690> val it = |- p /\ q \/ r \/ P z = r \/ P z \/ p /\ q : thm 2691\end{verbatim} 2692\end{session} 2693Si veda la Sezione~\ref{sec:simp-special-rewrite-forms} per maggiori informazioni su speciali 2694forme di riscrittura. 2695 2696\subsubsection{Incorporate codice} 2697\label{sec:simp-embedding-code} 2698 2699Il semplificatore dispone di due modi diversi in cui il codice dell'utente pu� essere 2700incorporato nel suo attraversamento e semplificazione dei termini di input. Incorporando 2701il loro proprio codice gli utenti possono personalizzare il comportamento del 2702semplificatore in una misura significativa. 2703 2704\paragraph{Conversioni utente} 2705Il pi� semplice dei due metodi permente al semplificatore di includere 2706conversioni fornite dall'utente. Queste sono aggiunte ai \simpset{} nel 2707campo {convs} dei frammenti \simpset{}. Questo campo prende liste di 2708valori di tipo 2709\begin{hol} 2710\begin{verbatim} 2711 { name: string, 2712 trace: int, 2713 key: (term list * term) option, 2714 conv: (term list -> term -> thm) -> term list -> term -> thm} 2715\end{verbatim} 2716\end{hol} 2717 2718I campo \ml{name} e \ml{trace} sono usati quando il tracing del semplificatore 2719� acceso. Se la conversione � applicata, e se il livello di traccia del 2720semplificatore � maggiore di o uguale al campo \ml{trace}, allora sar� 2721emesso un messagio circa l'applicazione della conversione 2722(che include il suo \ml{name}). 2723 2724Il campo \ml{key} del record di sopra � usato per specificare i 2725sotto-termini a cui la conversione dovrebbe essere applicata. Se il valore � 2726\ml{NONE}, allora la conversione sar� provata ad ogni posizione. 2727Altrimenti, la conversione � applicata a posizioni di termine che matchano il 2728pattern fornito. Il primo componente del pattern � una lista di 2729variabili che dovrebbero essere trattate come costanti quando si cercano match 2730del pattern. Il secondo componente � il pattern di termine stesso. Il matching 2731verso questa componente \emph{non} � fatto dal match di ordine superiore della 2732Sezione~\ref{sec:simp-homatch}, ma da una ``term-net'' di ordine superiore. 2733Questa forma di matching non cerca di essere precisa; essa � usata per 2734eliminare in modo efficiente match chiaramente impossibili. Non controlla 2735i tipi, e non controlla binding multipli. Questo significa che la 2736conversione non sar� applicata a termini che sono match esatti 2737per il pattern fornito. 2738 2739Infine, la conversione stessa. Molti usi di questa infrastruttura sono per aggiungere 2740normali conversioni \HOL{} (di tipo \ml{term->thm}), e questo pu� essere 2741fatto ignorando i primi due parametri del campo \ml{conv} Per una 2742conversione \ml{myconv}, l'idioma standard � di scrivere 2743\ml{K~(K~myconv)}. Se l'utente lo desidera, tuttavia, il suo codice 2744\emph{pu�} riferirsi ai primi due parametri. Il secondo parametro � 2745lo stack delle condizioni collaterali che sono state tentate fino ad ora. Il 2746primo permette al codice dell'utente di richiamare il semplificatore, passando 2747lo stack delle condizioni collaterali, e una nuova condizione per risolvere. 2748L'argomento \ml{term} deve essere di tipo \holtxt{:bool}, e la chiamata 2749ricorsiva lo semplificher� a vero (e richiamer� \ml{EQT\_ELIM} per trasformare un termine 2750$t$ nel teorema $\vdash t$). Questa restrizione pu� essere sollevata in una 2751futura versione di \HOL{} ma per come stanno le cose ora, la chiamata ricorsiva pu� 2752essere usata \emph{solo} per scaricare la condizione collaterale. Si noti anche che 2753� responsabilit� dell'utente passare uno stack appropriatamente aggiornato di 2754condizioni collaterali all'invocazione ricorsiva del semplificatore. 2755 2756Una conversione fornita dall'utente non dovrebbe mai restituire l'identit� riflessiva 2757(un'istanza di $\vdash t = t$). Questo far� andare in loop il 2758semplificatore. Piuttosto che restituire un tale risultato, si sollevi un \ml{HOL\_ERR} o 2759un'eccezione \ml{Conv.UNCHANGED}. (Entrambe sono trattate allo stesso modo dal semplificatore.) 2760 2761\paragraph{Procedure di decisione consapevoli del contesto} 2762Un altro metodo, pi� complicato, per incorporare codice utente nel 2763semplificatore � \emph{attraverso} il campo \ml{dprocs} della struttura 2764frammento \simpset{}. Questo metodo � pi� generale rispetto ad aggiungere 2765conversioni, e permette anche al codice utente di costruire e mantenere i suoi 2766propri contesti logici costruiti su misura. 2767 2768Il campo \ml{dprocs} richiede liste di valori di tipo 2769\ml{Traverse.reducer}. Questi valori sono costruiti con il 2770costruttore \ml{REDUCER}: 2771\begin{hol} 2772\begin{verbatim} 2773 REDUCER : {initial : context, 2774 addcontext : context * thm list -> context, 2775 apply : {solver : term list -> term -> thm, 2776 context : context, 2777 stack : term list} -> term -> thm} 2778 -> reducer 2779\end{verbatim} 2780\end{hol} 2781Il tipo \ml{context} � un alias per il tipo \ML{} incorporato 2782\ml{exn}, quello delle eccezioni. Le eccezioni sono qui usate come un 2783``tipo universale'', capace di archiviare dati di qualsiasi tipo. Per esempio, 2784se il dato desiderato � una coppia di un intero e un booleano, allora si 2785pu� fare la seguente dichiarazione: 2786\begin{hol} 2787\begin{verbatim} 2788 exception my_data of int * bool 2789\end{verbatim} 2790\end{hol} 2791Non � necessario rendere questa dichiarazione visibile con uno scopo 2792ampio. Infatti, solo le funzioni che accedono e creano contesti di questa 2793forma hanno bisogno di vederla. Per esempio: 2794\begin{hol} 2795\begin{verbatim} 2796 fun get_data c = (raise c) handle my_data (i,b) => (i,b) 2797 fun mk_ctxt (i,b) = my_data(i,b) 2798\end{verbatim} 2799\end{hol} 2800 2801Quando crea un valore di tipo \ml{reducer}, l'utente deve fornire un 2802contesto iniziale, e due funzioni. La prima, \ml{addcontext}, � 2803chiamata dal meccanismo di attraversamento del semplificatore per dare ad ogni 2804procedura di decisione incorporata accesso ai teoremi che rappresentano la nuova informazione 2805di contesto. Per esempio, questa funzione � chiamata con i teoremi dalle 2806assunzioni attuali in \ml{ASM\_SIMP\_TAC}, e con i teoremi 2807dagli argomenti lista di teoremi a tutt le varie funzioni di 2808semplificazione. Mentre un termine � attraversato, le regole di congruenza che governano 2809questo attraversamento possono fornire teoremi addizionali; questi saranno passati 2810anche alla funzione \ml{addcontext}. (Naturalmente, � del tutto a carico 2811della funzione \ml{addcontext} come questi teoremi saranno 2812gestiti; essi possono persino essere ignorati completamente.) 2813 2814Quando un riduttore � applicato a un termine, � richiamata la funzione 2815\ml{apply} fornita. Oltre che al termine da trasformare, la 2816funzione \ml{apply} � passata anche a un record che contiene un 2817risolutore di condizione collaterale, l'attuale contesto della procedura di decisione. e 2818allo stack delle condizioni collaterali tentate fino ad ora. Lo stack e il risolutore 2819sono gli stessi degli argomenti addizionali dati alle conversioni fornite 2820dall'utente. La potenza dell'astrazione del riduttore � di avere accesso a 2821un contesto che pu� essere costruito in modo appropriato per ogni procedura di decisione. 2822 2823Le procedure di decisione sono applicate per l'ultima volta quando un termine � incontrato dal 2824semplificatore. Inoltre, esse sono applicate \emph{dopo} che il semplificatore ha 2825gia� eseguito un ricorsione in ogni sotto-termine e ha tentato di fare quante pi� riscritture 2826possibili. Questo significa che bench� la riscrittura del semplificatore avvenda in un maniera che va 2827dall'alto verso il basso, le procedure di decisione saranno applicate dal basso verso l'alto e 2828solo come ultima risorsa. 2829 2830Come per le conversioni-utente, le procedure di decisione devono sollevare un'eccezione 2831piuttosto che restituire istanze di riflessivit�. 2832 2833\subsubsection{Forme speciali di riscrittura} 2834\label{sec:simp-special-rewrite-forms} 2835 2836Si pu� accedere ad alcune delle caratteristiche del semplificatore in un modo 2837relativamente semplice usando funzioni \ML{} per costruire speciali forme 2838di teorema. Questi teoremi speciali possono poi essere passati negli 2839argomenti lista-di-teoremi delle tattiche di semplificazione. 2840 2841A due delle caratteristiche avanzate del semplificatore, la normalizzazione-AC e 2842le regole di congruenza si pu� accedere in questo modo. Piuttosto che costruire un 2843frammento \simpset{} custom che include le regole AC o di congruenza 2844richieste, l'utente pu� usare piuttosto le funzioni \ml{AC} o \ml{Cong}: 2845\begin{hol} 2846\begin{verbatim} 2847 AC : thm -> thm -> thm 2848 Cong : thm -> thm 2849\end{verbatim} 2850\end{hol} 2851Per esempio, se il valore teorema 2852\begin{hol} 2853\begin{verbatim} 2854 AC DISJ_ASSOC DISJ_COMM 2855\end{verbatim} 2856\end{hol} 2857appare tra i teoremi passati a una tattica di semplificazionie, allora 2858il semplificatore eseguir� una normalizzazione-AC di disgiunzioni. La 2859funzione \ml{Cong} fornisce un'interfaccia analoga per l'aggiunta di 2860nuove regole di congruenza. 2861 2862\index{semplificazione!garantire la terminazione} 2863\index{Once (controllo delle applicazioni di riscrittura)@\ml{Once} (controllo delle applicazioni di riscrittura)|pin} 2864\index{Ntimes (controllo delle applicazioni di riscrittura)@\ml{Ntimes} (controllo delle applicazioni di riscrittura)|pin} 2865Altre due funzioni forniscono un meccanismo crudo per controllare il 2866numero di volte che una riscrittura individuale sar� applicata. 2867\begin{hol} 2868\begin{verbatim} 2869 Once : thm -> thm 2870 Ntimes : thm -> int -> thm 2871\end{verbatim} 2872\end{hol} 2873Un teorema ``avvolto'' nella funzione \ml{Once} sar� applicato 2874una sola volta quando il semplificatore � applicato a un termine dato. Un teorema 2875avvolto in \ml{Ntimes} sar� applicato tante volte quante sono date nel 2876parametro intero. 2877 2878\paragraph{Semplificare a particolari sotto-termini} 2879\index{semplificazione!a particolari sotto-termini} 2880Abbiamo gi� visto (Sezione~\ref{sec:simp-congruences} di sopra) che 2881la tecnologia di congruenza del semplificatore pu� essere usata per forzare il 2882semplificatore ad ignorare termini particolari. L'esempio nella sezione 2883di sopra ha discusso come un regola di congruenza potrebbe essere usata per assicurare che 2884solo le guardie delle espressioni condizionali dovrebbero essere semplificate. 2885 2886In molte dimostrazioni, � comune voler riscrivere solo un lato o 2887l'altro di un connettivo binario (spesso, questo connettivo � 2888un'eguaglianza). Per esempio, questo capita quando si riscrive con equazioni 2889da complicate definizioni ricorsive che non sono soltanto ricorsioni 2890strutturali. In tali definizioni, il lato sinistro dell'equazioni 2891avr� un simbolo funzione attaccato a una sequenza di variabili, ad esempio: 2892\begin{hol} 2893\begin{verbatim} 2894 |- f x y = ... f (g x y) z ... 2895\end{verbatim} 2896\end{hol} 2897Teoremi di una forma analoga sono anche restituiti come i teoremi 2898``casi'' dalle definizioni induttive. 2899 2900Qualunque sia la loro origine, tali teoremi sono il classico esempio di 2901qualcosa a cui si vorrebbe attaccare il qualificatore \ml{Once}. 2902Tuttavia, questo pu� non essere sufficiente: si pu� desiderare di dimostrare un risultato 2903come 2904\begin{hol} 2905\begin{verbatim} 2906 f (constructor x) y = ... f (h x y) z ... 2907\end{verbatim} 2908\end{hol} 2909(Con le relazioni, il goal pu� spesso rappresentare un'implicazione al posto di 2910un'eguaglianza.) In questa situazioni, spesso si vuole semplicemente espandere 2911l'istanza di \holtxt{f} sulla sinistra, lasciando l'altra occorrenza 2912da sola. Usare \ml{Once} espander� solo una di esse, ma senza 2913specificare quale deve essere espansa. 2914 2915La soluzione a questo problema � di usare speciali regole di congruenza, 2916costruite come forme speciali che possono essere passate come teoremi come 2917\ml{Once}. Le funzioni 2918\begin{hol} 2919\begin{verbatim} 2920 SimpL : term -> thm 2921 SimpR : term -> thm 2922\end{verbatim} 2923\end{hol} 2924costruiscono regole di congruenza per forzare la riscritture alla sinistra o alla destra di 2925termini particolari. Per esempio, se \holtxt{opn} � un operatore binario, 2926\ml{SimpL~\holquote{(opn)}} restituisce \ml{Cong} applicato al teorema 2927\begin{hol} 2928\begin{verbatim} 2929 |- (x = x') ==> (opn x y = opn x' y) 2930\end{verbatim} 2931\end{hol} 2932\index{SimpLHS@\ml{SimpLHS}|pin}\index{SimpRHS@\ml{SimpRHS}|pin} 2933Dal momento che il caso eguaglianza � cos� comune, gli speciali valori 2934\ml{SimpLHS} e \ml{SimpRHS} sono forniti per forzare 2935la semplificazione sulla sinistra o sulla destra di un'eguaglianza rispettivamente. 2936Queste sono definite essere solo applicazioni di \ml{SimpL} e \ml{SimpR} 2937all'eguaglianza. 2938 2939Si noti che queste regole si applicano per tutto un termine, non soltanto 2940all'occorrenza pi� alta di un operatore. Inoltre, l'operatore pi� alto nel 2941termine non ha bisogno di essere quello della regola di congruenza. Questo comportamento � 2942una conseguenza automatica dell'implementazione in termini di regole 2943di congruenza. 2944 2945\subsubsection{Limitare la semplificazione} 2946\label{sec:limit-simpl} 2947 2948\index{semplificazione!garantire la terminazione} 2949Oltre alle forme-di-teoremi \ml{Once} and \ml{Ntimes} appena 2950discusse, che limitano il numero di volte che una particolare riscrittura � 2951applicata, il semplificatore pu� anche essere limitato nel numero totale di 2952riscritture che esso esegue. La funzione \ml{limit} (in \ml{simpLib} e 2953\ml{bossLib}) 2954\begin{hol} 2955\begin{verbatim} 2956 limit : int -> simpset -> simpset 2957\end{verbatim} 2958\end{hol} 2959registra un limite numerico in un \simpset{}. Quando un \simpset{} limitato 2960poi lavora su un termine, non applicher� mai pi� del numero dato 2961di riscritture a quel termine. Quando sono usate riscritture condizionali, la 2962riscrittura fatta nello scaricamento delle condizioni collaterali pesano negativamente sul 2963limite, finch� la riscrittura � infine applicata. Anche l'applicazione 2964delle regole di congruenza, delle conversioni e delle procedure 2965di decisione fornite dall'utente pesano tutte negativamente sul limite. 2966 2967Quando il semplificatore cede il controllo a una conversione o a una procedura di 2968decisione fornita dall'utente non pu� garantire che queste funzioni restituiranno 2969alla fine un risultato (e inoltre esse possono prendere un tempo arbitrariamente lungo per terminare, spesso una preoccupazione 2970con le procedure di decisione aritmetica), ma l'uso di \ml{limit} � 2971altrimenti un buon metodo per assicurare che la semplificazione termina. 2972 2973\subsubsection{Riscrittura con pre-ordini arbitrari} 2974\label{sec:preorder-rewriting} 2975\index{semplificazione!con i pre-ordini} 2976 2977Oltre a semplificare rispetto all'eguaglianza, � anche 2978possibile usare il semplificatore per ``riscrivere'' rispetto a una relazione 2979che � riflessiva e transitiva (un \emph{preordine}). Questo pu� essere un 2980modo molto potente di lavorare con relazioni di transizione nella semantica 2981operazionale. 2982 2983{\newcommand{\bred}{\ensuremath{\rightarrow^*_\beta}} 2984 2985 Si immagini, per esempio, che si debba impostare un ``profondo incorporamento'' del 2986 $\lambda$-calcolo. Questo implicher� la definizione di un nuovo tipo 2987 (diciamo, \texttt{lamterm}) all'interno della logica, cos� come le definizioni delle 2988 funzioni appropriate (ad esempio, la sostituzione) e le relazioni su 2989 \texttt{lamterm}. E' probabile che si lavori con la chiusura riflessiva 2990 e transitiva della $\beta$-riduzione (\bred). Questa relazione ha 2991 regole di congruenza come 2992\[ 2993\begin{array}{c@{\qquad\qquad}c} 2994\infer{M_1 \,N\;\bred\;M_2\,N}{M_1 \;\bred\;M_2} & 2995\infer{M \,N_1\;\bred\;M\,N_2}{N_1 \;\bred\;N_2}\\[3mm] 2996\multicolumn{2}{c}{\infer{(\lambda v.M_1)\;\bred\;(\lambda v.M_2)}{M_1\;\bred M_2}} 2997\end{array} 2998\] e un'importante riscrittura 2999\[ 3000\infer{(\lambda v. M)\,N \;\bred\; M[v := N]}{} 3001\] 3002Dovendo applicare queste regole manualmente mostrare che un 3003dato termine iniziale si pu� ridurre a una particolare destinazione � di solito 3004molto doloroso, coinvolgendo molte applicazioni, non solo quelle dei teoremi 3005di sopra, ma anche quelle dei teoremi che descrivono la chiusura riflessiva e 3006transitiva (si veda la Sezione~\ref{relation}). 3007 3008Bench� il $\lambda$-calcolo sia non-deterministico, esso � anche confluente, cos� 3009vale il seguente teorema: 3010\[ 3011\infer{ 3012 M_1 \;\bred\;N\;\;=\;\;M_2\;\bred\; N 3013}{ 3014 \beta\textrm{-nf}\;N & M_1 \;\bred\;M_2 3015} 3016\] 3017Questo � il teorema critico che giustifica il cambio dalla riscrittura 3018con l'eguaglianza alla riscrittura con \bred. Esso dice che se si ha un termine 3019$M_1\bred N$, dove $N$ � una forma $\beta$-normale, e se $M_1$ riscrive a 3020$M_2$ sotto \bred, allora il termine originale � uguale a $M_2\bred N$. 3021Avendo fortuna, $M_2$ sar� sintatticamente identico a $N$, e 3022la riflessivit� di \bred{} dimostrer� il risultato desiderato. I teoremi 3023come questi, che giustificano il cambio da una relazione di riscrittura a 3024un'altra sono conosciuti come \emph{congruenze d'indebolimento}. 3025 3026Quando aggiustato in modo appropriato, il semplificatore pu� essere modificato per sfruttare 3027i cinque teoremi di sopra, e dimostrare automaticamente risultati come 3028\[ 3029u ((\lambda f\,x. f (f\,x)) v) \bred u (\lambda x. v(v\,x)) 3030\] 3031(sotto le assunzioni che i termini $u$ e $v$ siano variabili del 3032$\lambda$-calcolo, rendendo il risultato come una forma $\beta$-normale). 3033 3034Inoltre, si avranno probabilmente vari teoremi di riscrittura 3035che si vorranno usare oltre a quelli specificati di sopra. Per 3036esempio, se in precedenza si � dimostrato un teorema come 3037\[ 3038K\,x\,y \bred x 3039\] 3040allora il semplificatore pu� prendere anche questo in considerazione. 3041 3042La funzione che ottiene tutto questo � 3043\index{add_relsimp@\ml{add\_relsimp}} 3044\begin{verbatim} 3045 simpLib.add_relsimp : {trans: thm, refl: thm, weakenings: thm list, 3046 subsets: thm list, rewrs : thm list} -> 3047 simpset -> simpset 3048\end{verbatim} 3049I campo del record che � il primo argomento sono: 3050\begin{description} 3051\item[\texttt{trans}] Il teorema che afferma che la relazione � 3052 transitiva, nella forma $\forall x y z. R\,x\,y \land R\,y\,z \Rightarrow R x z$. 3053\item[\texttt{refl}] Il teorema che afferma che la relazione � 3054 riflessiva, nella forma $\forall x. R\,x\,x$. 3055\item[\texttt{weakenings}] Una lista di congruenze d'indebolimento, della 3056 forma generale $P_1 \Rightarrow P_2 \Rightarrow \cdots (t_1 = t_2)$, dove almeno una delle 3057 $P_i$ menzioner� presumibilmente la nuova relazione $R$ applicata a una 3058 variabile che appare in $t_1$. Altri 3059 antecedenti possono essere condizioni collaterali come il requisito 3060 nell'esempio di sopra che il termine $N$ sia in forma $\beta$-normale. 3061\item[\texttt{subsets}] Teoremi della forma $R'\,x\,y \Rightarrow R\,x\,y$. 3062 Questi sono usati per aumentare il risultante ``filtro'' del \simpset{} cos� che 3063 i teoremi nel contesto che menziona $R'$ deriveranno utili riscritture 3064 che coinvolgono $R$. Nell'esempio della $\beta$-riduzione, si potrebbe avere anche 3065 una relazione $\rightarrow_{wh}^*$ per la riduzione weak-head. Qualsiasi riduzione 3066 weak-head � anche una $\beta$-riduzione, cos� pu� essere utile anche avere che 3067 il semplificatore ``promuova'' automaticamente i fatti circa la riduzione weak-head 3068 a fatti circa la $\beta$-riduzione, e poi li usi come riscritture. 3069\item[\texttt{rewrs}] Possibilmente riscritture condizionali, presumibilmente la maggior parte 3070 della forma $P \Rightarrow R\,t_1\,t_2$. Qui possono anche essere 3071 incluse riscritture sull'eguaglianza, che permettono di includere utili fatti aggiuntivi. Per 3072 esempio, quando si lavora con il $\lambda$-calcolo, si potrebbe includere sia 3073 la riscrittura per $K$ di sopra, cos� come la definizione della 3074 sostituzione. 3075\end{description} 3076} % end of block defining \bred 3077 3078L'applicazione di questa funzione a un \simpset{} \texttt{ss} 3079produrr� un \texttt{ss} aumentato che ha tutti i comportamenti del 3080\texttt{ss} esistente, cos� come la capacit� di riscrivere con la relazione 3081data. 3082 3083 3084\index{semplificazione|)} 3085 3086\section{Efficient Applicative Order Reduction---\texttt{computeLib}} 3087\label{sec:computeLib} 3088 3089La Sezione~\ref{sec:datatype} e la Sezione~\ref{TFL} mostrano la capacit� di 3090\HOL{} di rappresentare molti dei costrutti standard della programmazione 3091funzionale. Se si vuole quindi `eseguire' programmi funzionali su 3092argomenti, ci sono molte scelte. Primo, si pu� applicare il 3093semplificatore, come mostrato nella Sezione~\ref{sec:simpLib}. Questo permette 3094di esercitare tutto il potere del processo di riscrittura, 3095inclusa, per esempio, l'applicazione delle procedure di decisione per 3096dimostrare vincoli sulle regole di riscrittura condizionale. Secondo, si potrebbe 3097scrivere il programma, e tutti i programmi da cui dipende in modo transitivo, 3098in un file in una sintassi concreta adatta, e invocare un compilatore o 3099un interprete. Questa funzionalit� � disponibile in \HOL{} attraverso l'uso di 3100\ml{EmitML.exportML}. 3101 3102Terzo, si pu� usare \ml{computeLib}. Questa libreria supporta una valutazione 3103call-by-value delle funzioni \HOL{} per passi deduttivi. In altre parole, � 3104molto simile ad avere un interprete \ML{} all'interno della logica \HOL{}, 3105lavorando per inferenza in avanti. Quando usati in questo modo, i programmi 3106funzionali possono essere eseguiti pi� velocemente che usando il semplificatore. 3107 3108Gli entry-point pi� accessibili per usare la libreria \ml{computeLib} 3109sono la conversione \ml{EVAL} e la sua tattica corrispondente 3110\ml{EVAL\_TAC}. Queste dipendono su un database interno che archivia 3111definizioni di funzione. Nel seguente esempio, caricare \ml{sortingTheory} 3112aumenta questo database con le definizioni rilevanti, in particolare quella 3113di Quicksort (\holtxt{QSORT}), e poi possiamo valutare 3114\holtxt{QSORT} su una lista concreta. 3115% 3116\setcounter{sessioncount}{0} 3117\begin{session} 3118\begin{verbatim} 3119 - load "sortingTheory"; 3120 3121 - EVAL ``QSORT (<=) [76;34;102;3;4]``; 3122 > val it = |- QSORT $<= [76; 34; 102; 3; 4] = [3; 4; 34; 76; 102] : thm 3123\end{verbatim} 3124\end{session} 3125Spesso, l'argomento a una funzione non ha variabili: in quel caso 3126l'applicazione di \ml{EVAL} dovrebbe restituire un risultato ground, 3127come nell'esempio di sopra. Tuttavia, \ml{EVAL} pu� anche valutare funzioni su 3128argomenti con variabili---la cosiddetta valutazione \emph{simbolica}---e 3129in quel caso, il comportamento di \ml{EVAL} dipende dalla struttura 3130dell'equazioni di ricorsione. Per esempio, nella seguente sessione, se c'� 3131sufficiente informazione nell'input, la valutazione simbolica pu� restituire 3132un risultato interessante. Tuttavia, se nell'input non c'� informazione 3133sufficiente a permettere all'algoritmo alcuna presa, non avr� luogo 3134alcuna espansione 3135% 3136\begin{session} 3137\begin{verbatim} 3138 - EVAL ``REVERSE [u;v;w;x;y;z]``; 3139 > val it = |- REVERSE [u; v; w; x; y; z] = [z; y; x; w; v; u] : thm 3140 3141 - EVAL ``REVERSE alist``; 3142 > val it = |- REVERSE alist = REVERSE alist : thm 3143\end{verbatim} 3144\end{session} 3145% 3146 3147\subsection{Trattare con la divergenza} 3148 3149La difficolt� maggiore con l'uso di \ml{EVAL} � la terminazione. Troppo 3150spesso, la valutazione simbolica con \ml{EVAL} diverger�, o generer� 3151termini enormi. Il caso usuale sono i condizionali con le variabili nel 3152test. Per esempio, la seguente definizione � probabilmente uguale a \holtxt{FACT}, 3153% 3154\begin{session} 3155\begin{verbatim} 3156 Define `fact n = if n=0 then 1 else n * fact (n-1)`; 3157 > val it = |- fact n = (if n = 0 then 1 else n * fact (n - 1)) : thm 3158\end{verbatim} 3159\end{session} 3160% 3161Ma le due definizioni sono valutate in modo completamente differente. 3162% 3163\begin{session} 3164\begin{verbatim} 3165 EVAL ``FACT n``; 3166 > val it = |- FACT n = FACT n : thm 3167 3168 - EVAL ``fact n``; 3169 <.... interrupt key struck ...> 3170 > Interrupted. 3171\end{verbatim} 3172\end{session} 3173% 3174La definizione ricorsiva primitiva di \holtxt{FACT} non si espande 3175per nulla, mentre la ricorsione stile-decostruttore di \holtxt{fact} non smette mai 3176di espandere. Un rudimentale strumento di monitoraggio mostra il comportamento, prima 3177su un argomento ground, poi su un argomento simbolico. 3178% 3179\begin{session} 3180\begin{verbatim} 3181 - val [fact] = decls "fact"; 3182 - computeLib.monitoring := SOME (same_const fact); 3183 3184 - EVAL ``fact 4``; 3185 fact 4 = (if 4 = 0 then 1 else 4 * fact (4 - 1)) 3186 fact 3 = (if 3 = 0 then 1 else 3 * fact (3 - 1)) 3187 fact 2 = (if 2 = 0 then 1 else 2 * fact (2 - 1)) 3188 fact 1 = (if 1 = 0 then 1 else 1 * fact (1 - 1)) 3189 fact 0 = (if 0 = 0 then 1 else 0 * fact (0 - 1)) 3190 > val it = |- fact 4 = 24 : thm 3191 3192 - EVAL ``fact n``; 3193 fact n = (if n = 0 then 1 else n * fact (n - 1)) 3194 fact (n - 1) = (if n - 1 = 0 then 1 else (n - 1) * fact (n - 1 - 1)) 3195 fact (n - 1 - 1) = 3196 (if n - 1 - 1 = 0 then 1 else (n - 1 - 1) * fact (n - 1 - 1 - 1)) 3197 fact (n - 1 - 1 - 1) = 3198 (if n - 1 - 1 - 1 = 0 then 3199 1 3200 else 3201 (n - 1 - 1 - 1) * fact (n - 1 - 1 - 1 - 1)) 3202 . 3203 . 3204 . 3205\end{verbatim} 3206\end{session} 3207% 3208In ogni espansione ricorsiva, il testo coinvolge una variabile, e di conseguenza 3209non pu� essere ridotta a \holtxt{T} o a \holtxt{F}. Cos�, l'espansione 3210non si ferma mai. 3211 3212Some simple remedies can be adopted in trying to deal with 3213non-terminating symbolic evaluation. 3214 3215Si possono adottare alcuni semplici rimedi nel provare a trattare con 3216una valutazione simbolica che non termina. 3217\begin{itemize} 3218\item \ml{RESTR\_EVAL\_CONV} si comporta come \ml{EVAL} eccetto 3219 che prende una lista extra di costanti. Durante 3220 la valutazione, se si incontra una delle costanti fornite, essa 3221 non sar� espansa. Questo permette di valutare gi� fino a un livello specificato. 3222 e pu� essere usato per tagliare alcune valutazioni circolari. 3223\item anche \ml{set\_skip} pu� essere usata per controllare 3224 la valutazione. Si veda la voce per \ml{CBV\_CONV} in \REFERENCE{} per 3225 una discussione di \ml{set\_skip} 3226 3227\end{itemize} 3228 3229\paragraph{Valutatori custom} 3230 3231Per alcuni problemi, � desiderabile costruire un valutatore 3232personalizzato, specializzato su un insieme fissato di definizioni. Il tipo 3233\ml{compset} che si trova in \ml{computeLib} � il tipo dei database di definizione. Le 3234funzioni \ml{new\_compset}, \ml{bool\_compset}, \ml{add\_funs}, e 3235\ml{add\_convs} forniscono il modo standard per costruire tali 3236database. Un altro \holtxt{compset} piuttosto utile � 3237\ml{reduceLib.num\_compset}, che pu� essere usato per valutare 3238termini con numeri e booleani. Dato un \ml{compset}, la funzione 3239\ml{CBV\_CONV} genera un valutatore: � usata per implementare \ml{EVAL}. 3240Si veda \REFERENCE{} per maggiori dettagli. 3241 3242\paragraph{Trattare con Funzioni sui Numeri di Peano} 3243 3244Le funzioni definite per pattern-matching su numeri nello stile di Peano non sono 3245nel formato giusto per \ml{EVAL}, dal momento che i calcoli saranno 3246asintoticamente inefficienti. Piuttosto, la stessa definizione dovrebbe essere 3247usata su numerali, che � una notazione posizionale descritta nella 3248Sezione~\ref{sec:numerals}. Tuttavia, � preferibile per le dimostrazioni 3249lavorare su numeri di Peano. Per colmare questa lacuna, la funzione 3250\ml{numLib.SUC\_TO\_NUMERAL\_DEFN\_CONV} � usata per convertire una funzione 3251su numeri di Peano in una su numerali, che � il formato che 3252\ml{Eval} preferisce. \ml{Define} chiamer� automaticamente 3253\ml{SUC\_TO\_NUMERAL\_DEFN\_CONV} sul suo risultato. 3254 3255\paragraph{Archiviare le definizioni} 3256 3257\ml{Define} aggiunge automaticamente la sua definizione al compset globale 3258usato da \ml{EVAL} e \ml{EVAL\_TAC}. Tuttavia, quando \ml{Hol\_defn} � 3259usata per definire una funzione, le sue equazioni di definizione non sono aggiunte al 3260compset globale fino a quando \ml{tprove} � usata per dimostrare i vincoli 3261di terminazione. Inoltre, \ml{tprove} non aggiunge la definizione 3262in modo persistente nel compset globale. Di conseguenza, si deve usare 3263\ml{add\_persistent\_funs} in una teoria per essere sicuri che le definizioni 3264fatte da \ml{Hol\_defn} siano disponibili a \ml{Eval} nelle teorie 3265discendenti. Un altro punto: si deve chiamare \ml{add\_persistent\_funs} 3266prima di chiamare \ml{export\_theory}. 3267 3268 3269\section{Le Librerie Aritmetiche---\texttt{numLib}, \texttt{intLib} and \texttt{realLib}} 3270\label{sec:numLib} 3271\index{procedure di decisione!Aritemtica Presburger su numeri naturali} 3272 3273Ognuna delle librerie aritmetiche di \HOL{} fornisce una 3274suite di definizioni e teoremi cos� come il supporto per l'inferenza automatica. 3275 3276\paragraph{numLib} 3277 3278I numeri pi� di base in \HOL{} sono i numeri naturali. La 3279libreria \ml{numLib} comprende le teorie \ml{numTheory}, 3280\ml{prim\_recTheory}, \ml{arithmeticTheory}, e \ml{numeralTheory}. 3281Questa libreria incorpora anche un valutatore per espressioni numeriche 3282da \ml{reduceLib} e una procedura di decisione per l'aritmetica lineare 3283\ml{ARITH\_CONV}. Il valutatore e la procedura di decisione sono 3284integrati nel simpset \ml{arith\_ss} usato dal semplificatore. 3285Allo stesso modo, la procedura di decisione dell'aritmetica lineare pu� essere invocata 3286direttamente attraverso \ml{DECIDE} e \ml{DECIDE\_TAC}, che si trovano entrambe in 3287\ml{bossLib}. 3288 3289 3290\index{procedure di decisione!Aritemtica Presburger su interi} 3291\paragraph{intLib} 3292 3293La libreria \ml{intLib} comprende \ml{integerTheory}, un'estesa 3294teoria degli interi, pi� due procedure di decisione 3295per la completa aritmetica Presburger. Queste sono disponibili come 3296\ml{intLib.COOPER\_CONV} e \ml{intLib.ARITH\_CONV}. Queste 3297procedure di decisione sono in grado di trattare con l'aritmetica lineare 3298sugli interi e i numeri naturali, cos� come di trattare 3299con un'alternanza arbitraria di quantificatori. La procedura 3300\ml{ARITH\_CONV} � un'implementazione dell'Omega Test, e sembra 3301in generale avere migliori performance rispetto all'algoritmo di Cooper. Ci sono 3302comunque problemi per cui questo non � vero, cos� � utile avere disponibili 3303entrambe le procedure. 3304 3305\paragraph{realLib} 3306 3307La libreria \ml{realLib} fornisce uno sviluppo fondazionale 3308dei numeri reali e dell'analisi. Si veda la Sezione~\ref{reals} 3309per una rapida descrizione delle teorie. 3310E' anche fornita una teoria dei polinomi, in \theoryimp{polyTheory}. 3311Una procedura di decisione per l'aritmetica lineare sui numeri reali 3312� anche fornita da \ml{realLib}, sotto il nome \ml{REAL\_ARITH\_CONV} 3313e \ml{REAL\_ARITH\_TAC}. 3314 3315\section{Libreria Bit Vector---\texttt{wordsLib}} 3316 3317La libreria \theoryimp{wordsLib} fornisce uno strumento di supporto per i bit-vectors, questo include infrastrutture per: la valutazione, il parsing, il pretty-printing e la semplificazione. 3318 3319\subsection{Valutazione} 3320 3321La libreria \theoryimp{wordsLib} dovrebbe essere caricata quando si valutano termini bit-vector ground. Questa libreria fornisce un \emph{compset} \ml{words\_compset}, che 3322pu� essere usato nella costruzione di \emph{compese} e conversioni personalizzati. 3323\setcounter{sessioncount}{0} 3324\begin{session} 3325\begin{verbatim} 3326- load "wordsLib"; 3327> val it = () : unit 3328 3329- EVAL ``8w + 9w:word4``; 3330> val it = |- 8w + 9w = 1w : thm 3331\end{verbatim} 3332\end{session} 3333Si noti che qui � usata un'annotazione di tipo per designare la dimensione word. Quando la dimensione word � rappresentata da una variabile di tipo (cio� per word i lunghezza arbitraria), la valutazione 3334pu� dare risultati parziali o insoddisfacenti. 3335 3336\subsection{Parsing e pretty-printing} 3337 3338I word possono essere parsati in binario, decimale e esadecimale. Per esempio: 3339\begin{session} 3340\begin{verbatim} 3341- ``0b111010w : word8``; 3342> val it = ``58w`` : term 3343 3344- ``0x3Aw : word8``; 3345> val it = ``58w`` : term 3346\end{verbatim} 3347\end{session} 3348E' possibile fare il parsing di numeri ottali, ma questo deve essere prima abilitato impostando la reference \ml{base\_tokens.allow\_octal\_input} a true. Per esempio: 3349\begin{session} 3350\begin{verbatim} 3351- ``072w : word8``; 3352> val it = ``72w`` : term 3353 3354- base_tokens.allow_octal_input:=true; 3355> val it = () : unit 3356 3357- ``072w : word8``; 3358> val it = ``58w`` : term 3359\end{verbatim} 3360\end{session} 3361 3362I word possono essere stampati usando le basi numeriche standard. Per esempio, la funzione 3363\ml{wordsLib.output\_words\_as\_bin} selezioner� il formato binario: 3364\begin{session} 3365\begin{verbatim} 3366- wordsLib.output_words_as_bin(); 3367> val it = () : unit 3368 3369- EVAL ``($FCP ODD):word16``; 3370> val it = |- $FCP ODD = 0b1010101010101010w : thm 3371\end{verbatim} 3372\end{session} 3373La funzione \ml{output\_words\_as} � pi� flessibile e permette alla base numerica di variare a seconda della 3374lunghezza del word e del valore numerico. Il pretty-printer di default (installato quando si carica \theoryimp{wordsLib}) stampa valori piccoli in decimale e valori grandi in esadecimale. 3375La funzione \ml{output\_words\_as\_oct} abiliter� automaticamente il parsing per i numeri ottali. 3376 3377La variabile di traccia \ml{"word printing"} fornisce un metodo alternativo per cambiare la base numerica di output --- � particolarmente adatta per selezionare temporaneamente una base numerica, per esempio: 3378\begin{session} 3379\begin{verbatim} 3380- Feedback.trace ("word printing", 1) Parse.print_term ``32w``; 3381<<HOL message: inventing new type variable names: 'a>> 33820b100000w> val it = () : unit 3383\end{verbatim} 3384\end{session} 3385Le scelte sono come segue: 0 (default) -- numeri piccoli in decimale, numeri grandi in esadecimale: 1 -- binario; 2 -- ottale; 3 -- decimale; e 4 -- esadecimale. 3386 3387\subsubsection{Tipi} 3388 3389Si pu� aver notato che \ty{:word4} e \ty{:word8} sono stati usati come convenienti abbreviazioni di parsing per \ty{:\bool[4]} e \ty{:\bool[8]} --- questa agevolazione � disponibile per molte dimensioni standard di word. Gli utenti che desiderano usare questa notazione per dimensioni di non-standard di word possono usare la funzione \ml{wordsLib.mk\_word\_size}: 3390\begin{session} 3391\begin{verbatim} 3392- ``:word15``; 3393! Uncaught exception: 3394! HOL_ERR 3395 3396- wordsLib.mk_word_size 15; 3397> val it = () : unit 3398 3399- ``:word15``; 3400> val it = ``:bool[15]`` : hol_type 3401\end{verbatim} 3402\end{session} 3403 3404\subsubsection{Overloading degli operatori} 3405 3406I simboli per le operazioni aritmetiche standard (addizione, sottrazione e moltiplicazione) sono sottoposte a overload con operatori per altre teorie standard, cio� per i numeri naturali, interi, razionali e reali. In molti casi l'inferenza di tipo risolver� l'overloading, tuttavia, in alcuni casi questo non � possibile. La scelta dell'operatore dipender� dall'ordine in cui le teorie sono caricate. Per cambiare questo comportamento sono fornite le funzioni \ml{wordsLib.deprecate\_word} e \ml{wordsLib.prefer\_word}. Per esempio, nella seguente sessione, la selezione degli operatori word � deprecata: 3407\begin{session} 3408\begin{verbatim} 3409- type_of ``a + b``; 3410<<HOL message: more than one resolution of overloading was possible>> 3411<<HOL message: inventing new type variable names: 'a>> 3412> val it = ``:bool['a]`` : hol_type 3413 3414- wordsLib.deprecate_word(); 3415> val it = () : unit 3416 3417- type_of ``a + b``; 3418<<HOL message: more than one resolution of overloading was possible>> 3419> val it = ``:num`` : hol_type 3420\end{verbatim} 3421\end{session} 3422Di sopra, l'addizione tra numeri naturali � scelta al posto dell'addizione word. Al contrario, i word sono preferiti rispetto agli interi di sotto: 3423\begin{session} 3424\begin{verbatim} 3425- load "intLib"; ... 3426 3427- type_of ``a + b``; 3428<<HOL message: more than one resolution of overloading was possible>> 3429> val it = ``:int`` : hol_type 3430 3431- wordsLib.prefer_word(); 3432> val it = () : unit 3433- type_of ``a + b``; 3434<<HOL message: more than one resolution of overloading was possible>> 3435<<HOL message: inventing new type variable names: 'a>> 3436> it = ``:bool['a]`` : hol_type 3437\end{verbatim} 3438\end{session} 3439Naturalmente, potrebbero essere state aggiunte annotazioni di tipo per evitare questo problema completamente. Si noti che, diversamente da \ml{deprecate\_int}, la funzione \ml{deprecate\_word} non rimuove gli overloading, semplicemente abbassa la loro precedenza. 3440 3441\subsubsection{Indovinare le lunghezze word} 3442 3443Pu� essere una seccatura aggiungere annotazioni di tipo quando si specifica il tipo di ritorno per operazioni come: \holtxt{word\_extract}, \holtxt{word\_concat}, \holtxt{concat\_word\_list} e \holtxt{word\_replicate}. Questo perch� c'� spesso una lunghezza ``standard'' che potrebbe essere indovinata, ad esempio la concatenazione di solito somma le lunghezze dei word costituenti. Un'agevolazione per indovinare la lunghezza word � controllata dalla reference \ml{wordsLib.guessing\_word\_lengths}, che � falsa di default. Le congetture sono eseguite durante un passo di post-processing che avviene dopo l'applicazione di \ml{Parse.Term}. Questo � mostrato di sotto. 3444\begin{session} 3445\begin{verbatim} 3446- wordsLib.guessing_word_lengths:=true; 3447> val it = () : unit 3448 3449- ``concat_word_list [(4 >< 1) (w:word32); w2; w3]``; 3450<<HOL message: inventing new type variable names: 'a, 'b>> 3451<<HOL message: assigning word length: 'a <- 4>> 3452<<HOL message: assigning word length: 'b <- 12>> 3453> val it = 3454 ``concat_word_list [(4 >< 1) w; w2; w3]`` 3455 : term 3456\end{verbatim} 3457\end{session} 3458Nell'esempio di sopra, le congetture sulla lunghezza dei word sono attivate. Sono fatte due congetture: ci si aspetta che l'estrazione dia un word di quattro bit, e che la concatenazione dia un word di dodici bit ($3 \times 4$). Se sono richieste lunghezze numeriche non standard allo si possono aggiungere delle annotazioni di tipo per evitare che siano fatte delle congetture. Quando la congettura � disattivata i tipi risultanti rimangono come variabili di tipo inventate, cio� come gli alfa e i beta di sopra. 3459 3460\subsection{Semplificazione e conversioni} 3461 3462Sono forniti i seguenti frammenti \emph{simpset}: 3463\begin{description} 3464\item[\ml{SIZES\_ss}] valuta un gruppo di funzioni che operano su tipi numerici, come \holtxt{dimindex} e \holtxt{dimword}. 3465\item[\ml{BIT\_ss}] prova a semplificare le occorrenze della funzione\holtxt{BIT}. 3466\item[\ml{WORD\_LOGIC\_ss}] semplifica operazioni logiche bitwise. 3467\item[\ml{WORD\_ARITH\_ss}] semplifica operazioni aritmetiche word. La sottrazione � sostituita con la moltiplicazione da -1. 3468\item[\ml{WORD\_SHIFT\_ss}] semplifica operazioni shift. 3469\item[\ml{WORD\_ss}] contiene tutti i frammenti di sopra, e fa anche una valutazione estra dei termini ground. Questo frammento � aggiunto a \ml{srw\_ss}. 3470\item[\ml{WORD\_ARITH\_EQ\_ss}] semplifica \holtxt{``a = b``} to \holtxt{``a - b = 0w``}. 3471\item[\ml{WORD\_BIT\_EQ\_ss}] espande in modo aggressivo operazioni bit-vector non-aritmetiche in espressioni booleane. (Dovrebbe essere usata con attenzione -- include \ml{fcpLib.FCP\_ss}.) 3472\item[\ml{WORD\_EXTRACT\_ss}] semplificazione per una variet� di operazioni: conversioni da word a word; concatenazione; shift e estrazione bit-field. Pu� essere usata in situationi dove \ml{WORD\_BIT\_EQ\_ss} non � adatta. 3473\item[\ml{WORD\_MUL\_LSL\_ss}] semplifica la moltiplicazione con un letterale word in una somma di prodotti parziali. 3474\end{description} 3475Molti di questi frammenti \emph{simpset} hanno delle conversioni corrispondenti. Per esempio, la conversione \ml{WORD\_ARITH\_CONV} � basata si \ml{WORD\_ARITH\_EQ\_ss}, tuttavia, fa del lavoro extra per assicurare che \holtxt{``a = b``} e \holtxt{``b = a``} si convertano nella stessa espressioni. Di conseguenza, questa conversione � adatta per ragionare circa l'eguaglianza delle espressioni aritmetiche word. 3476 3477Il comportamento dei frammenti elencati di sopra � mostrato usando la seguente funzione: 3478\begin{session} 3479\begin{verbatim} 3480- fun conv ss = SIMP_CONV (pure_ss++ss) []; 3481> val conv = fn : ssfrag -> term -> thm 3482\end{verbatim} 3483\end{session} 3484La seguente sessione mostra \ml{SIZES\_ss}: 3485\begin{session} 3486\begin{verbatim} 3487- conv wordsLib.SIZES_ss ``dimindex(:12)``; 3488> val it = |- dimindex (:12) = 12 : thm 3489 3490- conv wordsLib.SIZES_ss ``FINITE univ(:32)``; 3491> val it = |- FINITE univ(:32) <=> T : thm 3492\end{verbatim} 3493\end{session} 3494Il frammento \ml{BIT\_ss} converte \holtxt{BIT} in un test di appartenenza su un insieme di posizioni bit (pi� alte): 3495\begin{session} 3496\begin{verbatim} 3497- conv wordsLib.BIT_ss ``BIT 3 5``; 3498> val it = |- BIT 3 5 <=> (3 = 0) \/ (3 = 2) : thm 3499 3500- conv wordsLib.BIT_ss ``BIT i 123``; 3501> val it = |- BIT i 123 <=> i IN {0; 1; 3; 4; 5; 6} : 3502 thm 3503\end{verbatim} 3504\end{session} 3505Questa semplificazione fornisce supporto per il ragionamento circa le operazioni bitwise su lunghezze word arbitrarie. I frammenti aritmetico, logico e shift aiutano a ripulire espressioni word di base: 3506\begin{session} 3507\begin{verbatim} 3508- conv wordsLib.WORD_LOGIC_ss ``a && 12w || 11w && a``; 3509<<HOL message: inventing new type variable names: 'a>> 3510> val it = 3511 |- a && 12w || 11w && a = 15w && a : 3512 thm 3513 3514- conv wordsLib.WORD_ARITH_ss ``3w * b + a + 2w * b - a * 4w:word2``; 3515> val it = 3516 |- 3w * b + a + 2w * b - a * 4w = a + b 3517 : thm 3518 3519- conv wordsLib.WORD_SHIFT_ss ``0w << 12 + a >>> 0 + b << 2 << 3``; 3520<<HOL message: inventing new type variable names: 'a>> 3521> val it = 3522 |- 0w << 12 + a >>> 0 + b << 2 << 3 = 0w + a + b << (2 + 3) 3523 : thm 3524\end{verbatim} 3525\end{session} 3526 3527I frammenti rimanenti non sono inclusi in \ml{wordsLib.WORD\_ss} or \ml{srw\_ss}. Il frammento eguaglianza bit � mostrato di sotto. 3528\begin{session} 3529\begin{verbatim} 3530- SIMP_CONV (std_ss++wordsLib.WORD_BIT_EQ_ss) [] ``a && b = ~0w : word2``; 3531> val it = 3532 |- (a && b = ~0w) <=> (a ' 1 /\ b ' 1) /\ a ' 0 /\ b ' 0 3533 : thm 3534\end{verbatim} 3535\end{session} 3536Il frammento esatto � utile per il ragionamento circa operazioni bit-field ed � usato meglio in combinazione con \ml{wordsLib.SIZES\_ss} o \ml{wordsLib.WORD\_ss}, per esempio: 3537\begin{session} 3538\begin{verbatim} 3539- SIMP_CONV (std_ss++wordsLib.SIZES_ss++wordsLib.WORD_EXTRACT_ss) [] 3540 ``(4 -- 1) ((a:word3) @@ (b:word2)) : word5``; 3541> val it = 3542 |- (4 -- 1) (a @@ b) = (2 >< 0) a << 1 || (1 >< 1) b 3543 : thm 3544\end{verbatim} 3545\end{session} 3546Infine, il frammento \ml{WORD\_MUL\_LSL\_ss} � mostrato di sotto. 3547\begin{session} 3548\begin{verbatim} 3549- conv wordsLib.WORD_MUL_LSL_ss ``5w * a : word8``; 3550> val it = |- 5w * a = a << 2 + a : thm 3551\end{verbatim} 3552\end{session} 3553Riscrivere con il teorema \ml{wordsTheory.WORD\_MUL\_LSL} fornisce un mezzo per annullare questa semplificazione, per esempio: 3554\begin{session} 3555\begin{verbatim} 3556- SIMP_CONV (std_ss++wordsLib.WORD_ARITH_ss) [wordsTheory.WORD_MUL_LSL] 3557 ``a << 2 + a : word8``; 3558> val it = |- a << 2 + a = 5w * a : thm 3559\end{verbatim} 3560\end{session} 3561Ovviamente, senza aggiungere delle garanzie, questo teorema di riscrittura non pu� essere dispiegato in combinazione con il frammento \ml{WORD\_MUL\_LSL\_ss}. 3562 3563\subsubsection{Procedure di decisione} 3564 3565Una procedura di decisione per i word � fornita nella forma di 3566\ml{blastLib.BBLAST\_PROVE}. Questa procedura usa il \emph{bit-blasting} --- 3567convertire espressioni word in proposizioni e poi usare il risolutore SAT per 3568decidere il goal\footnote{Questo approccio permette di dare contro-esempi 3569quando la negazione di un goal � insoddisfacibile.}. Questo approccio � ragionevolmente generale e 3570pu� affrontare un ampia gamma di problemi bit-vector. Tuttavia, ci sono alcune 3571limitazioni: l'approccio funziona solo per lunghezze word costanti, artimetica 3572lineare (moltiplicazione per letterali) e per shift e estrazioni 3573bit-field rispetto a valori letterali. Si noti inoltre che alcuni problemi saranno 3574potenzialmente lenti da dimostrare, ad esempio quando le dimensioni dei word sono grandi e/o quando 3575ci sono molte addizioni annidate (magari attraverso la moltiplicazione). 3576 3577 3578I seguenti esempi mostrano \ml{BBLAST\_PROVE} in uso: 3579\begin{session} 3580\begin{verbatim} 3581- blastLib.BBLAST_PROVE ``a + 2w <+ 4w = a <+ 2w \/ 13w <+ a :word4``; 3582> val it = 3583 |- a + 2w <+ 4w <=> a <+ 2w \/ 13w <+ a 3584 : thm 3585 3586- blastLib.BBLAST_PROVE ``w2w (a:word8) <+ 256w : word16``; 3587> val it = |- w2w a <+ 256w : thm 3588\end{verbatim} 3589\end{session} 3590La procedura di decisione \ml{BBLAST\_PROVE} � basata sulla conversione 3591\ml{BBLAST\_CONV}. Questa conversione pu� essere usata per convertire problemi bit-vector 3592in una forma proposizionale; per esempio: 3593\begin{session} 3594\begin{verbatim} 3595- blastLib.BBLAST_CONV ``(((a : word16) + 5w) << 3) ' 5``; 3596> val it = 3597 |- ((a + 5w) << 3) ' 5 <=> (~a ' 2 <=> ~(a ' 1 /\ a ' 0)) 3598 : thm 3599\end{verbatim} 3600\end{session} 3601Ci sono anche tattiche bit-blasting: \ml{BBLAST\_TAC} e \ml{FULL\_BBLAST\_TAC}; dove solo la seconda fa uso delle assunzioni del goal. 3602 3603\section{La libreria \texttt{HolSat}}\label{sec:HolSatLib} 3604\input{HolSat.tex} 3605 3606 3607\section{La libreria \texttt{HolQbf}}\label{sec:HolQbfLib} 3608\input{HolQbf.tex} 3609 3610 3611\section{La libreria \texttt{HolSmt}}\label{sec:HolSmtLib} 3612\input{HolSmt.tex} 3613 3614\section{La libreria \texttt{Quantifier Heuristics}}\label{sec:QuantHeuristicsLib} 3615\input{QuantHeuristics.tex} 3616 3617 3618%%% Local Variables: 3619%%% mode: latex 3620%%% TeX-master: "description" 3621%%% End: 3622