1\chapter{Teorie Fondamentali}\label{HOLtheories} 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% Inside \begin{verbatim}, indent contents three spaces, unless 12% displaying a HOL session in a box (boxed or session environments). 13% In that case, put the session flush against the left margin 14 15% Rather than wrapping begin{verbatim} blocks in \small, which does 16% terrible things to line-spacing in the vicinity, use the hol 17% environment, thus \begin{hol}\begin{verbatim}...\end{verbatim}\end{hol} 18 19\setcounter{sessioncount}{0} 20 21 22\newcommand{\konst}[1]{\ensuremath{\mbox{\small{\textbf{\sf{#1}}}}}} 23\newcommand{\nil}{\mathbf{[} \;\mathbf{]}} 24\newcommand{\cons}[2]{{#1}\mathbf{:}\mathbf{:}{#2}} 25 26\index{teorie, nella logica HOL@theories, nella logica \HOL{}!gerarchie 27delle}% 28Il sistema \HOL{} fornisce una collezione di teorie sulla quali basare strumenti di verifica o un ulteriore sviluppo di teorie. 29Nel resto di questa sezione, queste teorie sono descritte brevemente. 30Le sessioni che seguono forniscono una panoramica del contenuto di ciascuna teoria. 31Per un elenco completo degli assiomi, definizioni e teoremi in \HOL, si vedano le risorse online distribuite con il sistema. 32In particolare, il file HTML \url{help/HOLindex.html} � un buon punto di partenza per esplorare le teorie disponibili. 33Per un'immagine grafica della gerarchia delle teorie, si veda \url{help/theorygraph/theories.html}. 34 35\section{La Teoria {\tt min}}\label{minTheory} 36 37La teoria di partenza di \HOL{} � la teoria \ml{min}. 38\index{min, la teoria HOL@\ml{min}, la teoria \HOL{}|(} 39In questa teoria sono dichiarate la costante di tipo {\small\verb+bool+} dei booleani, 40l'operatore di tipo binario $(\alpha,\beta)${\small\verb+fun+} delle funzioni, e la costante 41di tipo {\small\verb+ind+} degli individui. Sulla base di 42questi tipi, sono dichiarate tre costanti primitive: 43% 44\index{costanti, nella logica HOL@costanti, nella logica \HOL{}!logiche primitive} 45\index{costanti primitive, della logica HOL@costanti primitive, della logica \HOL{}} 46eguaglianza, implicazione, e un operatore di scelta: 47\index{ eguaglianza, nella logica HOL@\ml{=} (eguaglianza, nella logica \HOL{})} 48\index{eguaglianza, nella logica HOL@eguaglianza, nella logica \HOL{}} 49\begin{description} 50\item [Eguaglianza] ({\small\verb+= : 'a -> 'a -> bool+}) � un 51 operatore infisso. 52\index{eguaglianza, nella logica HOL@eguaglianza, nella logica \HOL{}} 53\item [Implicazione] Implicazione 54 ({\small\verb+==> : bool -> bool -> bool+}) � l' 55 \emph{implicazione materiale} ed � un operatore infisso che � 56 associativo a destra, cio�, \verb+x ==> y ==> z+ � parsato allo stesso termine 57 di \verb+x ==> (y ==> z)+. 58\index{implicazione, nella logica HOL@implicazione, nella logica \HOL{}} 59\item [Scelta] L'eguaglianza 60e l'implicazione sono nozioni standard del calcolo dei predicati, ma la scelta � 61pi� esotica: se $t$ � un termine che ha il tipo $\sigma${\small\verb+->bool+}, 62allora {\small\verb+@x.+}$t${\small\verb+ x+} (o, equivalentemente, 63{\small\verb+$@+}$t$) denota \emph{qualche} membro dell'insieme la cui 64funzione caratteristica\index{predicato caratteristico, delle definizioni di tipo} 65 � $t$. Se l'insieme � vuoto, allora 66{\small\verb+@x.+}$t${\small\verb+ x+} denota un membro arbitrario 67dell'insieme denotato da $\sigma$. La costante {\small\verb+@+} � una versione 68di ordine superiore dell'$\hilbert$-operatore 69\index{Hilbert, D.} 70\index{operatore epsilon} 71di Hilbert; � collegato alla costante 72$\iota$ nella formulazione di Church della logica di ordine superiore. Per maggiori dettagli, 73si veda lo scritto 74originale 75di Church\index{Church, A.} \cite{Church}, il libro di 76Leinsenring\index{Leisenring, A.} 77del simbolo-$\hilbert$ di Hilbert \cite{Leisenring}, oppure il libro di testo 78di Andrews sulla teoria dei tipi \cite{Andrews}. 79 80\end{description} 81 82\medskip 83 84\noindent Nella teoria \theoryimp{min} non si trova alcun teorema o assioma. 85Le regole primitive d'inferenza di \HOL{} dipendono dalla presenza di 86\theoryimp{min}. 87% 88\index{min, la teoria HOL@\ml{min}, la teoria \HOL{}|)} 89 90\section{Teorie di Base} 91 92Le teorie pi� di base in HOL forniscono il supporto per una collezione standard 93di tipi. La teoria \theoryimp{bool} definisce la base della 94logica \HOL{}, includendo le operazioni booleane e 95i quantificatori. Su questa piattaforma si pu� gi� costruire un bel p� 96d'infrastruttura di dimostrazione di teoremi. Ulteriori tipi base sono sviluppati 97nella teoria delle coppie (\theoryimp{prod}), delle somme disgiunte 98(\theoryimp{sum}), del tipo di un solo elemento (\theoryimp{one}), e del 99tipo (\theoryimp{option}). 100 101 102\subsection{La teoria \theoryimp{bool}}\label{boolfull} 103 104\index{assiomi!primitivi, della logica HOL@primitivi, della logica \HOL{}|(} 105% 106All'avvio, la teoria iniziale per gli utenti del sistema \HOL{} � 107chiamata \ml{bool}\index{HOL@\HOL{}}, che � costruita quando viene eseguito 108il build del sistema \HOL{}. La teoria \theoryimp{bool} � un'estensione 109della combinazione delle teorie ``concettuali'' \theory{LOG} e 110\theory{INIT}, descritte in \LOGIC. Cos� essa contiene i quattro assiomi 111% 112\index{assiomi!nella teoria bool@nella teoria \ml{bool}} 113% 114per la logica di ordine superiore. Questi assiomi, insieme con le regole 115d'inferenza descritte nella Sezione~\ref{rules}, costituiscono il nucleo della 116logica \HOL{}. A causa del modo in cui il sistema \HOL{} si � evoluto dall'\LCF% 117% 118\index{LCF@\LCF}% 119% 120\footnote{Per semplificare il porting degli strumenti di dimostrazione di teoremi LCF al 121 sistema HOL, la logica HOL � stata resa quanto pi� simile possibile a 122 PP$\lambda$ (la logica incorporata in LCF).}, la particolare assiomatizzazione 123della logica di ordine superiore che esso usa differisce dall'assiomatizzazione 124classica dovuta a Church\index{Church, A.} \cite{Church}. La 125differenza pi� grande � che nella formulazione di Church le variabili di tipo 126% 127\index{variabili di tipo, nella logica HOL@variabili di tipo, nella logica \HOL{}!differenza da quelle classiche} 128% 129sono nel meta-linguaggio, mentre nella logica \HOL{} esse sono parte del 130linguaggio oggetto. 131 132Le costanti logiche 133% 134\index{costanti logiche, nella logica HOL@costanti logiche, nella logica \HOL{}} 135% 136\holtxt{T}~(verit�), 137% 138\index{valori di verit�, nella logica HOL@valori di verit�, nella logica \HOL{}!costanti per} 139% 140\holtxt{F}~(falsit�), 141\holtxt{\~{}}~(negazione), 142% 143\index{ negazione, nella logica HOL@\holtxt{\~{}} (negazione, nella logica \HOL{})} 144% 145\holtxt{/\bs} (congiunzione), 146% 147\index{ congiunzione, nella logica HOL@\holtxt{/\bs} (congiunzione, nella logica \HOL{})} 148% 149\holtxt{\bs/} (disgiunzione), 150% 151\index{ disgiunzione, nella logica HOL@\holtxt{\bs/} (disgiunzione, nella logica \HOL{})} 152% 153\holtxt{!} (quantificazione universale), 154% 155\index{ quantificatore universale, nella logica HOL@\holtxt{"!} (quantificatore universale, nella logica \HOL{})} 156% 157\holtxt{?} (quantificazione esistenziale), 158% 159\index{ quantificatore esistenziale, nella logica HOL@\holtxt{?} (quantificatore esistenziale, nella logica \HOL{})} 160% 161e \holtxt{?!} (quantificatore di esistenza unica) 162% 163\index{ esiste un unico, nella logica HOL@\holtxt{?"!} (esiste un unico, nella logica \HOL{})} 164% 165possono essere tutte definite in termini di eguaglianza, 166% 167\index{eguaglianza, nella logica HOL@eguaglianza, nella logica \HOL{}} 168% 169implicazione e scelta. Le definizioni elencate di sotto sono abbastanza 170standard; ognuna � preceduta dal suo nome \ML{}. Le definizioni posteriori 171a volte sono costruite sulla base di quelle precedenti. 172 173\begin{hol} 174\index{valori di verit�, nella logica HOL@valori di verit�, nella logica \HOL{}!definizione dei} 175\index{T@\holtxt{T}!assioma definizionale per} 176\index{disgiunzione, nella logica HOL@disgiunzione, nella logica \HOL{}!assioma definizionale per} 177\index{congiunzione, nella logica HOL@congiunzione, nella logica \HOL{}!assioma definizionale per} 178\index{sse, nella logica HOL@sse, nella logica \HOL{}!assioma definizionale per} 179\index{negazione, nella logica HOL@negazione, nella logica \HOL{}!assioma definizionale per} 180\index{ esiste un unico, nella logica HOL@\holtxt{?"!} (esiste un unico, nella logica \HOL{})} 181\index{F (falsit�), la costante HOL@\holtxt{F} (falsit�), la costante \HOL{}!assioma definizionale per} 182\index{congiunzione, nella logica HOL@congiunzione, nella logica \HOL{}!assioma definizionale per} 183\index{disgiunzione, nella logica HOL@disgiunzione, nella logica \HOL{}!assioma definizionale per} 184\index{eguaglianza, nella logica HOL@eguaglianza, nella logica \HOL{}!assioma primitivo per} 185\index{quantificatore esistenziale, nella logica HOL@quantificatore esistenziale, nella logica \HOL{}!assioma definizionale per} 186\index{quantificatore universale, nella logica HOL@quantificatore universale, nella logica \HOL{}!assioma definizionale per} 187\index{esiste un unico, nella logica HOL@esiste un unico, nella logica \HOL{}!assioma definizionale per} 188\begin{verbatim} 189 T_DEF |- T = ((\x:bool. x) = (\x. x)) 190 191 FORALL_DEF |- ! = \P:'a->bool. P = (\x. T) 192 193 EXISTS_DEF |- ? = \P:'a->bool. P($@ P) 194 195 AND_DEF |- /\ = \t1 t2. !t. (t1 ==> t2 ==> t) ==> t 196 197 OR_DEF |- \/ = \t1 t2. !t. (t1 ==> t) ==> (t2 ==> t) ==> t 198 199 F_DEF |- F = !t. t 200 201 NOT_DEF |- ~ = (\t. t ==> F) 202 203 EXISTS_UNIQUE_DEF |- ?! = (\P. $? P /\ (!x y. P x /\ P y ==> (x = y))) 204\end{verbatim} 205\end{hol} 206 207 208Ci sono quattro 209% 210\index{quantificatore universale, nella logica HOL@quantificatore universale, nella logica \HOL{}!in quattro assiomi primitivi} 211% 212assiomi nella teoria \theoryimp{bool}; 213% 214\index{bool, la teoria HOL@\ml{bool}, the \HOL{} theory} 215% 216i primi tre sono i seguenti: 217 218\begin{hol} 219\index{BOOL_CASES_AX@\ml{BOOL\_CASES\_AX}} 220\index{ETA_AX@\ml{ETA\_AX}} 221\index{SELECT_AX@\ml{SELECT\_AX}} 222\index{implicazione, nella logica HOL@implicazione, nella logica \HOL{}!assioma primitivo per} 223\index{ funzione di scelta, nella logica HOL@\holtxt{"@} (funzione di scelta, nella logica \HOL{})} 224\index{scelta assioma} 225\index{assioma di scelta} 226\index{assiomi!di scelta} 227\index{operatore di scelta, nella logica HOL@operatore di scelta, nella logica \HOL{}!assioma primitivo per} 228\begin{verbatim} 229 BOOL_CASES_AX |- !t. (t = T) \/ (t = F) 230 231 ETA_AX |- !t. (\x. t x) = t 232 233 SELECT_AX |- !P:'a->bool x. P x ==> P($@ P) 234\end{verbatim} 235\end{hol} 236 237\noindent 238Il quarto ed ultimo assioma della logica \HOL{} � l'Assioma 239dell'Infinito\index{assioma dell'infinito}. Il suo enunciato � formulato in termini delle 240propriet� di funzione {\small\verb+ONE_ONE+} e {\small\verb+ONTO+}. Le 241definizioni sono: 242 243\begin{hol} 244\index{ONE_ONE_DEF@\ml{ONE\_ONE\_DEF}} 245\index{ONTO_DEF@\ml{ONTO\_DEF}} 246\index{one-to-one predicato, nella logica HOL@one-to-one predicato, nella logica \HOL{}!assioma definizionale per} 247\index{onto predicato, nella logica HOL@onto predicato, nella logica \HOL{}!assioma definizionale per} 248\begin{verbatim} 249 ONE_ONE_DEF |- ONE_ONE f = (!x1 x2. (f x1 = f x2) ==> (x1 = x2)) 250 251 ONTO_DEF |- ONTO f = (!y. ?x. y = f x) 252\end{verbatim} 253\end{hol} 254 255\noindent L'Assioma dell'Infinito\index{assiomi!nella teoria bool@nella teoria \ml{bool}} � 256% 257\begin{hol} 258\index{INFINITY_AX@\ml{INFINITY\_AX}} 259\index{assioma dell'infinito} 260\index{quantificatore esistenziale, nella logica HOL@quantificatore esistenziale, nella logica \HOL{}!nell'assioma dell'infinito} 261\begin{verbatim} 262 INFINITY_AX |- ?f:ind->ind. ONE_ONE f /\ ~(ONTO f) 263\end{verbatim} 264\end{hol} 265% 266\noindent 267Questo asserisce che esiste una mappa uno-a-uno da \holtxt{ind} a 268s� stesso che non � suriettiva. Questo implica che il tipo \holtxt{ind} 269denota un insieme infinito. 270% 271\index{assiomi!primitive, della logica HOL@primitive, della logica \HOL{}|)} 272 273Gli altri tre assiomi della teoria \theoryimp{bool}, le regole 274d'inferenza nella Sezione~\ref{rules} e l'Assioma dell'Infinito sono, 275insieme, sufficienti per sviluppare tutta la matematica standard. Cos�, 276in linea di principio, l'utente del sistema \HOL{} non dovrebbe avere mai bisogno 277di fare una teoria 278% 279\index{assiomi!dispensabilit� di aggiungere} 280\index{teorie definizionali} 281% 282non-definizionale. In pratica, � spesso molto allettante correre il rischio di 283introdurre nuovi assiomi perch� derivarli dalle definizioni pu� essere 284noioso---dimostrare che gli `assiomi' seguono da definizioni equivale a 285dimostrare la loro coerenza. 286 287\paragraph {Ulteriori definizioni} 288 289La teoria \theoryimp{bool} fornisce anche le definizioni di un numero di 290utili costanti. 291\begin{hol} 292\index{COND, la costante HOL@\holtxt{COND}, la costante \HOL{}} 293\index{LET, la costante HOL@\ml{LET}, la costante \HOL{}} 294\index{condizionali, nella logica HOL@condizionali, nella logica \HOL{}!assioma definizionale per} 295\begin{verbatim} 296 LET_DEF |- LET = \f x. f x 297 COND_DEF |- COND = \t t1 t2. @x. ((t=T)==>(x=t1)) /\ ((t=F)==>(x=t2)) 298 IN_DEF |- IN = \x (f:'a -> bool). f x 299\end{verbatim} 300\end{hol} 301 302La costante \holtxt{LET} 303% 304\index{termini-let, nella logica HOL@termini-\holtxt{let}, nella logica \HOL{}!costante per} 305% 306� usata nella rappresentazione di termini che contengono binding per variabili locali (cio� 307termini-\holtxt{let}). 308% 309\index{termini-let, nella logica HOL@termini-\holtxt{let}, nella logica \HOL{}!assioma definizionale per} 310% 311Per esempio, la sintassi concreta \holtxt{let v = M in N} � tradotta 312dal parser al termine \holtxt{LET (\bs{}v.N) M}. Per la descrizione 313completa di come le espressioni \holtxt{let} sono tradotte, si veda 314la Sezione \ref{prod}. 315 316La costante \holtxt{COND} � usata per rappresentare espressioni 317condizionali. La sintassi concreta 318% 319\index{termini, nella logica HOL@termini, nella logica \HOL{}!condizionali}% 320\index{condizionali, nella logica HOL@v, nella logica \HOL{}}% 321% 322$\holtxt{if}\;t_1\;\holtxt{then}\;t_2\;\holtxt{else}\;t_3$ abbrevia 323l'applicazione \holtxt{COND $t_1$ $t_2$ $t_3$}. 324 325La costante \holtxt{IN} (scritta come un infisso) � la base 326della modellazione degli insiemi attraverso funzioni caratteristiche. Il termine 327$x\holtxt{ IN }P$ pu� essere letto come ``$x$ � un elemento dell'insieme 328$P$'', o (pi� in linea con la sua definizione) come ``il predicato $P$ � 329vero di $x$''. 330 331Infine, la costante polimorfica $\holtxt{ARB}:\alpha$ denota un 332elemento arbitrario fissato. \holtxt{ARB} � occasionalmente utile quando 333si tenta di trattare con il problema della parzialit�. 334 335\subsubsection{Quantificatori ristretti}\label{res-quant} 336 337\index{quantificazione ristretta} 338% 339La teoria \theoryimp{bool} definisce anche costanti che implementano 340la \emph{quantificazione ristretta}. Questa fornisce un mezzo per simulare 341sotto-tipi e tipi dipendenti con dei predicati. Quelle usate pi� pesantemente 342sono le restrizioni dei quantificatori esistenziale e universale: 343% 344\begin{verbatim} 345 RES_FORALL_DEF |- RES_FORALL = \P m. !x. x IN P ==> m x 346 347 RES_EXISTS_DEF |- RES_EXISTS = \P m. ?x. x IN P /\ m x 348 349 RES_ABSTRACT_DEF |- (!P m x. x IN P ==> (RES_ABSTRACT P m x = m x) /\ 350 (!P m1 m2. 351 (!x. x IN P ==> (m1 x = m2 x)) ==> 352 (RES_ABSTRACT P m1 = RES_ABSTRACT P m2) 353\end{verbatim} 354% 355La definizione di \ml{RES\_ABSTRACT} � una formula caratterizzante, piuttosto 356che un'equazione diretta. Ci sono due propriet� importanti 357\begin{itemize} 358\item se $y$ � un elemento di $P$ allora $(\bs{}x :: P.\; M) 359 y = M[y/x]$ 360\item se due astrazioni ristrette concordano per tutti i valori sul loro 361 insieme (comune) di restrizione, allora sono uguali. 362\end{itemize} 363 364Per completezza, sono fornite le versioni ristrette dell'esistenza unica e 365della descrizione indefinita, bench� difficilmente usate. 366\begin{verbatim} 367 RES_EXISTS_UNIQUE_DEF 368 |- RES_EXISTS_UNIQUE = \P m. (?x :: P. m x) /\ 369 (!x y :: P. m x /\ m y ==> (x = y)) 370 371 RES_SELECT_DEF 372 |- RES_SELECT = \P m. @x. x IN P /\ m x 373\end{verbatim} 374 375La definizione di \ml{RES\_EXISTS\_UNIQUE} usa la sintassi della 376quantificazione ristretta con il simbolo {\small\verb+::+}, che si riferisce 377alle precedenti definizioni \ml{RES\_EXISTS} e \ml{RES\_FORALL}. 378La sintassi \texttt{::} � usata con i quantificatori ristretti per permettere 379predicati arbitrari per restringere le variabili di binding. Il parser \HOL{} 380permette la quantificazione ristretta su tutte le variabili di una sequenza di variabili 381di binding mettendo la restrizione alla fine della sequenza, cos� 382con una quantificazione universale: 383% 384\[ 385\forall x \, y \, z \, {\tt ::} \; P \, . \; Q(x,y,z) 386\] 387% 388Qui il predicato $P$ restringe ognuna delle $x$, $y$ e $z$. 389 390\subsubsection{Forme sintattiche derivate}\label{derived-terms} 391 392\index{quotation, nella logica HOL@quotation, nella logica \HOL{}!of non-primitive terms|(} 393% don't refill the \index entries above, it's important to keep each 394% entry on one line 395Il parser delle quotation di \HOL{} 396% 397\index{quotation, nella logica HOL@quotation, nella logica \HOL{}!parser per} 398% 399pu� tradurre varie notazioni logiche 400standard 401% 402\index{parsing, della logica HOL@parsing, della logica \HOL{}!delle notazioni standard} 403% 404in termini primitivi. Per esempio, se \ml{+} � stato dichiarato un 405infisso 406% 407\index{infissi, nella logica HOL@infissi, nella logica \HOL{}} 408% 409(come spiegato nella Sezione~\ref{theoryfns}), come avviene quando 410� stata caricata \ml{arithmeticTheory}, allora \ml{``x+1``} � 411tradotto in \ml{``\$+~x~1``}. Il carattere di escape \ml{\$} 412% 413\index{ escape, nel parser della logica HOL@\ml{\$} (escape, nel parser della logica \HOL{})} 414\index{costanti dichiarate, nella logica HOL@costanti dichiarate, nella logica \HOL{}} 415\index{infissi, nella logica HOL@infissi, nella logica \HOL{}} 416% 417sopprime il comportamento infisso di \ml{+} e impedisce al parser delle 418quotation di rimanere confuso. In generale, \ml{\$} pu� essere usato per sopprimere 419qualsiasi comportamento sintattico speciale che un token (come \texttt{if}, 420\texttt{+} o \texttt{let}) 421% 422\index{token!sopprimere il comportamento di parsing di} 423% 424potrebbe avere. Questo � illustrato nella tabella di sotto, in cui i termini 425nella colonna intestata \textit{`Quotation \ML{}'} sono tradotti dal 426parser di quotation nei corrispondenti termini nella colonna intestata 427\textit{`Termine primitivo'}. Invece, i termini nell'ultima colonna 428sono sempre stampati nella forma mostrata nella prima. Le espressioni 429costruttore \ML{} nella colonna pi� a destra sono valutate agli stessi 430valori (di tipo \ml{term}) come le altre quotation nella stessa riga. 431 432\bigskip 433 434\begin{center} 435\index{operatore di scelta, nella logica HOL@operatore di scelta, nella logica \HOL{}!sintassi del} 436\index{ negazione, nella logica HOL@\holtxt{\~{}} (negazione, nella logica \HOL{})} 437\index{ disgiunzione, nella logica HOL@\holtxt{\bs/} (disgiunzione, nella logica \HOL{})} 438\index{ congiunzione, nella logica HOL@\holtxt{/\bs} (congiunzione, nella logica \HOL{})} 439\index{ implicazione, nella logica HOL@\holtxt{==>} (implicazione, nella logica \HOL{})} 440\index{ eguaglianza, nella logica HOL@\ml{=} (eguaglianza, nella logica \HOL{})} 441\index{ quantificatore universale, nella logica HOL@\holtxt{"!} (quantificatore universale, nella logica \HOL{})} 442\index{ quantificatore esistenziale, nella logica HOL@\holtxt{?} (quantificatore esistenziale, nella logica \HOL{})} 443\index{ funzione di scelta, nella logica HOL@\holtxt{"@} (funzione di scelta, nella logica \HOL{})} 444\index{termini, nella logica HOL@termini, nella logica \HOL{}!non-primitivi} 445\index{termini, nella logica HOL@termini, nella logica \HOL{}!costruttori per} 446\index{condizionali, nella logica HOL@condizionali, nella logica \HOL{}} 447\index{congiunzione, nella logica HOL@congiunzione, nella logica \HOL{}!costruttore per} 448\index{disgiunzione, nella logica HOL@disgiunzione, nella logica \HOL{}!costruttore per} 449\index{eguaglianza, nella logica HOL@eguaglianza, nella logica \HOL{}!sintassi di} 450\index{negazione, nella logica HOL@negazione, nella logica \HOL{}!sintassi di} 451\index{negazione, nella logica HOL@negazione, nella logica \HOL{}!costruttore per} 452\index{quantificatore esistenziale, nella logica HOL@quantificatore esistenziale, nella logica \HOL{}!sintassi di} 453\index{quantificatore universale, nella logica HOL@quantificatore universale, nella logica \HOL{}!sintassi di} 454\index{implicazione, nella logica HOL@implicazione, nella logica \HOL{}!sintassi di} 455\index{mk_neg@\ml{mk\_neg}} 456\index{mk_disj@\ml{mk\_disj}} 457\index{mk_conj@\ml{mk\_conj}} 458\index{mk_imp@\ml{mk\_imp}} 459\index{mk_eq@\ml{mk\_eq}} 460\index{mk_forall@\ml{mk\_forall}} 461\index{mk_exists@\ml{mk\_exists}} 462\index{mk_select@\ml{mk\_select}} 463\index{mk_cond@\ml{mk\_cond}} 464\index{mk_let@\ml{mk\_let}} 465\index{congiunzione, nella logica HOL@congiunzione, nella logica \HOL{}!sintassi di} 466\begin{tabular}{|l|l|l|l|} \hline 467\multicolumn{4}{|c|}{ } \\ 468\multicolumn{4}{|c|}{\bf Termini non-primitivi} \\ 469\multicolumn{4}{|c|}{ } \\ 470{\it Specie di termine} & {\it Quotation \ML} & 471{\it Termine primitivo} & 472{\it Espressione costruttore} \\ \hline 473 & & & \\ 474Negazione & {\small\verb+~+}$t$ & {\small\verb+$~ +}$t$ & {\small\verb+mk_neg(+}$t${\small\verb+)+} \\ \hline 475Disgiunzione & $t_1${\small\verb+\/+}$t_2$ & {\small\verb+$\/ +}$t_1\ t_2$ & 476{\small\verb+mk_disj(+}$t_1${\small\verb+,+}$t_2${\small\verb+)+} \\ \hline 477% 478Congiunzione & $t_1$\holtxt{/\bs}$t_2$ & $\holtxt{\$/\bs}\ t_1\ t_2$ & 479{\small\verb+mk_conj(+}$t_1${\small\verb+,+}$t_2${\small\verb+)+} \\ 480\hline 481% 482Implicazione & $t_1${\small\verb+==>+}$t_2$ & {\small\verb+$==> +}$t_1\ t_2$ & 483{\small\verb+mk_imp(+}$t_1${\small\verb+,+}$t_2${\small\verb+)+} \\ \hline 484% 485Eguaglianza & $t_1${\small\verb+=+}$t_2$ & {\small\verb+$= +}$t_1\ t_2$ & 486{\small\verb+mk_eq(+}$t_1${\small\verb+,+}$t_2${\small\verb+)+} \\ \hline 487% 488Quantificazione-$\forall$ & {\small\verb+!+}$x${\small\verb+.+}$t$ & 489\holtxt{\$!(\bs}$x${\small\verb+.+}$t${\small\verb+)+} & {\small\verb+mk_forall(+}$x${\small\verb+,+}$t${\small\verb+)+} \\ \hline 490% 491Quantificazione-$\exists$ & {\small\verb+?+}$x${\small\verb+.+}$t$ & 492\holtxt{\$?(\bs}$x${\small\verb+.+}$t${\small\verb+)+} & {\small\verb+mk_exists(+}$x${\small\verb+,+}$t${\small\verb+)+} \\ \hline 493% 494Termine-$\hilbert$ & {\small\verb+@+}$x${\small\verb+.+}$t$ & 495\holtxt{\$@(\bs}$x${\small\verb+.+}$t${\small\verb+)+} & {\small\verb+mk_select(+}$x${\small\verb+,+}$t${\small\verb+)+} \\ \hline 496% 497Condizionale & {\small\verb+if +}$t\ ${\small\verb+then +}$t_1${\small\verb+ else +}$t_2$ & 498{\small\verb+COND +}$t\ t_1\ t_2$ & {\small\verb+mk_cond(+}$t${\small\verb+,+}$t_1${\small\verb+,+}$t_2${\small\verb+)+} 499 \\ \hline 500% 501Espressione-{\small\verb+let+} & {\small\verb+let +}$x${\small\verb+=+}$t_1${\small\verb+ in +}$t_2$ & 502\holtxt{LET(\bs}$x${\small\verb+.+}$t_2${\small\verb+)+}$t_1$ & 503\holtxt{mk\_let(mk\_abs($x$,$t_2$),$t_1$)} \\ \hline 504\end{tabular} 505\end{center} 506 507\bigskip 508 509Ci sono costruttori, de-costruttori, e indicatori per tutti i costrutti 510ovvi. (Gli indicatori, ad esempio \ml{is\_neg}, restituiscono valori di verit� 511che indicano se un termine appartiene o meno alla classe di sintassi in 512questione.) In aggiunta ai costruttori elencati nella tabella ci sono 513costruttori, de-costruttori, e indicatori per coppie e liste, 514cio� \ml{mk\_pair}, 515% 516\index{mk_pair@\ml{mk\_pair}} 517% 518\ml{mk\_cons} 519% 520\index{mk_cons@\ml{mk\_cons}} 521% 522e \ml{mk\_list} 523% 524\index{mk_list@\ml{mk\_list}} 525% 526(si veda \REFERENCE). Le costanti \holtxt{COND} e \holtxt{LET} sono 527spiegate nella Sezione~\ref{boolfull}. Le costanti \holtxt{\bs/}, 528% 529\index{disgiunzione, nella logica HOL@disgiunzione, nella logica \HOL{}!sintassi di} 530% 531\holtxt{/\bs}, \holtxt{==>} e \holtxt{=} sono esempi di 532\textit{infissi} e rappresentano $\vee$, $\wedge$, $\imp$ e l'eguaglianza, 533rispettivamente. Se $c$ � dichiarato essere un infisso, allora il parser 534\HOL{} tradurr� $t_1\ c\ t_2$ in {\small\verb+$+}$c\ t_1\ t_2$. 535 536Le costanti {\small\verb+!+}, {\small\verb+?+} e {\small\verb+@+} 537sono esempi di \label{binder} \textit{binder} 538% 539\index{binder, nella logica HOL@binder, nella logica \HOL{}} 540% 541e rappresentano $\forall$, $\exists$ e $\hilbert$, rispettivamente. Se 542$c$ � dichiarata essere un binder, allora il parser \HOL{} tradurr� 543\holtxt{$c$ $x$.$t$} nella combinazione \holtxt{\$$c$(\bs$x$.$t$)} 544(cio� l'applicazione della costante $c$ alla rappresentazione 545dell'astrazione $\lquant{x}t$). 546\index{ binder astrazione di funzione, nella logica HOL@\holtxt{\bs} (binder astrazione di funzione, nella logica \HOL{})} 547 548\begin{center} 549 550\index{variabili, nella logica HOL@variabili, nella logica \HOL{}!multiple legate} 551\index{list_mk_comb@\ml{list\_mk\_comb}|pin} 552\index{list_mk_abs@\ml{list\_mk\_abs}|pin} 553\index{list_mk_forall@\ml{list\_mk\_forall}|pin} 554\index{list_mk_exists@\ml{list\_mk\_exists}|pin} 555\index{combinazioni, nella logica HOL@combinazioni, nella logica \HOL{}!abbreviazione per ... multiple} 556\index{quantificatore esistenziale, nella logica HOL@quantificatore esistenziale, nella logica \HOL{}!abbreviazione per ... multiplo} 557\index{quantificatore universale, nella logica HOL@quantificatore universale, nella logica \HOL{}!abbreviazione per ... multiplo} 558\begin{tabular}{|l|l|l|} \hline 559\multicolumn{3}{|c|}{ } \\ 560\multicolumn{3}{|c|}{\bf Abbreviazioni sintattiche} \\ 561\multicolumn{3}{|c|}{ } \\ 562{\it Termine abbreviato} & {\it Significato} & 563{\it Espressione costruttore} \\ \hline 564 & & \\ 565$t\ t_1 \cdots t_n$ & 566{\small\verb+(+}$\cdots${\small\verb+(+}$t\ t_1${\small\verb+)+}$\cdots t_n${\small\verb+)+} & 567{\small\verb+list_mk_comb(+}$t${\small\verb+,[+}$t_1${\small\verb+, +}$\ldots${\small\verb+ ,+}$t_n${\small\verb+])+} \\ \hline 568\holtxt{\bs}$x_1\cdots x_n${\small\verb+.+}$t$ & 569\holtxt{\bs}$x_1${\small\verb+. +}$\cdots$\holtxt{ \bs}$x_n${\small\verb+.+}$t$ & 570{\small\verb+list_mk_abs([+}$x_1${\small\verb+, +}$\ldots${\small\verb+ ,+}$x_n${\small\verb+],+}$t${\small\verb+)+} 571\\ \hline 572{\small\verb+!+}$x_1\cdots x_n${\small\verb+.+}$t$ & 573{\small\verb+!+}$x_1${\small\verb+. +}$\cdots${\small\verb+ !+}$x_n${\small\verb+.+}$t$ & 574{\small\verb+list_mk_forall([+}$x_1${\small\verb+, +}$\ldots${\small\verb+ ,+}$x_n${\small\verb+],+}$t${\small\verb+)+} 575\\ \hline 576{\small\verb+?+}$x_1\cdots x_n${\small\verb+.+}$t$ & 577{\small\verb+?+}$x_1${\small\verb+. +}$\cdots${\small\verb+ ?+}$x_n${\small\verb+.+}$t$ & 578{\small\verb+list_mk_exists([+}$x_1${\small\verb+, +}$\ldots${\small\verb+ ,+}$x_n${\small\verb+],+}$t${\small\verb+)+} \\ 579\hline 580\end{tabular} 581\end{center} 582 583\noindent Ci sono anche costruttori 584\ml{list\_mk\_conj}\index{list_mk_conj@\ml{list\_mk\_conj}}, 585\ml{list\_mk\_disj}\index{list_mk_disj@\ml{list\_mk\_disj}} e 586\ml{list\_mk\_imp}\index{list_mk_imp@\ml{list\_mk\_imp}} 587per le congiunzioni, le disgiunzioni, e le implicazioni rispettivamente. 588Le corrispondenti funzioni de-costruttore sono chiamate \ml{strip\_comb}, ecc., 589% 590\index{costruttori di termine, nella logica HOL@costruttori di termine, nella logica \HOL{}|)} 591% 592\index{termini, nella logica HOL@termini, nella logica \HOL{}!costruttori per|)} 593% 594\index{quotation, nella logica HOL@quotation, nella logica \HOL{}!di termini non-primitivi|)} 595 596\subsubsection{Teoremi} 597 598Nella teoria \theoryimp{bool} sono pre-dimostrati molti teoremi che coinvolgono 599costanti logiche. I seguenti teoremi 600illustrano come la logica di ordine superiore permette l'espressione concisa di 601teoremi che supportano lo spostamento del quantificatore. 602 603\begin{holboxed} 604\begin{verbatim} 605 LEFT_AND_FORALL_THM |- !P Q. (!x. P x) /\ Q = !x. P x /\ Q 606 RIGHT_AND_FORALL_THM |- !P Q. P /\ (!x. Q x) = !x. P /\ Q x 607 608 LEFT_EXISTS_AND_THM |- !P Q. (?x. P x /\ Q) = (?x. P x) /\ Q 609 RIGHT_EXISTS_AND_THM |- !P Q. (?x. P /\ Q x) = P /\ ?x. Q x 610 611 LEFT_FORALL_IMP_THM |- !P Q. (!x. P x ==> Q) = (?x. P x) ==> Q 612 RIGHT_FORALL_IMP_THM |- !P Q. (!x. P ==> Q x) = P ==> !x. Q x 613 614 LEFT_EXISTS_IMP_THM |- !P Q. (?x. P x ==> Q) = (!x. P x) ==> Q 615 RIGHT_EXISTS_IMP_THM |- !P Q. (?x. P ==> Q x) = P ==> ?x. Q x 616 617 LEFT_FORALL_OR_THM |- !Q P. (!x. P x \/ Q) = (!x. P x) \/ Q 618 RIGHT_FORALL_OR_THM |- !P Q. (!x. P \/ Q x) = P \/ !x. Q x 619 620 LEFT_OR_EXISTS_THM |- !P Q. (?x. P x) \/ Q = ?x. P x \/ Q 621 RIGHT_OR_EXISTS_THM |- !P Q. P \/ (?x. Q x) = ?x. P \/ Q x 622 623 EXISTS_OR_THM |- !P Q. (?x. P x \/ Q x) = (?x. P x) \/ ?x. Q x 624 FORALL_AND_THM |- !P Q. (!x. P x /\ Q x) = (!x. P x) /\ !x. Q x 625 626 NOT_EXISTS_THM |- !P. ~(?x. P x) = !x. ~P x 627 NOT_FORALL_THM |- !P. ~(!x. P x) = ?x. ~P x 628 629 SKOLEM_THM |- !P. (!x. ?y. P x y) = ?f. !x. P x (f x) 630\end{verbatim} 631\end{holboxed} 632 633Inoltre, � dimostrato un teorema che giustifica la Skolemizzazione 634({\small\verb+SKOLEM_THM+}). Nella teoria \theoryimp{bool} si possono trovare molti altri teoremi. 635 636 637\subsection{Combinatori} 638\label{sec:combinTheory} 639 640\index{composizione di funzione, nella logica HOL@composizione di funzione, nella logica \HOL{}|(} 641 642La teoria \theoryimp{combin} 643\index{combin@\theoryimp{combin}} 644\index{combinatori, nella logica HOL@combinatori, nella logica \HOL{}} 645contiene le definizioni della composizione di funzione (\ml{o} infisso), 646\index{ operatore di composizione di funzioni, nella logica HOL@\ml{o} (operatore di composizione di funzioni), nella logica \HOL{}|(} 647un operatore di applicazione inversa di funzione, 648\index{ operatore applicazione di funzione, nella logica HOL@\ml{:>} (operatore applicazione di funzione (inversa)), nella logica \HOL{}} 649di override di funzione (\ml{=+} infisso), 650\index{ operatore di override di funzione, nella logica HOL@\ml{=+} (operatore di override di funzione), nella logica \HOL{}} 651e i combinatori 652\ml{S}, 653\index{S, la costante HOL@\ml{S}, la costante \HOL{}} 654\ml{K}, 655\index{K, la costante HOL@\ml{K}, la costante \HOL{}} 656\ml{I}, 657\index{I, la costante HOL@\ml{I}, la costante \HOL{}} 658\ml{W}, 659\index{W, la costante HOL@\ml{W}, la costante \HOL{}} 660and \ml{C}, 661\index{C, la costante HOL@\ml{C}, la costante \HOL{}} 662 663\begin{hol} 664\begin{verbatim} 665 o_DEF |- f o g = (\x. f(g x)) 666 APP_DEF |- x :> f = f x 667UPDATE_DEF |- (k =+ v) = (\f c. if k = c then v else f c) 668 K_DEF |- K = (\x y. x) 669 S_DEF |- S = (\f g x. f x(g x)) 670 I_DEF |- I = S K K 671 W_DEF |- W = (\f x. f x x) 672 C_DEF |- C = (\f x y. f y x) 673\end{verbatim} 674\end{hol} 675 676\noindent Le seguenti propriet� elementari sono dimostrate nella teoria 677\ml{combin}: 678 679\begin{hol} 680\begin{verbatim} 681 o_THM |- !f g x. (f o g) x = f(g x) 682 o_ASSOC |- !f g h. f o (g o h) = (f o g) o h 683 684 UPDATE_EQ 685 |- !f a b c. (a =+ c) ((a =+ b) f) = (a =+ c) f 686 UPDATE_COMMUTES 687 |- !f a b c d. a <> b ==> 688 ((a =+ c) ((b =+ d) f) = (b =+ d) ((a =+ c) f)) 689 690 K_THM |- !x y. K x y = x 691 S_THM |- !f g x. S f g x = f x (g x) 692 I_THM |- !x. I x = x 693 W_THM |- !f x. W f x = f x x 694 C_THM |- !f x y. C f x y = f y x 695\end{verbatim} 696\end{hol} 697 698\index{ operatore di applicazione di funzione, nella logica HOL@\ml{:>} (operatore di applicazione (inversa) di funzione), nella logica \HOL{}} 699Non ci sono teoremi circa \ml{:>}; il suo uso � una sintassi conveniente per le applicazioni di funzione. 700Per esempio, le catene di update possono perdere qualche parentesi se scritte 701\begin{hol} 702\begin{verbatim} 703 f :> (k1 += v1) :> (k2 += v2) :> (k3 += v3) 704\end{verbatim} 705\end{hol} 706Questa presentazione rende anche l'ordine in cui le funzione sono applicate da sinistra a destra. 707 708Avere i simboli \ml{o}, \ml{S}, \ml{K}, \ml{I}, \ml{W}, and \ml{C} 709come costanti incorporate 710% 711\index{variabili, nella logica HOL@variabili, nella logica \HOL{}!con nomi di costanti} 712% 713talvolta non � conveniente perch� spesso essi sono desiderati come nomi 714mnemonici per variabili (ad esempio \ml{S} varia su insiemi e \ml{o} 715varia su output)\footnote{Le costanti dichiarate nelle nuove teorie possono 716 riutilizzare liberamente questi nomi, con input ambigui risolti dall'inferenza 717 di tipo.}. Si possono usare variabili con questi nomi nel sistema 718attuale se \ml{o}, \ml{S}, \ml{K}, \ml{I}, \ml{W}, e \ml{C} sono prima 719nascosti (si veda la Sezione~\ref{hidden}). Di fatto, questo accade cos� spesso 720con la costante \holtxt{C} che essa � `nascosta' di default. Quando � 721nascosta, deve essere scritta nella sua forma completamente-qualificata, come 722\holtxt{combin\$C}. 723% 724\index{ operatore composizione di funzione, nella logica HOL@\ml{o} (operatore composizione di funzione), nella logica \HOL{}|)} 725\index{composizione di funzione, nella logica HOL@composizione di funzione, nella logica \HOL{}|)} 726\index{costanti, nella logica HOL@costanti, nella logica \HOL{}!nomi completamente-qualificati di} 727 728 729\subsection{Coppie}\label{prod} 730 731\index{tipi rappresentanti, nella logica HOL@tipi rappresentanti, nella logica \HOL{}!coppia esempio di|(} 732\index{coppie, nella logica HOL@coppie, nella logica \HOL{}|(} 733\index{tipi prodotto!nella logica HOL@in \HOL{} logic|(} 734% 735L'operatore di prodotto Cartesiano 736% 737\index{operatori di tipo, nella logica HOL@operatori di tipo, nella logica \HOL{}!per coppie} 738% 739\holtxt{prod} 740% 741\index{prod, l'operatore di tipo HOL@\holtxt{prod}, l'operatore di tipo \HOL{}} 742% 743� definito nella teoria \theoryimp{pair}. I valori di tipo 744\holtxt{($\sigma_1$,$\sigma_2$)prod} sono coppie ordinate il cui primo 745componente ha il tipo $\sigma_1$ e il cui secondo componente ha il tipo 746$\sigma_2$. Il parser di tipo \HOL{} 747% 748\index{parsing, della logica HOL@parsing, della logica \HOL{}!of pairs} 749% 750converte le espressioni di tipo della forma \holtxt{:$\sigma_1$\#$\sigma_2$} 751% 752\index{ operatore di tipo prodotto, nella logica HOL@\holtxt{\#} (operatore di tipo prodotto, nella logica \HOL{})} 753% 754in \holtxt{($\sigma_1$,$\sigma_2$)prod}, 755% 756\index{ costruttore di coppia, nella logica HOL@\ml{,} (costruttore di coppia, nella logica \HOL{})} 757% 758e il printer inverte questa trasformazione. Le coppie 759% 760\index{costruttore di accoppiamento, nella logica HOL@costruttore di accoppiamento, nella logica \HOL{}} 761% 762sono costruite con un simbolo di virgola infisso 763 764\begin{hol} 765\begin{verbatim} 766 $, : 'a -> 'b -> 'a # 'b 767\end{verbatim} 768\end{hol} 769 770\noindent 771cos�, per esempio, se $t_1$ e $t_2$ hanno i tipi $\sigma_1$ e 772$\sigma_2$ rispettivamente, allora $t_1$\ml{,}$t_2$ � un termine con tipo 773$\sigma_1$\holtxt{\#}$\sigma_2$. Di solito, le coppie sono scritte all'interno 774di parentesi: \holtxt{($t_1$,$t_2$)}. Il simbolo virgola associa 775% 776\index{costruttore di accoppiamento, nella logica HOL@costruttore di accoppiamento, nella logica \HOL{}!associativit� di} 777% 778a destra, cos� che \holtxt{($t_1$,$t_2$,$\ldots$,$t_n$)} significa 779\holtxt{($t_1$,($t_2$,$\ldots$,$t_n$))}. 780 781\paragraph {Definire il tipo prodotto} 782 783Il tipo dei prodotti Cartesiani � definito rappresentando una coppia 784{\small\verb%(%}$t_1${\small\verb%,%}$t_2${\small\verb%)%} 785per mezzo della funzione 786% 787\begin{hol} 788\begin{alltt} 789 \bs{}a b. (a=\m{t\sb{1}}) /\bs (b=\m{t\sb{2}}) 790\end{alltt} 791\end{hol} 792% 793\noindent Il tipo rappresentante di 794$\sigma_1${\small\verb%#%}$\sigma_2$ � cos� 795$\sigma_1${\small\verb%->%}$\sigma_2${\small\verb%->bool%}. 796E' facile dimostrare il seguente teorema\footnote{Questo teorema ha 797un $\beta$-redex non ridotto al fine di soddisfare l'interfaccia 798richiesta dal principio di definizione di tipo}. 799% 800\begin{hol} 801\begin{verbatim} 802 |- ?p:'a->'b->bool. (\p. ?x y. p = \a b. (a = x) /\ (b = y)) p 803\end{verbatim} 804\end{hol} 805% 806L'operatore di tipo {\small\verb%prod%} � definito invocando \ml{new\_type\_definition}\index{new_type_definition@\ml{new\_type\_definition}} con questo teorema che risulta nell'asserazione nella teoria \ml{pair} dell'assioma definizionale \index{assiomi!non-primitivi, della logica HOL@non-primitivi, della logica \HOL{}!per prodotti} \index{assiomi!nella teoria bool@nella teoria \ml{bool}} \ml{prod\_TY\_DEF} mostrato di sotto. 807% Perch� il glossario mette quest'assioma nella teoria bool? 808\begin{hol} 809\begin{verbatim} 810 prod_TY_DEF 811 |- ?rep. TYPE_DEFINITION (\p. ?x y. p = (\a b. (a = x) /\ (b = y))) rep 812\end{verbatim} 813\end{hol} 814% 815Poi, sono introdotte le funzioni di rappresentazione e astrazione \holtxt{REP\_prod} 816e \holtxt{ABS\_prod} per il nuovo tipo, insieme con il 817seguente teorema caratterizzante, per mezzo dell'uso della funzione 818\ml{define\_new\_type\_bijections}. 819% 820\begin{hol} 821\begin{verbatim} 822 |- (!a. ABS_prod (REP_prod a) = a) /\ 823 (!r. (\p. ?x y. p = (\a b. (a=x) /\ (b=y)) r = (REP_prod(ABS_prod r) = r) 824\end{verbatim} 825\end{hol} 826 827\paragraph {Coppie e proiezioni} 828 829Il costruttore infisso `{\small\verb%,%}' � poi definito 830essere un'applicazione della funzione di astrazione. Successivamente, sono 831dimostrati due teoremi cruciali: {\small\verb+PAIR_EQ+} afferma che coppie 832uguali hanno componenti uguali e {\small\verb+ABS_PAIR_THM+} mostra che 833ogni termine che ha un tipo prodotto pu� essere decomposto in una coppia di termini. 834\begin{hol} 835\index{costruttore di accoppiamento, nella logica HOL@costruttore di accoppiamento, nella logica \HOL{}!definizione di} 836\index{PAIR_EQ@\ml{PAIR\_EQ}} 837\index{ABS_PAIR_THM@\ml{ABS\_PAIR\_THM}} 838\begin{verbatim} 839 COMMA_DEF |- !x y. $, x y = ABS_prod (\a b. (a = x) /\(b = y)) 840 841 PAIR_EQ |- ((x,y) = (a,b)) = (x=a) /\ (y=b) 842 843 ABS_PAIR_THM |- !x. ?q r. x = (q,r) 844 $ 845\end{verbatim} 846\end{hol} 847% 848Skolemizzando {\small\verb+ABS_PAIR_THM+} e facendo le specifiche di costante 849per {\small\verb+FST+} e {\small\verb+SND+}, sono dimostrati i 850seguenti teoremi. 851% 852\begin{hol} 853\index{PAIR@\ml{PAIR}} 854\index{FST, la costante HOL@\ml{FST}, la costante \HOL{}!definizione di} 855\index{SND, la costante HOL@\ml{SND}, la costante \HOL{}!definizione di} 856\index{selettori, nella logica HOL@selettori, nella logica \HOL{}!per coppie} 857\begin{verbatim} 858 PAIR |- !x. (FST x,SND x) = x 859 FST |- !x y. FST(x,y) = x 860 SND |- !x y. SND(x,y) = y 861\end{verbatim} 862\end{hol} 863\index{coppie, nella logica HOL@coppie, nella logica \HOL{}|)} 864\index{tipi prodotto!nella logica HOL@nella logica \HOL{}|)} 865\index{tipi rappresentanti, nella logica HOL@tipi rappresentanti, nella logica \HOL{}!coppia esempio di|)} 866 867\paragraph{Coppie e funzioni} 868 869In \HOL{}, una funzione di tipo $\alpha \# \beta\to\gamma$ ha sempre una 870controparte di tipo $\alpha\to\beta\to\gamma$, e \emph{vice versa}. 871Questa conversione � compiuta attraverso le funzioni \holtxt{CURRY} e 872\holtxt{UNCURRY}. Queste funzioni sono inverse. 873% 874\begin{hol} 875\index{CURRY, la costante HOL@\ml{CURRY}, la costante \HOL{}} 876\index{UNCURRY, la costante HOL@\ml{UNCURRY}, la costante \HOL{}} 877\begin{verbatim} 878 CURRY_DEF |- !f x y. CURRY f x y = f (x,y) 879 UNCURRY_DEF |- !f x y. UNCURRY f (x,y) = f x y 880 881 CURRY_UNCURRY_THM |- !f. CURRY (UNCURRY f) = f 882 UNCURRY_CURRY_THM |- !f. UNCURRY (CURRY f) = f 883\end{verbatim} 884\end{hol} 885 886 887\paragraph {Mappare funzioni su una coppia} 888 889Le funzioni $f : \alpha \to \gamma_1$ e $g : \beta\to\gamma_2$ possono essere 890applicate in modo componente ({\small\verb+##+}, infisso) su una coppia di tipo 891$\alpha \# \beta$ per ottenere una coppia di tipo $\gamma_1 \# \gamma_2$. 892% 893\begin{hol} 894\index{mappare funzioni, in the HOL logic@mappare funzioni, nella logica \HOL{}!per coppie} 895\index{ PAIR_MAP funzione@\ml{\#\#} (\holtxt{PAIR\_MAP} funzione)} 896\begin{verbatim} 897 PAIR_MAP_THM |- !f g x y. (f ## g) (x,y) = (f x,g y) 898\end{verbatim} 899\end{hol} 900 901\paragraph {Binder e coppie} 902 903Quando si fanno dimostrazioni, gli enunciati che coinvolgono tuple possono prendere la forma di un 904binding (quantificazione o $\lambda$-astrazione) di una variabile con un 905tipo prodotto. Pu� essere conveniente nei successivi passi di ragionamento 906rimpiazzare le variabili con tuple di variabili. I seguenti teoremi 907supportano questo. 908% 909\begin{hol} 910\begin{verbatim} 911 FORALL_PROD |- (!p. P p) = !p_1 p_2. P (p_1,p_2) 912 EXISTS_PROD |- (?p. P p) = ?p_1 p_2. P (p_1,p_2) 913 LAMBDA_PROD |- !P. (\p. P p) = \(p1,p2). P (p1,p2) 914\end{verbatim} 915\end{hol} 916% 917Il teorema \ml{LAMBDA\_PROD} coinvolge una \emph{astrazione 918 accoppiata}, discussa nella Sezione \ref{HOL-varstruct}. 919 920 921\paragraph {Relazioni benfondate su coppie} 922 923La benfondatezza, definita nella Sezione \ref{prim-rec-conseq}, 924� una nozione utile, specialmente per dimostrare la terminazione delle 925funzioni ricorsive. Per le coppie, la combinazione lessicografica 926delle relazioni ({\small\verb+LEX+}, infisso) pu� essere definita usando 927astrazioni accoppiate. Poi il teorema che la combinazione lessicografica 928delle relazioni benfondate produce [delivers n.d.t.] una relazione benfondata � facile da 929dimostrare. 930% 931\begin{hol} 932\begin{verbatim} 933 LEX_DEF = 934 |- !R1 R2. R1 LEX R2 = (\(s,t) (u,v). R1 s u \/ (s = u) /\ R2 t v) 935 WF_LEX 936 |- !R Q. WF R /\ WF Q ==> WF (R LEX Q) 937\end{verbatim} 938\end{hol} 939 940\subsubsection{Astrazioni accoppiate} 941\label{HOL-varstruct} 942\index{coppie, nella logica HOL@coppie, nella logica \HOL{}!nelle astrazioni|(} 943\index{coppie, nella logica HOL@coppie, nella logica \HOL{}!parsing delle} 944\index{termini, nella logica HOL@termini, nella logica \HOL{}!coppia|(} 945\index{parsing, della logica HOL@parsing, della logica \HOL{}!delle astrazioni accoppiate} 946\index{astrazione di funzione, nella logica HOL@astrazione di funzione, nella logica \HOL{}!accoppiate|(} 947\index{astrazione di funzione, nella logica HOL@astrazione di funzione, nella logica \HOL{}!uncurrying, nella ... accoppiata|(} 948 949E' conveniente dal punto di vista della notazione includere l'accoppiamento nella lambda 950astrazione, come un semplice meccanismo di pattern-matching. Il parser delle quotation 951\index{parsing, della logica HOL@parsing, della logica \HOL{}!di astrazioni di funzione} 952\index{astrazione di funzione nella logica HOL@astrazione di funzione, nella logica \HOL{}!abbreviazione per ... multipla} 953\index{termini, nella logica HOL@termini, nella logica \HOL{}!astrazione di funzione} 954convertir� il termine 955{\small\bs\texttt{(}}$x_1${\small\verb%,%}$x_2${\small\verb%).%}$t$ 956in {\small\verb%UNCURRY(%\bs}$x_1\ x_2${\small\verb%.%}$t${\small\verb%)%}. 957La trasformazione � fatta ricorsivamente cos� che, per esempio, 958% 959\begin{hol} 960\begin{alltt} 961 \bs(\m{x\sb{1}},\m{x\sb{2}},\m{x\sb{3}}).\m{t} 962\end{alltt} 963\end{hol} 964% 965\noindent � convertito in 966% 967\begin{hol} 968\begin{alltt} 969 UNCURRY \bs\m{x\sb{1}}. UNCURRY(\bs\m{x\sb{2}} \m{x\sb{3}}.\m{t})) 970\end{alltt} 971\end{hol} 972% 973\noindent Pi� in generale, il parser delle quotation applica ripetutamente la 974trasformazione: 975% 976\begin{hol} 977\begin{alltt} 978 \bs(\m{v\sb{1}},\m{v\sb{2}}).\m{t}\m{\quad \leadsto\quad}UNCURRY(\bs\m{v\sb{1}}.\bs\m{v\sb{2}}.\m{t}) 979\end{alltt} 980\end{hol} 981% 982\noindent fino a quando non rimane pi� alcuna struttura variabili. Per esempio: 983 984\vspace{1ex} 985\begin{tabular}{ll} 986\texttt{\bs($x$,$y$).$t$} & 987 $\leadsto$ \texttt{UNCURRY(\bs$x\,y$.$t$)}\\ 988% 989\texttt{\bs($x_1$,$x_2$,$\ldots$,$x_n$).$t$} & 990 $\leadsto$ \texttt{UNCURRY(\bs$x_1$.\bs($x_2$,$\ldots$,$x_n$).$t$)}\\ 991% 992\texttt{\bs(($x_1$,$\ldots$,$x_n$),$y_1$,$\ldots$,$y_m$).$t$} & 993 $\leadsto$ 994 \texttt{UNCURRY(\bs($x_1$,$\ldots$,$x_n$).\bs($y_1$,$\ldots$,$y_m$).$t$)}\\ 995\end{tabular} 996 997\vspace{1ex} 998 999\noindent Come risultato di questa traduzione del parser, una struttura variabile, come \ml{(x,y)} in 1000\ml{\bs(x,y).x+y}, non � un sottotermine della astrazione 1001\index{astrazione di funzione, nella logica HOL@astrazione di funzione, nella logica \HOL{}!sottotermini di} 1002in cui occorre; essa scompare nel parsing. 1003\index{binder, nella logica HOL@binder, nella logica \HOL{}!parsing di} 1004\index{parsing, della logica HOL@parsing, della logica \HOL{}!di binders} 1005Questo pu� portare ad errori inaspettati (accompagnati da oscuri messaggi 1006di errore). Per esempio, l'antiquoting di una coppia nella posizione della variabile 1007legata di una lambda astrazione fallisce: 1008 1009\begin{session} 1010\begin{verbatim} 1011- ``\(x,y).x+y``; 1012> val it = `\(x,y). x + y` : term 1013 1014- val p = Term `(x:num,y:num)`; 1015> val p = `(x,y)` : term 1016 1017- Lib.try Term `\^p.x+y`; 1018 1019Exception raised at Term.dest_var: 1020not a var 1021! Uncaught exception: 1022\end{verbatim} 1023\end{session} 1024Se $b$ � un binder, allora \ml{$b$($x_1$,$x_2$).$t$} � parsato come 1025\ml{$b$(\bs($x_1$,$x_2$).$t$)}, e di conseguenza trasformato come di sopra. Per 1026esempio, 1027\ml{!(x,y).\ x > y} 1028� parsato a\linebreak 1029\ml{\$!(UNCURRY(\bs{}x.\bs{}y.\ x > y))}. 1030\index{astrazione di funzione, nella logica HOL@astrazione di funzione, nella logica \HOL{}!accoppiata|)} 1031\index{astrazione di funzione, nella logica HOL@astrazione di funzione, nella logica \HOL{}!uncurrying, nella ... accoppiata|)} 1032\index{coppie, nella logica HOL@coppie, nella logica \HOL{}!nelle astrazioni|)} 1033\index{termini, nella logica HOL@termini, nella logica \HOL{}!pair|)} 1034 1035 1036\subsubsection{Termini-\texttt{let}} 1037\label{let-exp} 1038 1039Il parser delle quotation 1040% 1041\index{parsing, della logica HOL@parsing, della logica \HOL{}!di termini-let@di termini-\holtxt{let}} 1042% 1043accetta termini-\ml{let} 1044\index{termini, nella logica HOL@termini, nella logica \HOL{}!let-@\holtxt{let}-} 1045\index{termini-let, nella logica HOL@termini-\holtxt{let}, nella logica \HOL{}!come abbreviazioni} 1046analoghi a quelli \ML. Per esempio, sono permessi i seguenti termini: 1047 1048\begin{hol} 1049\begin{verbatim} 1050 let x = 1 and y = 2 in x+y 1051 1052 let f(x,y) = (x*x)+(y*y) and a = 20*20 and b = 50*49 in f(a,b) 1053\end{verbatim} 1054\end{hol} 1055 1056i termini-\ml{let} sono di fatto abbreviazioni per termini ordinari che sono 1057supportati in modo speciale dal parser e dal pretty printer. 1058La costante \ml{LET} 1059% 1060\index{LET, la costante HOL@\ml{LET}, la costante \HOL{}} 1061% 1062� definita (nella teoria \ml{bool}) da: 1063 1064\begin{hol}\index{astrazione di funzione, nella logica HOL@astrazione di funzione, nella logica \HOL{}!relazione con i termini-let@relazione con i termini-\ml{let}} 1065\begin{verbatim} 1066 LET = (\f x. f x) 1067\end{verbatim} 1068\end{hol} 1069 1070\noindent ed � usata per codificare i termini-\ml{let} nella logica. Il parser 1071applica ripetutamente le trasformazioni: 1072 1073\bigskip 1074 1075{\small\begin{tabular}{ll} 1076\texttt{let~$f\,v_1\,\ldots\,v_n$~=~$t_1$~in~$t_2$} & 1077$\leadsto$~~\texttt{LET(\bs$f$.$t_2$)(\bs$v_1\,\ldots\,v_n$.$t_1$)}\\ 1078% 1079\texttt{let~($v_1$,$\ldots$,$v_n$)~=~$t_1$~in~$t_2$} & 1080$\leadsto$~~\texttt{LET(\bs($v_1$,$\ldots$,$v_n$).$t_2$)$t_1$}\\ 1081% 1082\texttt{let~$v_1$=$t_1$~and~$\ldots$~and~$v_n$=$t_n$~in~$t$} & 1083$\leadsto$~~\texttt{LET($\ldots$(LET(LET(\bs$v_1\ldots v_n$.$t$)$t_1$)$t_2$)$\ldots$)$t_n$}\\ 1084\end{tabular}} 1085 1086\bigskip 1087 1088 1089\noindent La struttura sottostante del termine si pu� vedere applicando 1090le operazioni di de-costruzione. Per esempio: 1091 1092\begin{session} 1093\begin{verbatim} 1094- Term `let x = 1 and y = 2 in x+y`; 1095> val it = `let x = 1 and y = 2 in x + y` : term 1096 1097- dest_comb it; 1098> val it = (`LET (LET (\x y. x + y) 1)`, `2`) : term * term 1099 1100- Term `let (x,y) = (1,2) in x+y`; 1101> val it = `let (x,y) = (1,2) in x + y` : Term.term 1102 1103- dest_comb it; 1104> val it = (`LET (\(x,y). x + y)`, `(1,2)`) : Term.term * Term.term 1105\end{verbatim} 1106\end{session} 1107 1108I lettori sono incoraggiati a convincersi che le traduzioni dei 1109termini-\ml{let} rappresentano il significato intuitivo suggerito dalla 1110sintassi di superficie.% 1111% 1112 1113\subsection{Somme disgiunte} 1114\label{sum} 1115\index{unioni disgiunte, la teoria HOL delle@unioni disgiunte, la teoria \HOL{} delle|(} 1116\index{somme (unioni disgiunte), la teoria HOL delle@somme (unioni disgiunte), la teoria \HOL{} delle|(} 1117 1118 1119La teoria \theoryimp{sum} definisce l'operatore di tipo binario unione 1120disgiunta \holtxt{sum}. Un tipo \holtxt{($\sigma_1$,$\sigma_2$)sum} 1121denota l'unione disgiunta dei tipi $\sigma_1$ and $\sigma_2$. L'operatore 1122di tipo \holtxt{sum} pu� essere definito, esattamente come � stato per \holtxt{prod}, 1123ma i dettagli sono qui omessi\footnote{La definizione delle unioni 1124 disgiunte nel sistema HOL � dovuta a Tom Melham. I dettagli tecnici 1125 di questa definizione si possono trovare in~\cite{Melham-banff}.} Il parser 1126di \HOL{} 1127% 1128\index{parsing, della logica HOL@parsing, della logica \HOL{}!dei tipi sum} 1129% 1130converte \holtxt{``:$\sigma_1$+$\sigma_2$``} 1131% 1132\index{ tipo operatore unione disgiunta, nella logica HOL@\ml{+} (tipo operatore unione disgiunta, nella logica HOL)} 1133% 1134in \holtxt{``:($\sigma_1$,$\sigma_2$)sum``}, e il printer inverte 1135questo. 1136 1137Le operazioni standard sulle somme sono: 1138 1139\begin{hol} 1140\index{INL, la costante HOL@\ml{INL}, la costante \HOL{}} 1141\index{INR, la costante HOL@\ml{INR}, la costante \HOL{}} 1142\index{ISL, la costante HOL@\ml{ISL}, la costante \HOL{}} 1143\index{ISR, la costante HOL@\ml{ISR}, la costante \HOL{}} 1144\index{OUTL, la costante HOL@\ml{OUTL}, la costante \HOL{}} 1145\index{OUTR, la costante HOL@\ml{OUTR}, la costante \HOL{}} 1146\begin{verbatim} 1147 INL : 'a -> 'a + 'b 1148 INR : 'b -> 'a + 'b 1149 ISL : 'a + 'b -> bool 1150 ISR : 'a + 'b -> bool 1151 OUTL : 'a + 'b -> 'a 1152 OUTR : 'a + 'b -> 'b 1153\end{verbatim} 1154\end{hol} 1155 1156\noindent Queste sono tutte definite come costanti nella teoria \ml{sum}. Le 1157costanti \ml{INL} e \ml{INR} iniettano nei sommandi sinistro e destro, 1158rispettivamente. Le costanti \ml{ISL} e \ml{ISR} testano l'appartenenza ai 1159sommandi sinistro e destro, rispettivamente. Le costanti \ml{OUTL} e \ml{OUTR} 1160proiettano da una somma ai sommandi sinistro e destro, rispettivamente. 1161 1162Il seguente teorema � dimostrato nella teoria \ml{sum}. Esso fornisce una 1163caratterizzazione completa e astratta del tipo somma disgiunta, ed 1164� usato per giustificare la definizione delle funzioni sulle somme. 1165 1166\begin{hol} 1167\begin{verbatim} 1168 sum_Axiom |- !f g. ?! h. (!x. h(INL x) = f x) /\ (!x. h(INR x) = g x) 1169\end{verbatim} 1170\end{hol} 1171 1172\noindent Inoltre sono forniti i seguenti teoremi che hanno a che fare 1173con le funzioni discriminatore \ml{ISL} e \ml{ISR}: 1174 1175\begin{hol} 1176\begin{verbatim} 1177 ISL |- (!x. ISL(INL x)) /\ (!y. ~ISL(INR y)) 1178 ISR |- (!x. ISR(INR x)) /\ (!y. ~ISR(INL y)) 1179 1180 ISL_OR_ISR |- !x. ISL x \/ ISR x 1181\end{verbatim} 1182\end{hol} 1183 1184\noindent La teoria \ml{sum} fornisce anche i seguenti teoremi 1185relativi alle funzioni di proiezione e ai discriminatori. 1186 1187\begin{hol} 1188\begin{verbatim} 1189 OUTL |- !x. OUTL(INL x) = x 1190 OUTR |- !x. OUTR(INR x) = x 1191 1192 INL |- !x. ISL x ==> (INL(OUTL x) = x) 1193 INR |- !x. ISR x ==> (INR(OUTR x) = x) 1194\end{verbatim} 1195\end{hol} 1196 1197\index{unioni disgiunte, la teoria HOL delle@unioni disgiunte, la teoria \HOL{} delle|)} 1198\index{somme (unioni disgiunte), la teoria HOL delle@somme (unioni disgiunte), la teoria HOL \HOL{} delle|)} 1199 1200 1201\subsection{Il tipo di un-unico-elemento}% 1202\index{one, la teoria e il tipo HOL@\ml{one}, la teoria e il tipo \HOL{}}% 1203 1204La teoria \ml{one} definisce il tipo \ml{one} che contiene un solo elemento. 1205La costante \ml{one} � specificata denotare questo elemento. I teoremi 1206pre-dimostrati nella teoria \ml{one} sono: 1207 1208\begin{hol} 1209\index{one_Axiom@\ml{one\_Axiom}} 1210\begin{verbatim} 1211 one_axiom |- !(f:'a->one) (g:'a -> one). f = g 1212 one |- !(v:one). v = one 1213 one_Axiom |- !(e:'a). ?!(fn:one->'a). fn one = e 1214\end{verbatim} 1215\end{hol} 1216 1217\noindent Questi tre teoremi sono caratterizzazioni equivalenti del tipo 1218con un solo valore. La teoria \ml{one} � usata tipicamente nella 1219costruzione di tipi pi� elaborati. L'unico valore del tipo 1220\ml{one}, pu� anche essere scritto \ml{()} per analogia con il valore 1221unit nell'\ML. Questo � anche il modo di default in cui questo valore 1222� stampato dal pretty-printer del sistema. 1223 1224\subsubsection{Il tipo itself} 1225\index{itself, l'operatore di tipo HOL@\holtxt{itself}, l'operatore di tipo \HOL{}}% 1226L'operatore di tipo \holtxt{itself} fornisce una famiglia di tipi singleton simili a \holtxt{one}. 1227Cos�, per ogni tipo $\alpha$, \holtxt{$\alpha$~itself} � un tipo che contiene solo un unico valore. 1228Il nome di questo valore � \holtxt{the\_value}, ma il parser e il pretty-printere sono impostati cos� che per il tipo \holtxt{$\alpha$~itself}, \holtxt{the\_value} pu� essere scritto come \holtxt{(:$\alpha$)} (la sintassi include le parentesi). 1229Per esempio, \holtxt{(:num)} � il singolo valore che abita il tipo \holtxt{num~itself}. 1230 1231Il punto del tipo itself � che se si definisce una funzione con \holtxt{$\alpha$~itself} come dominio, la funzione sceglie un solo valore nel suo rango, e cos� si pu� pensare alla funzione come se fosse una dal tipo a un valore per l'intero tipo. 1232 1233Per esempio, si potrebbe definire 1234\begin{hol} 1235\begin{verbatim} 1236 finite_univ (:'a) = FINITE (UNIV :'a set) 1237\end{verbatim} 1238\end{hol} 1239Sarebbe quindi semplice dimostrare i seguenti teoremi 1240\begin{hol} 1241\begin{alltt} 1242 \(\vdash\) finite_univ(:bool) 1243 \(\vdash\) \(\neg\)finite_univ(:num) 1244 \(\vdash\) finite_univ(:'a) \(\land\) finite_univ(:'b) \(\Rightarrow\) finite_univ(:'a # 'b) 1245\end{alltt} 1246\end{hol} 1247 1248Il tipo itself � usato nella costruzione del Prodotto Cartesiano Finito sottostante al tipo delle parole a larghezza fissa (si veda la Sezione~\ref{sec:bit-vectors} di sotto). 1249 1250\subsection{Il tipo option} 1251\index{option, la teoria HOL delle@option, la teoria \HOL{} delle} 1252 1253La teoria \theoryimp{option} definisce un operatore di tipo \verb+option+ 1254che `solleva' il suo tipo argomento, creando un tipo con tutti i valori 1255dell'argomento e un altro valore distinto in modo speciale. 1256I costruttori di questo tipo sono 1257\begin{hol} 1258\begin{verbatim} 1259 NONE : 'a option 1260 SOME : 'a -> 'a option 1261\end{verbatim} 1262\end{hol} 1263Le option possono essere usate per modellizzare le funzioni parziali. Se una funzione di tipo 1264$\alpha\rightarrow\beta$ non valori $\beta$ utili per tutti 1265gli input $\alpha$, allora questa distinzione pu� essere contrassegnata rendendo il 1266rango della funzione $\beta\,\konst{option}$, e mappando i 1267valori $\alpha$ indefiniti su \holtxt{NONE}. 1268 1269Come tipo induttivo, le option hanno un teorema di ricorsione che supporta la 1270definizione di funzioni ricorsive primitive su valori option. 1271% 1272\begin{hol} 1273\begin{verbatim} 1274 option_Axiom 1275 |- !e f. 1276 ?h:'a option -> 'b. 1277 (!x. h (SOME x) = f x) /\ 1278 (h NONE = e) 1279\end{verbatim} 1280\end{hol} 1281La teoria \theoryimp{option} definisce anche una costante case che permette 1282di ispezionare i valori option in un stile ``pattern-matching''. 1283\begin{hol} 1284\begin{verbatim} 1285 case e of 1286 NONE => u 1287 | SOME x => f x 1288\end{verbatim} 1289\end{hol} 1290% 1291La costante sottostante a questo addolcimento sintattico � \verb+option_case+ 1292con la definizione 1293\begin{hol} 1294\begin{verbatim} 1295 option_case_def |- (option_case u f NONE = u) /\ 1296 (option_case u f (SOME x) = f x) 1297\end{verbatim} 1298\end{hol} 1299% 1300Un altre funzione utile mappa una funzione su un'option: 1301% 1302\index{mapping di funzioni, nella logica HOL@mapping di funzioni, nella logica \HOL{}!per le option} 1303\begin{hol} 1304\begin{verbatim} 1305 OPTION_MAP_DEF |- (OPTION_MAP f NONE = NONE) /\ 1306 (OPTION_MAP f (SOME x) = SOME (f x)) 1307\end{verbatim} 1308\end{hol} 1309Infine, la funzione \holtxt{THE} prende un valore 1310\holtxt{SOME} per quell'argomento del costruttore, ed � indefinita su 1311\holtxt{NONE}: 1312\begin{hol} 1313\begin{verbatim} 1314 THE_DEF |- THE (SOME x) = x 1315\end{verbatim} 1316\end{hol} 1317 1318\section{Numeri} 1319 1320I numeri naturali, gli interi, e i numeri reali sono forniti in una 1321serie di teorie. Sono anche disponibili teorie di parole di $n$-bit 1322(numeri modulo $2^n$), numeri a virgola mobile e numeri a virgola fissa. 1323 1324\subsection{Numeri naturali} 1325 1326I numeri naturali sono sviluppati in una serie di teorie: 1327\theoryimp{num}, \theoryimp{prim\_rec}, \theoryimp{arithmetic}, e 1328\theoryimp{numeral}. In \theoryimp{num}, il tipo dei numeri � 1329definito dall'Assioma dell'Infinito, e sono derivati gli assiomi di Peano. In 1330\theoryimp{prim\_rec} � dimostrato il teorema di Ricorsione Primitiva. Sulla base 1331di questo, in \theoryimp{arithmetic} � sviluppata un'ampia teoria che tratta le operazioni aritmetiche 1332standard. Da ultimo, � sviluppata una teoria dei 1333numerali. 1334 1335\subsubsection{La teoria \theoryimp{num}} 1336 1337La teoria \theoryimp{num} 1338\index{num, la teoria nella logica HOL@\ml{num}, la teoria nella logica \HOL{}} 1339definisce che il tipo \ml{num} dei numeri naturali � 1340isomorfo a un sottoinsieme numerabile del tipo primitivo \ml{ind}. In questa 1341teoria, sono definite le costanti \ml{0} 1342\index{ zero, nella logica HOL@\ml{0} (zero, nella logica \HOL{})} 1343e \ml{SUC} (la funzione successore) 1344e gli assiomi di Peano 1345\index{assiomi!nella teoria num@nella teoria \ml{num}} 1346\index{gli assiomi di Peano} 1347\index{assiomi!non-primitivi, della logica HOL@non-primitive, della logica \HOL{}!per i numeri naturali} 1348sono pre-dimostrati nella forma: 1349 1350\begin{hol} 1351\index{NOT_SUC@\ml{NOT\_SUC}} 1352\index{INV_SUC@\ml{INV\_SUC}} 1353\index{teoremi d'induzione, nella logica HOL@teoremi d'induzione, nella logica \HOL{}!per i numeri naturali} 1354\begin{verbatim} 1355 NOT_SUC |- !n. ~(SUC n = 0) 1356 INV_SUC |- !m n. (SUC m = SUC n) ==> (m = n) 1357 INDUCTION |- !P. P 0 /\ (!n. P n ==> P(SUC n)) ==> (!n. P n) 1358\end{verbatim} 1359\end{hol} 1360 1361Nella logica di ordine superiore, gli assiomi di Peano sono sufficienti per sviluppare 1362la teoria dei numeri perch� possono essere definite l'addizione e la moltiplicazione. Nella 1363logica del primo ordine queste devono essere prese come primitive. Si noti anche che 1364\ml{INDUCTION} non potrebbe essere enunciato come un singolo assioma nella logica del 1365primo ordine perch� i predicati (ad esempio \holtxt{P}) non possono essere quantificati. 1366 1367\subsubsection{La teoria \theoryimp{prim\_rec}} 1368\label{prim_rec} 1369 1370\index{teorema per la ricorsione primitiva!per i numeri} 1371\index{prim_rec, la teoria HOL@\ml{prim\_rec}, la teoria \HOL{}|(} 1372Nella logica classica, diversamente dalle logiche domain theory come \PPL, 1373% 1374\index{PPlambda (same as PPLAMBDA), del sistema LCF@\ml{PP}$\lambda$ (same as \ml{PPLAMBDA}), del sistema \ml{LCF}} 1375% 1376le definizioni arbitrariamente ricorsive 1377% 1378\index{definizioni ricorsive, nelle logiche classiche} 1379% 1380non sono permesse. Per esempio, non c'� alcuna funzione $f$ (di tipo 1381\ml{num->num}) tale che 1382 1383\begin{alltt} 1384 !\(x\). \(f\) \(x\) = (\(f\) \(x\)) + 1 1385\end{alltt} 1386Certe ristrette forme di definizione 1387% 1388\index{funzioni ricorsive primitive} 1389% 1390ricorsiva, comunque, definiscono funzioni in modo univoco. Un esempio 1391importante sono le funzioni \emph{ricorsive primitive}\footnote{Nella 1392 logica di ordine superiore, la ricorsione primitiva � molto pi� potente che 1393 nella logica del primo ordine; per esempio la funzione di Ackermann pu� essere 1394 definita per ricorsione primitiva nella logica di ordine superiore.}. Per qualsiasi $x$ 1395e $f$ il \emph{teorema di ricorsione primitiva} ci dice che c'� 1396un'unica funzione \holtxt{fn} tale che: 1397 1398\begin{alltt} 1399 (fn 0 = \(x\)) /\bs (!\(n\). fn(SUC \(n\)) = f (fn \(n\)) \(n\)) 1400\end{alltt} 1401 1402Il teorema di ricorsione primitiva, chiamato \ml{num\_Axiom} in \HOL, 1403segue dagli assiomi 1404% 1405\index{assiomi di Peano} 1406% 1407di Peano. 1408 1409\begin{hol}\index{num_Axiom@\ml{num\_Axiom}} 1410\index{teorema di caratterizzazione!per i numeri} 1411\begin{verbatim} 1412 num_Axiom |- !x f. ?fn. (fn 0 = x) /\ (!n. fn(SUC n) = f n (fn n)) 1413\end{verbatim} 1414\end{hol} 1415 1416\noindent Il teorema stabilisce la validit� delle definizioni ricorsive 1417primitive sui numeri naturali: per qualsiasi \ml{x} e \ml{f} esiste una 1418corrispondente funzione totale \ml{fn} che soddisfa 1419la definizione ricorsiva primitiva la cui forma � determinata da \ml{x} e 1420\ml{f}. 1421 1422\paragraph{La relazione minore-di} 1423 1424La relazione minore-di `\holtxt{<}' 1425\index{ minore di, nella logica HOL@\ml{<} (minore di, nella logica \HOL{})} 1426\index{minore di, nella logica HOL@minore di, nella logica \HOL{}} 1427� definita in modo pi� naturale per ricorsione primitiva. Tuttavia, nel nostro 1428sviluppo � richiesta per la dimostrazione del 1429 teorema di ricorsione primitiva, cos� deve essere definita prima che la definizione 1430 per ricorsione primitiva sia disponibile. La teoria \theoryimp{prim\_rec} 1431 di conseguenza contiene la seguente definizione non ricorsiva di \ml{<}: 1432 1433\begin{hol} 1434\index{LESS@\ml{LESS}} 1435\begin{verbatim} 1436 LESS |- !m n. m < n = ?P. (!n. P(SUC n) ==> P n) /\ P m /\ ~P n 1437\end{verbatim} 1438\end{hol} 1439 1440\noindent 1441Questa definizione dice che {\small\verb%m < n%} se esiste un insieme (con 1442funzione caratteristica {\small\verb%P%}) che � chiuso 1443verso il basso\footnote{Un insieme di numeri � \textit{chiuso verso il basso} se ogni volta che 1444contiene il successore di un numero, contiene anche il numero.} e 1445contiene {\small\verb%m%} ma non {\small\verb%n%}. 1446\index{prim_rec, la teoria HOL@\ml{prim\_rec}, la teoria \HOL{}|)} 1447 1448 1449\subsubsection{Meccanizzazione delle definizioni ricorsive primitive} 1450\label{num-prim-rec} 1451 1452\index{definizioni ricorsive, nella logica HOL@definizioni ricorsive, nella logica \HOL{}!automatiche, per i numeri} 1453\index{teorema di ricorsione primitiva!uso automatico del, nel sistema HOL@uso automatico del, nel sistema \HOL{}|(} 1454Il teorema 1455\index{definizioni ricorsive primitive, nella logica HOL@definizioni ricorsive primitive, nella logica \HOL{}!giustificazione delle} 1456di ricorsione primitiva pu� essere usato per giustificare qualsiasi definizione di una funzione 1457sui numeri naturali per ricorsione primitiva. Per esempio, una 1458definizione ricorsiva primitiva nella logica di ordine superiore della forma 1459 1460\begin{hol} 1461\begin{alltt} 1462 fun 0 x\(\sb{1}\) \m{\dots} x\(\sb{i}\) = \m{f\sb{1}[}x\(\sb{1}\)\m{,\ldots,\,} x\(\sb{i}]\) 1463 fun (SUC n) x\(\sb{1}\) \m{\dots} x\(\sb{i}\) = \m{f\sb{2}[}fun n \m{t\sb{1} \dots t\sb{i},} n\m{,} x\(\sb{1}\)\m{,\ldots,\,}x\(\sb{i}]\) 1464\end{alltt} 1465\end{hol} 1466 1467\noindent dove tutte le variabili libere nei termini $t_1$, 1468\dots, $t_i$ sono contenute in $\{$\ml{n}, $\ml{x}_1$, \dots, $\ml{x}_i\}$, 1469� logicamente equivalente a: 1470 1471\begin{hol} 1472\begin{alltt} 1473 fun 0 = \bs{}x\(\sb{1}\) \m{\dots} x\(\sb{i}\).\m{f\sb{1}[}x\(\sb{1}\)\m{,\ldots,\,}x\(\sb{i}]\) 1474 fun (SUC n) = \bs{}x\(\sb{1}\) \m{\dots} x\(\sb{i}\).\m{f\sb{2}[}fun n \m{t\sb{1} \dots t\sb{i},} n\m{,}x\(\sb{1}\)\m{,\ldots,\,}x\(\sb{i}]\) 1475 = (\bs{}f n x\(\sb{1}\) \m{\dots} x\(\sb{i}\).\m{f\sb{2}[}f \m{t\sb{1} \dots t\sb{i},} n\m{,} x\(\sb{1}\)\m{,\ldots,\,}x\(\sb{i}]\)) (fun n) n 1476\end{alltt} 1477\end{hol} 1478 1479L'esistenza di una funzione ricorsiva \ml{fun} che soddisfa queste due 1480equazioni segue direttamente dal teorema di ricorsione primitiva 1481\ml{num\_Axiom} mostrato di sopra. La specializzazione delle variabili quantificate \verb!x! 1482e \verb!f! con un'adeguata istanziazione dei tipi di \ml{num\_Axiom} cos� 1483che 1484 1485\begin{hol} 1486\begin{alltt} 1487 x\m{=}\bs{}x\(\sb{1}\) \(\dots\) x\(\sb{i}\).\m{f\sb{1}[}x\(\sb{1}\)\(,\ldots,\,\)x\(\sb{i}]\) {\rm e} f\(=\)\bs{}f n x\(\sb{1}\) \(\dots\) x\(\sb{i}\).\m{f\sb{2}[}f \m{t\sb{1} \dots t\sb{i},} n\(,\) x\(\sb{1}\)\(,\ldots,\,\)x\(\sb{i}]\)) 1488\end{alltt} 1489\end{hol} 1490 1491\noindent restituisce il teorema di esistenza mostrato di sotto: 1492 1493\begin{hol} 1494\begin{alltt} 1495 |- ?fn. fn 0 = \bs{}x\(\sb{1}\) \(\dots\) x\(\sb{i}\).\m{f\sb{1}[}x\(\sb{1}\)\(,\ldots,\,\)x\(\sb{i}]\) /\bs{} 1496 fn (SUC n) = (\bs{}f n x\(\sb{1}\) \(\dots\) x\(\sb{i}\).\m{f\sb{2}[}f \m{t\sb{1} \dots t\sb{i},} n\(,\) x\(\sb{1}\)\(,\ldots,\,\)x\(\sb{i}]\)) (fn n) n 1497\end{alltt} 1498\end{hol} 1499 1500\noindent Questo teorema permette d'introdurre una costante \ml{fun} (attraverso il 1501meccanismo\linebreak definizionale delle specifiche di costante---si veda la Sezione~\ref{conspec}) 1502per denotare la funzione ricorsiva che soddisfa le due equazioni nel corpo 1503del teorema. L'introduzione di una costante \ml{fun} per nominare la funzione che � affermata 1504esistere dal teorema mostrato di sopra, e la semplificazione per mezzo di una $\beta$-riduzione, 1505porta al seguente teorema: 1506 1507\begin{hol} 1508\begin{alltt} 1509 |- fun 0 = \bs{}x\(\sb{1}\) \(\dots\) x\(\sb{i}\).\m{f\sb{1}[}x\(\sb{1}\)\(,\ldots,\,\)x\(\sb{i}]\) /\bs{} 1510 fun (SUC n) = \bs{}x\(\sb{1}\) \(\dots\) x\(\sb{i}\).\m{f\sb{2}[}fun n \m{t\sb{1} \dots t\sb{i},} n\(,\) x\(\sb{1}\)\(,\ldots,\,\)x\(\sb{i}]\) 1511\end{alltt} 1512\end{hol} 1513 1514\noindent Segue immediatamente da questo teorema che la costante \ml{fun} 1515soddisfa le equazioni di definizione ricorsiva primitiva date dal teorema mostrato 1516di sotto: 1517 1518\begin{hol} 1519\begin{alltt} 1520 |- fun 0 x\(\sb{1}\) \(\dots\) x\(\sb{i}\) = \m{f\sb{1}[}x\(\sb{1}\)\(,\ldots,\,\)x\(\sb{i}]\) 1521 fun (SUC n) x\(\sb{1}\) \(\dots\) x\(\sb{i}\) = \m{f\sb{2}[}fun n \m{t\sb{1} \dots t\sb{i},} n\(,\) x\(\sb{1}\)\(,\ldots,\,\)x\(\sb{i}]\) 1522\end{alltt} 1523\end{hol} 1524 1525Per automatizzare l'uso del teorema di ricorsione primitiva nel derivare 1526definizioni ricorsive di questo genere, il sistema \HOL{} fornisce una funzione 1527che automaticamente dimostra l'esistenza di funzioni ricorsive 1528primitive e poi fa una specifica di costante per introdurre la costante 1529che denota una tale funzione: 1530 1531\begin{holboxed} 1532\index{new_recursive_definition@\ml{new\_recursive\_definition}|pin} 1533\begin{verbatim} 1534 new_recursive_definition : 1535 {def : term, name : string, rec_axiom : thm} -> thm 1536\end{verbatim} 1537\end{holboxed} 1538 1539\noindent Di fatto, \ml{new\_recursive\_definition} gestisce 1540definizioni ricorsive primitive su un range di tipi, non solo sui 1541numeri naturali. Per i dettagli, si veda la documentazione \REFERENCE. 1542 1543In modo ancora pi� conveniente, la funzione \ml{Define} (si veda 1544la Sezione~\ref{sec:high-level-proof-steps}) supporta la ricorsione 1545primitiva, insieme con altri stili di ricorsione, e non richiede 1546all'utente di citare l'assioma di ricorsione primitiva. Pu�, tuttavia, 1547richiedere di eseguire dimostrazioni di terminazione; fortunatamente, non � necessario 1548fare queste dimostrazioni per le ricorsioni primitive. 1549 1550\subsubsection{Scelta dipendente e benfondatezza} 1551\label{prim-rec-conseq} 1552 1553Il teorema di ricorsione primitiva � utile oltre il suo scopo principale di 1554giustificare le definizioni ricorsive. Per esempio, la teoria 1555\theoryimp{prim\_rec} dimostra l'Assioma di Scelta Dipendente ({\small\verb+DC+}). 1556 1557\begin{hol} 1558\index{assioma di scelta dipendente (DC)@assioma di scelta dipendente (\ml{DC})} 1559\index{assiomi!di scelta} 1560\begin{verbatim} 1561 DC |- !P R a. 1562 P a /\ (!x. P x ==> ?y. P y /\ R x y) 1563 ==> 1564 ?f. (f 0 = a) /\ !n. P (f n) /\ R (f n) (f (SUC n)) 1565\end{verbatim} 1566\end{hol} 1567 1568La dimostrazione usa {\small\verb+SELECT_AX+}. Il teorema {\small\verb+DC+} 1569� utile quando si desidera costruire una funzione che ha una certa 1570propriet� da una relazione. Per esempio, un modo di definire la 1571benfondatezza di una relazione $R$ � quello di dire che non ha infinite 1572$R$ catene discendenti. 1573% 1574\begin{hol} 1575\index{benfondata@\ml{benfondata}} 1576\begin{verbatim} 1577 wellfounded_def 1578 |- wellfounded (R:'a->'a->bool) = ~?f. !n. R (f (SUC n)) (f n) 1579 1580 WF_IFF_WELLFOUNDED 1581 |- !R. WF R = wellfounded R 1582\end{verbatim} 1583\end{hol} 1584Per mezzo dell'uso di {\small\verb+DC+}, questo enunciato pu� essere dimostrato 1585essere uguale alla nozione di benfondatezza {\small\verb+WF+} 1586(cio�, che ogni insieme ha un elemento $R$-minimale) definita nella teoria 1587\theoryimp{relation}. 1588 1589Nella teoria \theoryimp{prim\_rec} sono anche dimostrati teoremi che affermano la benfondatezza della relazione di predecessore e 1590della relazione minore-di, esattamente come la benfondatezza delle funzioni 1591di misura. 1592 1593\begin{hol} 1594\index{WF_PRED@\ml{WF\_PRED}} 1595\index{WF_LESS@\ml{WF\_LESS}} 1596\index{measure_def@\ml{measure\_def}} 1597\index{WF_measure@\ml{WF\_measure}} 1598\begin{verbatim} 1599 WF_PRED |- WF (\x y. y = SUC x) 1600 WF_LESS |- WF $< 1601 1602 measure_def |- measure = inv_image $< 1603 measure_thm |- !f x y. measure f x y = f x < f y 1604 WF_measure |- !m. WF (measure m) 1605\end{verbatim} 1606\end{hol} 1607 1608 1609\subsection{Aritmetica} 1610\index{aritmetica, la teoria HOL della@aritmetica, la teoria \HOL{} della} 1611 1612La teoria \HOL{} \theoryimp{arithmetic} contiene le definizioni ricorsive 1613primitive, dei seguenti operatori aritmetici standard. 1614 1615\begin{hol} 1616\index{ADD@\ml{ADD}} 1617\index{SUB@\ml{SUB}} 1618\index{MULT@\ml{MULT}} 1619\index{EXP, la costante HOL@\holtxt{EXP}, la costante \HOL{}} 1620\index{ sottrazione, nella logica HOL@\holtxt{-} (sottrazione, nella logica \HOL{})} 1621\index{ moltiplicazione, nella logica HOL@\holtxt{*} (moltiplicazione, nella logica \HOL{})} 1622\index{ esponenziazione, nella logica HOL@\holtxt{**} (esponenziazione, nella logica \HOL{})} 1623\begin{verbatim} 1624 ADD |- (!n. 0 + n = n) /\ 1625 (!m n. (SUC m) + n = SUC(m + n)) 1626 1627 SUB |- (!m. 0 - m = 0) /\ 1628 (!m n. (SUC m) - n = if m < n then 0 else SUC(m - n)) 1629 1630 MULT |- (!n. 0 * n = 0) /\ 1631 (!m n. (SUC m) * n = (m * n) + n) 1632 1633 EXP |- (!m. m EXP 0 = 1) /\ 1634 (!m n. m EXP (SUC n) = m * (m EXP n)) 1635\end{verbatim} 1636\end{hol} 1637% 1638Si noti che \holtxt{EXP} � un infisso. La notazione infissa 1639\holtxt{**} pu� essere usata al posto di \holtxt{EXP}. Cos� 1640(\holtxt{x EXP y}) significa $x^y$, e lo stesso vale per (\holtxt{x ** y}). 1641 1642\paragraph{Operatori di confronto} 1643 1644Un completo insieme di operatori di confronto � definito in termini di \verb+<+. 1645 1646\begin{hol} 1647\index{ maggiore di, nella logica HOL@\ml{>} (maggiore di, nella logica \HOL{})} 1648\index{ minore o uguale, nella logica HOL@\ml{<=} (minore o uguale, nella logica \HOL{})} 1649\index{ maggiore o uguale, nella logica HOL@\ml{>=} (maggiore o uguale, nella logica \HOL{})} 1650\begin{verbatim} 1651 GREATER_DEF |- !m n. m > n = (n < m) 1652 LESS_OR_EQ |- !m n. m <= n = (m < n \/ (m = n)) 1653 GREATER_OR_EQ |- !m n. m >= n = (m > n \/ (m = n)) 1654\end{verbatim} 1655\end{hol} 1656 1657\paragraph{Divisione e modulo} 1658 1659Per introdurre gli operatori divisione ({\small\verb+DIV+}, infisso) e 1660modulo ({\small\verb+MOD+}, infisso) � usata una specifica di costante, insieme con le loro 1661propriet� caratterizzanti. 1662\begin{hol} 1663\index{MOD, la costante HOL@\ml{MOD}, la costante \HOL{}} 1664\index{DIV, la costante HOL@\ml{DIV}, la costante \HOL{}} 1665\begin{verbatim} 1666 DIVISION 1667 |- !n. 0 < n ==> !k. (k = ((k DIV n) * n) + (k MOD n)) /\ (k MOD n) < n 1668\end{verbatim} 1669\end{hol} 1670 1671\paragraph{Pari e dispari} 1672 1673Le propriet� di un numero di essere pari o dispari sono definite ricorsivamente. 1674% 1675\begin{hol} 1676\index{EVEN, la costante HOL@\ml{EVEN}, la costante \HOL{}} 1677\index{ODD, la costante HOL@\ml{ODD}, la costante \HOL{}} 1678\begin{verbatim} 1679 EVEN |- (EVEN 0 = T) /\ !n. EVEN (SUC n) = ~EVEN n 1680 1681 ODD |- (ODD 0 = F) /\ !n. ODD (SUC n) = ~ODD n 1682\end{verbatim} 1683\end{hol} 1684 1685\paragraph{Massimo e minimo} 1686 1687Il minimo e il massimo di due numeri sono definiti nel modo usuale. 1688% 1689\begin{hol} 1690\index{MIN, la costante HOL@\ml{MIN}, la costante \HOL{}} 1691\index{MAX, la costante HOL@\ml{MAX}, la costante \HOL{}} 1692\begin{verbatim} 1693 MAX_DEF |- !m n. MAX m n = (if m < n then n else m) 1694 MIN_DEF |- !m n. MIN m n = (if m < n then m else n) 1695\end{verbatim} 1696\end{hol} 1697 1698\paragraph{Fattoriale} 1699\index{FACT, la costante HOL@\ml{FACT}, la costante \HOL{}} 1700 1701Il fattoriale di un numero � una definizione ricorsiva primitiva. 1702% 1703\begin{hol} 1704\begin{verbatim} 1705 FACT |- (FACT 0 = 1) /\ !n. FACT (SUC n) = SUC n * FACT n 1706\end{verbatim} 1707\end{hol} 1708 1709\paragraph{Iterazione di funzione} 1710\index{FUNPOW, la costante HOL@\ml{FUNPOW}, la costante \HOL{}} 1711 1712L'applicazione iterata $f^n x$ di una funzione $f : \alpha \to 1713\alpha$ � definita per ricorsione primitiva. La definizione 1714(\ml{FUNPOW}) � tail-recursive, il che pu� essere scomodo per ragionarci 1715sopra. Una caratterizzazione alternativa (\ml{FUNPOW\_SUC}) pu� essere pi� facile 1716da applicare quando si fanno delle dimostrazioni. 1717% 1718\begin{hol} 1719\begin{verbatim} 1720 FUNPOW 1721 |- (!f x. FUNPOW f 0 x = x) /\ 1722 (!f n x. FUNPOW f (SUC n) x = FUNPOW f n (f x)) 1723 FUNPOW_SUC 1724 |- !f n x. FUNPOW f (SUC n) x = f (FUNPOW f n x) 1725\end{verbatim} 1726\end{hol} 1727 1728\medskip 1729 1730Su questa base, quando � eseguito il build di \HOL{} una serie \adhoc\ ma utile di pi� duecentocinquanta 1731teoremi elementari sono dimostrati 1732e archiviati nella teoria \theoryimp{arithmetic}. Per una lista 1733completa dei teoremi disponibili, si veda \REFERENCE. Si veda inoltre 1734la Sezione~\ref{sec:while-loops} per la discussione dell'operatore 1735\holtxt{LEAST}, che restituisce il pi� piccolo numero che soddisfa un predicato. 1736 1737\subsubsection{Informazioni sulla grammatica} 1738 1739La seguente tabella da lo status di parsing delle costanti 1740aritmetiche. 1741 1742\begin{center} 1743{\small 1744\begin{tabular}{@{}ccc} 1745Operatore & Forza & Associativit� \\ \hline 1746\holtxt{>=} & 450 & nessuna \\ 1747\holtxt{<=} & 450 & nessuna \\ 1748\holtxt{>} & 450 & nessuna \\ 1749\holtxt{<} & 450 & nessuna \\ 1750\holtxt{+} & 500 & sinistra \\ 1751\holtxt{-} & 500 & sinistra \\ 1752\holtxt{*} & 600& sinistra \\ 1753\holtxt{DIV} & 600 & sinistra \\ 1754\holtxt{MOD} & 650 & sinistra \\ 1755\holtxt{EXP} & 700 & destra \\ 1756\end{tabular}} 1757\end{center} 1758 1759\subsection{Numerali}\label{sec:numerals} 1760 1761Il tipo \ml{num} 1762\index{num, il tipo ... nella logica \HOL{}@\ml{num}, il tipo ... nella logica \HOL{}} 1763di solito � pensato essere fornito di una collezione infinita di 1764numerali: \ml{1}, \ml{2}, \ml{3}, \etc. Tuttavia, la logica \HOL{} non ha 1765alcun modo di definire tali famiglie infinite di costanti; piuttosto, tutti 1766i numerali diversi da $0$ sono di fatto costruiti dalle costanti 1767introdotte dalle seguenti definizioni: 1768 1769\begin{verbatim} 1770 NUMERAL_DEF |- !x. NUMERAL x = x 1771 1772 BIT1 |- !n. BIT1 n = n + (n + SUC 0) 1773 BIT2 |- !n. BIT2 n = n + (n + SUC(SUC 0)) 1774 1775 ALT_ZERO |- ZERO = 0 1776\end{verbatim} 1777 1778\noindent Per esempio, il numerale $5$ � rappresentato dal termine 1779\[ 1780 \ml{NUMERAL}(\ml{BIT1}(\ml{BIT2}\;\ml{ZERO})) 1781\] 1782e il parser e il pretty-printer di \HOL{} fanno apparire tali termini come 1783numerali. Questa rappresentazione binaria per i numerali permette un 1784calcolo asintoticamente efficiente. I teoremi che supportano i calcoli 1785aritmetici sui numerali si possono trovare nella teoria 1786\theoryimp{numeral}; questi sono meccanizzati dalla libreria \verb+reduce+. Cos�, 1787i calcoli aritmetici sono eseguiti per passi deduttivi in \HOL. Per 1788esempio il seguente calcolo di $2 ^{(1023 + 14)/9}$ richiede 1789approssimativamente 4,200 passi d'inferenza primitiva e si completa in 30 1790milli-secondi. 1791% 1792\setcounter{sessioncount}{0} 1793\begin{session} 1794\begin{verbatim} 1795- reduceLib.REDUCE_CONV ``2 EXP ((1023 + 14) DIV 9)``; 1796 1797> val it = |- 2 ** ((1023 + 14) DIV 9) = 41538374868278621028243970633760768 1798\end{verbatim} 1799\end{session} 1800 1801\paragraph {Costruzione dei numerali} 1802\index{numerali, nella logica HOL@numerali, nella logica \HOL{}!costruzione dei} 1803 1804I numerali si possono naturalmente costruire usando\linebreak \ml{mk\_comb}, e si possono scomporre con 1805\ml{dest\_comb}; comunque, un'interfaccia pi� conveniente per questa 1806funzionalit� � fornita dalle funzioni \ml{mk\_numeral}, 1807\ml{dest\_numeral}, e \ml{is\_numeral} (che si trovano nella structure 1808\ml{numSyntax}). Questi entry-point fanno uso di una structure \ML 1809\ml{Arbnum} che implementa numeri di precisione arbitraria {\verb+num+}. La 1810seguente sessione mostra come i numerali \HOL{} sono costruiti da elementi del 1811tipo \verb+num+ e come i numerali sono de-costruiti. La structure 1812{\small\verb+Arbnum+} fornisce una collezione completa di operazioni 1813aritmetiche, che usano i nomi usuali per le operazioni, ad esempio \verb|+|, 1814\verb|*|, \verb|-|, ecc. 1815 1816\begin{session} 1817\begin{verbatim} 1818- numSyntax.mk_numeral 1819 (Arbnum.fromString "3432432423423423234"); 1820> val it = ``3432432423423423234`` : term 1821 1822- numSyntax.dest_numeral it; 1823> val it = 3432432423423423234 : num 1824 1825- Arbnum.+(it,it); 1826> val it = 6864864846846846468 : num 1827\end{verbatim} 1828\end{session} 1829 1830\paragraph{I numerali e il parser} 1831% 1832\index{parsing, della logica HOL@parsing, della logica \HOL{}!di numerali} 1833\index{token!parsing dei numerali} 1834\index{numerali, nella logica HOL@numerali, nella logica \HOL{}!parsing dei} 1835% 1836Le sequenze semplici di cifre sono rese dal parser come numeri decimali, ma il parser 1837supporta anche l'input di numeri in notazione binaria, ottale ed 1838esadecimale. I numeri possono essere scritti in forma binaria ed esadecimale aggiungendo ad essi 1839come prefisso le stringhe \holtxt{0b} e \holtxt{0x} rispettivamente. Le 1840`cifre' A--F nei numeri esadecimali possono essere scritte con le lettere maiuscole o 1841minuscole. I numeri binari hanno le loro cifre pi� significative pi� a sinistra. Ai 1842fini della retro-compatibilit� i numeri ottali non sono 1843abilitati di default, ma se la reference 1844\ml{base\_tokens.allow\_octal\_input} � impostata a \ml{true}, i numeri 1845ottali sono quelli che appaiono con gli zero in testa. 1846 1847Infine, tutti i numeri possono essere intervallati da caratteri di underscore 1848(\ml{\_}). Questi possono essere usati per raggruppare le cifre per aggiungere leggibilit� 1849e non hanno alcun effetto semantico. 1850 1851Cos� 1852\begin{session} 1853\begin{verbatim} 1854- ``0xAA``; 1855> val it = ``170`` : term 1856 1857- ``0b1010_1011``; 1858> val it = ``171`` : term 1859 1860- base_tokens.allow_octal_input := true; 1861> val it = () : unit 1862 1863- ``067``; 1864> val it = ``55`` : term 1865\end{verbatim} 1866\end{session} 1867 1868\paragraph{Numerali e numeri di Peano} 1869 1870I numerali sono collegati ai numeri costruiti da \holtxt{0} e \holtxt{SUC} 1871attraverso la regola d'inferenza derivata \ml{num\_CONV}, che si trova 1872nella libreria \ml{numLib}. 1873 1874\begin{holboxed} 1875\index{num_CONV@\ml{num\_CONV}|pin} 1876\begin{verbatim} 1877 num_CONV : term -> thm 1878\end{verbatim} 1879\end{holboxed} 1880 1881\noindent \ml{num\_CONV} pu� essere usata per generare l'equazione 1882`\ml{SUC}' per qualsiasi numerale diverso da zero. Per esempio: 1883 1884\begin{session} 1885\begin{verbatim} 1886- load "numLib"; open numLib; 1887 1888- num_CONV ``2``; 1889> val it = |- 2 = SUC 1 : thm 1890 1891- num_CONV ``3141592653``; 1892> val it = |- 3141592653 = SUC 3141592652 : thm 1893\end{verbatim} 1894\end{session} 1895 1896\noindent La funzione \ml{num\_CONV} funziona puramente per inferenza. 1897 1898\subsubsection{Overloading degli operatori aritmetici} 1899\label{arith-overloading} 1900 1901Quando sono caricate altre teorie numeriche (come quelle per i reali o 1902gli interi), i numerali sono sottoposti all'overloading cos� che il numerale {\small\verb+1+} pu� 1903stare di fatto per un numero naturale, un intero o un valore reale. Il 1904parser ha un passo di risoluzione dell'overloading in cui tenta di 1905determinare il tipo corrente da dare a un numero. Per esempio, nella 1906seguente sessione, la teoria degli interi � caricata, dopo di che il 1907numerale \verb+2+ � considerato essere un intero. 1908% 1909\begin{session} 1910\begin{verbatim} 1911- load "integerTheory"; 1912> val it = () : unit 1913 1914- ``2``; 1915<<HOL message: more than one resolution of overloading was possible.>> 1916> val it = `2` : term 1917 1918- type_of it; 1919> val it = `:int` : hol_type 1920\end{verbatim} 1921\end{session} 1922 1923Al fine di specificare in modo preciso il tipo desiderato, l'utente pu� usare dei suffissi 1924di un singolo carattere (`\ml{n}' per i numeri naturali, e `\ml{i}' per 1925gli interi): 1926\begin{session} 1927\begin{verbatim} 1928- type_of ``2n``; 1929> val it = `:num` : hol_type 1930 1931- type_of ``42i``; 1932> val it = `:int` : hol_type 1933\end{verbatim} 1934\end{session} 1935 1936Un letterale numerico per un tipo \HOL{} diverso da \verb+num+, come 1937\verb+42i+, � rappresentato dall'applicazione di una funzione 1938d'\emph{iniezione} di tipo {\small\verb+num -> ty+} per un 1939numerale. La funzione di iniezione � differente per ogni tipo 1940{\small\verb+ty+}. Si veda la Sezione \ref{integers} per un'ulteriore discussione. 1941 1942Le funzioni {\verb+mk_numeral+}, {\verb+dest_numeral+}, e 1943{\verb+is_numeral+} funzionano solo per numerali, e per letterali 1944numerici con suffissi di un carattere diverso da {\small\verb+n+}. Per 1945informazioni su come installare nuovi suffissi di un carattere, si consulti la 1946voce \ml{add\_numeral\_form} in \REFERENCE. 1947 1948\subsection{Interi} 1949\label{integers} 1950\index{interi, la teoria HOL degli@interi, la teoria \HOL{} degli} 1951 1952In \HOL{} c'� un'estesa teoria degli interi. Il tipo degli interi 1953� costruito come un quoziente su coppie di numeri naturali. E' definita 1954una collezione standard di operatori. Questi sono degli overload con 1955operazioni analoghe sui numeri naturali, e sui numeri reali. 1956Le costanti definite nella teoria degli interi includono quelle che si trovano nella 1957seguente tabella. 1958 1959\begin{center} 1960{\small 1961\begin{tabular}{@{}cccc} 1962Costante & Simbolo sottoposto a overload & Forza & Associativit� \\ \hline 1963{\small\verb+int_ge+} &{\small\verb+>=+} & 450 & nessuna \\ 1964{\small\verb+int_le+} &{\small\verb+<=+} & 450 & nessuna \\ 1965{\small\verb+int_gt+} &{\small\verb+>+} & 450 & nessuna \\ 1966{\small\verb+int_lt+} &{\small\verb+<+} & 450 & nessuna \\ 1967{\small\verb+int_add+} &{\small\verb%+%} & 500 & sinistra \\ 1968{\small\verb+int_sub+} &{\small\verb%-%} & 500 & sinistra \\ 1969{\small\verb+int_neg+} &{\small\verb%~%} & 900 & vero prefisso \\ 1970{\small\verb+int_mul+} &{\small\verb%*%} & 600 & sinistra \\ 1971{\small\verb%/%} & & 600 & sinistra \\ 1972{\small\verb+%+} & & 650 & sinistra \\ 1973{\small\verb+int_exp+} &{\small\verb%**%} & 700 & destra \\ 1974{\small\verb+int_of_num+} &{\small\verb%&%} & & prefisso \\ 1975\end{tabular}} 1976\end{center} 1977 1978Il simbolo sottoposto a overload {\small\verb+& : num -> int+} denota la 1979funzione d'iniezione dai numeri naturali agli interi. La seguente 1980sessione illustra come sono trattati l'overloading e i letterali interi. 1981 1982\setcounter{sessioncount}{0} 1983\begin{session} 1984\begin{verbatim} 1985Term `1i = &(1n + 0n)`; 1986> val it = `1 = & (1 + 0)` : term 1987 1988- show_numeral_types := true; 1989> val it = () : unit 1990 1991- Term `&1 = &(1n + 0n)`; 1992<<HOL message: more than one resolution of overloading was possible.>> 1993> val it = `1i = & (1n + 0n)` : Term.term 1994\end{verbatim} 1995\end{session} 1996 1997 1998\subsection{Numeri razionali}\label{rationals} 1999\index{numeri razionali, la teoria HOL dei@razionali, la teoria \HOL{} dei|(} 2000 2001Il tipo dei razionali � costruito come un quoziente di coppie ordinate di 2002interi (il numeratore e il denominatore di una frazione) il cui secondo 2003componente non deve essere zero. Per rendere le cose pi� semplici nella teoria \HOL\, 2004il segno di un numero razionale � sempre spostato al numeratore. 2005Cos�, il denominatore � sempre positivo. 2006 2007E' definita una collezione di operatori, che sono sottoposti a overload con 2008operazioni analoghe sugli interi. Questi includono quelli che si trovano nella 2009seguente tabella. L'iniezione dai numeri naturali � supportata 2010dal simbolo sottoposto a overload {\small\verb+& : num -> rat+} e dal 2011suffisso {\small\verb+q+}. 2012 2013 2014\begin{center} 2015{\small 2016\begin{tabular}{@{}cccc} 2017Costante & Simbolo sottoposto a overload & Forza & Associativit� \\ \hline 2018{\small\verb+rat_geq+} &{\small\verb+>=+} & 450 & nessuna \\ 2019{\small\verb+rat_leq+} &{\small\verb+<=+} & 450 & nessuna \\ 2020{\small\verb+rat_gre+} &{\small\verb+>+} & 450 & nessuna \\ 2021{\small\verb+rat_les+} &{\small\verb+<+} & 450 & nessuna \\ 2022{\small\verb+rat_add+} &{\small\verb%+%} & 500 & sinistra \\ 2023{\small\verb+rat_sub+} &{\small\verb%-%} & 500 & sinistra \\ 2024{\small\verb+rat_ainv+} &{\small\verb%~%} & 900 & vero prefisso \\ 2025{\small\verb+rat_minv+} & & & \\ 2026{\small\verb+rat_mul+} &{\small\verb%*%} & 600 & sinistra \\ 2027{\small\verb+rat_div+} &{\small\verb%/%} & 600 & sinistra \\ 2028{\small\verb+rat_of_num+} &{\small\verb%&%} & & \\ 2029\end{tabular}} 2030\end{center} 2031 2032I teoremi nella teoria dei numeri razionali includono le propriet� del campo, 2033le regole aritmetiche la manipolazione delle (in)equazioni e la loro riduzione a 2034(in)equazioni tra interi, le propriet� delle relazioni minore-di e la 2035densit� dei numeri razionali. Per i dettagli, si consulti \REFERENCE\ e i 2036file sorgenti. 2037 2038\index{numeri razionali, la teoria HOL dei@razionali, la teoria \HOL{} dei|)} 2039 2040\subsection{Numeri reali}\label{reals} 2041\index{numeri reali, la teoria HOL dei@numeri reali, la teoria \HOL{} dei|(} 2042 2043C'� un'estesa collezione di teorie che costituisce lo 2044sviluppo dei numeri reali e dell'analisi in HOL, dovuta a John Harrison 2045\cite{jrh:thesis}. Daremo solo una panoramica approssimativa dello 2046sviluppo; il lettore interessato dovrebbe consultare \REFERENCE\ e 2047la tesi di Harrison. 2048 2049Gli assiomi per i numeri reali sono derivati dai `mezzi reali' che 2050sono costruiti dai `mezzi razionali'. Questa parte dello sviluppo 2051� registrata in {\small\verb+hratTheory+} e 2052{\small\verb+hrealTheory+}, ma non � usata una volta che i reali sono stati 2053costruiti. Gli assiomi reali sono derivati nella teoria 2054{\small\verb+realaxTheory+}. Una collezione standard di operatori sui 2055reali, e di teoremi che li riguardano, si trova in {\small\verb+realaxTheory+} 2056and {\small\verb+realTheory+}. Gli operatori e il loro status di parsing sono 2057elencati nella seguente tabella. 2058 2059\begin{center} 2060{\small 2061\begin{tabular}{@{}cccc} 2062Constante & Simbolo sottoposto a overload & Forza & Associativit� \\ \hline 2063{\small\verb+real_ge+} &{\small\verb+>=+} & 450 & nessuna \\ 2064{\small\verb+real_lte+} &{\small\verb+<=+} & 450 & nessuna \\ 2065{\small\verb+real_gt+} &{\small\verb+>+} & 450 & nessuna \\ 2066{\small\verb+real_lt+} &{\small\verb+<+} & 450 & nessuna \\ 2067{\small\verb+real_add+} &{\small\verb%+%} & 500 & sinistra \\ 2068{\small\verb+real_sub+} &{\small\verb%-%} & 500 & sinistra \\ 2069{\small\verb+real_neg+} &{\small\verb%~%} & 900 & trueprefix \\ 2070{\small\verb+real_mul+} &{\small\verb%*%} & 600 & sinistra \\ 2071{\small\verb+real_div+} & {\small\verb%/%} & 600 & sinistra \\ 2072{\small\verb+pow+} & &700 & right \\ 2073{\small\verb+real_of_num+} &{\small\verb%&%} & & prefisso \\ 2074\end{tabular}} 2075\end{center} 2076 2077Sulla base di {\small\verb+realTheory+}, � costruita la seguente sequenza di 2078teorie: 2079 2080\begin{description} 2081\item [topology] Topologie e spazi metrici, inclusa la metrica sulla 2082linea reale. 2083\item [nets] Reti di convergenza Moore-Smith, e casi speciali come 2084le sequenze. 2085\item [seq] Sequenze e serie di numeri reali. 2086\item [lim] Limiti, continuit� e differenziazione. 2087\item [powser] Serie potenza. 2088\item [transc] Funzioni trascendenti, \emph{ad esempio}, exp, sin, 2089cos, ln, root, sqrt, pi, tan, asn, acs, atn. Inoltre la misura integrale 2090Kurzweil-Henstock il teorema fondamentale del calcolo, e il teorema di 2091McLaurin 2092 2093\end{description} 2094\index{numeri reali, la teoria HOL dei@numeri reali, la teoria \HOL{} dei|)} 2095 2096\index{numeri complessi, la teoria HOL dei@numeri complessi, la teoria \HOL{} dei} 2097\noindent 2098\HOL{} include anche una teoria di base dei numeri complessi (\ml{complexTheory}), dove il tipo \holtxt{complex} � un'abbreviazione di tipo per una coppia di numeri reali. 2099Il valore $\sqrt{-1}$ � la costante \HOL{} \holtxt{i}. 2100I numerali sono supportati (con il suffisso \holtxt{c} disponibile per forzare il parsing dei numerali come numeri complessi). 2101Sono definite le operazioni aritmetiche standard, con dimostrati gli appropriati teoremi che le riguardano. 2102 2103\subsection{Teoria della probabilit�}\label{prob} 2104\index{probabilit�, la teoria HOL della@probabilit�, la teoria \HOL{} della} 2105 2106Una costruzione fondazionale della teoria della probabilit� sviluppata da Joe 2107Hurd~\cite{hurd-thesis}. Per prima cosa � definito un tipo di sequenze booleane 2108per modellare una sequenza infinita di lanci di monete. Poi � formalizzata 2109una funzione di probabilit� che prende come input un insieme di sequenze 2110booleane, e restituisce un numero reale tra 0 e 1. Sfortunatamente 2111non a tutti gli insiemi pu� essere assegnata una probabilit� (il paradosso di 2112Banach-Tarski), piuttosto gli insiemi a cui pu� essere assegnata una probabilit� sono 2113chiamati \emph{insiemi misurabili}, e anche questi sono formalizzati nella 2114teoria HOL. 2115 2116Su questa base, la teoria della probabilit� � usata per definire 2117una funzione di esempio che prende una sequenza infinita di lanci di monete e 2118un intero positivo $N$, e restituisce un intero $n$ nel range $0\le 2119n < N$, selezionato uniformemente a caso tra le scelte possibili. Questa 2120funzione di esempio per la distribuzione uniforme � usata pi� avanti per verificare 2121il test di primalit� di Miller-Rabin. 2122 2123\subsection{Vettori di bit} 2124\label{sec:bit-vectors} 2125\index{bit vectors, the HOL theory of@bit vectors, the \HOL{} theory of|(} 2126 2127{ 2128\newcommand{\fcp}[2]{\ty{#1}[\ty{#2}]} 2129\newcommand{\worda}{\fcp{\bool}{\ensuremath\alpha}} 2130\newcommand{\wordb}{\fcp{\bool}{\ensuremath\beta}} 2131\newcommand{\wordc}{\fcp{\bool}{\ensuremath\gamma}} 2132\newcommand{\rarr}{\ensuremath\rightarrow} 2133\newcommand{\hash}{\,\holtxt{\#}\,} 2134\newcommand{\oo}[2]{\mbox{\holtxt{#1\,'\,#2}}} 2135 2136\HOL{} fornisce una teoria di vettori du bit, o parole di $n$-bit. Per esempio, nelle architetture 2137informatiche si trovano: 2138byte/octet ($n = 8$), mezze-parole ($n = 16$), parole ($n = 32$) e parole-lunghe 2139($n = 64$). Nella teoria \theoryimp{words}, i vettori di bit sono rappresentati come 2140\emph{prodotti cartesiani finiti}: a una parola di $n$-bit � dato il tipo $\worda$ 2141dove la \emph{dimensione} del tipo $\alpha$ determina la lunghezza $n$ della parola. Questo 2142approccio viene da un'idea di John Harrison, che fu presentata al TPHOLs del 21432005\footnote{La teoria attuale sussume teorie di parola precedenti -- si � evoluta da uno sviluppo basato su una costruzione di classi di equivalenza. La teoria di parola di Wai Wong, che era basata sulla teoria \ml{rich\_list} di Paul Curzon, non � pi� distribuita con HOL. I principali vantaggi della teoria attuale sono che c'� un'unica teoria per tutte le dimensioni di parole e che non sono richiesti effetti secondari della lunghezza delle parole.} 2144 2145\subsubsection{Prodotti cartesiani finiti} 2146 2147La teoria \HOL{} \theoryimp{fcp} introduce un operatore di tipo infisso 2148\holtxt{**}, che � usato per rappresentare prodotti cartesiani finiti\footnote{La teoria dei 2149prodotti cartesiani finiti � stata portata da HOL Light.}. Il tipo \holtxt{'a ** 'b}, o equivalentemente \fcp{'a}{'b}, � concettualmente equivalente a: 2150\begin{hol} 2151$\underbrace{\ty{'a}\;\hash\;\ty{'a}\;\hash\;\cdots\;\hash\;\ty{'a}}_{\holtxt{dimindex('b)}}$ 2152\end{hol} 2153dove \holtxt{dimindex('b)} � la cardinalit� di \holtxt{univ(:'b)} quando \ty{'b} � finito e uno quando � infinito. Cos�, \fcp{'a}{\num} � analogo a \ty{'a}, e \fcp{'a}{\bool} � analogo a \ty{'a}\hash\ty{'a}. Sono supportati nomi di tipo numerici, cos� si pu� lavorare liberamente con insiemi indicizzati di qualsiasi dimensione, ad esempio il tipo \ty{32} ha trentadue elementi e \fcp{\bool}{32} rappresenta parole di 32-bit. 2154 2155Si accede alle \emph{componenti} di un prodotto cartesiano finito con una 2156funzione di indicizzazione 2157\begin{hol} 2158\begin{alltt} 2159 fcp_index : \fcp{'a}{'b}\rarr\num\rarr\ty{'a} 2160\end{alltt} 2161\end{hol} 2162che tipicamente � scritta con un apostrofo infisso: 2163\oo{x}{i} denota il valore del vettore \holtxt{x} alla posizione \holtxt{i}. 2164Tipicamente, gli indici sono vincolati ad essere minori della dimensione di \ty{'b}. 2165 2166Il seguente teorema mostra che due prodotti cartesiani \holtxt{x} e 2167\holtxt{y} sono uguali se, e solo se, tutte le loro componenti \oo{x}{i} e 2168\oo{y}{i} sono uguali: 2169\begin{hol} 2170\begin{verbatim} 2171CART_EQ: |- !x y. (x = y) = !i. i < dimindex (:'a) ==> (x ' i = y ' i) 2172\end{verbatim} 2173\end{hol} 2174 2175Al fine di costruire prodotti cartesiani, la teoria \theoryimp{fcp} introduce un 2176binder \holtxt{FCP}, che � caratterizzato dai seguenti teoremi: 2177\begin{hol} 2178\begin{verbatim} 2179FCP_BETA: |- !i. i < dimindex (:'a) ==> ($FCP g ' i = g i) 2180FCP_ETA: |- !x. (FCP i. x ' i) = x 2181$ 2182\end{verbatim} 2183\end{hol} 2184Il teorema \ml{FCP\_BETA} mostra che i componenti di \holtxt{\$FCP g} sono 2185determinati dalla funzione \holtxt{g:\num\rarr\ty{'a}}. Il teorema 2186\ml{FCP\_ETA} mostra che si pu� eliminare un binding quando tutte le componenti 2187sono identiche a quelle di \holtxt{x}. 2188Questi due teoremi, insieme con \ml{CART\_EQ}, si possono trovare nel 2189frammento \ml{fcpLib.FCP\_ss} di \emph{simpset}. 2190 2191I prodotti cartesiani finiti forniscono un buon mezzo per modellare parole di $n$-bit. Vale a 2192dire, il tipo \fcp{bool}{'a} pu� rappresentare una parola binaria la cui lunghezza $n$ 2193corrisponde alla dimensione del tipo \ty{'a}. Il binder \holtxt{FCP} 2194fornisce un mezzo flessibile per definire parole -- si pu� fornire una funzione 2195\holtxt{f:\num\rarr\bool} che da i valori bit della parola, a ciascuno dei quali si pu� accedere usando la mappa d'indicizzazione \holtxt{fcp\_index}. 2196 2197\subsubsection{Teoria bit} 2198 2199La teoria \theoryimp{bit} definisce alcune operazioni bit sui numeri naturali, 2200ad esempio \holtxt{BITS}, \holtxt{SLICE}, \holtxt{BIT}, \holtxt{BITWISE} e 2201\holtxt{BIT\_MODIFY}. In questo contesto, i numeri naturali sono trattati come parole binarie di 2202lunghezza slegata. Le operazioni in \theoryimp{bit} principalmente sono definite usando \holtxt{DIV}, \holtxt{MOD} e \holtxt{EXP}. Pe esempio, dalla definizione di \holtxt{BIT}, vale il seguente teorema: 2203\begin{hol} 2204\begin{verbatim} 2205|- !b n. BIT b n = ((n DIV 2 ** b) MOD 2 = 1) 2206\end{verbatim} 2207\end{hol} 2208 2209Questa teoria � usata nello sviluppo della teoria word e fornisce anche 2210un meccanismo per la valutazione efficiente di alcune operazioni su parole attraverso la teoria 2211\theoryimp{numeral\_bit}. 2212 2213\subsubsection{La teoria words} 2214 2215La teoria \theoryimp{words} introduce una selezione di costanti ed operazioni polimorfiche, i cui tipi possono essere istanziati a parole di qualsiasi dimensione. Per esempio, l'addizione word 2216ha il tipo: 2217\begin{hol} 2218+:\worda\rarr\worda\rarr\worda 2219\end{hol} 2220Se \ty{'a} � istanziato a \ty{32} allora questa operazione corrisponde all'addizione 32-bit. 2221Tutti i teoremi circa operazioni word si applicano a word di qualsiasi lunghezza\footnote{Si noti 2222che � impossibile introdurre word di lunghezza zero perch� tutti i tipi 2223devono essere abitati, e di conseguenza la loro dimensione sar� sempre maggiore o uguale a 2224uno.} 2225 2226\paragraph{Alcune operazioni di base} 2227 2228La funzione \holtxt{w2n:\worda\rarr\num} da il valore del numero naturale di una 2229parola. Se $x\in\bools^{\{0, 1, \ldots, n - 1\}}$ � un prodotto cartesiano finito 2230che rappresenta una parola di $n$-bit allora il valore del suo numero naturale �: 2231\[ \mathrm{w2n}(x) = \sum_{i = 0}^{n - 1} \textbf{if } x_i \textbf{ then } 2^i 2232\textbf{ else } 0\ .\] 2233La lunghezza di una parola (il numero $n$) � dato dalla funzione 2234\holtxt{word\_len:\worda\rarr\num}. 2235La funzione \holtxt{n2w:\num\rarr\worda} mappa un numero a una parola ed � 2236definita in \HOL{} da: 2237\begin{hol} 2238\begin{verbatim} 2239|- !n. n2w n = FCP i. BIT i n 2240\end{verbatim} 2241\end{hol} 2242Il suffisso \holtxt{w} � usato per denotare parole letterali, ad esempio 2243\holtxt{255w} � lo stesso di \holtxt{n2w 255}. 2244 2245La funzione \holtxt{w2w:\worda\rarr\wordb} fornisce conversioni da-parola-a-parola (casting): 2246\begin{hol} 2247\begin{verbatim} 2248|- !w. w2w w = n2w (w2n w) 2249\end{verbatim} 2250\end{hol} 2251Se $\beta$ � pi� piccolo di $\alpha$ allora i bit pi� alti di \holtxt{w} saranno 2252persi (esegue un'estrazione di bit), altrimenti la parola pi� lunga avr� lo stesso valore dell'originale (fornendo in effetti zero padding). 2253Tuttavia, se si stesse trattando \holtxt{w} come un numero complemento di due allora la 2254parola dovrebbe essere sign extended, cio� 2255\begin{eqnarray*} 2256\mbox{\small ($-$ve)}\quad 1b_{n-2} \cdots b_0\ \mapsto \ 1 \cdots 1 1 b_{n-2} 2257\cdots b_0 \\ 2258\mbox{\small ($+$ve)}\quad 0b_{n-2} \cdots b_0\ \mapsto \ 0 \cdots 0 0 b_{n-2} 2259\cdots b_0 2260\end{eqnarray*} 2261La funzione \holtxt{sw2sw:\worda\rarr\wordb} fornisce questa versione sign extending di 2262\holtxt{w2w}. 2263 2264E' fornita una collezione di operazioni per mappare da stringhe a liste di numeri (cifre) e vice versa, ad esempio 2265\begin{hol} 2266\begin{verbatim} 2267|- word_to_dec_string 876w = "876" 2268\end{verbatim} 2269\end{hol} 2270e 2271\begin{hol} 2272\begin{verbatim} 2273|- word_to_hex_list 876w = [12; 6; 3] 2274\end{verbatim} 2275\end{hol} 2276Queste funzioni sono versioni specializzate di \holtxt{w2s} e \holtxt{w2l} rispettivamente. 2277 2278\paragraph{Concatenazione} 2279 2280L'operazione \holtxt{word\_concat:\worda\rarr\wordb\rarr\wordc} concatena parole. Si noti che il tipo restituito non � vincolato. Questo significa che due parole di sedici bit possono essere concatenate per dare una parola di qualsiasi lunghezza -- che pu� essere pi� piccola o pi� grande del valore atteso di 32. La funzione correlata \holtxt{word\_join} restituisce una parola della lunghezza attesa, cio� di tipo fcp{\bool}{$\alpha+\beta$}; comunque, l'operazione di concatenazione � pi� utile perch� spesso vogliamo \fcp{\bool}{\ty{32}} e non il logicamente distinto \fcp{\bool}{\ty{16}+\ty{16}}. 2281 2282\paragraph{Parole con e senza segno} 2283 2284Le parole possono essere \emph{viste} sia come aventi segno (usando la rappresentazione 2285in complemento a due) o come non aventi segno. Tuttavia, questo non � 2286reso esplicito all'interno della teoria\footnote{Le parole non sono etichettate come 2287 aventi/non aventi segno. Sono forniti mapping a/da interi (\holtxt{w2i} e 2288 \holtxt{i2w}) nella teoria \theoryimp{integer\_word}.} 2289e tutte le operazioni aritmetiche sono definite usando i numeri 2290naturali, cio� attraverso \holtxt{w2n} e \holtxt{n2w}. In particolare, 2291l'addizione e la moltiplicazione funzionano in modo naturale (hanno la stessa definizione) 2292sotto la rappresentazione in complemento a due. Questo tuttavia non avviene 2293nella conversione da-parola-a-parola, negli ordinamenti, nella divisione e nello shifting 2294a destra, dove sono necessarie le varianti con segno e senza segno. Quando 2295si opera su numeri naturali, alcune delle versioni complemento 2296a due hanno delle presentazioni leggermente innaturali da vedere. Per esempio, 2297con la versione (complemento a due) con segno di ``minore di'' abbiamo 2298\holtxt{255w < (0w:word8)} perch� la parola \holtxt{255w} � di fatto 2299considerata rappresentare l'intero $-1$, mentre la versione 2300senza segno � pi� naturale: \holtxt{0w <+ (255w:word8)}. 2301 2302\paragraph{Operazioni bit field} 2303 2304Sono fornite le operazioni booleane bit field standard, cio� la negazione bitwise 2305(complemento a uno), la congiunzione bitwise, la disgiunzione bitwise e l'or-esclusivo bitwise. Queste funzioni 2306sono definite in modo piuttosto naturale usando il binder prodotto cartesiano; per esempio, 2307la congiunzione bitwise � definita da: 2308\begin{hol} 2309\begin{verbatim} 2310|- !v w. v && w = FCP i. v ' i /\ w ' i . 2311\end{verbatim} 2312\end{hol} 2313C'� anche una collezione di operazioni di \emph{riduzione} parola, che riducono vettori di bit a parole di 1 bit, ad esempio 2314\[ \mathrm{reduce\_and}(x)\;'\; 0= \bigwedge_{i = 0}^{n - 1} x_i\ .\] 2315 2316Le funzioni \holtxt{word\_lsb}, \holtxt{word\_msb} e \holtxt{word\_bit(i)} 2317danno il valore bit di una parola alle posizioni $0$, $n - 1$ e $i$ 2318rispettivamente. Sono fornite quattro operazioni per selezionare bit 2319field, o sotto-parole: \holtxt{word\_bits} (\holtxt{--}), \holtxt{word\_signed\_bits} (\holtxt{---}), \holtxt{word\_slice} (\holtxt{''}) e 2320\holtxt{word\_extract} (\holtxt{><}). Per esempio, \holtxt{word\_bits 4 1} selezioner� quattro bit iniziando dalla posizione bit 1. La funzione slice � una variante in-place 8azzeira i bit fuori dal bit range) e la funzione extract combina \holtxt{word\_bits} con un cast di parola (\holtxt{w2w}). L'operazione \holtxt{word\_signed\_bits} � analoga a \holtxt{word\_bits}, eccetto che segna-estende il bit field. 2321 2322 2323L'operazione \holtxt{bit\_field\_insert} inserisce un bit field. Per esempio, 2324\begin{hol} 2325\begin{verbatim} 2326bit_field_insert 5 2 a b 2327\end{verbatim} 2328\end{hol} 2329� una parola \holtxt{b} con i bit 5--2 sostituiti dai bit 3--0 di \holtxt{a}. 2330 2331L'ordinamento di un bit di parola pu� essere capovolto con \holtxt{word\_reverse}, cio� il bit zero � scambiato con il bit $n - 1$ e cos� via. 2332 2333La funzione 2334\holtxt{word\_modify:(\num\,\rarr\,\bool\,\rarr\,\bool)\,\rarr\,\worda\,\rarr\,\worda} cambia 2335una parola applicando una mappa ad ogni posizione bit. 2336Questa operazione fornisce un meccanismo molto flessibile e conveniente per 2337manipolare parole, as esempio 2338\begin{hol} 2339\holtxt{word\_modify ($\lambda$i b.\,if EVEN i then $\sim$b else b) w} 2340\end{hol} 2341nega i bit di \holtxt{w} che sono nelle posizioni pari. Naturalmente, il 2342binder \holtxt{FCP} fornisce anche un mezzo molto generale per rappresentare parole usando 2343un predicato ad esempio \holtxt{\$FCP ODD} rappresenta una parola dove tutti i bit dispari 2344sono insiemi. 2345 2346\paragraph{Shift} 2347 2348Sono fornite sei tipi di shift: shift logico sinistra/destra (\holtxt{<<} e 2349\holtxt{>>>}), shift aritmetico destro (\holtxt{>>}), ruotare a sinistra/destra 2350(\holtxt{\#<<} e \holtxt{\#>>}) e ruotare a destra propagato di 1 posto 2351(\holtxt{word\_rrx}). Questi shisft sono illustrati nella Figura~\ref{fig:shifts} e sono definiti in un maniera analoga alle operazioni bit field. Per 2352esempio, la rotazione a destra � definita da: 2353 2354\begin{hol} 2355\begin{verbatim} 2356|- !w n. w #>> x = FCP i. w ' (i + x) MOD dimindex (:'a) . 2357\end{verbatim} 2358\end{hol} 2359La rotazione a sinistra di $x$ posti � definita come rotazione a destra di $n - x \bmod n$ 2360posti. 2361 2362\begin{figure} 2363\begin{center} 2364\small 2365\begin{tabular}{ll} 2366\scalebox{.8}{\includegraphics{figs/lsl}} & 2367\scalebox{.8}{\includegraphics{figs/lsr}} \\ 2368(a) Logical shift left: \holtxt{w = v << x}. & (b) Logical shift right: 2369\holtxt{w = v >>> x}. \\[12pt] 2370\scalebox{.8}{\includegraphics{figs/asr}} & 2371\hspace{-5mm}\scalebox{.8}{\includegraphics{figs/ror}} \\ 2372(c) Arithmetic shift right: \holtxt{w = v >> x}. & (d) Rotate right: \holtxt{w 2373= v \#>> x}. \\[12pt] 2374\multicolumn{2}{c}{\scalebox{.8}{\includegraphics{figs/rrx}}} \\ 2375\multicolumn{2}{c}{(e) Rotate right extended by 1 place: \holtxt{(d,w) = 2376word\_rrx (c,v)}.} 2377\end{tabular} 2378\caption{Shift operations.} 2379\label{fig:shifts} 2380\end{center} 2381\end{figure} 2382 2383\paragraph{Aritmetica e ordinamenti} 2384 2385Le operazioni aritmetiche sono: addizione, sottrazione, meno unario (coplemento a 2386due), logaritmo (base-2), moltiplicazione, modulo e divisione (con e senza 2387segno). 2388Queste operazioni sono definite rispetto ai numeri naturali. Per esempio, 2389l'addizione parola � definita da: 2390\begin{hol} 2391\begin{verbatim} 2392|- !v w. v + w = n2w (w2n v + w2n w) 2393\end{verbatim} 2394\end{hol} 2395Il \holtxt{+} sul lato sinistro � un'addizione parola e quello sul lato destro � 2396l'addizione sui numeri naturali. 2397 2398Sono forniti tutti gli ordinamenti parola standard, con le versioni con e senza 2399segno di $<$, $\leq$, $>$ e $\geq$. Le versioni senza segno hanno un suffisso 2400con un pi�; per esempio, \holtxt{<+} � il ``minore di'' senza segno. 2401 2402\paragraph{Costanti} 2403 2404La teoria word definisce anche alcune costanti parola: 2405\begin{center}\small 2406\begin{tabular}{lll} 2407\multicolumn{1}{l}{Costante} & \multicolumn{1}{l}{Valore} & 2408\multicolumn{1}{l}{Binario} \\ 2409\noalign{\smallskip} 2410\hline 2411\noalign{\smallskip} 2412\holtxt{word\_T} or \holtxt{UINT\_MAXw} & $2^l - 1$ & $11\cdots 11$ \\ 2413\holtxt{word\_L} or \holtxt{INT\_MINw} & $2^{l - 1}$ & $10\cdots 00$ \\ 2414\holtxt{word\_H} or \holtxt{INT\_MAXw} & $2^{l - 1} - 1$ & $01\cdots 11$ 2415\end{tabular} 2416\end{center} 2417 2418\paragraph{Elenco di operazioni su vettori di bit} 2419 2420Un elenco di operazioni � fornito nella tabella di sotto. 2421{ 2422\setlength{\tabcolsep}{4pt} 2423\begin{center} 2424\tablefirsthead{% 2425\hline 2426\multicolumn{1}{|c}{Operazione\rule{0pt}{14pt}} & 2427\multicolumn{1}{c}{Simbolo} & 2428Type & 2429\multicolumn{1}{c|}{Descrizione} \\[4pt] 2430\hline} 2431\tablehead{% 2432\hline 2433\multicolumn{4}{|l|}{\small\sl continua dalla pagina precedente}\\ 2434\hline 2435\multicolumn{1}{|c}{Operazione\rule{0pt}{14pt}} & 2436\multicolumn{1}{c}{Simbolo} & 2437Type & 2438\multicolumn{1}{c|}{Descrizione} \\[4pt] 2439\hline} 2440\tabletail{% 2441\hline 2442\multicolumn{4}{|r|}{\small\sl continua sulla pagina successiva}\\ 2443\hline} 2444\tablelasttail{\hline} 2445\small 2446\begin{supertabular}{|l|c|l|l|} 2447\holtxt{n2w} & & \num\rarr\worda & Map from a natural number \\ 2448\holtxt{w2n} & & \worda\rarr\num & Map to a natural number \\ 2449\holtxt{w2w} & & \worda\rarr\wordb & Map word-to-word (unsigned) \\ 2450\holtxt{sw2sw} & & \worda\rarr\wordb & Map word-to-word (signed) \\ 2451\holtxt{w2l} & & \num\rarr\worda\rarr\num~\ty{list} & Map word to digit list \\ 2452\holtxt{l2w} & & \num\rarr\num~\ty{list}\rarr\worda & Map digit list to word \\ 2453\holtxt{w2s} & & \num\rarr(\num\rarr\ty{char})\rarr\worda\rarr\ty{string} & Map word to string \\ 2454\holtxt{s2w} & & \num\rarr(\ty{char}\rarr\num)\rarr\ty{string}\rarr\worda & Map string to word \\ 2455\holtxt{word\_len} & & \worda\rarr\num & The word length \\ 2456\holtxt{word\_lsb} & & \worda\rarr\bool & The least significant bit \\ 2457\holtxt{word\_msb} & & \worda\rarr\bool & The most significant bit \\ 2458\holtxt{word\_bit} & & \num\rarr\worda\rarr\bool & Test bit position \\ 2459\holtxt{word\_bits} & \holtxt{--} & \num\rarr\num\rarr\worda\rarr\worda & Select a bit field \\ 2460\holtxt{word\_signed\_bits} & \holtxt{---} & \num\rarr\num\rarr\worda\rarr\worda & Sign-extend selected bit field \\ 2461\holtxt{word\_slice} & \holtxt{''} & \num\rarr\num\rarr\worda\rarr\worda & Set bits outside field to zero \\ 2462\holtxt{word\_extract} & \holtxt{><} & \num\rarr\num\rarr\worda\rarr\wordb & Extract (cast) a bit field \\ 2463\holtxt{word\_reverse} & & \worda\rarr\worda & Reverse the bit order \\ 2464\holtxt{bit\_field\_insert} & & {\setlength{\tabcolsep}{0pt}\begin{tabular}[t]{ll}\num\rarr\num\rarr\worda\rarr\\\wordb\rarr\wordb\end{tabular}} & Insert a bit field \\ 2465\holtxt{word\_modify} & & {\setlength{\tabcolsep}{0pt}\begin{tabular}[t]{ll}(\num\rarr\bool\rarr\bool)\rarr\\\worda\rarr\worda\end{tabular}} & Apply a function to each bit \\ 2466\holtxt{word\_join} & & \worda\rarr\wordb\rarr\fcp{\bool}{$\alpha+\beta$} & Join words \\ 2467\holtxt{word\_concat} & \holtxt{@@} & \worda\rarr\wordb\rarr\wordc & Concatenate words \\ 2468\holtxt{concat\_word\_list} & & \worda~\ty{list}\rarr\wordb & Concatenate list of words \\ 2469\holtxt{word\_replicate} & & \num\rarr\worda\rarr\wordb & Replicate word \\ 2470\holtxt{word\_or} & \holtxt{||} & \worda\rarr\worda\rarr\worda & Bitwise disjunction \\ 2471\holtxt{word\_xor} & \holtxt{??} & \worda\rarr\worda\rarr\worda & Bitwise exclusive-or \\ 2472\holtxt{word\_and} & \holtxt{\&\&} & \worda\rarr\worda\rarr\worda & Bitwise conjunction \\ 2473\holtxt{word\_nor} & \holtxt{\~{}||} & \worda\rarr\worda\rarr\worda & Bitwise NOR \\ 2474\holtxt{word\_xnor} & \holtxt{\~{}??} & \worda\rarr\worda\rarr\worda & Bitwise XNOR \\ 2475\holtxt{word\_nand} & \holtxt{\~{}\&\&} & \worda\rarr\worda\rarr\worda & Bitwise NAND \\ 2476\holtxt{word\_reduce} & & {\setlength{\tabcolsep}{0pt}\begin{tabular}[t]{ll}(\bool\rarr\bool\rarr\bool)\rarr\\\worda\rarr\fcp{\bool}{1}\end{tabular}} & Word reduction \\ 2477\holtxt{reduce\_or} & & \worda\rarr\fcp{\bool}{1} & Disjunction reduction \\ 2478\holtxt{reduce\_xor} & & \worda\rarr\fcp{\bool}{1} & Exclusive-or reduction \\ 2479\holtxt{reduce\_and} & & \worda\rarr\fcp{\bool}{1} & Conjunction reduction \\ 2480\holtxt{reduce\_nor} & & \worda\rarr\fcp{\bool}{1} & NOR reduction \\ 2481\holtxt{reduce\_xnor} & & \worda\rarr\fcp{\bool}{1} & XNOR reduction \\ 2482\holtxt{reduce\_nand} & & \worda\rarr\fcp{\bool}{1} & NAND reduction \\ 2483\holtxt{word\_{}1comp} & \holtxt{\~} & \worda\rarr\worda & One's complement \\ 2484\holtxt{word\_{}2comp} & \holtxt{-} & \worda\rarr\worda & Two's complement \\ 2485\holtxt{word\_add} & \holtxt{+} & \worda\rarr\worda\rarr\worda & Addition \\ 2486\holtxt{word\_sub} & \holtxt{-} & \worda\rarr\worda\rarr\worda & Subtraction \\ 2487\holtxt{word\_mul} & \holtxt{*} & \worda\rarr\worda\rarr\worda & Multiplication \\ 2488\holtxt{word\_div} & \holtxt{//} & \worda\rarr\worda\rarr\worda & Division (unsigned) \\ 2489\holtxt{word\_sdiv} & \holtxt{/} & \worda\rarr\worda\rarr\worda & Division (signed) \\ 2490\holtxt{word\_mod} & & \worda\rarr\worda\rarr\worda & Modulus \\ 2491\holtxt{word\_log2} & & \worda\rarr\worda & Logarithm base-2 \\ 2492\holtxt{word\_lsl} & \holtxt{<<} & \worda\rarr\num\rarr\worda & Logical shift left \\ 2493\holtxt{word\_lsr} & \holtxt{>>>} & \worda\rarr\num\rarr\worda & Logical shift right \\ 2494\holtxt{word\_asr} & \holtxt{>>} & \worda\rarr\num\rarr\worda & Arithmetic shift right \\ 2495\holtxt{word\_ror} & \holtxt{\#>>} & \worda\rarr\num\rarr\worda & Rotate right \\ 2496\holtxt{word\_rol} & \holtxt{\#<<} & \worda\rarr\num\rarr\worda & Rotate left \\ 2497\holtxt{word\_rrx} & & \bool\#\worda\rarr\bool\#\worda & Rotate right extended by 1 place \\ 2498\holtxt{word\_lt} & \holtxt{<} & \worda\rarr\worda\rarr\bool & Signed ``less than'' \\ 2499\holtxt{word\_le} & \holtxt{<=} & \worda\rarr\worda\rarr\bool & Signed ``less than or equal'' \\ 2500\holtxt{word\_gt} & \holtxt{>} & \worda\rarr\worda\rarr\bool & Signed ``greater than'' \\ 2501\holtxt{word\_ge} & \holtxt{>=} & \worda\rarr\worda\rarr\bool & Signed ``greater than or equal'' \\ 2502\holtxt{word\_lo} & \holtxt{<+} & \worda\rarr\worda\rarr\bool & Unsigned ``less than'' \\ 2503\holtxt{word\_ls} & \holtxt{<=+} & \worda\rarr\worda\rarr\bool & Unsigned ``less than or equal'' \\ 2504\holtxt{word\_hi} & \holtxt{>+} & \worda\rarr\worda\rarr\bool & Unsigned ``greater than'' \\ 2505\holtxt{word\_hs} & \holtxt{>=+} & \worda\rarr\worda\rarr\bool & Unsigned ``greater than or equal'' \\ 2506\end{supertabular} 2507\end{center}} 2508 2509\index{vettori di bit, la teoria HOL dei@vettori di bit, la teoria \HOL{} dei|)} 2510} % matches bracket at beginning of n-bit section, where some n-bit 2511 % specific macros are defined 2512 2513\section{Sequenze} 2514 2515\HOL{} fornisce teorie per vari generi di sequenze: liste finite, liste lazy, 2516percorsi, e stringhe finite. 2517 2518\subsection{Liste}\label{avra_list} 2519\index{list, l'operatore di tipo ... nella logica HOL@\ml{list}, l'operatore di tipo ... nella logica \HOL{}} 2520\index{tipi, nella logica HOL@tipi, nella logica \HOL{}!strumenti per la costruzione di} 2521\index{liste, la teoria HOL dei@liste, la teoria \HOL{} dei|(} 2522\index{ liste, la teoria HOL dei@\ml{[} $\cdots$ \ml{;} $\cdots$ \ml{]} (liste, la teoria \HOL{} dei)|(} 2523 2524Le liste \HOL{} sono sequenze finite definite induttivamente dove ogni 2525elemento in una lista ha lo stesso tipo. La teoria \ml{list} introduce 2526l'operatore di tipo unario $\alpha \; \konst{list}$ per mezzo di una definizione di tipo 2527ed � definita una collezione standard di funzioni di elaborazioni di 2528liste. I costruttori primitivi {\small\verb+NIL+} e {\small\verb+CONS+} 2529% 2530\begin{hol} 2531\index{NIL, la costante HOL@\holtxt{NIL}, la costante \HOL{}} 2532\index{CONS, la costante HOL@\holtxt{CONS}, la costante \HOL{}} 2533\begin{verbatim} 2534 NIL : 'a list 2535 CONS : 'a -> 'a list -> 'a list 2536\end{verbatim} 2537\end{hol} 2538% 2539sono usati per costruire liste e sono state definite dal tipo rappresentante per 2540le liste. Il parser \HOL{} 2541% 2542\index{parsing, della logica HOL@parsing, della logica \HOL{}!delle espressioni lista} 2543% 2544� stato modificato in modo speciale per eseguire il parsing dell'espressione \holtxt{[]} in 2545\holtxt{NIL}, per eseguire il parsing dell'espressione \holtxt{h::t} in \holtxt{CONS 2546 h t}, e il parsing dell'espressione \holtxt{[$t_1$;$t_2$;\dots;$t_n$]} 2547in \holtxt{CONS $t_1$ (CONS $t_2$ $\cdots$ (CONS $t_n$ NIL) 2548 $\cdots$)}. Il printer di \HOL{} 2549% 2550\index{printing, nella logica HOL@printing, nella logica \HOL{}!delle espressioni lista} 2551% 2552inverte queste trasformazioni. 2553 2554\index{teoremi sulle liste, nella logica HOL@teoremi sulle liste, nella logica \HOL{}} 2555Sulla base della caratterizzazione induttiva del tipo, i seguenti 2556teoremi fondamentali sulle liste sono dimostrati e archiviati nella teoria 2557\ml{list}. 2558 2559\begin{hol} 2560\index{list_Axiom@\ml{list\_Axiom}} 2561\index{assiomi!non-primitivi, della logica HOL@non-primitivi, della logica \HOL{}!per le liste} 2562\index{teoremi d'induzione, nella logica HOL@teoremi d'induzione, nella logica \HOL{}!per le liste} 2563\index{teorema caratterizzante!per le liste} 2564\begin{verbatim} 2565 list_Axiom 2566 |- !x f. ?fn. (fn [] = x) /\ (!h t. fn (h::t) = f(fn t)h t) 2567 list_INDUCT 2568 |- !P. P [] /\ (!t. P t ==> (!h. P(h::t))) ==> (!l. P l) 2569 list_CASES 2570 |- !l. (l = []) \/ (?t h. l = h::t) 2571 CONS_11 2572 |- !h t h' t'. (h::t = h'::t') = (h = h') /\ (t = t') 2573 NOT_NIL_CONS 2574 |- !h t. ~([] = h::t) 2575 NOT_CONS_NIL 2576 |- !h t. ~(h::t = []) 2577\end{verbatim} 2578\end{hol} 2579 2580Il teorema \ml{list\_Axiom} mostrato di sopra � analogo al teorema di 2581ricorsione primitiva 2582% 2583\index{teorema di ricorsione primitiva!per le liste} 2584% 2585sui numeri naturali discusso di sopra nella Sezione~\ref{num-prim-rec}. 2586Esso afferma la validit� delle definizioni ricorsive primitive sulle liste, 2587e pu� essere usato per giustificare qualsiasi di tali definizioni. La funzione \ML{} 2588\ml{new\_recursive\_definition} usa questo teorema per fare 2589% 2590\index{teorema di ricorsione primitiva!uso automatizzato del, nel sistema HOL@uso automatizzato del, nel sistema \HOL{}|)} 2591% 2592dimostrazioni di esistenza delle funzioni ricorsive primitive sulle liste e 2593quindi fare specifiche di costanti per introdurre costanti che denotano 2594tali funzioni. 2595 2596Il teorema d'induzione per le liste, \ml{list\_INDUCT}, fornisce lo strumento 2597di dimostrazione principale usato per ragionare su operazioni che manipolano liste. Il 2598teorema \ml{list\_CASES} � usato per eseguire l'analisi dei casi riguardo al fatto che una 2599lista sia vuota o meno. 2600 2601Il teorema {\small\verb+CONS_11+} mostra che {\small\verb+CONS+} � iniettiva; 2602i teoremi {\small\verb+NOT_NIL_CONS+} e {\small\verb+NOT_CONS_NIL+} mostrano che 2603{\small\verb+NIL+} e {\small\verb+CONS+} sono distinte, cio�, 2604non possono dare origine alla stessa struttura. Insieme, questi tre teoremi 2605sono usati per il ragionamento equazionale circa le liste. 2606 2607Il predicato \ml{NULL} e i selettori 2608% 2609\index{selettori, nella logica HOL@selettori, nella logica \HOL{}!per le liste} 2610% 2611\ml{HD} e \ml{TL} sono definiti nella teoria \theoryimp{list} da 2612% 2613\begin{hol} 2614\index{NULL, la costante HOL@\ml{NULL}, la costante \HOL{}} 2615\index{HD, la costante HOL@\ml{HD}, la costante \HOL{}} 2616\index{TL, la costante HOL@\ml{TL}, la costante \HOL{}} 2617\begin{verbatim} 2618 NULL |- NULL [] /\ (!h t. ~NULL(h::t)) 2619 HD |- !h t. HD(h::t) = h 2620 TL |- !h t. TL(h::t) = t 2621\end{verbatim} 2622\end{hol} 2623 2624\noindent Nella teoria \ml{list} sono definite anche le seguenti funzioni. 2625% 2626% 2627\paragraph{Espressioni case} 2628\index{espressioni case!sulle liste} 2629 2630Le espressioni composte \HOL{} che ramificano sulla base del fatto che un termine sia 2631un lista vuota o non vuota hanno la sintassi di superficie (grossomodo presa in prestito 2632dall'ML) 2633\begin{hol} 2634\begin{verbatim} 2635 case e1 2636 of [] => e2 2637 | (h::t) => e3 2638\end{verbatim} 2639\end{hol} 2640% 2641Una tale espressione � tradotta in 2642$\holtxt{list\_CASE}\ e_1\ e_2\ (\lambda h\; t.\ e_3)$ dove la costante 2643\holtxt{list\_CASE} � definita come segue: 2644\begin{hol} 2645\begin{verbatim} 2646 list_case_def 2647 |- (!v f. list_CASE [] v f = v) /\ 2648 (!v f a0 a1. list_CASE (a0::a1) v f = f a0 a1) 2649\end{verbatim} 2650\end{hol} 2651 2652\paragraph{Appartenenza a una lista} 2653\index{MEM, la costante HOL@\ml{MEM}, la costante \HOL{}} 2654 2655L'appartenenza a una lista, \ml{MEM}, � definita come segue: 2656% 2657\begin{hol} 2658\begin{verbatim} 2659 MEM |- (!x. MEM x [] = F) /\ 2660 (!x h t. MEM x (h::t) = (x = h) \/ MEM x t) 2661\end{verbatim} 2662\end{hol} 2663 2664\paragraph {Concatenazione di liste} 2665\index{APPEND, la costante HOL@\ml{APPEND}, la costante \HOL{}} 2666\index{concatenazione di liste!nella logica HOL@nella logica \HOL{}} 2667\index{FLAT, la costante HOL@\ml{FLAT}, la costante \HOL{}} 2668 2669La concatenazione binaria di liste ({\small\verb+APPEND+}) pu� anche essere denotata 2670dall'operatore infisso {\small\verb|++|}; cos� l'espressione 2671{\small\verb|L1 ++ L2|} � tradotta in {\small\verb+APPEND L1 L2+}. 2672La concatenazione di una lista di liste in una lista � ottenuta da 2673{\small\verb+FLAT+}. 2674% 2675\begin{hol} 2676\begin{verbatim} 2677 APPEND 2678 |- (!l. APPEND [] l = l) /\ 2679 (!l1 l2 h. APPEND (h::l1) l2 = h::APPEND l1 l2) 2680 FLAT 2681 |- (FLAT [] = []) /\ (!h t. FLAT(h::t) = h ++ FLAT t) 2682\end{verbatim} 2683\end{hol} 2684 2685\paragraph {Numeri e liste} 2686\index{LENGTH, la costante HOL@\ml{LENGTH}, la costante \HOL{}} 2687\index{EL, la costante HOL@\ml{EL}, la costante \HOL{}} 2688\index{list_size, la costante HOL@\ml{list\_size}, la costante \HOL{}} 2689 2690La lunghezza (\holtxt{LENGTH}) e la dimensione (\holtxt{list\_size}) di una lista 2691sono nozioni correlate. La dimensione di una lista tiene conto della dimensione di 2692ciascun elemento della lista (data dal parametro 2693$f:\alpha\to\konst{num}$), mentre la lunghezza della lista ignora la 2694dimensione di ciascun elemento della lista. La definizione alternativa della lunghezza 2695(\holtxt{LEN}) � tail-recursive. Si possono inoltre usare numeri come indici 2696nelle liste, estraendo l'elemento alla posizione specificata. 2697% 2698\begin{hol} 2699\begin{verbatim} 2700 LENGTH 2701 |- (LENGTH [] = 0) /\ (!h t. LENGTH (h::t) = SUC(LENGTH t)) 2702 LEN_DEF 2703 |- (!n. LEN [] n = n) /\ !h t n. LEN (h::t) n = LEN t (n + 1) 2704 list_size_def 2705 |- (!f. list_size f [] = 0) /\ 2706 !f a0 a1. list_size f (a0::a1) = 1 + (f a0 + list_size f a1)) 2707 EL 2708 |- (!l. EL 0 l = HD l) /\ (!l n. EL (SUC n) l = EL n (TL l)) 2709\end{verbatim} 2710\end{hol} 2711 2712\noindent 2713Si noti che l'estrazione dell'elemento $n$-esimo (\holtxt{EL}) di una lista 2714inizia la sua indicizzazione da 0. Se la lunghezza della lista $\ell$ � minore 2715o uguale a $n$, il risultato di \holtxt{EL~$n$~$\ell$~} non � 2716specificato. 2717 2718\paragraph {Funzioni di mapping sulle liste} 2719\index{MAP, la costante HOL@\ml{MAP}, la costante \HOL{}} 2720\index{MAP2, la costante HOL@\ml{MAP2}, la costante \HOL{}} 2721\index{funzioni di mapping, nella logica HOL@funzioni di mapping, nella logica \HOL{}!per liste} 2722 2723Ci sono delle funzioni per mappare una funzione $f : \alpha \to \beta$ su 2724una singola lista (\holtxt{MAP}) o una funzione $f : \alpha \to \beta 2725\to \gamma$ sopra due liste (\holtxt{MAP2}). 2726\begin{hol} 2727\begin{verbatim} 2728 MAP 2729 |- (!f. MAP f [] = []) /\ 2730 (!f h t. MAP f (h::t) = f h::MAP f t) 2731 MAP2 2732 |- (!f. MAP2 f [] [] = []) /\ 2733 !f h1 t1 h2 t2. MAP2 f (h1::t1) (h2::t2) = f h1 h2::MAP2 f t1 t2 2734\end{verbatim} 2735\end{hol} 2736Il comportamento di \holtxt{MAP2} nel caso in cui le siano date liste di 2737lunghezza diversa � indeterminato. 2738 2739\paragraph {Predicati su liste} 2740\index{FILTER, la costante HOL@\ml{FILTER}, la costante \HOL{}} 2741\index{EVERY, la costante HOL@\ml{EVERY}, la costante \HOL{}} 2742\index{ALL_DISTINCT, la costante HOL@\ml{ALL\_DISTINCT}, la costante \HOL{}} 2743\index{EXISTS, la costante HOL (sulle liste)@\ml{EXISTS}, la costante \HOL{} 2744 (sulle liste)} 2745 2746I predicati possono essere applicati a liste in un senso universale (il predicato 2747deve valere per ogni elemento nella lista) o in un senso esistenziale (il 2748predicato deve valere per qualche elemento nella lista). Questa funzionalit� 2749� supportata da \holtxt{EVERY} e \holtxt{EXISTS}, rispettivamente. L'eliminazione 2750di tutti gli elementi in una lista che non soddisfano il predicato dato 2751� eseguita da \holtxt{FILTER}. 2752\begin{hol} 2753\begin{verbatim} 2754 EVERY_DEF 2755 |- (!P. EVERY P [] = T) /\ 2756 (!P h t. EVERY P (h::t) = P h /\ EVERY P t) 2757 EXISTS_DEF 2758 |- (!P. EXISTS P [] = F) /\ 2759 (!P h t. EXISTS P (h::t) = P h \/ EXISTS P t) 2760 FILTER 2761 |- (!P. FILTER P [] = []) /\ 2762 (!P h t. FILTER P (h::t) = if P h then h::FILTER P t else FILTER P t) 2763 ALL_DISTINCT 2764 |- (ALL_DISTINCT [] = T) /\ 2765 (!h t. ALL_DISTINCT (h::t) = ~MEM h t /\ ALL_DISTINCT t) 2766\end{verbatim} 2767\end{hol} 2768Il predicato \holtxt{ALL\_DISTINCT} vale su una lista solo nel caso in cui 2769nessun elemento nella lista � uguale ad uno qualsiasi degli altri. 2770 2771\paragraph {Folding} 2772\index{FOLDL, la costante HOL@\ml{FOLDL}, la costante \HOL{}} 2773\index{FOLDR, la costante HOL@\ml{FOLDR}, la costante \HOL{}} 2774 2775L'applicare una funzione binaria $f : \alpha\to\beta\to\beta$ in modo accoppiato 2776attraverso una lista e accumulando il risultato � conosciuto come 2777\emph{folding}. A volte, � necessario eseguire questa operazione 2778da sinistra a destra (\holtxt{FOLDL}), e altre volte � richieste la 2779direzione da destra a sinistra (\holtxt{FOLDR}). 2780\begin{hol} 2781\begin{verbatim} 2782 FOLDL 2783 |- (!f e. FOLDL f e [] = e) /\ 2784 (!f e x l. FOLDL f e (x::l) = FOLDL f (f e x) l) 2785 FOLDR 2786 |- (!f e. FOLDR f e [] = e) /\ 2787 (!f e x l. FOLDR f e (x::l) = f x (FOLDR f e l)) 2788\end{verbatim} 2789\end{hol} 2790 2791\paragraph {Capovolgimento di liste} 2792 2793Il capovolgimento di una lista (\holtxt{REVERSE}) e la sua controparte 2794tail recursive \holtxt{REV} sono definite in \theoryimp{list}. 2795\begin{hol} 2796\begin{verbatim} 2797 REVERSE_DEF 2798 |- (REVERSE [] = []) /\ 2799 (!h t. REVERSE (h::t) = REVERSE t ++ [h]) 2800 REV_DEF 2801 |- (!acc. REV [] acc = acc) /\ 2802 (!h t acc. REV (h::t) acc = REV t (h::acc)) 2803\end{verbatim} 2804\end{hol} 2805 2806\paragraph {Conversione a insiemi} 2807 2808Le liste possono essere convertite in insiemi (\ml{LIST\_TO\_SET}) attraverso l'applicazione 2809parziale di of \holtxt{MEM}. La definizione in qualche modo concisa � usata per 2810derivare il teorema \ml{IN\_LIST\_TO\_SET}. 2811% 2812\begin{hol} 2813\begin{verbatim} 2814 LIST_TO_SET 2815 |- LIST_TO_SET = combin$C MEM 2816 IN_LIST_TO_SET 2817 |- x IN LIST_TO_SET l = MEM x l 2818 $ 2819\end{verbatim} 2820\end{hol} 2821% 2822Ulteriore supporto per tradurre tra differenti generi di 2823collezioni si pu� trovare nella teoria \theoryimp{container}. 2824 2825\paragraph {Coppie e liste} 2826 2827Due liste di uguale lunghezza possono essere accoppiate componente per componente attraverso 2828l'operazione {\small\verb+ZIP+}. Il risultato non � specificato 2829quando le liste non sono della stessa lunghezza. L'operazione inversa, 2830{\small\verb+UNZIP+}, traduce una lista di coppie in una coppia di 2831liste. 2832\begin{hol} 2833\begin{verbatim} 2834 ZIP 2835 |- (ZIP ([],[]) = []) /\ 2836 (!x1 l1 x2 l2. ZIP (x1::l1,x2::l2) = (x1,x2)::ZIP (l1,l2)) 2837 UNZIP_THM 2838 |- (UNZIP [] = ([],[])) /\ 2839 (UNZIP ((x,y)::t) = let (L1,L2) = UNZIP t in (x::L1,y::L2)) 2840\end{verbatim} 2841\end{hol} 2842 2843\paragraph {Accesso alternativo} 2844\index{LAST, la costante HOL@\ml{LAST}, la costante \HOL{}} 2845\index{FRONT, la costante HOL@\ml{FRONT}, la costante \HOL{}} 2846% 2847Le liste sono trattate essenzialmente in modo simile a uno stack. Tuttavia, a 2848volte � conveniente accedere all'ultimo elemento 2849(\holtxt{LAST}) di una lista non vuota in modo diretto. L'ultimo elemento 2850di una lista non vuota � eliminato attraverso \holtxt{FRONT}. 2851\begin{hol} 2852\begin{verbatim} 2853 LAST_DEF 2854 |- !h t. LAST (h::t) = if t = [] then h else LAST t 2855 FRONT_DEF 2856 |- !h t. FRONT (h::t) = if t = [] then [] else h::FRONT t 2857 APPEND_FRONT_LAST 2858 |- !l. ~(l = []) ==> (FRONT l ++ [LAST l] = l) 2859\end{verbatim} 2860\end{hol} 2861% 2862Concatenare la parte frontale e l'ultimo elemento di una lista non vuota porta 2863alla lista originale. Entrambi \holtxt{LAST} e \holtxt{FRONT} 2864sono non specificate su liste vuote. 2865 2866 2867\paragraph {Controllo prefisso} 2868 2869\index{isPREFIX, la costante HOL@\ml{isPREFIX}, la costante \HOL{}} 2870La relazione che cattura se una lista $\ell_1$ � un prefisso di $\ell_2$ 2871({\holtxt{isPREFIX}) pu� essere definita per ricorsione. L'infisso 2872\holtxt{<{}<=} pu� anche essere usato come una notazione per questo ordine parziale. 2873% use of {} above is just a trick to stop Emacs font-lock colouring 2874% this file disgustingly 2875% 2876\begin{hol} 2877\begin{verbatim} 2878 isPREFIX_THM 2879 |- ([] <<= l <=> T) /\ 2880 (h::t <<= [] <=> F) /\ 2881 (h1::t1 <<= h2::t2 <=> (h1 = h2) /\ t1 <<= t2) 2882\end{verbatim} 2883\end{hol} 2884Il teorema di sopra afferma che: la lista vuota � un prefisso di ogni altra 2885lista (clausola 1); che nessuna lista non vuota � un prefisso della lista vuota 2886(clausola 2); e che una lista non vuota � un prefisso di un'altra lista 2887non vuota se i primi elementi delle liste sono gli stessi, e se la coda 2888della prima � un prefisso della coda della seconda. 2889 2890\vspace{1ex} 2891\noindent Per una lista completa dei teoremi disponibili in 2892\theoryimp{list}, si veda \REFERENCE. Un ulteriore sviluppo della teoria 2893delle liste si pu� trovare in \theoryimp{rich\_list}. 2894 2895 2896\subsubsection{Permutazioni e ordinamento di liste} 2897\index{permutazioni (di liste), la teoria HOL delle@permutazioni (di liste), la teoria \HOL{} delle} 2898\index{ordinamento, la teoria HOL del@ordinamento, la teoria \HOL{} del} 2899 2900La teoria \theoryimp{sorting} definisce la nozione per cui due liste sono 2901permutazioni l'una dell'altra, poi definisce una nozione generale di ordinamento, 2902quindi mostra che Quicksort � una funzione di ordinamento. 2903 2904\paragraph{Permutazione di liste} 2905 2906Due liste sono in permutazione se hanno esattamente gli stessi membri, 2907e ogni membro ha lo stesso numero di occorrenze in entrambe le liste. Una 2908definizione (\holtxt{PERM}) che cattura questa relazione � la 2909seguente: 2910% 2911\begin{hol} 2912\begin{verbatim} 2913 PERM_DEF 2914 |- !L1 L2. PERM L1 L2 = !x. FILTER ($= x) L1 = FILTER ($= x) L2 2915 PERM_IND = 2916 |- !P. 2917 P [] [] /\ 2918 (!x l1 l2. P l1 l2 ==> P (x::l1) (x::l2)) /\ 2919 (!x y l1 l2. P l1 l2 ==> P (x::y::l1) (y::x::l2)) /\ 2920 (!l1 l2 l3. P l1 l2 /\ P l2 l3 ==> P l1 l3) 2921 ==> 2922 !l1 l2. PERM l1 l2 ==> P l1 l2 2923\end{verbatim} 2924\end{hol} 2925% 2926Un teorema di induzione derivato (\holtxt{PERM\_IND}) � molto 2927utile nelle dimostrazioni circa le permutazioni. 2928 2929\paragraph{Ordinamento} 2930 2931Una lista � $R$-ordinata se $R$ vale a coppie attraverso la lista. Questa 2932nozione (\holtxt{SORTED}) � catturata da una definizione ricorsiva. Quindi 2933una funzione di tipo 2934% 2935\begin{hol} 2936\begin{verbatim} 2937 ('a -> 'a -> bool) -> 'a list -> 'a list 2938\end{verbatim} 2939\end{hol} 2940% 2941� una funzione di ordinamento (\holtxt{SORTS}) rispetto a $R$ se 2942emette una permutazione del suo input, e il risultato � $R$-ordinato. 2943% 2944\begin{hol} 2945\begin{verbatim} 2946 SORTED_DEF 2947 |- (SORTED R [] = T) /\ 2948 (SORTED R [x] = T) /\ 2949 (SORTED R (x::y::rst) = R x y /\ SORTED R (y::rst)) 2950 SORTS_DEF 2951 |- !f R. SORTS f R = !l. PERM l (f R l) /\ SORTED R (f R l) 2952\end{verbatim} 2953\end{hol} 2954% 2955Quicksort � definito nell'usuale stile di programmazione funzionale, ed 2956� di fatto una funzione di ordinamento, purch� $R$ sia una relazione 2957transitiva e totale. 2958% 2959\begin{hol} 2960\begin{verbatim} 2961 QSORT_DEF = 2962 |- (QSORT ord [] = []) /\ 2963 (QSORT ord (h::t) = 2964 let (l1,l2) = PARTITION (\y. ord y h) t 2965 in 2966 QSORT ord l1 ++ [h] ++ QSORT ord l2) 2967 QSORT_SORTS 2968 |- !R. transitive R /\ total R ==> SORTS QSORT R 2969\end{verbatim} 2970\end{hol} 2971 2972 2973 2974\index{liste, la teoria HOL delle@liste, la teoria \HOL{} delle|)} 2975\index{ liste, la teoria HOL delle@\ml{[} $\cdots$ \ml{;} $\cdots$ \ml{]} (liste, la teoria \HOL{} delle)|)} 2976 2977\subsection{Sequenze potenzialmente infinite (\theoryimp{llist})} 2978 2979\index{liste lazy, la teoria HOL delle@liste ``lazy'', la teoria \HOL{} delle|(} 2980 2981La teoria \theoryimp{llist} contiene la definizione di un tipo di 2982sequenze potenzialmente infinite. Questo tipo � analogo alle ``liste 2983lazy'' di linguaggi di programmazione come l'Haskell, da qui il nome 2984della teoria. La teoria \theoryimp{llist} ha un numero di costanti che 2985sono analoghe alle costanti nella teoria delle liste 2986finite. Le versioni \theoryimp{llist} di queste costanti hanno gli 2987stessi nomi, ma con una `L\/' maiuscola anteposta. Cos�, alcune delle costanti 2988core in questa teoria sono: 2989\begin{hol} 2990\begin{verbatim} 2991 LNIL : 'a llist 2992 LCONS : 'a -> 'a llist -> 'a llist 2993 LHD : 'a llist -> 'a option 2994 LTL : 'a llist -> 'a llist option 2995\end{verbatim} 2996\end{hol} 2997 2998Le costanti \ml{LHD} e \ml{LTL} restituiscono \ml{NONE} quando applicate alla 2999sequenza vuota, \ml{LNIL}. Questo uso di un tipo opzione � un altro 3000modo di modellare la parzialit� essenziale di queste costanti. (Nella 3001teoria delle liste, le analoghe funzioni \ml{HD} e \ml{TL} hanno 3002semplicemente dei valori non specificati quando applicate alle liste vuote.) 3003 3004Il tipo \ml{llist} non � induttivo, e non c'� alcun teorema di 3005ricorsione primitiva che supporti la definizione di funzioni che hanno 3006domini di tipo \ml{llist}. Piuttosto, \ml{llist} � un tipo coinduttivo, 3007e ha un assioma che giustifica la definizione di funzioni 3008(co-)ricorsive che mappano \emph{al} tipo \ml{llist}: 3009\begin{hol} 3010\begin{verbatim} 3011 llist_Axiom 3012 |- !f : 'a -> ('a # 'b) option. 3013 ?g : 'a -> 'b llist. 3014 (!x. LHD (g x) = OPTION_MAP SND (f x)) /\ 3015 (!x. LTL (g x) = OPTION_MAP (g o FST) (f x)) 3016\end{verbatim} 3017\end{hol} 3018\noindent Una forma equivalente a quella di sopra 3019\begin{hol} 3020\begin{verbatim} 3021 llist_Axiom_1 3022 |- !f. ?g. 3023 !x. g x = 3024 case f x 3025 of NONE => LNIL 3026 | SOME (x',y) => LCONS y (g x') 3027\end{verbatim} 3028\end{hol} 3029 3030Altre costanti, nella teoria \theoryimp{llist} includono \ml{LMAP}, \ml{LFINITE}, 3031\ml{LNTH}, \ml{LTAKE}, \ml{LDROP}, e \ml{LFILTER}. I loro tipi sono 3032% 3033\index{mapping di funzioni, nella logica HOL@mapping di funzioni, nella logia \HOL{}!per sequenze potenzialmente infinite} 3034\begin{hol} 3035\begin{verbatim} 3036 LMAP : ('a -> 'b) -> 'a llist -> 'b llist 3037 LFINITE : 'a llist -> bool 3038 LNTH : num -> 'a llist -> 'a option 3039 LTAKE : num -> 'a llist -> 'a list option 3040 LDROP : num -> 'a llist -> 'a llist option 3041 LFILTER : ('a -> bool) -> 'a llist -> 'a llist 3042\end{verbatim} 3043\end{hol} 3044Esse sono caratterizzate dai seguenti teoremi 3045\begin{hol} 3046\begin{verbatim} 3047 LMAP 3048 |- (LMAP f LNIL = LNIL) /\ 3049 (LMAP f (LCONS h t) = LCONS (f h) (LMAP f t)) 3050 LFINITE_THM 3051 |- (LFINITE LNIL = T) /\ 3052 (LFINITE (LCONS h t) = LFINITE t) 3053 LNTH_THM 3054 |- (!n. LNTH n LNIL = NONE) /\ 3055 (!h t. LNTH 0 (LCONS h t) = SOME h) /\ 3056 (!n h t. LNTH (SUC n) (LCONS h t) = LNTH n t) 3057 LTAKE_THM 3058 |- (LTAKE 0 l = SOME []) /\ 3059 (LTAKE (SUC n) LNIL = NONE) /\ 3060 (LTAKE (SUC n) (LCONS h t) = OPTION_MAP (CONS h) (LTAKE n t) 3061 LDROP_THM 3062 |- (LDROP 0 ll = SOME ll) /\ 3063 (LDROP (SUC n) ll = NONE) /\ 3064 (LDROP (SUC n) (LCONS h t) = LDROP n t) 3065 LFILTER_THM 3066 |- (LFILTER P LNIL = LNIL) /\ 3067 (LFILTER P (LCONS h t) = if P h then LCONS h (LFILTER P t) 3068 else LFILTER P t) 3069\end{verbatim} 3070\end{hol} 3071 3072\paragraph{Concatenazione} 3073 3074Due liste lazy possono essere concatenate per mezzo di \ml{LAPPEND}. Se la prima lista 3075lazy � infinita, gli elementi della seconda sono inaccessibili nel 3076risultato. Una lista lazy di liste lazy pu� essere appiattita per mezzo 3077di \ml{LFLATTEN}. 3078\begin{hol}\begin{verbatim} 3079 LAPPEND 3080 |- (!x. LAPPEND LNIL x = x) /\ 3081 (!h t x. LAPPEND (LCONS h t) x = LCONS h (LAPPEND t x)) 3082 LFLATTEN_THM 3083 |- (LFLATTEN LNIL = LNIL) /\ 3084 (!tl. LFLATTEN (LCONS LNIL t) = LFLATTEN t) /\ 3085 (!h t tl. LFLATTEN (LCONS (LCONS h t) tl) = 3086 LCONS h (LFLATTEN (LCONS t tl))) 3087\end{verbatim}\end{hol} 3088 3089\paragraph{Liste e liste lazy} 3090 3091Il mapping da liste a liste lazy e vice versa si ottiene 3092per mezzo di \ml{fromList} and \ml{toList}: 3093\begin{hol}\begin{verbatim} 3094 fromList 3095 |- (fromList [] = LNIL) /\ 3096 (!h t. fromList (h::t) = LCONS h (fromList t)) 3097 toList_THM 3098 |- (toList LNIL = SOME []) /\ 3099 (!h t. toList (LCONS h t) = OPTION_MAP (CONS h) (toList t)) 3100\end{verbatim}\end{hol} 3101 3102\paragraph{Principi di dimostrazione} 3103 3104In fine, ci sono due principi di dimostrazione molto importanti per dimostrare 3105che due valori \ml{llist} sono uguali. Il primo afferma che due 3106sequenze sono uguali se restituiscono gli stessi prefissi di lunghezza $n$ per 3107tutti i valori possibili di $n$: 3108\begin{hol} 3109\begin{verbatim} 3110 LTAKE_EQ |- (ll1 = ll2) = (!n. LTAKE n ll1 = LTAKE n ll2) 3111\end{verbatim} 3112\end{hol} 3113Questo teorema � usato successivamente per derivare il principio 3114di bi-simulazione: 3115\begin{hol} 3116\begin{verbatim} 3117 LLIST_BISIMULATION 3118 |- (ll1 = ll2) = 3119 ?R. R ll1 ll2 /\ 3120 !ll3 ll4. R ll3 ll4 ==> 3121 (ll3 = LNIL) /\ (ll4 = LNIL) \/ 3122 (LHD ll3 = LHD ll4) /\ 3123 R (THE (LTL ll3)) (THE (LTL ll4)) 3124\end{verbatim} 3125\end{hol} 3126Il principio di bi-simulazione afferma che due valori \ml{llist} $l_1$ 3127e $l_2$ sono uguali se (e solo se) � possibile trovare una 3128relazione $R$ tale che 3129\begin{itemize} 3130\item $R$ collega i due valori, cio�, $R\;l_1\;l_2$; and 3131\item se $R$ vale di due valori qualsiasi $l_3$ e $l_4$, allora o 3132 \begin{itemize} 3133 \item entrambi $l_3$ e $l_4$ sono vuoti; o 3134 \item gli elementi testa di $l_3$ e $l_4$ sono gli stessi, e le 3135 code di quei due valori sono di nuovo collegati da $R$ 3136 \end{itemize} 3137\end{itemize} 3138Naturalmente, un $R$ possibile � l'eguaglianza stessa, ma la forza 3139di questo teorema � che possono essere usate anche altre relazioni 3140pi� convenienti. 3141\index{liste lazy, la teoria HOL delle@liste ``lazy'', la teoria \HOL{} delle|)} 3142 3143\subsection{Percorsi etichettati (\theoryimp{path})} 3144 3145La teoria \theoryimp{path} 3146% 3147\index{percorsi etichettati, la teoria HOL dei@percorsi etichettati, la teoria \HOL{} dei|(} 3148\index{sequenze di riduzione, la teoria HOL delle@sequenze di riduzione, la teoria \HOL{} delle|(} 3149\index{percorsi (sequenze di riduzione), la teoria HOL delle@percorsi (sequenze di riduzione), la teoria \HOL{} delle|(} 3150% 3151definisce un operatore di tipo binario $(\alpha,\beta)\ml{path}$, che 3152sta per percorsi potenzialmente infiniti della seguente forma 3153\[ 3154 \alpha_1 \stackrel{\beta_1}{\longrightarrow} 3155 \alpha_2 \stackrel{\beta_2}{\longrightarrow} 3156 \alpha_3 \stackrel{\beta_3}{\longrightarrow} \cdots 3157 \alpha_n \stackrel{\beta_n}{\longrightarrow} 3158 \alpha_{n+1} \stackrel{\beta_{n+1}}{\longrightarrow} \cdots 3159 \] 3160Il tipo \ml{path} � cos� un modello appropriato per sequenze 3161di riduzione, dove il parametro $\alpha$ corrisponde a ``stati'', e 3162il parametro $\beta$ corrisponde alle etichette sulle frecce. 3163 3164Il modello di $(\alpha,\beta)\ml{path}$ � $\alpha \times 3165((\alpha\times\beta)\ml{llist})$. Il tipo dei percorsi ha due 3166costruttori: 3167\begin{hol} 3168\begin{verbatim} 3169 stopped_at : 'a -> ('a,'b) path 3170 pcons : 'a -> 'b -> ('a,'b) path -> ('a,'b) path 3171\end{verbatim} 3172\end{hol} 3173Il costruttore \holtxt{stopped\_at} restituisce un percorso che contiene solo uno 3174stato, e nessuna transizione. (Cos�, la sequenza di riduzione ha 3175questo stato ``fermato'' [``stopped at'' ndt].) Il costruttore \ml{pcons} prende uno stato, 3176un'etichetta, e un percorso, e restituisce un percorso che � ora intestato 3177dall'argomento stato, e che si sposta da quello stato attraverso l'argomento etichetta 3178al percorso. Graficamente, $\ml{pcons}\;x\;l\;p$ � uguale a 3179\[ 3180x \stackrel{l}{\longrightarrow} 3181\underbrace{p_1 \stackrel{l_1}{\longrightarrow} p_2 3182 \stackrel{l_2}{\longrightarrow} \cdots\quad}_p 3183\] 3184Altre costanti definite nella teoria \theoryimp{path} includono 3185% 3186\index{funzioni di mapping, nella logica HOL@funzioni di mapping, nella logica \HOL{}!per percorsi etichettati} 3187% 3188\begin{hol} 3189\begin{verbatim} 3190 finite : ('a,'b) path -> bool 3191 first : ('a,'b) path -> 'a 3192 labels : ('a,'b) path -> 'b llist 3193 last : ('a,'b) path -> 'a 3194 length : ('a,'b) path -> num option 3195 okpath : ('a -> 'b -> 'a -> bool) -> ('a,'b) path -> bool 3196 pconcat : ('a,'b) path -> 'b -> ('a,'b) path -> ('a,'b) path 3197 pmap : ('a -> 'c) -> ('b -> 'd) -> ('a,'b)path -> ('c,'d)path 3198\end{verbatim} 3199\end{hol} 3200 3201La funzione \ml{first} restituisce il primo elemento di un percorso. 3202C'� sempre un tale elemento, e le equazioni di definizione sono 3203\begin{hol} 3204\begin{verbatim} 3205 first_thm |- (first (stopped_at x) = x) /\ 3206 (first (pcons x l p) = x) 3207\end{verbatim} 3208\end{hol} 3209 3210Dall'altro lato, la funzione \ml{last} non ha sempre un 3211valore ben-specificato, bench� abbia ancora delle eleganti equazioni 3212di caratterizzazione. 3213\begin{hol} 3214\begin{verbatim} 3215 last_thm |- (last (stopped_at x) = x) /\ 3216 (last (pcons x l p) = last p) 3217\end{verbatim} 3218\end{hol} 3219 3220Il teorema per \ml{finite} ha un aspetto simile, ma ha un valore 3221definito (\ml{F}, o \emph{false}) su percorsi infiniti, mentre il 3222valore di \ml{last} su tali percorsi non � specificato: 3223\begin{hol} 3224\begin{verbatim} 3225 finite_thm |- (finite (stopped_at x) = T) /\ 3226 (finite (pcons x l p) = finite p) 3227\end{verbatim} 3228\end{hol} 3229 3230La funzione \ml{pconcat} concatena due percorsi, collegandoli 3231con un'etichetta fornita. Se il primo percorso � infinito, allora il risultato 3232� uguale a quello del primo percorso. Le equazioni di definizioni � 3233\begin{hol} 3234\begin{verbatim} 3235 pconcat_thm |- (pconcat (stopped_at x) lab p2 = pcons x lab p2) /\ 3236 (pconcat (pcons x r p) lab p2 = 3237 pcons x r (pconcat p lab p2) 3238\end{verbatim} 3239\end{hol} 3240% 3241Queste equazioni sono vere persino quando il primo argomento a 3242\ml{pconcat} � un percorso infinito. 3243 3244Il predicato \ml{okpath} testa se un percorso � o meno una transizione 3245valida data una relazione di transizione ternaria. Il suo teorema 3246di caratterizzazione � 3247\begin{hol} 3248\begin{verbatim} 3249 okpath_thm |- 3250 (okpath R (stopped_at x)) /\ 3251 (okpath R (pcons x r p) = R x r (first p) /\ okpath R p) 3252\end{verbatim} 3253\end{hol} 3254% 3255C'� anche un principio d'induzione che semplifica il ragionamento circa 3256$R$-percorsi finiti: 3257% 3258\begin{hol} 3259\begin{verbatim} 3260 finite_okpath_ind |- 3261 (!x. P (stopped_at x)) /\ 3262 (!x r p. okpath R p /\ finite p /\ R x r (first p) /\ P p ==> 3263 P (pcons x r p)) ==> 3264 !p. okpath R p /\ finite p ==> P p 3265\end{verbatim} 3266\end{hol} 3267 3268Si pu� mostrare che un insieme \holtxt{P} di percorsi sono tutti $R$-percorsi con il 3269principio di co-induzione: 3270\begin{hol} 3271\begin{verbatim} 3272 okpath_co_ind |- 3273 !P. 3274 (!x r p. P (pcons x r p) ==> R x r (first p) /\ P p) ==> 3275 !p. P p ==> okpath R p 3276\end{verbatim} 3277\end{hol} 3278\index{percorsi etichettati, la teoria HOL dei@percorsi etichettati, la teoria \HOL{} dei|)} 3279\index{sequenze di riduzione, la teoria HOL delle@sequenze di riduzione, la teoria \HOL{} delle|)} 3280\index{percorsi (sequenze di riduzione),la teoria HOL dei@percorsi (sequenze di riduzione), la teoria \HOL{} dei|)} 3281 3282 3283\subsection{Le stringhe di caratteri (\theoryimp{string})} 3284\index{stringhe, la teoria HOL delle@stringhe, la teoria \HOL{} delle|(} 3285 3286La teoria \theoryimp{string} definisce un tipo di caratteri e un tipo 3287di stringhe finite costruite da quei caratteri, insieme con un'utile suite di 3288definizioni per operare su stringhe. 3289 3290\paragraph {Caratteri} 3291\index{caratteri, la teoria HOL dei@caratteri, la teoria \HOL{} dei} 3292 3293Il tipo \holtxt{char} � rappresentato dai numeri minori di 256. Sono 3294definite due costanti: {\small\verb+CHR +}$: \konst{num}\to\konst{char}$ e 3295{\small\verb+ORD +}$: \konst{char}\to\konst{num}$. Valgono i seguenti 3296teoremi: 3297\begin{hol} 3298\begin{verbatim} 3299 CHR_ORD |- !a. CHR (ORD a) = a 3300 ORD_CHR |- !r. r < 256 = (ORD (CHR r) = r) 3301\end{verbatim} 3302\end{hol} 3303 3304\index{letterali carattere} 3305I letterali carattere possono essere inseriti usando la sintassi \ML{}, con un carattere 3306hash immediatamente seguito da un letterale stringa di lunghezza uno. 3307Cos�: 3308\setcounter{sessioncount}{0} 3309\begin{session} 3310\begin{verbatim} 3311- val t = ``f #"c" #"\n"``; 3312<<HOL message: inventing new type variable names: 'a>> 3313> val t = ``f #"c" #"\n"`` : term 3314 3315- dest_term ``#"\t"``; 3316> val it = COMB(``CHR``, ``9``) : lambda 3317\end{verbatim} 3318\end{session} 3319 3320 3321 3322\paragraph {Stringhe} 3323 3324Il tipo \holtxt{string} � un alias per il tipo \holtxt{char list}. 3325Tutte le funzioni e i predicati sulle liste sono cos� disponibili per l'uso 3326sulle stringhe. Alcune di queste costanti sono sottoposte a overload cos� che sono 3327stampate (e possono essere elaborate dal parsing) con nomi che sono pi� appropriate per 3328il particolare caso delle liste di caratteri. 3329 3330Per esempio, \holtxt{NIL} e \holtxt{CONS} su liste hanno 3331i nomi alternativi \holtxt{EMPTYSTRING} e \holtxt{STRING} 3332rispettivamente: 3333% 3334\begin{hol} 3335\index{EMPTYSTRING, la costante HOL@\holtxt{EMPTYSTRING}, la costante \HOL{}} 3336\index{STRING, la costante HOL@\holtxt{STRING}, la costante \HOL{}} 3337\begin{verbatim} 3338 EMPTYSTRING : string 3339 STRING : char -> string -> string 3340\end{verbatim} 3341\end{hol} 3342\index{letterali stringa} 3343Il parser \HOL{} mappa la sintassi \holtxt{""} a \holtxt{EMPTYSTRING}, 3344e il printer \HOL{} inverte questo. Il parser espande i letterali 3345stringa della forma \holtxt{"$c_1 c_2 \ldots c_n$"} al termine 3346composto 3347\[ 3348\holtxt{STRING} \;c_1\; (\holtxt{STRING}\;c_2\,\ldots\, 3349 (\holtxt{STRING} \;c_{n-1} \; (\holtxt{STRING}\; 3350c_n \; \holtxt{EMPTYSTRING})) \,\ldots\, ) 3351\] 3352Naturalmente, si potrebbe anche scrivere 3353\begin{session} 3354\begin{verbatim} 3355- ``[#"a"; #"b"]``; 3356> val it = ``"ab"`` : term 3357\end{verbatim} 3358\end{session} 3359 3360I letterali stringa possono essere costruiti usando le varie speciali sequenze 3361di escape che sono usate in \ML{}. Per esempio, \ml{\bs{}n} per il 3362carattere di nuova linea, e un backslash seguite da tre cifre decimali 3363per caratteri del numero dato. 3364\begin{session} 3365\begin{verbatim} 3366- val t = ``"foo bar\n\001"``; 3367> val t = ``"foo bar\n\^A"`` : term 3368\end{verbatim} 3369\end{session} 3370Si noti che se si vuole usare la sintassi di controllo caratteri con il 3371caret che il pretty-printer ha scelto di usare per stampare la stringa 3372data, e questo accade all'interno di una quotation, allora il caret dovr� 3373essere duplicato. (Si veda la Sezione~\ref{sec:quotation-antiquotation}.) 3374 3375C'� anche una funzione de-costruttore {\small\verb+DEST_STRING+} per 3376le stringhe che restituisce un tipo opzione. 3377\begin{hol} 3378\begin{verbatim} 3379 DEST_STRING 3380 |- (DEST_STRING "" = NONE) /\ 3381 (DEST_STRING (STRING c rst) = SOME(c,rst)) 3382\end{verbatim} 3383\end{hol} 3384 3385 3386\paragraph{Espressioni case} 3387\index{espressioni case!su stringhe} 3388 3389Le espressioni \HOL{} composte che ramificano sulla base del fatto che 3390un termine sia una stringa vuota o non vuota possono essere scritte con la 3391sintassi di superficie 3392\begin{hol} 3393\begin{verbatim} 3394 case s 3395 of "" => e1 3396 | STRING c rst => e2 3397\end{verbatim} 3398\end{hol} 3399 3400Una tale espressione � di fatto un'espressione case sulla lista sottostante, e cos� la costante sottostante � quella per le liste. 3401 3402\paragraph {Lunghezza e concatenazione} 3403 3404Una funzione standard \holtxt{LENGTH} pu� essere scritta \holtxt{STRLEN} 3405quando applicata a una stringa, e \holtxt{APPEND} pu� essere scritta come 3406\holtxt{STRCAT}. Ci sono anche teoremi che caratterizzano queste 3407costanti in \ml{stringTheory}, bench� esse siano semplicemente istanziazioni 3408dei risultati da \ml{listTheory}: 3409\begin{hol} 3410\begin{verbatim} 3411 STRLEN_THM 3412 |- (STRLEN "" = 0) /\ 3413 (STRLEN (STRING c s) = 1 + STRLEN s) 3414 3415 STRCAT_EQNS = 3416 |- (STRCAT "" s = s) /\ 3417 (STRCAT s "" = s) /\ 3418 (STRCAT (STRING c s1) s2 = STRING c (STRCAT s1 s2)) 3419\end{verbatim} 3420\end{hol} 3421 3422 3423\index{stringhe, la teoria HOL delle@stringhe, la teoria \HOL{} delle|)} 3424 3425\section{Collezioni} 3426 3427In \HOL{} sono disponibili alcune nozioni differenti di collezione di elementi: 3428insiemi, multi-insiemi, relazioni, e mappe finite. 3429 3430\subsection{Insiemi (\theoryimp{pred\_set})} 3431\label{sec:theory-of-sets} 3432\index{insiemi, la teoria HOL dei@insiemi, la teoria \HOL{} dei} 3433 3434Un esteso sviluppo della teoria degli insiemi � disponibile nella teoria 3435\theoryimp{pred\_set}. Gli insiemi sono rappresentati da funzione del tipo 3436$\alpha \to \konst{bool}$, cio�, essi sono le cosiddette funzioni 3437caratteristiche. 3438% 3439\index{funzioni caratteristiche!come base della teoria \HOL{} degli insiemi} 3440% 3441Si pu� usare l'abbreviazione di tipo $\alpha\; \konst{set}$ 3442al posto di $\alpha \to \konst{bool}$. Gli insiemi possono essere finiti o 3443infiniti. Tutti gli elementi in un insieme devono avere lo stesso tipo. 3444 3445L'\emph{appartenenza a un insieme} � la nozione base sui cui � basata la teoria degli insiemi 3446formalizzata. In \HOL, l'appartenenza � rappresentata da una costante 3447infissa \holtxt{IN}, definita per convenienza nella teoria 3448\theoryimp{bool}. 3449\begin{hol} 3450\begin{verbatim} 3451 IN_DEF |- IN = \x f. f x 3452\end{verbatim} 3453\end{hol} 3454L'operatore \holtxt{IN} � semplicemente un modo di applicare la 3455funzione caratteristica a un elemento, come mostra la seguente conseguenza 3456banale della definizione: 3457\begin{hol} 3458\begin{verbatim} 3459 SPECIFICATION |- !P x. x IN P = P x 3460\end{verbatim} 3461\end{hol} 3462Due insiemi sono uguali se hanno gli stessi elementi. 3463\begin{hol} 3464\begin{verbatim} 3465 EXTENSION |- !s t. (s = t) = (!x. (x IN s) = (x IN t)) 3466\end{verbatim} 3467\end{hol} 3468 3469\paragraph{Insiemi vuoti e universali} 3470\index{insieme universale} 3471L'insieme vuoto � la funzione caratteristica che � costantemente falsa. La costante \holtxt{EMPTY} denota l'insieme vuoto; essa pu� essere scritta come \holtxt{\{\}} and \holtxt{$\emptyset$} (U+2205). 3472L'insieme universale, \holtxt{UNIV}, su un tipo � la funzione caratteristica che � sempre vera per elementi di quel tipo. 3473\begin{hol} 3474\begin{verbatim} 3475 EMPTY_DEF |- {} = (\x. F) 3476 UNIV_DEF |- UNIV = (\x. T) 3477\end{verbatim} 3478\end{hol} 3479In aggiunta a \holtxt{UNIV} (magari con un'annotazione di tipo \holtxt{:'a~set}), si pu� anche scrivere \holtxt{univ(:'a)} per rappresentare l'insieme universale sul tipo \holtxt{:'a}. 3480La sintassi Unicode \holtxt{$\mathbb{U}$(:'a)} significa la stessa cosa. 3481Il simbolo Unicode per $\mathbb{U}$ � U+1D54C, e potrebbe non esistere in molti set di font. 3482 3483Una di queste forme sar� usata per stampare \holtxt{UNIV} di default. 3484La traccia utente (si veda la Sezione~\ref{sec:traces}) \ml{"Univ~pretty-printing"} pu� essere impostata a zero per cancellare questo comportamento. 3485Inoltre, la traccia \ml{"Unicode Univ printing"} pu� essere usata per smettere di usare la sintassi U+1D54C, persino se � attiva la traccia Unicode. 3486 3487I simboli \holtxt{univ} e \holtxt{$\mathbb{U}$} sono prefissi di priorit� alta (si veda la Sezione~\ref{sec:parseprint:fixities}), e pattern sottoposti a overload (si veda la Sezione~\ref{sec:parser:syntactic-patterns}) che mappano un valore dello tipo stesso alla costante corrispondente \holtxt{UNIV}. 3488Un effetto � che si pu� scrivere cose del tipo 3489\begin{hol} 3490\begin{verbatim} 3491 FINITE univ(:'a) 3492\end{verbatim} 3493\end{hol} 3494senza il bisogno di parentesi intorno all'argomento di \holtxt{FINITE}. 3495 3496\paragraph{Inserimento, unione, e intersezione} 3497 3498L'inserimento ({\small\verb+INSERT+}, scritto infisso) di un elemento 3499in un insieme � definito con una comprensione d'insieme. La comprensione d'insieme � 3500discussa nella sottosezione successiva. Le definizioni usuali per l'unione insiemistica ({\small\verb+UNION+}, 3501scritto infisso) e l'intersezione ({\small\verb+INTER+}, anch'esso infisso) 3502sono date attraverso la comprensione d'insieme. 3503\begin{hol} 3504\begin{verbatim} 3505 INSERT_DEF |- !x s. x INSERT s = {y | (y = x) \/ y IN s} 3506 UNION_DEF |- !s t. s UNION t = {x | x IN s \/ x IN t} 3507 INTER_DEF |- !s t. s INTER t = {x | x IN s /\ x IN t} 3508\end{verbatim} 3509\end{hol} 3510\holtxt{UNION} e \holtxt{INTER} sono operazioni 3511binarie. Le operazioni di unione e intersezione indicizzata, cio�, 3512$\bigcup_{i \in P}$ e $\bigcap_{i \in P}$ sono fornite dalle 3513definizioni di \holtxt{BIGUNION} e \holtxt{BIGINTER}. 3514\begin{hol} 3515\begin{verbatim} 3516 BIGUNION |- !P. BIGUNION P = {x | ?s. s IN P /\ x IN s} 3517 BIGINTER |- !P. BIGINTER P = {x | !s. s IN P ==> x IN s} 3518\end{verbatim} 3519\end{hol} 3520Sia \holtxt{BIGUNION} che \holtxt{BIGINTER} riducono un insieme di insiemi a un 3521insieme e cos� hanno il tipo 3522$((\alpha\to\konst{bool})\to\konst{bool})\to (\alpha\to\konst{bool})$. 3523 3524\paragraph{Sottoinsiemi} 3525 3526L'inclusione di insiemi (\holtxt{SUBSET}, infisso), l'inclusione propria 3527(\holtxt{PSUBSET}, infisso), e l'insieme potenza (\holtxt{POW}) sono definite come 3528segue: 3529% 3530\begin{hol} 3531\begin{verbatim} 3532 SUBSET_DEF |- !s t. s SUBSET t = !x. x IN s ==> x IN t 3533 PSUBSET_DEF |- !s t. s PSUBSET t = s SUBSET t /\ ~(s = t) 3534 POW_DEF |- !set. POW set = {s | s SUBSET set} 3535\end{verbatim} 3536\end{hol} 3537 3538\paragraph{Differenza di insiemi e complemento} 3539 3540La differenza tra due insiemi (\holtxt{DIFF}, infisso) � definita da una 3541comprensione di insieme. Sulla base di quella, la cancellazione di un singolo elemento 3542(\holtxt{DELETE}, infisso) da un insieme � diretta. Dal momento che 3543l'universo di un tipo � sempre disponibile attraverso \holtxt{UNIV}, si pu� prendere il 3544complemento (\holtxt{COMPL}) di un insieme. 3545\begin{hol} 3546\begin{verbatim} 3547 DIFF_DEF |- !s t. s DIFF t = {x | x IN s /\ ~(x IN t)} 3548 DELETE_DEF |- !s x. s DELETE x = s DIFF {x} 3549 COMPL_DEF |- !P. COMPL P = UNIV DIFF P 3550\end{verbatim} 3551\end{hol} 3552 3553\paragraph{Funzioni su insiemi} 3554L'immagine di una funzione $f :\alpha \to \beta$ su 3555un insieme (\holtxt{IMAGE}) � definito con una comprensione d'insieme. 3556\begin{hol} 3557\begin{verbatim} 3558 IMAGE_DEF |- !f s. IMAGE f s = {f x | x IN s} 3559\end{verbatim} 3560\end{hol} 3561% 3562Iniezioni, suriezioni, e biezioni tra insiemi sono definite 3563come segue: 3564% 3565\begin{hol} 3566\begin{verbatim} 3567 INJ_DEF 3568 |- !f s t. 3569 INJ f s t = 3570 (!x. x IN s ==> f x IN t) /\ 3571 !x y. x IN s /\ y IN s ==> (f x = f y) ==> (x = y) 3572 SURJ_DEF 3573 |- !f s t. 3574 SURJ f s t = 3575 (!x. x IN s ==> f x IN t) /\ 3576 !x. x IN t ==> ?y. y IN s /\ (f y = x) 3577 3578 BIJ_DEF |- !f s t. BIJ f s t = INJ f s t /\ SURJ f s t 3579\end{verbatim} 3580\end{hol} 3581 3582\paragraph{Insiemi finiti} 3583\index{finitezza!di insiemi} 3584Gli insiemi finiti (\holtxt{FINITE}) sono definiti induttivamente come quelli 3585costruiti dall'insieme vuoto per mezzo di un numero finito di inserimenti. 3586% 3587\begin{hol} 3588\begin{verbatim} 3589 FINITE_DEF 3590 |- !s. FINITE s = !P. P {} /\ (!s. P s ==> !e. P (e INSERT s)) ==> P s 3591\end{verbatim} 3592\end{hol} 3593% 3594\noindent 3595Un insieme � infinito sse non � finito, e c'� un'abbreviazione nel sistema che esegue il parsing di \holtxt{\holquote{INFINITE~s}} in \holtxt{\holquote{\td{}FINITE~s}}. 3596Il pretty-printer inverte questa trasformazione. 3597 3598\medskip\noindent 3599Gli insiemi finiti hanno un teorema d'induzione: 3600% 3601\index{teoremi d'induzione, nella logica HOL@teoremi d'induzione, nella logica \HOL{}!per insiemi finiti} 3602% 3603\begin{hol} 3604\begin{verbatim} 3605 FINITE_INDUCT 3606 |- !P. P {} /\ 3607 (!s. FINITE s /\ P s ==> !e. ~(e IN s) ==> P (e INSERT s)) 3608 ==> !s. FINITE s ==> P s 3609\end{verbatim} 3610\end{hol} 3611% 3612Come menzionato, le operazioni su insiemi si applicano sia a insiemi finiti che 3613infiniti. Tuttavia, alcune operazioni, come la cardinalit� 3614(\holtxt{CARD}), sono definite soltanto per insiemi finiti. La 3615cardinalit� di un insieme infinito non � specificata. 3616\index{cardinalit� d'insiemi (finiti)} 3617% 3618\begin{hol} 3619\begin{verbatim} 3620 CARD_DEF 3621 |- (CARD {} = 0) /\ 3622 !s. FINITE s ==> 3623 !x. CARD (x INSERT s) = if x IN s then CARD s else SUC (CARD s) 3624\end{verbatim} 3625\end{hol} 3626% 3627Dal momento che gli insiemi finiti e infiniti sono gestiti in modo uniforme in 3628\theoryimp{pred\_set}, le propriet� delle operazioni su insiemi finiti devono 3629includere esplicitamente dei vincoli circa la finitezza. Per esempio il 3630seguente teorema che collega la cardinalit� e i sottoinsiemi � vero solo per 3631insiemi finiti. 3632% 3633\begin{hol} 3634\begin{verbatim} 3635 CARD_PSUBSET 3636 |- !s. FINITE s ==> !t. t PSUBSET s ==> CARD t < CARD s 3637\end{verbatim} 3638\end{hol} 3639% 3640In \theoryimp{pred\_set} � disponibile un'estesa suite di teoremi che trattano 3641con la finitezza e la cardinalit�. 3642 3643\paragraph{Prodotto incrociato} 3644Il prodotto di due insiemi ({\small\verb+CROSS+}, infisso) � definito 3645con una comprensione d'insieme. 3646% 3647\begin{hol} 3648\begin{verbatim} 3649 CROSS_DEF |- !P Q. P CROSS Q = {p | FST p IN P /\ SND p IN Q} 3650\end{verbatim} 3651\end{hol} 3652% 3653\noindent La cardinalit� e il prodotto incrociato sono collegati dal seguente teorema: 3654\begin{hol} 3655\begin{verbatim} 3656 CARD_CROSS 3657 |- !P Q. FINITE P /\ FINITE Q ==> (CARD (P CROSS Q) = CARD P * CARD Q) 3658\end{verbatim} 3659\end{hol} 3660 3661\paragraph{Funzioni ricorsive su insiemi} 3662 3663Le funzioni ricorsive su insiemi possono essere definite dalla ricorsione 3664benfondata. Di solito, la totalit� di una tale funzione � stabilita 3665misurando la cardinalit� dell'insieme (finito). Tuttavia, si pu� usare 3666un altro teorema per giustificare un fold ({\small\verb+ITSET+}) per insiemi finiti. 3667Purch� una funzione $f:\alpha\to\beta\to\beta$ obbedisca a una condizione 3668conosciuta come \emph{commutativa-a-sinistra}, cio�, $f\;x\;(f\;y\;z) = 3669f\;y\;(f\;x\;z)$, allora $f$ pu� essere applicata eseguendo il suo folding sull'insieme 3670in un modo tail-ricorsivo. 3671\begin{hol} 3672\begin{verbatim} 3673 ITSET_EMPTY 3674 |- !f b. ITSET f {} b = b 3675 COMMUTING_ITSET_INSERT 3676 |- !f s. (!x y z. f x (f y z) = f y (f x z)) /\ FINITE s ==> 3677 !x b. ITSET f (x INSERT s) b = ITSET f (s DELETE x) (f x b) 3678\end{verbatim} 3679\end{hol} 3680E' disponibile anche una versione ricorsiva: 3681\begin{hol} 3682\begin{verbatim} 3683 COMMUTING_ITSET_RECURSES 3684 |- !f e s b. 3685 (!x y z. f x (f y z) = f y (f x z)) /\ FINITE s ==> 3686 (ITSET f (e INSERT s) b = f e (ITSET f (s DELETE e) b)) 3687\end{verbatim} 3688\end{hol} 3689Per la completa derivazione, si vedano i sorgenti di {\small\verb+pred_set+}. 3690La definizione di {\small\verb+ITSET+} permette, per esempio, la 3691definizione della sommatoria dei risultati di una funzione su un insieme finito di 3692elementi, da cui sono derivati una caratterizzazione ricorsiva e altri utili 3693teoremi. 3694% 3695\begin{hol} 3696\begin{verbatim} 3697 SUM_IMAGE_DEF 3698 |- !f s. SIGMA f s = ITSET (\e acc. f e + acc) s 0 3699 SUM_IMAGE_THM 3700 |- !f. (SIGMA f {} = 0) /\ 3701 !e s. FINITE s ==> 3702 (SIGMA f (e INSERT s) = f e + SIGMA f (s DELETE e)) 3703\end{verbatim} 3704\end{hol} 3705 3706\paragraph{Altre definizioni e teoremi} 3707 3708TCi sono molte altre definizioni in \theoryimp{pred\_set}, ma non sono 3709usate cos� pesantemente come quelle presentate qui. Analogamente, la maggior parte dei teoremi 3710in \theoryimp{pred\_set} collegano varie operazioni comuni sugli insiemi l'una 3711con le altre, ma non esprimono al cun teorema profondo della teoria degli insiemi. 3712 3713Comunque, un teorema degno di nota � il Lemma di Koenig, che afferma che 3714ogni albero infinito finitamente ramificato ha un percorso infinito. Ci sono 3715molti modi di formulare questo teorema, a seconda di come la nozione di 3716albero � formalizzata. In \theoryimp{pred\_set}, la ramificazione finita � 3717definita come un predicato su una relazione. 3718% 3719\begin{hol} 3720\begin{verbatim} 3721 finite_branching_def 3722 |- !R. finitely_branching R = !x. FINITE {y | R x y} 3723\end{verbatim} 3724\end{hol} 3725% 3726Da questo, la seguente versione del Lemma di Koenig � enunciata e 3727dimostrata: 3728\begin{hol} 3729\begin{verbatim} 3730 KoenigsLemma 3731 |- finitely_branching R ==> 3732 !x. ~FINITE {y | RTC R x y} ==> 3733 ?f. (f 0 = x) /\ !n. R (f n) (f (SUC n)) 3734\end{verbatim} 3735\end{hol} 3736 3737 3738\subsubsection{Sintassi per gli insiemi}\index{notazione insiemistica} 3739 3740Le notazioni insiemistiche special purpose 3741{\small\verb%{%}$t_1 ;t_2 ; \ldots ; t_n${\small\verb%}%} e 3742{\small\verb%{%}$t${\small\verb% | %}$p${\small\verb%}%} sono riconosciute 3743dal parser e dal printer di \HOL{} quando la teoria \theoryimp{pred\_set} 3744� caricata. 3745 3746L'interpretazione normale di \lb$t_1 ;t_2 ; \ldots ; t_n$\rb{} � l'insieme finito 3747che contiene solo $t_1,t_2,\ldots, 3748t_n$. Questo pu� essere modellato iniziando con l'insieme vuoto e 3749eseguendo una sequenza di inserimenti. Per esempio, \holtxt{\lb{}1;2;3;4\rb{}} 3750� parsato a 3751 3752\begin{hol} 3753\begin{verbatim} 3754 1 INSERT (2 INSERT (3 INSERT (4 INSERT EMPTY))) 3755\end{verbatim} 3756\end{hol} 3757 3758\paragraph {Comprensioni d'inseime} 3759 3760L'interpretazione normale di 3761{\small\verb%{%}$t${\small\verb% | %}$p${\small\verb%}%} � 3762l'insieme di tutti i $t$ tali che $p$. In \HOL, tale sintassi � analizzata dal parser a: 3763% 3764\ml{GSPEC(\bs($x_1$,$\ldots$,$x_n$).($t$,$p$))} 3765% 3766\noindent dove $x_1, \ldots, x_n$ sono quelle variabili libere che 3767occorrono sia in $t$ sia in $p$ se entrambi hanno almeno una variabile libera. Se 3768$t$ o $p$ non hanno variabili libere, allora $x_1, \ldots, x_n$ sono considerate 3769essere le variabili libere dell'altro termine. Se entrambi hanno variabili 3770libere, ma non c'� sovrapposizione, allora risulta un errore. L'ordine 3771in cui le variabili sono elencate nella struttura di variabili 3772dell'astrazione accoppiata � una funzione nn specificata della struttura di $t$ 3773(� approssimativamente da sinistra a destra). Per esempio, 3774% 3775\begin{hol} 3776\begin{verbatim} 3777 {p+q | p < q /\ q < r} 3778\end{verbatim} 3779\end{hol} 3780% 3781� analizzata dal parser a: 3782% 3783\begin{hol} 3784\begin{verbatim} 3785 GSPEC(\(p,q). ((p+q), (p < q /\ q < r))) 3786\end{verbatim} 3787\end{hol} 3788% 3789dove \ml{GSPEC} � caratterizzata da: 3790% 3791\begin{hol} 3792\begin{verbatim} 3793 GSPECIFICATION |- !f v. (v IN GSPEC f) = (?x. (v,T) = f x) 3794\end{verbatim} 3795\end{hol} 3796 3797Questa specifica in qualche modo criptica si pu� comprendere attraverso 3798un esempio. La sintassi 3799% 3800\begin{hol} 3801\begin{verbatim} 3802 a IN {p+q | p < q /\ q < r} 3803\end{verbatim} 3804\end{hol} 3805% 3806� mappata dal parser \HOL{} a 3807\begin{hol} 3808\begin{verbatim} 3809 a IN GSPEC(\(p,q). ((p+q), (p < q /\ q < r))) 3810\end{verbatim} 3811\end{hol} 3812% 3813che, per \ml{GSPECIFICATION}, � uguale a 3814\begin{hol} 3815\begin{verbatim} 3816 ?x. (a,T) = (\(p,q). ((p+q), (p < q /\ q < r))) x 3817\end{verbatim} 3818\end{hol} 3819% 3820La variabile quantificata esistenzialmente \verb+x+ ha un tipo coppia, 3821cos� che pu� essere sostituita da una coppia \verb+(p,q)+ e 3822si pu� eseguire una $\beta$-riduzione-accoppiata, portando a 3823% 3824\begin{hol} 3825\begin{verbatim} 3826 ?(p,q). (a,T) = ((p+q), (p < q /\ q < r)) 3827\end{verbatim} 3828\end{hol} 3829% 3830che � uguale al significato inteso della sintassi 3831originale: 3832% 3833\begin{hol} 3834\begin{verbatim} 3835 ?(p,q). (a = p+q) /\ (p < q /\ q < r) 3836\end{verbatim} 3837\end{hol} 3838 3839\paragraph{Comprensioni d'insieme non ambigue} C'� anche una sintassi 3840della comprensione d'insieme non ambigua, che permetter all'utente di 3841specificare quali variabili devono essere quantificate nell'astrazione 3842cio� l'argomento di \holtxt{GSPEC}. Termini della forma 3843\begin{hol} 3844\begin{verbatim} 3845 { t | vs | P } 3846\end{verbatim} 3847\end{hol} 3848generano insiemi che contengono valori della forma data da \holtxt{t}, dove 3849le variabili menzionate in \holtxt{vs} devono soddisfare il vincolo 3850\holtxt{P}. Per esempio, l'insieme 3851\begin{hol} 3852\begin{verbatim} 3853 { x + y | x | x < y } 3854\end{verbatim} 3855\end{hol} 3856� l'insieme dei numeri da \holtxt{y} fino a ma non incluso 3857\holtxt{2~*~y}. L'insieme pu� essere ``letto'' in modo computazionale: escludere tutte 3858quelle \holtxt{x} che sono minori di \holtxt{y}, e ad ognuna di tali 3859\holtxt{x} aggiungere \holtxt{y}, generando con ci� un insieme di numeri. 3860 3861Nell'esempio di sopra, il termine \holtxt{GSPEC} sottostante sar� 3862\begin{hol} 3863\begin{verbatim} 3864 GSPEC (\x. (x + y, x < y)) 3865\end{verbatim} 3866\end{hol} 3867 3868Il componente \holtxt{vs} della notazione non ambigua deve essere una singola 3869``struttura variabile'' che potrebbe apparire sotto un'astrazione possibilmente 3870accoppiata come nella Sezione~\ref{HOL-varstruct}. In altre parole, questo 3871\begin{hol} 3872\begin{verbatim} 3873 { x + y | (x,y) | x < y } 3874\end{verbatim} 3875\end{hol} 3876va bene, ma questo 3877\begin{hol} 3878\begin{verbatim} 3879 { x + y | x y | x < y } 3880\end{verbatim} 3881\end{hol} 3882sollever� un errore. (Inoltre, le parentesi pi� esterne intorno 3883alle coppie nella posizione \holtxt{vs} si possono omettere.) 3884 3885La notazione non ambigua � stampata dal pretty-printere ogni volta che 3886l'insieme da stampare non pu� essere espressa con la notazione di default, o 3887se la variabile di traccia con nome \ml{pp\_unambiguous\_comprehensions} 3888� impostata a \ml{true}. 3889 3890 3891\subsection{Multi-insiemi (\theoryimp{bag})}\label{multiset} 3892 3893I multinsiemi, anche conosciuti come \emph{bag}, sono simili agli insiemi, eccetto per il fatto che 3894essi permettono occorrenze ripetute di un elemento. Mentre gli insiemi sono 3895rappresentati da funzioni di tipo $\alpha\to\konst{bool}$, che segnalano 3896la presenza, o l'assenza, di un elemento, i multinsiemi sono rappresentati 3897da funzioni di tipo $\alpha\to\konst{num}$, che danno la 3898molteplicit� di ciascun elemento nel multinsieme. I multinsiemi possono essere finiti 3899o infiniti. 3900 3901Le abbreviazioni di tipo $\alpha\;\konst{multiset}$ e 3902$\alpha\;\konst{bag}$ possono essere usate al posto di $\alpha\to\konst{num}$. 3903 3904\paragraph {Multinsieme vuoto} 3905 3906Il multinsieme vuoto non ha elementi. Cos�, la funzione che lo implementa 3907restituisce $0$ per ogni input. 3908% 3909\begin{hol} 3910\begin{verbatim} 3911 EMPTY_BAG |- EMPTY_BAG = K 0 3912\end{verbatim} 3913\end{hol} 3914 3915\noindent La sintassi speciale {\verb+{||}+} pu� essere usata per rappresentare il multinsieme 3916vuoto. 3917 3918\paragraph {Appartenenza} 3919 3920Much of the theory can be based on the notion of membership in a 3921bag. There are two notions: does an element occur at least $n$ times 3922in a bag ({\small\verb+BAG_INN+}); and does an element occur in a bag 3923at all ({\small\verb+BAG_IN+}). 3924 3925La maggior parte della teoria si pu� basare sulla nozione di appartenenza a un 3926multinsieme. Ci sono due nozioni: un elemento occorre al meno $n$ volte 3927in una bag 3928% 3929\begin{hol} 3930\begin{verbatim} 3931 BAG_INN |- BAG_INN e n b = (b e >= n) 3932 BAG_IN |- BAG_IN e b = BAG_INN e 1 b 3933\end{verbatim} 3934\end{hol} 3935% 3936Due bag sono uguali se tutti gli elemento hanno lo stesso conteggio. 3937% 3938\begin{hol} 3939\begin{verbatim} 3940 BAG_EXTENSION 3941 |- !b1 b2. (b1 = b2) = (!n e. BAG_INN e n b1 = BAG_INN e n b2) 3942\end{verbatim} 3943\end{hol} 3944 3945\paragraph{Sotto-multinsieme} 3946 3947Una relazione sotto-bag (\holtxt{SUB\_BAG}) vale tra $b_1$ e 3948$b_2$ a condizione che ogni elemento in $b_1$ occorra almeno le stesse volte in 3949$b_2$. La nozione di una sotto-bag propria (\holtxt{PSUB\_BAG}) � facilmente 3950definita. 3951% 3952\begin{hol} 3953\begin{verbatim} 3954 SUB_BAG 3955 |- SUB_BAG b1 b2 = !x n. BAG_INN x n b1 ==> BAG_INN x n b2 3956 PSUB_BAG 3957 |- PSUB_BAG b1 b2 = SUB_BAG b1 b2 /\ ~(b1 = b2) 3958\end{verbatim} 3959\end{hol} 3960 3961\paragraph{Inserimento} 3962 3963L'inserimento di un elemento in una bag (\holtxt{BAG\_INSERT}) aggiorna il 3964conteggio di quell'elemento e lascia gli altri inalterati. 3965% 3966\begin{hol} 3967\begin{verbatim} 3968 BAG_INSERT 3969 |- BAG_INSERT e b = (\x. if (x = e) then b e + 1 else b x) 3970\end{verbatim} 3971\end{hol} 3972 3973Multinsiemi esplicitamente-dati sono supportati dalla sintassi 3974{\small\verb%{|%}$t_1 ;t_2 ; \ldots ; t_n${\small\verb%|}%}, dove 3975ci possono essere, naturalmente, ripetizioni. Questo � modellando iniziando con il multinsieme 3976vuoto ed eseguendo una sequenza di inserimenti. Per esempio, 3977\verb+{|1; 2; 3; 2; 1|}+ � analizzato dal parser a 3978 3979\begin{hol} 3980\begin{verbatim} 3981 BAG_INSERT 1 (BAG_INSERT 2 (BAG_INSERT 3 3982 (BAG_INSERT 2 (BAG_INSERT 1 {||})))) 3983\end{verbatim} 3984\end{hol} 3985 3986 3987\paragraph{Unione and differenza} 3988 3989Le operazioni di unione (\holtxt{BAG\_UNION}) e differenza (\holtxt{BAG\_DIFF}) 3990su bag si riducono entrambe a un calcolo aritmetico sui loro 3991elementi. L'eliminazione di un singolo elemento da un bag pu� essere espresso come il 3992prendere la differenza tra il multinsieme con un multinsieme di un singolo elemento; 3993tuttavia, c'� anche una presentazione relazionale 3994(\holtxt{BAG\_DELETE}) che collega i suoi primi e ultimi argomenti solo 3995se il primo contiene esattamente una occorrenza in pi� dell'argomento 3996di mezzo rispetto all'ultimo. Questa non � la stessa cosa di usare 3997\holtxt{BAG\_DIFF} per rimuovere una bag di un elemento perch� insiste sul fatto che 3998l'elemento che viene rimosso appare effettivamente nella bag pi� grande. 3999% 4000\begin{hol} 4001\begin{verbatim} 4002 BAG_UNION 4003 |- BAG_UNION b c = \x. b x + c x 4004 BAG_DIFF 4005 |- BAG_DIFF b1 b2 = \x. b1 x - b2 x 4006 BAG_DELETE 4007 |- BAG_DELETE b0 e b = (b0 = BAG_INSERT e b) 4008\end{verbatim} 4009\end{hol} 4010 4011\paragraph {Intersezione, merge, e filtro} 4012 4013L'intersezione di due bag (\holtxt{BAG\_INTER}) prende il minimo 4014puntuale. L'operazione duale, il merging (\holtxt{BAG\_MERGE}), prende il 4015massimo puntuale. Una bag pu� essere `filtrata' da un insieme per restituire la bag 4016dove tutti gli elementi che non sono nell'insieme sono stati rimossi. 4017% 4018\begin{hol} 4019\begin{verbatim} 4020 BAG_INTER 4021 |- BAG_INTER b1 b2 = (\x. if (b1 x < b2 x) then b1 x else b2 x) 4022 BAG_MERGE 4023 |- BAG_MERGE b1 b2 = (\x. if (b1 x < b2 x) then b2 x else b1 x) 4024 BAG_FILTER_DEF 4025 |- BAG_FILTER P b = (\e. if P e then b e else 0) 4026\end{verbatim} 4027\end{hol} 4028 4029\paragraph {Insiemi e Multinsiemi} 4030 4031Lo spostamento tra bag e insiemi si ottiene con le seguenti due 4032definizioni 4033% 4034\begin{hol} 4035\begin{verbatim} 4036 SET_OF_BAG 4037 |- SET_OF_BAG b = \x. BAG_IN x b 4038 BAG_OF_SET 4039 |- BAG_OF_SET P = \x. if x IN P then 1 else 0 4040\end{verbatim} 4041\end{hol} 4042 4043\paragraph {Immagine} 4044 4045Prendere l'immagina di una funzione su un multinsieme per ottenere un nuovo multinsieme 4046sembrerebbe essere semplicemente una questione di applicare la funzione a ciascun elemento 4047del multinsieme. Tuttavia, c'� un problema se $f$ non � iniettiva 4048e il multinsieme � infinito. Per esempio, si prenda il multinsieme 4049che consiste di tutti i numeri naturali e si applichi $\lambda x.\; 1$ a 4050ciascun elemento. Il multinsieme risultante conterrebbe un numero infinito di 4051$1$. Per evitare questo sono richiesti alcuni vincoli: per esempio, 4052stipulare che la funzione sia solo finitamente non-iniettiva, o che 4053il multinsieme di input sia finito. Tali condizioni sarebbero onerose alla prova 4054dei fatti; il compromesso � mappare la molteplicit� degli elementi 4055problematici a $0$. 4056% 4057\begin{hol} 4058\begin{verbatim} 4059 BAG_IMAGE_DEF 4060 |- BAG_IMAGE f b = 4061 \e. let sb = BAG_FILTER (\e0. f e0 = e) b 4062 in 4063 if FINITE_BAG sb then BAG_CARD sb else 0 4064\end{verbatim} 4065\end{hol} 4066 4067 4068\paragraph {Multinsiemi finiti} 4069\index{finitezza!dei multinsiemi} 4070I multinsiemi finiti (\holtxt{FINITE\_BAG}) sono definiti in modo induttivo come 4071quelli costruiti dalla bag vuota attraverso un numero finito di inserimenti. 4072% 4073\begin{hol} 4074\begin{verbatim} 4075 FINITE_BAG 4076 |- FINITE_BAG b = 4077 !P. P EMPTY_BAG /\ 4078 (!b. P b ==> (!e. P (BAG_INSERT e b))) ==> P b 4079\end{verbatim} 4080\end{hol} 4081% 4082I multinsiemi finiti hanno un teorema d'induzione, e anche un teorema 4083d'induzione completa. 4084% 4085\index{teoremi d'induzione, nella logica HOL@teoremi d'induzione, nella logica \HOL{}!per bag finite} 4086% 4087\begin{hol} 4088\begin{verbatim} 4089 FINITE_BAG_INDUCT 4090 |- !P. P {||} /\ 4091 (!b. P b ==> (!e. P (BAG_INSERT e b))) 4092 ==> (!b. FINITE_BAG b ==> P b) 4093 4094 STRONG_FINITE_BAG_INDUCT 4095 |- !P. P {||} /\ 4096 (!b. FINITE_BAG b /\ P b ==> !e. P (BAG_INSERT e b)) 4097 ==> (!b. FINITE_BAG b ==> P b) 4098\end{verbatim} 4099\end{hol} 4100% 4101La cardinalit� (\holtxt{BAG\_CARD}) di un multinsieme conta il 4102numero totale di occorrenze. Essa � specificata solo per multinsiemi finiti. 4103% 4104\begin{hol} 4105\begin{verbatim} 4106 BAG_CARD_THM 4107 |- (BAG_CARD {||} = 0) /\ 4108 (!b. FINITE_BAG b ==> 4109 !e. BAG_CARD (BAG_INSERT e b) = BAG_CARD b + 1) 4110\end{verbatim} 4111\end{hol} 4112 4113\paragraph{Funzioni ricorsive su multinsiemi} 4114 4115Le funzioni ricorsive su multinsiemi possono essere definite per ricorsione 4116benfondata. Di solito, la totalit� di una tale funzione � stabilita 4117misurando la cardinalit� del multinsieme (finito). Tuttavia, � fornito 4118un fold (\holtxt{ITBAG}) per insiemi [multinsiemi? ndt] finiti. A condizione che una funzione 4119$f:\alpha\to\beta\to\beta$ obbedisca a una condizione conosciuta come 4120\emph{commutativit�-a-sinistra}, cio�, $f\;x\;(f\;y\;z) = 4121f\;y\;(f\;x\;z)$, allora $f$ pu� essere applicata eseguendone il folding sul 4122multinsieme in una maniera tail-ricorsiva. 4123% 4124\begin{hol} 4125\begin{verbatim} 4126 ITBAG_EMPTY 4127 |- !f acc. ITSET f {||} acc = acc 4128 COMMUTING_ITBAG_INSERT 4129 |- !f b. (!x y z. f x (f y z) = f y (f x z)) /\ FINITE_BAG b ==> 4130 !x a. ITBAG f (BAG_INSERT x b) a = ITBAG f b (f x a) 4131\end{verbatim} 4132\end{hol} 4133% 4134E' disponibile anceh una versione ricorsiva: 4135\begin{hol} 4136\begin{verbatim} 4137 COMMUTING_ITBAG_RECURSES 4138 |- !f e b a. (!x y z. f x (f y z) = f y (f x z)) /\ FINITE_BAG b ==> 4139 (ITBAG f (BAG_INSERT e b) a = f e (ITBAG f b a)) 4140\end{verbatim} 4141\end{hol} 4142 4143\subsection{Relazioni (\theoryimp{relation})}\label{relation} 4144 4145Le relazioni matematiche possono essere rappresentate in \HOL{} dal tipo 4146$\alpha \to\beta\to\konst{bool}$. (Nella maggior parte delle applicazioni, il tipo di una 4147relazione � un'istanza di $\alpha \to\alpha\to\konst{bool}$, ma la 4148generalit� extra non fa male.) La teoria \theoryimp{relation} 4149fornisce definizioni delle propriet� e delle operazioni di base sulle relazioni, 4150definisce vari generi di ordini e chiusure, definisce la benfondatezza 4151e dimostra il teorema di ricorsione benfondata, e sviluppa alcuni 4152risultati base usati nella Riscrittura dei Termini. 4153 4154\paragraph {Propriet� base} 4155 4156Le seguenti propriet� base delle relazioni sono definite. 4157% 4158\begin{hol} 4159\begin{verbatim} 4160 transitive_def 4161 |- transitive R = !x y z. R x y /\ R y z ==> R x z 4162 reflexive_def 4163 |- reflexive R = (!x. R x x) 4164 irreflexive_def 4165 |- irreflexive R = (!x. ~R x x) 4166 symmetric_def 4167 |- symmetric R = (!x y. R x y = R y x) 4168 antisymmetric_def 4169 |- antisymmetric R = (!x y. R x y /\ R y x ==> (x = y)) 4170 equivalence_def 4171 |- equivalence R = reflexive R /\ symmetric R /\ transitive R 4172 trichotomous 4173 |- trichotomous R = !a b. R a b \/ R b a \/ (a = b) 4174 total_def 4175 |- total R = (!x y. R x y \/ R y x) 4176\end{verbatim} 4177\end{hol} 4178 4179\paragraph{Operazioni base} 4180 4181Le seguenti operazioni base sulle relazioni sono definite: la relazione 4182vuota (\holtxt{EMPTY\_REL}), la composizione di relazione (\holtxt{O}, 4183infisso), l'inversione (\holtxt{inv}), il dominio (\holtxt{RDOM}), e il rango 4184(\holtxt{RRANGE}). 4185% 4186\begin{hol} 4187\begin{verbatim} 4188 EMPTY_REL_DEF 4189 |- !x y. EMPTY_REL x y = F 4190 O_DEF 4191 |- $O R1 R2 x z = ?y. R1 x y /\ R2 y z 4192 inv_DEF 4193 |- inv R x y = R y x 4194 RDOM_DEF 4195 |- RDOM R x = ?y. R x y 4196 RRANGE 4197 |- RRANGE R y = ?x. R x y 4198\end{verbatim} 4199\end{hol} 4200 4201\noindent Le operazioni sugli insiemi riutilizzate per lavorare sulle relazioni includono il sottoinsieme 4202(\holtxt{RSUBSET}, infisso), l'unione (\holtxt{RUNION}, infisso), 4203l'intersezione (\holtxt{RINTER}, infisso), il complemento (\holtxt{RCOMPL}), 4204e l'universo (\holtxt{RUNIV}). 4205% 4206\begin{hol} 4207\begin{verbatim} 4208 RSUBSET 4209 |- $RSUBSET R1 R2 = !x y. R1 x y ==> R2 x y 4210 RUNION 4211 |- $RUNION R1 R2 x y = R1 x y \/ R2 x y 4212 RINTER 4213 |- $RINTER R1 R2 x y = R1 x y /\ R2 x y 4214 RCOMPL 4215 |- RCOMPL R x y = ~R x y 4216 RUNIV 4217 |- RUNIV x y = T 4218\end{verbatim} 4219\end{hol} 4220 4221\paragraph {Ordini} 4222 4223In \theoryimp{relation} � fatta una serie di definizioni che catturano varie 4224nozioni. 4225% 4226\begin{hol} 4227\begin{verbatim} 4228 PreOrder 4229 |- PreOrder R = reflexive R /\ transitive R 4230 Order 4231 |- Order Z = antisymmetric Z /\ transitive Z 4232 WeakOrder 4233 |- WeakOrder Z = reflexive Z /\ antisymmetric Z /\ transitive Z 4234 StrongOrder 4235 |- StrongOrder Z = irreflexive Z /\ antisymmetric Z /\ transitive Z 4236 LinearOrder 4237 |- LinearOrder R = Order R /\ trichotomous R 4238 WeakLinearOrder 4239 |- WeakLinearOrder R = WeakOrder R /\ trichotomous R 4240 StrongLinearOrder 4241 |- StrongLinearOrder R = StrongOrder R /\ trichotomous R 4242\end{verbatim} 4243\end{hol} 4244 4245\paragraph {Chiusure} 4246 4247La chiusura transitiva (\holtxt{TC}) di una relazione $R : \alpha 4248\to\alpha\to\konst{bool}$ � definita in modo induttivo, come la pi� piccola 4249relazione che include $R$ ed � chiusa sotto la transitivit�. Analogamente, la 4250chiusura riflessiva-transitiva (\holtxt{RTC}) � definita essere la pi� piccola 4251relazione chiusa sotto la transitivit� e la riflessivit�. 4252% 4253\begin{hol} 4254\begin{verbatim} 4255 TC_DEF 4256 |- TC R a b = 4257 !P. (!x y. R x y ==> P x y) /\ 4258 (!x y z. P x y /\ P y z ==> P x z) ==> P a b 4259 RTC_DEF 4260 |- RTC R a b = 4261 !P. (!x. P x x) /\ 4262 (!x y z. R x y /\ P y z ==> P x z) ==> P a b 4263\end{verbatim} 4264\end{hol} 4265 4266\noindent 4267Da queste definizioni, si possono recuperare le regole iniziali. 4268% 4269\begin{hol} 4270\begin{verbatim} 4271 TC_RULES 4272 |- !R. (!x y. R x y ==> TC R x y) /\ 4273 (!x y z. TC R x y /\ TC R y z ==> TC R x z) 4274 RTC_RULES 4275 |- !R. (!x. RTC R x x) /\ 4276 (!x y z. R x y /\ RTC R y z ==> RTC R x z) 4277 RTC_RULES_RIGHT1 4278 |- !R. (!x. RTC R x x) /\ 4279 (!x y z. RTC R x y /\ R y z ==> RTC R x z) 4280\end{verbatim} 4281\end{hol} 4282% 4283Si noti che {\small\verb+RTC_RULES+}, in linea con la definizione 4284di {\small\verb+RTC+}, estende un \verb+R+-passo da \verb+x+ a 4285\verb+y+ con una sequenza di \verb+R+-passi da \verb+y+ a \verb+z+ 4286per costruire \verb+RTC x z+. Il teorema 4287{\small\verb+RTC_RULES_RIGHT1+} prima fa una serie di \verb+R+ 4288passi e poi un singolo \verb+R+ passo per formare \verb+RTC x z+. Analoghi 4289teoremi alternatici sono dimostrati per l'analisi dei casi e l'induzione. 4290 4291Per esempio, {\small\verb+TC_CASES1+} e {\small\verb+TC_CASES2+} in ci� che 4292segue de-compongono {\small\verb+RTC R x z+} o a 4293{\small\verb+R x y+} seguito da {\small\verb+RTC R y z+} 4294({\small\verb+TC_CASES1+}) 4295o a 4296{\small\verb+RTC R x y+} seguito da {\small\verb+R y z+} 4297({\small\verb+TC_CASES2+}). 4298 4299% 4300\begin{hol} 4301\begin{verbatim} 4302 TC_CASES1 4303 |- !R x z. TC R x z ==> R x z \/ ?y. R x y /\ TC R y z 4304 TC_CASES2 4305 |- !R x z. TC R x z ==> R x z \/ ?y. TC R x y /\ R y z 4306 4307 RTC_CASES1 4308 |- !R x y. RTC R x y = (x = y) \/ ?u. R x u /\ RTC R u y 4309 RTC_CASES2 4310 |- !R x y. RTC R x y = (x = y) \/ ?u. RTC R x u /\ R u y 4311 RTC_CASES_RTC_TWICE 4312 |- !R x y. RTC R x y = ?u. RTC R x u /\ RTC R u y 4313\end{verbatim} 4314\end{hol} 4315 4316Esattamente come i teoremi d'induzione di base per {\small\verb+TC+} e 4317{\small\verb+RTC+}, ci sono i cosiddetti teoremi d'induzione 4318\emph{completa}, che hanno ipotesi d'induzione pi� forti. 4319% 4320\begin{hol} 4321\begin{verbatim} 4322 TC_INDUCT 4323 |- !R P. (!x y. R x y ==> P x y) /\ 4324 (!x y z. P x y /\ P y z ==> P x z) 4325 ==> !u v. TC R u v ==> P u v 4326 RTC_INDUCT 4327 |- ! R P. (!x. P x x) /\ 4328 (!x y z. R x y /\ P y z ==> P x z) ==> 4329 (!x y. RTC R x y ==> P x y) 4330 TC_STRONG_INDUCT 4331 |- !R P. (!x y. R x y ==> P x y) /\ 4332 (!x y z. P x y /\ P y z /\ TC R x y /\ TC R y z ==> P x z) ==> 4333 (!u v. TC R u v ==> P u v) 4334 RTC_STRONG_INDUCT 4335 |- !R P. (!x. P x x) /\ 4336 (!x y z. R x y /\ RTC R y z /\ P y z ==> P x z) ==> 4337 (!x y. RTC R x y ==> P x y) 4338\end{verbatim} 4339\end{hol} 4340Sono anche disponibili varianti di questi teoremi d'induzione che dividono 4341la chiusura dalla sinistra o dalla destra, come per i teoremi di analisi dei casi. 4342 4343\medskip 4344 4345Le chiusure riflessiva~(\holtxt{RC}) e simmetrica~(\holtxt{SC}) sono 4346facili da definire. La chiusura di equivalenza 4347({\small\verb+EQC+}) � la chiusura simmetrica poi transitiva poi riflessiva 4348di $R$. 4349% 4350\begin{hol} 4351\begin{verbatim} 4352 RC_DEF |- RC R x y = (x = y) \/ R x y 4353 SC_DEF |- SC R x y = R x y \/ R y x 4354 EQC_DEF |- EQC R = RC (TC (SC R)) 4355\end{verbatim} 4356\end{hol} 4357 4358\paragraph {Relazioni benfondate} 4359 4360Una relazione $R$ � benfondata ({\small\verb+WF+}) se ogni insieme non-vuoto 4361ha un elemento $R$-minimo. La benfondatezza � usata per giustificare il 4362principio d'induzione benfondata ({\small\verb+WF_INDUCTION_THM+}). 4363% 4364\begin{hol} 4365\begin{verbatim} 4366 WF_DEF 4367 |- !R. WF R = !B. (?w. B w) ==> ?min. B min /\ !b. R b min ==> ~B b 4368 WF_INDUCTION_THM 4369 |- !R WF R ==> !P. (!x. (!y. R y x ==> P y) ==> P x) ==> !x. P x 4370\end{verbatim} 4371\end{hol} 4372 4373La \emph{parte benfondata} ({\small\verb+WFP+}) di una relazione pu� essere 4374definita induttivamente, da essa possono essere derivate le sue regole, il teorema di analisi dei casi e 4375i teoremi d'induzione. 4376% 4377\begin{hol} 4378\begin{verbatim} 4379 WFP_DEF 4380 |- WFP R a = !P. (!x. (!y. R y x ==> P y) ==> P x) ==> P a 4381 WFP_RULES 4382 |- !R x. (!y. R y x ==> WFP R y) ==> WFP R x 4383 WFP_CASES 4384 |- !R x. WFP R x = !y. R y x ==> WFP R y 4385 WFP_INDUCT 4386 |- !R P. (!x. (!y. R y x ==> P y) ==> P x) 4387 ==> !x. WFP R x ==> P x 4388 WFP_STRONG_INDUCT 4389 |- !R. (!x. WFP R x /\ (!y. R y x ==> P y) ==> P x) 4390 ==> !x. WFP R x ==> P x 4391\end{verbatim} 4392\end{hol} 4393 4394La benfondatezza pu� essere usata anche per giustificare un teorema di ricorsione 4395generale. Intuitivamente, una collezione di equazioni di ricorsione possono essere 4396ammesse nella logica \HOL{} senza perdita di coerenza purch� 4397ogni sequenza possibile di chiamate ricorsive sia finita. Le relazioni 4398benfondate sono usate per catturare questa nozione: se c'� una relazione 4399benfondata $R$ sul dominio della funzione desiderata tale che ogni 4400sequenza di chiamate ricorsive � $R$-decrescente, allora le equazioni 4401di ricorsione specificano un'unica funzione totale e le equazioni possono essere 4402ammesse nella logica. 4403 4404I teoremi di ricorsione {\small\verb+WFREC_COROLLARY+} e 4405{\small\verb+WF_RECURSION_THM+} usano la nozione di una restrizione 4406di funzione ({\small\verb+RESTRICT+}) al fine di forzare l'applicazione della funzione 4407ricorsiva ad argomenti $R$-pi�-piccoli nelle chiamate ricorsive. 4408% 4409\begin{hol} 4410\begin{verbatim} 4411 RESTRICT_DEF 4412 |- !f R x. RESTRICT f R x = \y. if R y x then f y else ARB 4413 4414 WFREC_COROLLARY 4415 |- !M R f. (f = WFREC R M) ==> WF R ==> !x. f x = M (RESTRICT f R x) x 4416 4417 WF_RECURSION_THM 4418 |- !R. WF R ==> !M. ?!f. !x. f x = M (RESTRICT f R x) x 4419\end{verbatim} 4420\end{hol} 4421 4422\noindent I teoremi {\small\verb+WF_INDUCTION_THM+} e 4423{\small\verb+WFREC_COROLLARY+} sono usati per automatizzare le definizioni 4424ricorsive; si veda la Sezione \ref{TFL}. Sono anche definiti alcuni operatori 4425di base per le relazioni benfondate, insieme con i teoremi che affermano 4426che essi propagano la benfondatezza. 4427 4428\begin{hol} 4429\begin{verbatim} 4430 inv_image_def |- !R f. inv_image R f = \x y. R (f x) (f y) 4431 4432 WF_inv_image |- !R f. WF R ==> WF (inv_image R f) 4433 WF_SUBSET |- !R P. WF R /\ (!x y. P x y ==> R x y) ==> WF P 4434 WF_TC |- !R. WF R ==> WF (TC R) 4435 WF_Empty |- WF EMPTY_REL 4436\end{verbatim} 4437\end{hol} 4438 4439\paragraph {Riscrittura di termini} 4440 4441Alcune definizioni di base prese dalla teoria della Riscrittura di Termini 4442(la propriet� diamante (\verb+diamond+), la propriet� 4443Church-Rosser ({\small\verb+CR+} e {\small\verb+WCR+}), e la Normalizzazione 4444Forte ({\small\verb+SN+})) appaiono 4445in \theoryimp{relation}. 4446% 4447\begin{hol} 4448\begin{verbatim} 4449 diamond_def 4450 |- diamond R = !x y z. R x y /\ R x z ==> ?u. R y u /\ R z u 4451 CR_def 4452 |- CR R = diamond (RTC R) 4453 WCR_def 4454 |- WCR R = !x y z. R x y /\ R x z ==> ?u. RTC R y u /\ RTC R z u 4455 SN_def 4456 |- SN R = WF (inv R) 4457\end{verbatim} 4458\end{hol} 4459% 4460Da queste, � dimostrato il Lemma di Newman. 4461% 4462\begin{hol} 4463\begin{verbatim} 4464 Newmans_lemma |- !R. WCR R /\ SN R ==> CR R 4465\end{verbatim} 4466\end{hol} 4467 4468\subsection{Mappe finite (\theoryimp{finite\_map})}\label{finite_map} 4469 4470La teoria \theoryimp{finite\_map} formalizza un tipo 4471$(\alpha,\beta)\,\holtxt{fmap}$ di funzioni finite. Queste teoricamente 4472hanno il tipo $\alpha\to\beta$, ma in pi� hanno solo un numero finito di 4473elementi nel loro dominio. Le mappe finite sono utili per formalizzare 4474le sostituzioni e gli array. Il tipo rappresentate � $\alpha\to\beta + 4475\konst{one}$, dove solo un numero finito degli $\alpha$ mappano a un 4476$\beta$ e il resto mappano a \verb+one+. la sintassi 4477$\alpha\,\holtxt{|->}\,\beta$ � riconosciuta dal parser come 4478un'alternativa a $(\alpha,\beta)\,\holtxt{fmap}$. 4479 4480\paragraph {Nozioni base} 4481 4482La mappa vuota (\holtxt{FEMPTY}), l'aggiornamento di una mappa 4483(\holtxt{FUPDATE}), l'applicazione di una mappa a un argomento 4484(\holtxt{FAPPLY}), e il dominio di una mappa (\holtxt{FDOM}) sono le 4485nozioni principali nella teoria. 4486\begin{hol} 4487\begin{verbatim} 4488 FEMPTY : 'a |-> 'b 4489 FUPDATE : ('a |-> 'b) -> 'a # 'b -> ('a |-> 'b) 4490 FAPPLY : ('a |-> 'b) -> 'a -> 'b 4491 FDOM : ('a |-> 'b) -> 'a set 4492\end{verbatim} 4493\end{hol} 4494 4495Il parser e il printer \HOL{} tratteranno la sintassi \holtxt{f\,'\,x} come 4496l'applicazione della mappa finita \verb+f+ to argument \verb+x+, cio�, come 4497\holtxt{FAPPLY\,f\,x}. La notazione \holtxt{f\,|+\,(x,y)} rappresenta 4498\holtxt{FUPDATE\,f\,(x,y)}, cio�, l'aggiornamento della mappa finita 4499\verb+f+ per mezzo della coppia \verb+(x,y)+. 4500 4501Le costanti base hanno delle definizioni oscure, dalle quali sono poi derivate 4502propriet� pi� utili. {\small\verb+FAPPLY_FUPDATE_THM+} collega 4503l'aggiornamento di una mappa con l'applicazione di una mappa. {\small\verb+fmap_EXT+} � un 4504risultato di estensionalit�: due mappe sono uguali se hanno lo stesso dominio 4505e si accordano quando applicate ad argomenti in quel dominio. Si possono dimostrare 4506propriet� delle mappe finite per induzione sulla costruzione della mappa 4507({\small\verb+fmap_INDUCT+}). La cardinalit� di una mappa finita � 4508semplicemente la cardinalit� del suo dominio ({\small\verb+FCARD_DEF+}); da 4509questo � derivata una caratterizzazione ricorsiva 4510({\small\verb+FCARD_FUPDATE+}). 4511\begin{hol} 4512\begin{verbatim} 4513 FAPPLY_FUPDATE_THM 4514 |- !f a b x. (f |+ (a,b)) ' x = (if x = a then b else f ' x) 4515 fmap_EXT 4516 |- !f g. (f = g) = 4517 (FDOM f = FDOM g) /\ (!x. x IN FDOM f ==> (f ' x = g ' x)) 4518 fmap_INDUCT 4519 |- !P. P FEMPTY /\ 4520 (!f. P f ==> !x y. ~(x IN FDOM f) ==> P (f |+ (x,y))) ==> !f. P f 4521 FCARD_DEF |- FCARD fm = CARD (FDOM fm) 4522 FCARD_FUPDATE 4523 |- !fm a b. FCARD(fm |+ (a,b)) = 4524 if a IN FDOM fm then FCARD fm else 1 + FCARD fm 4525\end{verbatim} 4526\end{hol} 4527Aggiornamenti iterati (\holtxt{FUPDATE\_LIST}) a una mappa sono utili. Si pu� anche usare 4528la notazione infissa \holtxt{|++}. Per esempio, \holtxt{fm\,|++\,[(k1,v1);\,(k2,v2)]} � uguale a \holtxt{(fm\,|+\,(k1,v1))\,|+\,(k2,v2)}. 4529\begin{hol} 4530\begin{verbatim} 4531 FUPDATE_LIST |- FUPDATE_LIST = FOLDL FUPDATE 4532 FUPDATE_LIST_THM 4533 |- !f. (f |++ [] = f) /\ 4534 (!h t. f |++ (h::t) = (f |+ h) |++ t) 4535\end{verbatim} 4536\end{hol} 4537 4538 4539\paragraph {Dominio e rango} 4540 4541Il dominio di una mappa finita � l'insieme di elementi a cui essa si applica; 4542questo pu� essere caratterizzato ricorsivamente 4543({\small\verb+FDOM_FUPDATE+}). Il rango di una mappa � definito nel 4544modo usuale. 4545\begin{hol} 4546\begin{verbatim} 4547 FDOM_FUPDATE 4548 |- !f a b. FDOM (f |+ (a,b)) = a INSERT (FDOM f) 4549 FRANGE_DEF 4550 |- FRANGE f = {y | ?x. x IN FDOM f /\ (f ' x = y)} 4551\end{verbatim} 4552\end{hol} 4553% 4554Una mappa finita pu� avere il suo dominio ({\small\verb+DRESTRICT+}) 4555o rango ({\small\verb+RRESTRICT+}) ristretti per intersezione con un 4556insieme. Queste nozioni hanno anche delle versioni ricorsive 4557({\small\verb+DRESTRICT_FUPDATE+} e {\small\verb+RRESTRICT_FUPDATE+}). 4558% 4559\begin{hol} 4560\begin{verbatim} 4561 DRESTRICT_DEF 4562 |- !f r. (FDOM (DRESTRICT f r) = (FDOM f) INTER r) /\ 4563 (!x. DRESTRICT f r ' x = 4564 (if x IN ((FDOM f) INTER r) then f ' x else FEMPTY'x)) 4565 RRESTRICT_DEF 4566 |- !f r. (FDOM (RRESTRICT f r) = {x | x IN FDOM f /\ f ' x IN r}) /\ 4567 (!x. RRESTRICT f r ' x = 4568 (if x IN (FDOM f) /\ f ' x IN r then f ' x 4569 else FEMPTY ' x)) 4570 DRESTRICT_FUPDATE 4571 |- !f r x y. 4572 DRESTRICT (f |+ (x,y)) r = 4573 if x IN r then (DRESTRICT f r) |+ (x,y) else DRESTRICT f r 4574 RRESTRICT_FUPDATE 4575 |- !f r x y. 4576 RRESTRICT (f |+ (x,y)) r = 4577 if y IN r then (RRESTRICT f r) |+ (x,y) 4578 else RRESTRICT (DRESTRICT f (COMPL {x})) r) 4579\end{verbatim} 4580\end{hol} 4581La rimozione di un singolo elemento dal dominio di una mappa 4582(\holtxt{\bs\bs}, infisso) � una semplice applicazione di 4583(\holtxt{DRESTRICT}), ma sufficientemente utile per essere degno di una sua propria 4584definizione. Di nuovo, questo concetto ha una presentazione ricorsiva alternativa 4585(\holtxt{DOMSUB\_FUPDATE\_THM}). 4586% 4587\begin{hol} 4588\begin{verbatim} 4589 fmap_domsub 4590 |- (fm \\ k) = DRESTRICT fm (COMPL {k}) 4591 DOMSUB_FUPDATE_THM 4592 |- !fm k1 k2 v. (fm |+ (k1,v)) \\ k2 = 4593 if (k1 = k2) then (fm \\ k2) else (fm \\ k2) |+ (k1, v) 4594\end{verbatim} 4595\end{hol} 4596 4597\paragraph {Unione e sotto-mappe} 4598 4599Diversamente dall'unione d'insiemi, l'unione di due mappe finite 4600(\holtxt{FUNION\_DEF}) non � simmetrica: il dominio della prima mappa 4601prende la precedenza. La nozione dell'essere una mappa finita una sotto-mappa di un'altra 4602(\holtxt{SUBMAP}, infisso) � un'estensione di come sono formalizzati i 4603sottoinsiemi. 4604\begin{hol} 4605\begin{verbatim} 4606 FUNION_DEF 4607 |- !f g. 4608 (FDOM (FUNION f g) = FDOM f UNION FDOM g) /\ 4609 !x. FUNION f g ' x = (if x IN FDOM f then f ' x else g ' x) 4610 SUBMAP_DEF 4611 |- !f g. (f SUBMAP g) = (!x. x IN FDOM f ==> x IN FDOM g /\ 4612 (f ' x = g ' x)) 4613\end{verbatim} 4614\end{hol} 4615 4616\paragraph {Mappe finite e funzioni} 4617 4618Per quanto possibile, le mappe finite dovrebbero essere come funzioni ordinarie. 4619Cos�, se \holtxt{f} � una mappa finita, allora \holtxt{FAPPLY f} � una 4620funzione ordinaria. Analogamente, c'� un'operazione per 4621\emph{totalizzare} una mappa finita (\holtxt{lookup}) cos� che 4622un'applicazione di essa restituisca una funzione ordinaria, il rango della quale � 4623il tipo option. Una funzione ordinaria pu� essere trasformata in una mappa finita 4624restringendo la funzione a un insieme finito di argomenti 4625(\ml{FUN\_FMAP\_DEF}). 4626% 4627\begin{hol} 4628\begin{verbatim} 4629 lookup_DEF 4630 |- FLOOKUP f x = (if x IN FDOM f then SOME (f ' x) else NONE) 4631 FUN_FMAP_DEF 4632 |- !f P. FINITE P ==> 4633 (FDOM (FUN_FMAP f P) = P) /\ 4634 (!x. x IN P ==> (FUN_FMAP f P ' x = f x)) 4635\end{verbatim} 4636\end{hol} 4637 4638\paragraph {Composizione di mappe} 4639\index{composizione di funzione, nella logica HOL@composizione di funzione, nella logica \HOL{}!di mappe finite} 4640 4641Ci sono tre nuove definizioni di composizione, determinate dal fatto se 4642le funzioni composte sono mappe finite o no. La composizione di due 4643mappe finite (\verb+f_o_f+, infisso) ha attaccati dei vincoli 4644di dominio. La composizione di una mappa finita con una funzione ordinaria 4645(\verb+o_f+, infisso) applica prima la mappa finita, poi la funzione 4646ordinaria. La composizione di una funzione ordinaria con una mappa finita 4647(\verb+f_o+, infisso) applica la funzione ordinaria e poi la mappa 4648finita; l'applicazione della funzione ordinaria � ottenuta trasformandola 4649in una mappa finita. 4650% 4651\begin{hol} 4652\begin{verbatim} 4653 f_o_f_DEF 4654 |- !f g. 4655 (FDOM (f f_o_f g) = (FDOM g) INTER {x | g ' x IN FDOM f}) /\ 4656 !x. x IN FDOM (f f_o_f g) ==> ((f f_o_f g) ' x = f ' (g ' x)) 4657 o_f_DEF 4658 |- !f g. 4659 (FDOM (f o_f g) = FDOM g) /\ 4660 !x. x IN FDOM (f o_f g) ==> ((f o_f g) ' x = f (g ' x)) 4661 f_o_DEF 4662 |- (f f_o g) = f f_o_f (FUN_FMAP g {x | g x IN FDOM f}) 4663\end{verbatim} 4664\end{hol} 4665 4666\section{Cicli While} 4667\label{sec:while-loops} 4668 4669E' un fatto curioso che la logica di ordine superiore, bench� sia una logica di 4670funzioni totali, permetta la definizione di funzioni che non sembrano 4671totali, almeno da un punto di vista computazionale. Un esempio 4672sono i cicli-\holtxt{WHILE}. La seguente equazione � derivata nella teoria 4673\theoryimp{while}: 4674% 4675\begin{hol} 4676\begin{verbatim} 4677 WHILE |- !P g x. WHILE P g x = if P x then WHILE P g (g x) else x 4678\end{verbatim} 4679\end{hol} 4680% 4681Chiaramente, se \holtxt{P} in questo teorema fosse istanziato a $\lambda 4682x.\;\konst{T}$, l'istanza risultante di \holtxt{WHILE} sarebbe `va avanti 4683per sempre' se eseguita. Perch� una tale funzione ``ovviamente'' parziale 4684� definibile in HOL? 4685% 4686La risposta si trova in una sottile definizione di \holtxt{WHILE}, 4687\footnote{L'idea originale � dovuta a J. Moore, 4688 che la sugger� per l'uso in ACL2.} 4689che usa il potere espressivo di HOL per un effetto sorprendente. Si consideri 4690la seguente funzione totale e non-ricorsiva: 4691% 4692\begin{hol} 4693\begin{verbatim} 4694 \x. if (?n. P (FUNPOW g n x)) 4695 then FUNPOW g (@n. P (FUNPOW g n x) /\ 4696 !m. m < n ==> ~P (FUNPOW g m x)) x 4697 else ARB 4698\end{verbatim} 4699\end{hol} 4700% 4701Questa funzione fa un'analisi dei casi sulle iterazioni della funzione 4702\holtxt{g}: quelle finite restituiscono il primo valore nell'iterazione per 4703cui \holtxt{P} vale (cio�, quando l'iterazione si ferma); quelle 4704infinite sono mappate a \holtxt{ARB}. Questa funzione � usata come il testimone 4705per \verb+f+ nella dimostrazione del seguente teorema: 4706% 4707\begin{hol} 4708\begin{verbatim} 4709 ITERATION 4710 |- !P g. ?f. !x. f x = if P x then x else f (g x) 4711\end{verbatim} 4712\end{hol} 4713% 4714Da questo, � semplicemente questione di applicare la Skolemizzazione e 4715di \holtxt{new\_specification} per ottenere l'equazione per \holtxt{WHILE}. 4716 4717\paragraph{Ragionare circa i cicli \holtxt{WHILE}} 4718 4719Il teorema d'induzione per i cicli \holtxt{WHILE} � dimostrato per 4720induzione benfondata, e porta con s� dei vincoli di benfondatezza 4721che ne limitano la sua applicazione. Al fine di applicare \verb+WHILE_INDUCTION+, 4722le istanziazione per \verb+B+ e \verb+C+ devono essere conosciute prima 4723che una relazione benfondata per \verb+R+ sia trovata e usata per eliminare i 4724vincoli. 4725% 4726\begin{hol} 4727\begin{verbatim} 4728 WHILE_INDUCTION 4729 |- !B C R. 4730 WF R /\ (!s. B s ==> R (C s) s) ==> 4731 !P. (!s. (B s ==> P (C s)) ==> P s) ==> !v. P v 4732\end{verbatim} 4733\end{hol} 4734% 4735Un livello di supporto pi� raffinato � fornito dalla regola \holtxt{WHILE} 4736standard della Logica di Hoare, espressa in termini di triple Hoare 4737(\holtxt{HOARE\_SPEC}). 4738% 4739\begin{hol} 4740\begin{verbatim} 4741 HOARE_SPEC_DEF 4742 |- !P C Q. HOARE_SPEC P C Q = !s. P s ==> Q (C s) 4743 WHILE_RULE 4744 |- !R B C. 4745 WF R /\ (!s. B s ==> R (C s) s) ==> 4746 HOARE_SPEC (\s. P s /\ B s) C P ==> 4747 HOARE_SPEC P (WHILE B C) (\s. P s /\ ~B s) 4748\end{verbatim} 4749\end{hol} 4750% 4751Come seguito, � definito un operatore per trovare l'ultimo numero con la propriet� 4752\verb+P+. 4753% 4754\begin{hol} 4755\begin{verbatim} 4756 LEAST_DEF |- !P. $LEAST P = WHILE ($~ o P) SUC 0 4757\end{verbatim} 4758\end{hol} 4759% 4760Alcuni teoremi per ragionare su \holtxt{LEAST} si possono trovare nella 4761teoria \theoryimp{while}. 4762 4763 4764%\section{Partial orders} 4765 4766\section{Altre Teorie} 4767Altre teorie di interesse in \HOL{} sono elencate e brevemente descritte 4768nella Figura~\ref{fig:further-hol-theories}. 4769 4770\begin{figure}[hbtp] 4771\renewcommand{\arraystretch}{1.5} 4772\begin{tabular}{|p{0.2\textwidth}p{0.7\textwidth}|} 4773 \hline 4774 \theoryimp{poset} & Ordini Parziali, teorema Knaster-Tarski 4775 \\ 4776 \theoryimp{divides}, \theoryimp{gcd} & 4777 Divisibilit� e il massimo comun divisore. 4778 \\ 4779 \theoryimp{poly} & 4780 Una teoria di polinomi su $\mathbb{R}$, che fornisce 4781 una collezione di operazioni su polinomi, e teoremi che li riguardano. 4782 \\ 4783 \theoryimp{Temporal\_Logic},\newline \theoryimp{Omega\_Automata} 4784 & 4785 Lo sviluppo di Klaus Schneider della logica temporale e\newline di $\omega$-automi. 4786 \\ 4787 \theoryimp{ctl}, \theoryimp{mu} 4788 & 4789 La logica Computation Tree Logic e l'$\mu$-calculo. Si veda la tesi di 4790 Hasan Amjad. \\ 4791 \theoryimp{lbtree} & Alberi binari possibilmente infinitamente profondi (cio�, co-algebrici).\\ 4792 \theoryimp{inftree} & Alberi algebrici possibilmente infinitamente ramificanti\\ 4793 \hline 4794\end{tabular} 4795\caption{Una selezione di teorie \HOL{}} 4796\label{fig:further-hol-theories} 4797\end{figure} 4798 4799 4800%%% Local Variables: 4801%%% mode: latex 4802%%% TeX-master: "description" 4803%%% End: 4804