1\chapter*{Prefazione}\markboth{Prefazione}{Prefazione}
2\label{intro}
3
4Questo volume contiene la descrizione del sistema \HOL.
5E' uno di quattro volumi che compongono la documentazione per \HOL:
6
7\begin{myenumerate}
8\item \LOGIC: una descrizione formale della logica di ordine superiore
9  implementata dal sistema \HOL{}.
10\item \TUTORIAL: un tutorial d'introduzione a \HOL, con dei casi di studio.
11\item \DESCRIPTION: una guida utente dettagliata per il sistema \HOL{}.
12\item \REFERENCE: il manuale di riferimento per \HOL.
13\end{myenumerate}
14
15\noindent Si far� riferimento a questi quattro documenti con i nomi abbreviati (in
16maiuscoletto inclinato) dati di sopra.
17
18Questo documento, \DESCRIPTION, � una guida avanzata per utenti con qualche
19esperienza precedente del sistema. I principianti dovrebbero iniziare con il
20documento di accompagnamento \TUTORIAL.
21
22Il sistema \HOL\ � sviluppato per supportare la dimostrazione interattiva di teoremi nella
23logica di ordine superiore (da qui l'acronimo `\HOL' [Higher Order Logic (ndt)]). A questo scopo, la logica
24formale � interfacciata a un linguaggio di programmazione di scopo generale (\ML, per
25meta-linguaggio) in cui possono essere denotati i termini e i teoremi della logica,
26possono essere espresse ed applicate le strategie di dimostrazione, e sviluppate le teorie logiche.
27La versione della logica di ordine superiore usata in \HOL\ � il calcolo dei predicati
28con termini dal lambda calcolo tipizzato (cio� la teoria dei
29tipi semplici). Questo fu inizialmente sviluppato come una fondazione per la matematica
30\cite{Church}. La principale area di applicazione di \HOL\ fu inizialmente
31intesa essere la specifica e la verifica dei modelli hardware.
32(L'uso della logica di ordine superiore a questo scopo fu inizialmente difesa da
33Keith Hanna \cite{Hanna-Daeche}.) Tuttavia, la logica non limita
34le applicazione all'hardware; \HOL\ � stato applicato a molte altre aree.
35
36Questo documento presenta la logica \HOL\ nella sua forma \ML{}, e
37spiega i mezzi con cui le funzioni del meta-linguaggio possono essere usate per
38generare dimostrazioni nella logica. Cos�. descrive come il sistema
39astratto di \LOGIC{} � di fatto implementato nel linguaggio di programmazione
40\ML{}, fornendo una descrizione complessiva delle principali caratteristiche
41del sistema.
42
43L'approccio di meccanizzare le dimostrazioni formali usato in \HOL\ � dovuto a Robin
44Milner \cite{Edinburgh-LCF}, che ha anche diretto il team che ha progettato
45e implementato il linguaggio \ML. Quel lavoro era centrato su un sistema
46chiamato \LCF\ (logica per le funzioni computabili), che era inteso per
47il ragionamento interattivo automatizzato circa funzioni di ordine superiore definite
48ricorsivamente. L'interfaccia della logica al meta-linguaggio era reso
49esplicito, usando la struttura di tipi dell'\ML, con l'intenzione che alla fine
50altre logiche sarebbe state provate al posto della logica originaria. Il
51sistema \HOL\ � un discendente diretto di \LCF; questo � riflesso in
52ogni cosa dalla sua struttura e aspetto alla sua incorporazione dell'\ML,
53e persino a parti della sua implementazione. Cos� \HOL\ soddisfa il
54piano iniziale di applicare la metodologia \LCF\ ad altre logiche.
55
56L'\LCF\ originario fu implementato ad Edimburgo nei primi anni 1970, ed ora ci si
57riferisce ad esso come all'`\LCF di Edimburgo'. Il suo codice fu portato dallo Stanford Lisp
58al Franz Lisp da G\'erard Huet presso l'{\small INRIA}, e fu usato in un progetto di ricerca
59francese chiamato `Formel'. La versione Franz Lisp dell'\LCF\ di Huet fu
60ulteriormente sviluppata a Cambridge da Larry Paulson, e divenne conosciuta come il
61`Cambridge \LCF'. Il sistema \HOL\ � implementato sulla base di una prima versione del Cambridge
62\LCF\ e di conseguenza molte delle caratteristiche sia dell'Edinburgh che del Cambridge \LCF\ furono
63ereditate da \HOL. Per esempio, l'assiomatizzazione della logica di ordine superiore utilizzata
64non � quella classica dovuta a Church, ma una formulazione equivalente
65influenzata da \LCF.
66
67Una versione avanzata e razionalizzata di \HOL, chiamata \HOL 88, fu
68rilasciata (nel 1988), dopo che il sistema \HOL\ originario era stato in uso
69per molti anni. \HOL 90 (rilasciato nel 1990) fu un porting di \HOL 88
70in SML \cite{sml} da parte di Konrad Slind presso l'Universit� di Calgary. Esso � stato
71ulteriormente sviluppato nel corso degli anni 1990. \HOL{} 4 � l'ultima
72versione di \HOL, e anch'esso � implementato in SML; � dotato di un numero
73di novit� rispetto ai suoi predecessori. \HOL{} 4 � anche la
74versione del sistema supportata per la comunit� internazionale \HOL.
75
76Abbiamo deciso di numerare le implementazioni di \HOL{} retroattivamente nel
77modo seguente
78\begin{enumerate}
79\item \HOL88 e precedenti: implementazioni basate su un substrato Lisp,
80	con l'ML Classico.
81\item \HOL90: implementazioni in Standard ML, che usano principalmente
82	l'implementazione SML/NJ.
83\item \HOL98 (distribuzioni Athabasca e Taupo): implementazioni che usano
84	il Moscow ML, e con una nuova libreria e un nuovo meccanismo di teoria.
85\item \HOL{} (distribuzioni Kananaskis)
86\end{enumerate}
87Di conseguenza, con \HOL{}~4, facciamo a meno dell'abitudine di associare
88le implementazioni con i numeri degli anni. Le distribuzioni individuali all'interno
89di \HOL{}~4 conservano lo schema di nome \textit{lake-number}.
90
91In questo documento, l'acronimo `\HOL' si riferisce sia al sistema di dimostrazione
92interattiva di teoremi sia alla versione di logica di ordine superiore che il sistema
93supporta; dove c'� una seria ambiguit�, il primo � chiamato `il sistema
94\HOL' e la seconda `la logica \HOL'.
95
96
97%%% Local Variables:
98%%% mode: latex
99%%% TeX-master: "description"
100%%% End:
101