Lines Matching defs:di
28 Il sistema \HOL{} fornisce una collezione di teorie sulla quali basare strumenti di verifica o un ulteriore sviluppo di teorie.
29 Nel resto di questa sezione, queste teorie sono descritte brevemente.
30 Le sessioni che seguono forniscono una panoramica del contenuto di ciascuna teoria.
32 In particolare, il file HTML \url{help/HOLindex.html} � un buon punto di partenza per esplorare le teorie disponibili.
37 La teoria di partenza di \HOL{} � la teoria \ml{min}.
39 In questa teoria sono dichiarate la costante di tipo {\small\verb+bool+} dei booleani,
40 l'operatore di tipo binario $(\alpha,\beta)${\small\verb+fun+} delle funzioni, e la costante
41 di tipo {\small\verb+ind+} degli individui. Sulla base di
46 eguaglianza, implicazione, e un operatore di scelta:
57 di \verb+x ==> (y ==> z)+.
64 funzione caratteristica\index{predicato caratteristico, delle definizioni di tipo}
68 di ordine superiore dell'$\hilbert$-operatore
71 di Hilbert; � collegato alla costante
72 $\iota$ nella formulazione di Church della logica di ordine superiore. Per maggiori dettagli,
75 di Church\index{Church, A.} \cite{Church}, il libro di
77 del simbolo-$\hilbert$ di Hilbert \cite{Leisenring}, oppure il libro di testo
78 di Andrews sulla teoria dei tipi \cite{Andrews}.
85 Le regole primitive d'inferenza di \HOL{} dipendono dalla presenza di
90 \section{Teorie di Base}
92 Le teorie pi� di base in HOL forniscono il supporto per una collezione standard
93 di tipi. La teoria \theoryimp{bool} definisce la base della
96 d'infrastruttura di dimostrazione di teoremi. Ulteriori tipi base sono sviluppati
98 (\theoryimp{sum}), del tipo di un solo elemento (\theoryimp{one}), e del
114 per la logica di ordine superiore. Questi assiomi, insieme con le regole
120 \footnote{Per semplificare il porting degli strumenti di dimostrazione di teoremi LCF al
123 della logica di ordine superiore che esso usa differisce dall'assiomatizzazione
125 differenza pi� grande � che nella formulazione di Church le variabili di tipo
127 \index{variabili di tipo, nella logica HOL@variabili di tipo, nella logica \HOL{}!differenza da quelle classiche}
138 \index{valori di verit�, nella logica HOL@valori di verit�, nella logica \HOL{}!costanti per}
161 e \holtxt{?!} (quantificatore di esistenza unica)
165 possono essere tutte definite in termini di eguaglianza,
169 implicazione e scelta. Le definizioni elencate di sotto sono abbastanza
171 a volte sono costruite sulla base di quelle precedenti.
174 \index{valori di verit�, nella logica HOL@valori di verit�, nella logica \HOL{}!definizione dei}
223 \index{ funzione di scelta, nella logica HOL@\holtxt{"@} (funzione di scelta, nella logica \HOL{})}
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}
240 propriet� di funzione {\small\verb+ONE_ONE+} e {\small\verb+ONTO+}. Le
276 in linea di principio, l'utente del sistema \HOL{} non dovrebbe avere mai bisogno
277 di fare una teoria
279 \index{assiomi!dispensabilit� di aggiungere}
282 non-definizionale. In pratica, � spesso molto allettante correre il rischio di
289 La teoria \theoryimp{bool} fornisce anche le definizioni di un numero di
306 � usata nella rappresentazione di termini che contengono binding per variabili locali (cio�
313 completa di come le espressioni \holtxt{let} sono tradotte, si veda
329 vero di $x$''.
333 si tenta di trattare con il problema della parzialit�.
355 La definizione di \ml{RES\_ABSTRACT} � una formula caratterizzante, piuttosto
358 \item se $y$ � un elemento di $P$ allora $(\bs{}x :: P.\; M)
361 insieme (comune) di restrizione, allora sono uguali.
375 La definizione di \ml{RES\_EXISTS\_UNIQUE} usa la sintassi della
379 predicati arbitrari per restringere le variabili di binding. Il parser \HOL{}
380 permette la quantificazione ristretta su tutte le variabili di una sequenza di variabili
381 di binding mettendo la restrizione alla fine della sequenza, cos�
395 Il parser delle quotation di \HOL{}
411 tradotto in \ml{``\$+~x~1``}. Il carattere di escape \ml{\$}
417 sopprime il comportamento infisso di \ml{+} e impedisce al parser delle
418 quotation di rimanere confuso. In generale, \ml{\$} pu� essere usato per sopprimere
422 \index{token!sopprimere il comportamento di parsing di}
424 potrebbe avere. Questo � illustrato nella tabella di sotto, in cui i termini
426 parser di quotation nei corrispondenti termini nella colonna intestata
430 valori (di tipo \ml{term}) come le altre quotation nella stessa riga.
435 \index{operatore di scelta, nella logica HOL@operatore di scelta, nella logica \HOL{}!sintassi del}
443 \index{ funzione di scelta, nella logica HOL@\holtxt{"@} (funzione di scelta, nella logica \HOL{})}
449 \index{eguaglianza, nella logica HOL@eguaglianza, nella logica \HOL{}!sintassi di}
450 \index{negazione, nella logica HOL@negazione, nella logica \HOL{}!sintassi di}
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}
465 \index{congiunzione, nella logica HOL@congiunzione, nella logica \HOL{}!sintassi di}
470 {\it Specie di termine} & {\it Quotation \ML} &
510 ovvi. (Gli indicatori, ad esempio \ml{is\_neg}, restituiscono valori di verit�
511 che indicano se un termine appartiene o meno alla classe di sintassi in
529 \index{disgiunzione, nella logica HOL@disgiunzione, nella logica \HOL{}!sintassi di}
531 \holtxt{/\bs}, \holtxt{==>} e \holtxt{=} sono esempi di
537 sono esempi di \label{binder} \textit{binder}
546 \index{ binder astrazione di funzione, nella logica HOL@\holtxt{\bs} (binder astrazione di funzione, nella logica \HOL{})}
590 \index{costruttori di termine, nella logica HOL@costruttori di termine, nella logica \HOL{}|)}
594 \index{quotation, nella logica HOL@quotation, nella logica \HOL{}!di termini non-primitivi|)}
600 illustrano come la logica di ordine superiore permette l'espressione concisa di
640 \index{composizione di funzione, nella logica HOL@composizione di funzione, nella logica \HOL{}|(}
645 contiene 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{}|(}
647 un operatore di applicazione inversa di funzione,
648 \index{ operatore applicazione di funzione, nella logica HOL@\ml{:>} (operatore applicazione di funzione (inversa)), nella logica \HOL{}}
649 di override di funzione (\ml{=+} infisso),
650 \index{ operatore di override di funzione, nella logica HOL@\ml{=+} (operatore di override di funzione), nella logica \HOL{}}
698 \index{ operatore di applicazione di funzione, nella logica HOL@\ml{:>} (operatore di applicazione (inversa) di funzione), nella logica \HOL{}}
699 Non ci sono teoremi circa \ml{:>}; il suo uso � una sintassi conveniente per le applicazioni di funzione.
700 Per esempio, le catene di update possono perdere qualche parentesi se scritte
711 \index{variabili, nella logica HOL@variabili, nella logica \HOL{}!con nomi di costanti}
717 di tipo.}. Si possono usare variabili con questi nomi nel sistema
720 con la costante \holtxt{C} che essa � `nascosta' di default. Quando �
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}
731 \index{tipi rappresentanti, nella logica HOL@tipi rappresentanti, nella logica \HOL{}!coppia esempio di|(}
735 L'operatore di prodotto Cartesiano
737 \index{operatori di tipo, nella logica HOL@operatori di tipo, nella logica \HOL{}!per coppie}
741 \index{prod, l'operatore di tipo HOL@\holtxt{prod}, l'operatore di tipo \HOL{}}
743 � definito nella teoria \theoryimp{pair}. I valori di tipo
746 $\sigma_2$. Il parser di tipo \HOL{}
750 converte le espressioni di tipo della forma \holtxt{:$\sigma_1$\#$\sigma_2$}
752 \index{ operatore di tipo prodotto, nella logica HOL@\holtxt{\#} (operatore di tipo prodotto, nella logica \HOL{})}
756 \index{ costruttore di coppia, nella logica HOL@\ml{,} (costruttore di coppia, nella logica \HOL{})}
760 \index{costruttore di accoppiamento, nella logica HOL@costruttore di accoppiamento, nella logica \HOL{}}
762 sono costruite con un simbolo di virgola infisso
774 di parentesi: \holtxt{($t_1$,$t_2$)}. Il simbolo virgola associa
776 \index{costruttore di accoppiamento, nella logica HOL@costruttore di accoppiamento, nella logica \HOL{}!associativit� di}
793 \noindent Il tipo rappresentante di
797 un $\beta$-redex non ridotto al fine di soddisfare l'interfaccia
798 richiesta dal principio di definizione di tipo}.
806 L'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.
815 Poi, sono introdotte le funzioni di rappresentazione e astrazione \holtxt{REP\_prod}
830 essere un'applicazione della funzione di astrazione. Successivamente, sono
833 ogni termine che ha un tipo prodotto pu� essere decomposto in una coppia di termini.
835 \index{costruttore di accoppiamento, nella logica HOL@costruttore di accoppiamento, nella logica \HOL{}!definizione di}
848 Skolemizzando {\small\verb+ABS_PAIR_THM+} e facendo le specifiche di costante
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}
865 \index{tipi rappresentanti, nella logica HOL@tipi rappresentanti, nella logica \HOL{}!coppia esempio di|)}
869 In \HOL{}, una funzione di tipo $\alpha \# \beta\to\gamma$ ha sempre una
870 controparte di tipo $\alpha\to\beta\to\gamma$, e \emph{vice versa}.
890 applicate in modo componente ({\small\verb+##+}, infisso) su una coppia di tipo
891 $\alpha \# \beta$ per ottenere una coppia di tipo $\gamma_1 \# \gamma_2$.
903 Quando si fanno dimostrazioni, gli enunciati che coinvolgono tuple possono prendere la forma di un
904 binding (quantificazione o $\lambda$-astrazione) di una variabile con un
905 tipo prodotto. Pu� essere conveniente nei successivi passi di ragionamento
906 rimpiazzare le variabili con tuple di variabili. I seguenti teoremi
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|(}
949 E' conveniente dal punto di vista della notazione includere l'accoppiamento nella lambda
950 astrazione, 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}
999 \noindent Come risultato di questa traduzione del parser, una struttura variabile, come \ml{(x,y)} in
1001 \index{astrazione di funzione, nella logica HOL@astrazione di funzione, nella logica \HOL{}!sottotermini di}
1003 \index{binder, nella logica HOL@binder, nella logica \HOL{}!parsing di}
1004 \index{parsing, della logica HOL@parsing, della logica \HOL{}!di binders}
1006 di errore). Per esempio, l'antiquoting di una coppia nella posizione della variabile
1007 legata di una lambda astrazione fallisce:
1025 \ml{$b$(\bs($x_1$,$x_2$).$t$)}, e di conseguenza trasformato come di sopra. Per
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|)}
1041 \index{parsing, della logica HOL@parsing, della logica \HOL{}!di termini-let@di termini-\holtxt{let}}
1056 i termini-\ml{let} sono di fatto abbreviazioni per termini ordinari che sono
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}}
1090 le operazioni di de-costruzione. Per esempio:
1110 sintassi di superficie.%
1119 La teoria \theoryimp{sum} definisce l'operatore di tipo binario unione
1122 di tipo \holtxt{sum} pu� essere definito, esattamente come � stato per \holtxt{prod},
1125 di questa definizione si possono trovare in~\cite{Melham-banff}.} Il parser
1126 di \HOL{}
1185 relativi alle funzioni di proiezione e ai discriminatori.
1201 \subsection{Il tipo di un-unico-elemento}%
1219 costruzione di tipi pi� elaborati. L'unico valore del tipo
1221 unit nell'\ML. Questo � anche il modo di default in cui questo valore
1225 \index{itself, l'operatore di tipo HOL@\holtxt{itself}, l'operatore di tipo \HOL{}}%
1226 L'operatore di tipo \holtxt{itself} fornisce una famiglia di tipi singleton simili a \holtxt{one}.
1228 Il 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).
1248 Il 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).
1253 La teoria \theoryimp{option} definisce un operatore di tipo \verb+option+
1256 I costruttori di questo tipo sono
1263 Le option possono essere usate per modellizzare le funzioni parziali. Se una funzione di tipo
1269 Come tipo induttivo, le option hanno un teorema di ricorsione che supporta la
1270 definizione di funzioni ricorsive primitive su valori option.
1282 di ispezionare i valori option in un stile ``pattern-matching''.
1302 \index{mapping di funzioni, nella logica HOL@mapping di funzioni, nella logica \HOL{}!per le option}
1321 serie di teorie. Sono anche disponibili teorie di parole di $n$-bit
1326 I numeri naturali sono sviluppati in una serie di teorie:
1329 definito dall'Assioma dell'Infinito, e sono derivati gli assiomi di Peano. In
1330 \theoryimp{prim\_rec} � dimostrato il teorema di Ricorsione Primitiva. Sulla base
1331 di questo, in \theoryimp{arithmetic} � sviluppata un'ampia teoria che tratta le operazioni aritmetiche
1344 e gli assiomi di Peano
1346 \index{gli assiomi di Peano}
1361 Nella logica di ordine superiore, gli assiomi di Peano sono sufficienti per sviluppare
1380 non sono permesse. Per esempio, non c'� alcuna funzione $f$ (di tipo
1386 Certe ristrette forme di definizione
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$
1395 e $f$ il \emph{teorema di ricorsione primitiva} ci dice che c'�
1402 Il teorema di ricorsione primitiva, chiamato \ml{num\_Axiom} in \HOL,
1405 \index{assiomi di Peano}
1407 di Peano.
1410 \index{teorema di caratterizzazione!per i numeri}
1422 \paragraph{La relazione minore-di}
1424 La 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{}}
1429 teorema di ricorsione primitiva, cos� deve essere definita prima che la definizione
1431 di conseguenza contiene la seguente definizione non ricorsiva di \ml{<}:
1443 verso il basso\footnote{Un insieme di numeri � \textit{chiuso verso il basso} se ogni volta che
1444 contiene il successore di un numero, contiene anche il numero.} e
1453 \index{teorema di ricorsione primitiva!uso automatico del, nel sistema HOL@uso automatico del, nel sistema \HOL{}|(}
1456 di ricorsione primitiva pu� essere usato per giustificare qualsiasi definizione di una funzione
1458 definizione ricorsiva primitiva nella logica di ordine superiore della forma
1479 L'esistenza di una funzione ricorsiva \ml{fun} che soddisfa queste due
1480 equazioni segue direttamente dal teorema di ricorsione primitiva
1481 \ml{num\_Axiom} mostrato di sopra. La specializzazione delle variabili quantificate \verb!x!
1482 e \verb!f! con un'adeguata istanziazione dei tipi di \ml{num\_Axiom} cos�
1491 \noindent restituisce il teorema di esistenza mostrato di sotto:
1501 meccanismo\linebreak definizionale delle specifiche di costante---si veda la Sezione~\ref{conspec})
1503 del teorema. L'introduzione di una costante \ml{fun} per nominare la funzione che � affermata
1504 esistere dal teorema mostrato di sopra, e la semplificazione per mezzo di una $\beta$-riduzione,
1515 soddisfa le equazioni di definizione ricorsiva primitiva date dal teorema mostrato
1516 di sotto:
1525 Per automatizzare l'uso del teorema di ricorsione primitiva nel derivare
1526 definizioni ricorsive di questo genere, il sistema \HOL{} fornisce una funzione
1527 che automaticamente dimostra l'esistenza di funzioni ricorsive
1528 primitive e poi fa una specifica di costante per introdurre la costante
1540 definizioni ricorsive primitive su un range di tipi, non solo sui
1545 primitiva, insieme con altri stili di ricorsione, e non richiede
1546 all'utente di citare l'assioma di ricorsione primitiva. Pu�, tuttavia,
1547 richiedere di eseguire dimostrazioni di terminazione; fortunatamente, non � necessario
1553 Il teorema di ricorsione primitiva � utile oltre il suo scopo principale di
1555 \theoryimp{prim\_rec} dimostra l'Assioma di Scelta Dipendente ({\small\verb+DC+}).
1558 \index{assioma di scelta dipendente (DC)@assioma di scelta dipendente (\ml{DC})}
1559 \index{assiomi!di scelta}
1570 propriet� da una relazione. Per esempio, un modo di definire la
1571 benfondatezza di una relazione $R$ � quello di dire che non ha infinite
1584 Per mezzo dell'uso di {\small\verb+DC+}, questo enunciato pu� essere dimostrato
1585 essere uguale alla nozione di benfondatezza {\small\verb+WF+}
1589 Nella teoria \theoryimp{prim\_rec} sono anche dimostrati teoremi che affermano la benfondatezza della relazione di predecessore e
1590 della relazione minore-di, esattamente come la benfondatezza delle funzioni
1591 di misura.
1639 \holtxt{**} pu� essere usata al posto di \holtxt{EXP}. Cos�
1642 \paragraph{Operatori di confronto}
1644 Un completo insieme di operatori di confronto � definito in termini di \verb+<+.
1647 \index{ maggiore di, nella logica HOL@\ml{>} (maggiore di, nella logica \HOL{})}
1660 modulo ({\small\verb+MOD+}, infisso) � usata una specifica di costante, insieme con le loro
1673 Le propriet� di un numero di essere pari o dispari sono definite ricorsivamente.
1687 Il minimo e il massimo di due numeri sono definiti nel modo usuale.
1701 Il fattoriale di un numero � una definizione ricorsiva primitiva.
1709 \paragraph{Iterazione di funzione}
1712 L'applicazione iterata $f^n x$ di una funzione $f : \alpha \to
1730 Su questa base, quando � eseguito il build di \HOL{} una serie \adhoc\ ma utile di pi� duecentocinquanta
1739 La seguente tabella da lo status di parsing delle costanti
1763 di solito � pensato essere fornito di una collezione infinita di
1765 alcun modo di definire tali famiglie infinite di costanti; piuttosto, tutti
1766 i numerali diversi da $0$ sono di fatto costruiti dalle costanti
1782 e il parser e il pretty-printer di \HOL{} fanno apparire tali termini come
1788 esempio il seguente calcolo di $2 ^{(1023 + 14)/9}$ richiede
1808 \ml{numSyntax}). Questi entry-point fanno uso di una structure \ML
1809 \ml{Arbnum} che implementa numeri di precisione arbitraria {\verb+num+}. La
1812 {\small\verb+Arbnum+} fornisce una collezione completa di operazioni
1832 \index{parsing, della logica HOL@parsing, della logica \HOL{}!di numerali}
1836 Le sequenze semplici di cifre sono rese dal parser come numeri decimali, ma il parser
1837 supporta anche l'input di numeri in notazione binaria, ottale ed
1843 abilitati di default, ma se la reference
1847 Infine, tutti i numeri possono essere intervallati da caratteri di underscore
1868 \paragraph{Numerali e numeri di Peano}
1903 stare di fatto per un numero naturale, un intero o un valore reale. Il
1904 parser ha un passo di risoluzione dell'overloading in cui tenta di
1906 seguente sessione, la teoria degli interi � caricata, dopo di che il
1923 Al fine di specificare in modo preciso il tipo desiderato, l'utente pu� usare dei suffissi
1924 di un singolo carattere (`\ml{n}' per i numeri naturali, e `\ml{i}' per
1937 \verb+42i+, � rappresentato dall'applicazione di una funzione
1938 d'\emph{iniezione} di tipo {\small\verb+num -> ty+} per un
1939 numerale. La funzione di iniezione � differente per ogni tipo
1944 numerici con suffissi di un carattere diverso da {\small\verb+n+}. Per
1945 informazioni su come installare nuovi suffissi di un carattere, si consulti la
1953 � costruito come un quoziente su coppie di numeri naturali. E' definita
1954 una collezione standard di operatori. Questi sono degli overload con
2001 Il tipo dei razionali � costruito come un quoziente di coppie ordinate di
2002 interi (il numeratore e il denominatore di una frazione) il cui secondo
2004 il segno di un numero razionale � sempre spostato al numeratore.
2007 E' definita una collezione di operatori, che sono sottoposti a overload con
2034 (in)equazioni tra interi, le propriet� delle relazioni minore-di e la
2043 C'� un'estesa collezione di teorie che costituisce lo
2047 la tesi di Harrison.
2054 {\small\verb+realaxTheory+}. Una collezione standard di operatori sui
2055 reali, e di teoremi che li riguardano, si trova in {\small\verb+realaxTheory+}
2056 and {\small\verb+realTheory+}. Gli operatori e il loro status di parsing sono
2077 Sulla base di {\small\verb+realTheory+}, � costruita la seguente sequenza di
2083 \item [nets] Reti di convergenza Moore-Smith, e casi speciali come
2085 \item [seq] Sequenze e serie di numeri reali.
2090 Kurzweil-Henstock il teorema fondamentale del calcolo, e il teorema di
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.
2107 Hurd~\cite{hurd-thesis}. Per prima cosa � definito un tipo di sequenze booleane
2108 per modellare una sequenza infinita di lanci di monete. Poi � formalizzata
2109 una funzione di probabilit� che prende come input un insieme di sequenze
2111 non a tutti gli insiemi pu� essere assegnata una probabilit� (il paradosso di
2117 una funzione di esempio che prende una sequenza infinita di lanci di monete e
2120 funzione di esempio per la distribuzione uniforme � usata pi� avanti per verificare
2121 il test di primalit� di Miller-Rabin.
2123 \subsection{Vettori di bit}
2136 \HOL{} fornisce una teoria di vettori du bit, o parole di $n$-bit. Per esempio, nelle architetture
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$
2142 approccio viene da un'idea di John Harrison, che fu presentata al TPHOLs del
2143 2005\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.}
2147 La teoria \HOL{} \theoryimp{fcp} introduce un operatore di tipo infisso
2153 dove \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.
2155 Si accede alle \emph{componenti} di un prodotto cartesiano finito con una
2156 funzione di indicizzazione
2164 Tipicamente, gli indici sono vincolati ad essere minori della dimensione di \ty{'b}.
2175 Al fine di costruire prodotti cartesiani, la teoria \theoryimp{fcp} introduce un
2184 Il teorema \ml{FCP\_BETA} mostra che i componenti di \holtxt{\$FCP g} sono
2187 sono identiche a quelle di \holtxt{x}.
2189 frammento \ml{fcpLib.FCP\_ss} di \emph{simpset}.
2191 I prodotti cartesiani finiti forniscono un buon mezzo per modellare parole di $n$-bit. Vale a
2201 \holtxt{BIT\_MODIFY}. In questo contesto, i numeri naturali sono trattati come parole binarie di
2202 lunghezza 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:
2210 un meccanismo per la valutazione efficiente di alcune operazioni su parole attraverso la teoria
2215 La 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
2221 Tutti i teoremi circa operazioni word si applicano a word di qualsiasi lunghezza\footnote{Si noti
2222 che � impossibile introdurre word di lunghezza zero perch� tutti i tipi
2223 devono essere abitati, e di conseguenza la loro dimensione sar� sempre maggiore o uguale a
2226 \paragraph{Alcune operazioni di base}
2228 La funzione \holtxt{w2n:\worda\rarr\num} da il valore del numero naturale di una
2230 che rappresenta una parola di $n$-bit allora il valore del suo numero naturale �:
2233 La lunghezza di una parola (il numero $n$) � dato dalla funzione
2243 \holtxt{255w} � lo stesso di \holtxt{n2w 255}.
2251 Se $\beta$ � pi� piccolo di $\alpha$ allora i bit pi� alti di \holtxt{w} saranno
2252 persi (esegue un'estrazione di bit), altrimenti la parola pi� lunga avr� lo stesso valore dell'originale (fornendo in effetti zero padding).
2253 Tuttavia, se si stesse trattando \holtxt{w} come un numero complemento di due allora la
2261 La funzione \holtxt{sw2sw:\worda\rarr\wordb} fornisce questa versione sign extending di
2264 E' fornita una collezione di operazioni per mappare da stringhe a liste di numeri (cifre) e vice versa, ad esempio
2276 Queste funzioni sono versioni specializzate di \holtxt{w2s} e \holtxt{w2l} rispettivamente.
2280 L'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}}.
2297 con la versione (complemento a due) con segno di ``minore di'' abbiamo
2298 \holtxt{255w < (0w:word8)} perch� la parola \holtxt{255w} � di fatto
2313 C'� anche una collezione di operazioni di \emph{riduzione} parola, che riducono vettori di bit a parole di 1 bit, ad esempio
2317 danno il valore bit di una parola alle posizioni $0$, $n - 1$ e $i$
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.
2329 � una parola \holtxt{b} con i bit 5--2 sostituiti dai bit 3--0 di \holtxt{a}.
2331 L'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.
2341 nega i bit di \holtxt{w} che sono nelle posizioni pari. Naturalmente, il
2348 Sono fornite sei tipi di shift: shift logico sinistra/destra (\holtxt{<<} e
2350 (\holtxt{\#<<} e \holtxt{\#>>}) e ruotare a destra propagato di 1 posto
2359 La rotazione a sinistra di $x$ posti � definita come rotazione a destra di $n - x \bmod n$
2399 segno di $<$, $\leq$, $>$ e $\geq$. Le versioni senza segno hanno un suffisso
2400 con un pi�; per esempio, \holtxt{<+} � il ``minore di'' senza segno.
2418 \paragraph{Elenco di operazioni su vettori di bit}
2420 Un elenco di operazioni � fornito nella tabella di sotto.
2509 \index{vettori di bit, la teoria HOL dei@vettori di bit, la teoria \HOL{} dei|)}
2515 \HOL{} fornisce teorie per vari generi di sequenze: liste finite, liste lazy,
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}
2526 l'operatore di tipo unario $\alpha \; \konst{list}$ per mezzo di una definizione di tipo
2527 ed � definita una collezione standard di funzioni di elaborazioni di
2548 $\cdots$)}. Il printer di \HOL{}
2580 Il teorema \ml{list\_Axiom} mostrato di sopra � analogo al teorema di
2583 \index{teorema di ricorsione primitiva!per le liste}
2585 sui numeri naturali discusso di sopra nella Sezione~\ref{num-prim-rec}.
2587 e pu� essere usato per giustificare qualsiasi di tali definizioni. La funzione \ML{}
2590 \index{teorema di ricorsione primitiva!uso automatizzato del, nel sistema HOL@uso automatizzato del, nel sistema \HOL{}|)}
2592 dimostrazioni di esistenza delle funzioni ricorsive primitive sulle liste e
2593 quindi fare specifiche di costanti per introdurre costanti che denotano
2597 di dimostrazione principale usato per ragionare su operazioni che manipolano liste. Il
2631 un lista vuota o non vuota hanno la sintassi di superficie (grossomodo presa in prestito
2664 \paragraph {Concatenazione di liste}
2666 \index{concatenazione di liste!nella logica HOL@nella logica \HOL{}}
2669 La concatenazione binaria di liste ({\small\verb+APPEND+}) pu� anche essere denotata
2672 La concatenazione di una lista di liste in una lista � ottenuta da
2690 La lunghezza (\holtxt{LENGTH}) e la dimensione (\holtxt{list\_size}) di una lista
2691 sono nozioni correlate. La dimensione di una lista tiene conto della dimensione di
2694 dimensione di ciascun elemento della lista. La definizione alternativa della lunghezza
2713 Si noti che l'estrazione dell'elemento $n$-esimo (\holtxt{EL}) di una lista
2715 o uguale a $n$, il risultato di \holtxt{EL~$n$~$\ell$~} non �
2718 \paragraph {Funzioni di mapping sulle liste}
2721 \index{funzioni di mapping, nella logica HOL@funzioni di mapping, nella logica \HOL{}!per liste}
2736 Il comportamento di \holtxt{MAP2} nel caso in cui le siano date liste di
2750 di tutti gli elementi in una lista che non soddisfano il predicato dato
2791 \paragraph {Capovolgimento di liste}
2793 Il capovolgimento di una lista (\holtxt{REVERSE}) e la sua controparte
2809 parziale di of \holtxt{MEM}. La definizione in qualche modo concisa � usata per
2822 Ulteriore supporto per tradurre tra differenti generi di
2827 Due liste di uguale lunghezza possono essere accoppiate componente per componente attraverso
2830 {\small\verb+UNZIP+}, traduce una lista di coppie in una coppia di
2849 (\holtxt{LAST}) di una lista non vuota in modo diretto. L'ultimo elemento
2850 di una lista non vuota � eliminato attraverso \holtxt{FRONT}.
2862 Concatenare la parte frontale e l'ultimo elemento di una lista non vuota porta
2870 La relazione che cattura se una lista $\ell_1$ � un prefisso di $\ell_2$
2884 Il teorema di sopra afferma che: la lista vuota � un prefisso di ogni altra
2886 (clausola 2); e che una lista non vuota � un prefisso di un'altra lista
2896 \subsubsection{Permutazioni e ordinamento di liste}
2897 \index{permutazioni (di liste), la teoria HOL delle@permutazioni (di liste), la teoria \HOL{} delle}
2901 permutazioni l'una dell'altra, poi definisce una nozione generale di ordinamento,
2902 quindi mostra che Quicksort � una funzione di ordinamento.
2904 \paragraph{Permutazione di liste}
2907 e ogni membro ha lo stesso numero di occorrenze in entrambe le liste. Una
2926 Un teorema di induzione derivato (\holtxt{PERM\_IND}) � molto
2933 una funzione di tipo
2941 � una funzione di ordinamento (\holtxt{SORTS}) rispetto a $R$ se
2955 Quicksort � definito nell'usuale stile di programmazione funzionale, ed
2956 � di fatto una funzione di ordinamento, purch� $R$ sia una relazione
2981 La teoria \theoryimp{llist} contiene la definizione di un tipo di
2983 lazy'' di linguaggi di programmazione come l'Haskell, da qui il nome
2984 della teoria. La teoria \theoryimp{llist} ha un numero di costanti che
2986 finite. Le versioni \theoryimp{llist} di queste costanti hanno gli
2999 sequenza vuota, \ml{LNIL}. Questo uso di un tipo opzione � un altro
3000 modo di modellare la parzialit� essenziale di queste costanti. (Nella
3004 Il tipo \ml{llist} non � induttivo, e non c'� alcun teorema di
3005 ricorsione primitiva che supporti la definizione di funzioni che hanno
3006 domini di tipo \ml{llist}. Piuttosto, \ml{llist} � un tipo coinduttivo,
3007 e ha un assioma che giustifica la definizione di funzioni
3018 \noindent Una forma equivalente a quella di sopra
3033 \index{mapping di funzioni, nella logica HOL@mapping di funzioni, nella logia \HOL{}!per sequenze potenzialmente infinite}
3074 Due liste lazy possono essere concatenate per mezzo di \ml{LAPPEND}. Se la prima lista
3076 risultato. Una lista lazy di liste lazy pu� essere appiattita per mezzo
3077 di \ml{LFLATTEN}.
3092 per mezzo di \ml{fromList} and \ml{toList}:
3102 \paragraph{Principi di dimostrazione}
3104 In fine, ci sono due principi di dimostrazione molto importanti per dimostrare
3106 sequenze sono uguali se restituiscono gli stessi prefissi di lunghezza $n$ per
3107 tutti i valori possibili di $n$:
3114 di bi-simulazione:
3126 Il principio di bi-simulazione afferma che due valori \ml{llist} $l_1$
3131 \item se $R$ vale di due valori qualsiasi $l_3$ e $l_4$, allora 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$
3139 di questo teorema � che possono essere usate anche altre relazioni
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|(}
3151 definisce un operatore di tipo binario $(\alpha,\beta)\ml{path}$, che
3161 di riduzione, dove il parametro $\alpha$ corrisponde a ``stati'', e
3164 Il modello di $(\alpha,\beta)\ml{path}$ � $\alpha \times
3174 stato, e nessuna transizione. (Cos�, la sequenza di riduzione ha
3186 \index{funzioni di mapping, nella logica HOL@funzioni di mapping, nella logica \HOL{}!per percorsi etichettati}
3201 La funzione \ml{first} restituisce il primo elemento di un percorso.
3202 C'� sempre un tale elemento, e le equazioni di definizione sono
3212 di caratterizzazione.
3222 valore di \ml{last} su tali percorsi non � specificato:
3232 � uguale a quello del primo percorso. Le equazioni di definizioni �
3245 valida data una relazione di transizione ternaria. Il suo teorema
3246 di caratterizzazione �
3268 Si pu� mostrare che un insieme \holtxt{P} di percorsi sono tutti $R$-percorsi con il
3269 principio di co-induzione:
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|)}
3283 \subsection{Le stringhe di caratteri (\theoryimp{string})}
3286 La teoria \theoryimp{string} definisce un tipo di caratteri e un tipo
3287 di stringhe finite costruite da quei caratteri, insieme con un'utile suite di
3293 Il tipo \holtxt{char} � rappresentato dai numeri minori di 256. Sono
3306 hash immediatamente seguito da un letterale stringa di lunghezza uno.
3326 sulle stringhe. Alcune di queste costanti sono sottoposte a overload cos� che sono
3328 il particolare caso delle liste di caratteri.
3361 di escape che sono usate in \ML{}. Per esempio, \ml{\bs{}n} per il
3362 carattere di nuova linea, e un backslash seguite da tre cifre decimali
3370 Si noti che se si vuole usare la sintassi di controllo caratteri con il
3371 caret che il pretty-printer ha scelto di usare per stampare la stringa
3372 data, e questo accade all'interno di una quotation, allora il caret dovr�
3391 sintassi di superficie
3400 Una tale espressione � di fatto un'espressione case sulla lista sottostante, e cos� la costante sottostante � quella per le liste.
3427 In \HOL{} sono disponibili alcune nozioni differenti di collezione di elementi:
3441 Si pu� usare l'abbreviazione di tipo $\alpha\; \konst{set}$
3442 al posto di $\alpha \to \konst{bool}$. Gli insiemi possono essere finiti o
3454 L'operatore \holtxt{IN} � semplicemente un modo di applicare la
3472 L'insieme universale, \holtxt{UNIV}, su un tipo � la funzione caratteristica che � sempre vera per elementi di quel tipo.
3479 In 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}.
3481 Il simbolo Unicode per $\mathbb{U}$ � U+1D54C, e potrebbe non esistere in molti set di font.
3483 Una di queste forme sar� usata per stampare \holtxt{UNIV} di default.
3485 Inoltre, la traccia \ml{"Unicode Univ printing"} pu� essere usata per smettere di usare la sintassi U+1D54C, persino se � attiva la traccia Unicode.
3487 I 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}.
3494 senza il bisogno di parentesi intorno all'argomento di \holtxt{FINITE}.
3498 L'inserimento ({\small\verb+INSERT+}, scritto infisso) di un elemento
3511 binarie. Le operazioni di unione e intersezione indicizzata, cio�,
3513 definizioni di \holtxt{BIGUNION} e \holtxt{BIGINTER}.
3520 Sia \holtxt{BIGUNION} che \holtxt{BIGINTER} riducono un insieme di insiemi a un
3526 L'inclusione di insiemi (\holtxt{SUBSET}, infisso), l'inclusione propria
3538 \paragraph{Differenza di insiemi e complemento}
3541 comprensione di insieme. Sulla base di quella, la cancellazione di un singolo elemento
3543 l'universo di un tipo � sempre disponibile attraverso \holtxt{UNIV}, si pu� prendere il
3544 complemento (\holtxt{COMPL}) di un insieme.
3554 L'immagine di una funzione $f :\alpha \to \beta$ su
3583 \index{finitezza!di insiemi}
3585 costruiti dall'insieme vuoto per mezzo di un numero finito di inserimenti.
3595 Un 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}}.
3615 cardinalit� di un insieme infinito non � specificata.
3640 In \theoryimp{pred\_set} � disponibile un'estesa suite di teoremi che trattano
3644 Il prodotto di due insiemi ({\small\verb+CROSS+}, infisso) � definito
3664 benfondata. Di solito, la totalit� di una tale funzione � stabilita
3689 Per la completa derivazione, si vedano i sorgenti di {\small\verb+pred_set+}.
3690 La definizione di {\small\verb+ITSET+} permette, per esempio, la
3691 definizione della sommatoria dei risultati di una funzione su un insieme finito di
3713 Comunque, un teorema degno di nota � il Lemma di Koenig, che afferma che
3715 molti modi di formulare questo teorema, a seconda di come la nozione di
3726 Da questo, la seguente versione del Lemma di Koenig � enunciata e
3743 dal parser e dal printer di \HOL{} quando la teoria \theoryimp{pred\_set}
3746 L'interpretazione normale di \lb$t_1 ;t_2 ; \ldots ; t_n$\rb{} � l'insieme finito
3749 eseguendo una sequenza di inserimenti. Per esempio, \holtxt{\lb{}1;2;3;4\rb{}}
3760 L'interpretazione normale di
3762 l'insieme di tutti i $t$ tali che $p$. In \HOL, tale sintassi � analizzata dal parser a:
3771 in cui le variabili sono elencate nella struttura di variabili
3772 dell'astrazione accoppiata � una funzione nn specificata della struttura di $t$
3840 della comprensione d'insieme non ambigua, che permetter all'utente di
3842 cio� l'argomento di \holtxt{GSPEC}. Termini della forma
3858 quelle \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.
3861 Nell'esempio di sopra, il termine \holtxt{GSPEC} sottostante sar�
3886 l'insieme da stampare non pu� essere espressa con la notazione di default, o
3887 se la variabile di traccia con nome \ml{pp\_unambiguous\_comprehensions}
3894 essi permettono occorrenze ripetute di un elemento. Mentre gli insiemi sono
3895 rappresentati da funzioni di tipo $\alpha\to\konst{bool}$, che segnalano
3896 la presenza, o l'assenza, di un elemento, i multinsiemi sono rappresentati
3897 da funzioni di tipo $\alpha\to\konst{num}$, che danno la
3898 molteplicit� di ciascun elemento nel multinsieme. I multinsiemi possono essere finiti
3901 Le abbreviazioni di tipo $\alpha\;\konst{multiset}$ e
3902 $\alpha\;\konst{bag}$ possono essere usate al posto di $\alpha\to\konst{num}$.
3925 La maggior parte della teoria si pu� basare sulla nozione di appartenenza a un
3949 $b_2$. La nozione di una sotto-bag propria (\holtxt{PSUB\_BAG}) � facilmente
3963 L'inserimento di un elemento in una bag (\holtxt{BAG\_INSERT}) aggiorna il
3964 conteggio di quell'elemento e lascia gli altri inalterati.
3976 vuoto ed eseguendo una sequenza di inserimenti. Per esempio,
3989 Le operazioni di unione (\holtxt{BAG\_UNION}) e differenza (\holtxt{BAG\_DIFF})
3991 elementi. L'eliminazione di un singolo elemento da un bag pu� essere espresso come il
3992 prendere la differenza tra il multinsieme con un multinsieme di un singolo elemento;
3996 di 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
4013 L'intersezione di due bag (\holtxt{BAG\_INTER}) prende il minimo
4045 Prendere l'immagina di una funzione su un multinsieme per ottenere un nuovo multinsieme
4046 sembrerebbe essere semplicemente una questione di applicare la funzione a ciascun elemento
4049 che consiste di tutti i numeri naturali e si applichi $\lambda x.\; 1$ a
4050 ciascun elemento. Il multinsieme risultante conterrebbe un numero infinito di
4053 il multinsieme di input sia finito. Tali condizioni sarebbero onerose alla prova
4071 quelli costruiti dalla bag vuota attraverso un numero finito di inserimenti.
4101 La cardinalit� (\holtxt{BAG\_CARD}) di un multinsieme conta il
4102 numero totale di occorrenze. Essa � specificata solo per multinsiemi finiti.
4116 benfondata. Di solito, la totalit� di una tale funzione � stabilita
4146 $\alpha \to\beta\to\konst{bool}$. (Nella maggior parte delle applicazioni, il tipo di una
4147 relazione � un'istanza di $\alpha \to\alpha\to\konst{bool}$, ma la
4149 fornisce definizioni delle propriet� e delle operazioni di base sulle relazioni,
4150 definisce vari generi di ordini e chiusure, definisce la benfondatezza
4151 e dimostra il teorema di ricorsione benfondata, e sviluppa alcuni
4182 vuota (\holtxt{EMPTY\_REL}), la composizione di relazione (\holtxt{O},
4223 In \theoryimp{relation} � fatta una serie di definizioni che catturano varie
4247 La chiusura transitiva (\holtxt{TC}) di una relazione $R : \alpha
4284 di {\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+
4287 {\small\verb+RTC_RULES_RIGHT1+} prima fa una serie di \verb+R+
4316 Esattamente come i teoremi d'induzione di base per {\small\verb+TC+} e
4340 Sono anche disponibili varianti di questi teoremi d'induzione che dividono
4341 la chiusura dalla sinistra o dalla destra, come per i teoremi di analisi dei casi.
4346 facili da definire. La chiusura di equivalenza
4348 di $R$.
4373 La \emph{parte benfondata} ({\small\verb+WFP+}) di una relazione pu� essere
4374 definita induttivamente, da essa possono essere derivate le sue regole, il teorema di analisi dei casi e
4394 La benfondatezza pu� essere usata anche per giustificare un teorema di ricorsione
4395 generale. Intuitivamente, una collezione di equazioni di ricorsione possono essere
4396 ammesse nella logica \HOL{} senza perdita di coerenza purch�
4397 ogni sequenza possibile di chiamate ricorsive sia finita. Le relazioni
4400 sequenza di chiamate ricorsive � $R$-decrescente, allora le equazioni
4401 di ricorsione specificano un'unica funzione totale e le equazioni possono essere
4404 I teoremi di ricorsione {\small\verb+WFREC_COROLLARY+} e
4405 {\small\verb+WF_RECURSION_THM+} usano la nozione di una restrizione
4406 di funzione ({\small\verb+RESTRICT+}) al fine di forzare l'applicazione della funzione
4425 di base per le relazioni benfondate, insieme con i teoremi che affermano
4439 \paragraph {Riscrittura di termini}
4441 Alcune definizioni di base prese dalla teoria della Riscrittura di Termini
4460 Da queste, � dimostrato il Lemma di Newman.
4471 $(\alpha,\beta)\,\holtxt{fmap}$ di funzioni finite. Queste teoricamente
4472 hanno il tipo $\alpha\to\beta$, ma in pi� hanno solo un numero finito di
4482 La 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
4503 l'aggiornamento di una mappa con l'applicazione di una mappa. {\small\verb+fmap_EXT+} � un
4504 risultato di estensionalit�: due mappe sono uguali se hanno lo stesso dominio
4507 ({\small\verb+fmap_INDUCT+}). La cardinalit� di una mappa finita �
4541 Il dominio di una mappa finita � l'insieme di elementi a cui essa si applica;
4543 ({\small\verb+FDOM_FUPDATE+}). Il rango di una mappa � definito nel
4581 La 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
4599 Diversamente dall'unione d'insiemi, l'unione di due mappe finite
4601 prende 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
4622 un'applicazione di essa restituisca una funzione ordinaria, il rango della quale �
4624 restringendo la funzione a un insieme finito di argomenti
4638 \paragraph {Composizione di mappe}
4639 \index{composizione di funzione, nella logica HOL@composizione di funzione, nella logica \HOL{}!di mappe finite}
4641 Ci sono tre nuove definizioni di composizione, determinate dal fatto se
4642 le funzioni composte sono mappe finite o no. La composizione di due
4644 di dominio. La composizione di una mappa finita con una funzione ordinaria
4646 ordinaria. La composizione di una funzione ordinaria con una mappa finita
4669 E' un fatto curioso che la logica di ordine superiore, bench� sia una logica di
4670 funzioni totali, permetta la definizione di funzioni che non sembrano
4671 totali, almeno da un punto di vista computazionale. Un esempio
4682 x.\;\konst{T}$, l'istanza risultante di \holtxt{WHILE} sarebbe `va avanti
4686 La risposta si trova in una sottile definizione di \holtxt{WHILE},
4689 che usa il potere espressivo di HOL per un effetto sorprendente. Si consideri
4714 Da questo, � semplicemente questione di applicare la Skolemizzazione e
4715 di \holtxt{new\_specification} per ottenere l'equazione per \holtxt{WHILE}.
4720 induzione benfondata, e porta con s� dei vincoli di benfondatezza
4721 che ne limitano la sua applicazione. Al fine di applicare \verb+WHILE_INDUCTION+,
4735 Un livello di supporto pi� raffinato � fornito dalla regola \holtxt{WHILE}
4736 standard della Logica di Hoare, espressa in termini di triple Hoare
4767 Altre teorie di interesse in \HOL{} sono elencate e brevemente descritte
4780 Una teoria di polinomi su $\mathbb{R}$, che fornisce
4781 una collezione di operazioni su polinomi, e teoremi che li riguardano.
4785 Lo sviluppo di Klaus Schneider della logica temporale e\newline di $\omega$-automi.
4789 La logica Computation Tree Logic e l'$\mu$-calculo. Si veda la tesi di
4795 \caption{Una selezione di teorie \HOL{}}