\chapter{Altri Esempi}
\label{chap:more-examples}

In aggiunta agli esempi già trattati in questo testo, la distribuzione
\holn{} fornisce una varietà di esempi istruttivi nella
directory \verb|examples| Li si possono trovare (tra gli
altri) i seguenti esempi:

\begin{description}

\item [\tt autopilot.sml]

  Questo esempio è un'interpretazione \holn{} (di Mark Staples) di un
	esempio PVS dovuto a Ricky Butler della NASA. L'esempio mostra l'uso del
	pacchetto di definizione record, così come illustra alcuni aspetti
	dell'automazione disponibile in \holn{}.

\item [\tt bmark]

  In questa directory, c'è un benchmarck standard di HOL: la dimostrazione della
	correttezza di un circuito moltiplicatore, dovuto a Mike Gordon.

\item [\tt euclid.sml]

  Questo esempio è lo stesso di quello trattato nel
	Capitolo~\ref{chap:euclid}: una dimostrazione del teorema di Euclide
	sull'infintità dei numeri primi, estratto e modificato da uno sviluppo
	molto più ampio dovuto a John Harrison. Esso illustra
	l'automazione di \HOL{} su una dimostrazione classica.

\item[\tt ind\_def]

Questa directory contiene alcuni esempi di un pacchetto di definizione induttiva
in azione. In primo piano ci sono una semantica operazionale per un piccolo linguaggio
di programmazione imperativa, un piccolo sistema di algebra, una logica combinatoria
con il suo sistema di tipi. I file furono sviluppati originariamente da Tom Melham
e Juanito Camilleri e sono estesamente commentati. L'ultimo è la
base per il Capitolo~\ref{chap:combin}.

La maggior parte delle dimostrazioni in queste teorie ora possono essere fatte più facilmente
usando alcuni degli strumenti di dimostrazione sviluppati recentemente, cioè il semplificatore
e il dimostratore al primo ordine.

\item [\tt fol.sml]

  Questo file illustra l'implementazione di John Harrison di
	un dimostratore al primo ordine nello stile del model-elimination.

\item[\tt lambda]

Questa directory sviluppa le teorie di  un lambda calcolo nello stile ``de Bruijn'',
e anche una versione name-carrying. (Entrambe sono non tipizzate.) Lo sviluppo
è una revisione delle dimostrazioni che sottostanno al documento
{\it ``5 Axioms of Alpha Conversion'',
            Andy Gordon and Tom Melham,
            Proceedings of TPHOLs'96, Springer LNCS 1125}.


\item[\tt parity]

  Questa sotto directory contiene i file usati nell'esempio di parità del
	Capitolo~\ref{parity}.

\item [\tt MLsyntax]

  Questa sotto directory contiene un ampio esempio di un'infrastruttura per
	definire tipi reciprocamente ricorsivi, dovuto a Elsa Gunter del Bell Labs.
	Nell'esempio, è definito il tipo di sintassi astratta per un sottoinsieme piccolo
	ma non totalmente irrealistico di ML, insieme con una semplice funzione
	reciprocamente ricorsiva sulla sintassi.

\item[\tt Thery.sml]

  Un esempio molto breve dovuto a Laurent Thery, che mostra un'acuta
	dimostrazione induttiva.

\item[\tt RSA]

       Questa directory sviluppa parte della matematica sottostante
			 lo schema RSA di crittografia. Le teorie sono state
			 prodotte da Laurent Thery dell'INRIA Sophia-Antipolis.

\end{description}


%%% Local Variables:
%%% mode: latex
%%% TeX-master: "tutorial"
%%% End: