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