1 2\chapter{Altri Esempi} 3\label{chap:more-examples} 4 5In aggiunta agli esempi gi� trattati in questo testo, la distribuzione 6\holn{} fornisce una variet� di esempi istruttivi nella 7directory \verb|examples| Li si possono trovare (tra gli 8altri) i seguenti esempi: 9 10\begin{description} 11 12\item [\tt autopilot.sml] 13 14 Questo esempio � un'interpretazione \holn{} (di Mark Staples) di un 15 esempio PVS dovuto a Ricky Butler della NASA. L'esempio mostra l'uso del 16 pacchetto di definizione record, cos� come illustra alcuni aspetti 17 dell'automazione disponibile in \holn{}. 18 19\item [\tt bmark] 20 21 In questa directory, c'� un benchmarck standard di HOL: la dimostrazione della 22 correttezza di un circuito moltiplicatore, dovuto a Mike Gordon. 23 24\item [\tt euclid.sml] 25 26 Questo esempio � lo stesso di quello trattato nel 27 Capitolo~\ref{chap:euclid}: una dimostrazione del teorema di Euclide 28 sull'infintit� dei numeri primi, estratto e modificato da uno sviluppo 29 molto pi� ampio dovuto a John Harrison. Esso illustra 30 l'automazione di \HOL{} su una dimostrazione classica. 31 32\item[\tt ind\_def] 33 34Questa directory contiene alcuni esempi di un pacchetto di definizione induttiva 35in azione. In primo piano ci sono una semantica operazionale per un piccolo linguaggio 36di programmazione imperativa, un piccolo sistema di algebra, una logica combinatoria 37con il suo sistema di tipi. I file furono sviluppati originariamente da Tom Melham 38e Juanito Camilleri e sono estesamente commentati. L'ultimo � la 39base per il Capitolo~\ref{chap:combin}. 40 41La maggior parte delle dimostrazioni in queste teorie ora possono essere fatte pi� facilmente 42usando alcuni degli strumenti di dimostrazione sviluppati recentemente, cio� il semplificatore 43e il dimostratore al primo ordine. 44 45\item [\tt fol.sml] 46 47 Questo file illustra l'implementazione di John Harrison di 48 un dimostratore al primo ordine nello stile del model-elimination. 49 50\item[\tt lambda] 51 52Questa directory sviluppa le teorie di un lambda calcolo nello stile ``de Bruijn'', 53e anche una versione name-carrying. (Entrambe sono non tipizzate.) Lo sviluppo 54� una revisione delle dimostrazioni che sottostanno al documento 55{\it ``5 Axioms of Alpha Conversion'', 56 Andy Gordon and Tom Melham, 57 Proceedings of TPHOLs'96, Springer LNCS 1125}. 58 59 60\item[\tt parity] 61 62 Questa sotto directory contiene i file usati nell'esempio di parit� del 63 Capitolo~\ref{parity}. 64 65\item [\tt MLsyntax] 66 67 Questa sotto directory contiene un ampio esempio di un'infrastruttura per 68 definire tipi reciprocamente ricorsivi, dovuto a Elsa Gunter del Bell Labs. 69 Nell'esempio, � definito il tipo di sintassi astratta per un sottoinsieme piccolo 70 ma non totalmente irrealistico di ML, insieme con una semplice funzione 71 reciprocamente ricorsiva sulla sintassi. 72 73\item[\tt Thery.sml] 74 75 Un esempio molto breve dovuto a Laurent Thery, che mostra un'acuta 76 dimostrazione induttiva. 77 78\item[\tt RSA] 79 80 Questa directory sviluppa parte della matematica sottostante 81 lo schema RSA di crittografia. Le teorie sono state 82 prodotte da Laurent Thery dell'INRIA Sophia-Antipolis. 83 84\end{description} 85 86 87%%% Local Variables: 88%%% mode: latex 89%%% TeX-master: "tutorial" 90%%% End: 91