1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
|
\chapter*{Preface}\markboth{Preface}{Preface}
\label{intro}
This volume contains the description of the \HOL\ system.
It is one of three volumes making up the documentation for \HOL:
\begin{myenumerate}
\item \TUTORIAL: a tutorial introduction to \HOL, with case studies.
\item \DESCRIPTION: a description of higher order logic,
the \ML\ programming language, and theorem proving methods in the \HOL\ system;
\item \REFERENCE: the reference manual for \HOL.
\end{myenumerate}
\noindent These three documents will be referred to by the short names (in
small slanted capitals) given above.
This document, \DESCRIPTION, is intended to serve both as a definition of \HOL\
and as an advanced guide for users with some prior experience of the system.
Beginners should start with the companion document \TUTORIAL.
The \HOL\ system is designed to support interactive theorem proving in higher
order logic (hence the acronym `\HOL'). To this end, the formal logic is
interfaced to a general purpose programming language (\ML, for meta-language)
in which terms and theorems of the logic can be denoted, proof strategies
expressed and applied, and logical theories developed. This document presents
the definitions of the meta-language and the logic, and it explains the means
by which meta-language functions can be used to generate proofs in the logic.
The version of higher order logic used in \HOL\ is predicate calculus with
terms from the typed lambda calculus (\ie\ simple type theory). This was
originally developed as a foundation for mathematics \cite{Church}. The
primary application area of \HOL\ was initially intended to be the
specification and verification of hardware designs. (The use of higher order
logic for this purpose was first advocated by Keith Hanna \cite{Hanna-Daeche}.)
However, the logic does not restrict applications to hardware; \HOL\ has been
applied to many other areas.
The approach to mechanizing formal proof used in \HOL\ is due to Robin Milner
\cite{Edinburgh-LCF}, who also headed the team that designed and implemented
the language \ML. That work centred on a system called \LCF\ (logic for
computable functions), which was intended for interactive automated reasoning
about higher order recursively defined functions. The interface of the logic
to the meta-language was made explicit, using the type structure of \ML, with
the intention that other logics eventually be tried in place of the original
logic. The \HOL\ system is a direct descendant of \LCF; this is reflected in
everything from its structure and outlook to its incorporation of \ML, and even
to parts of its implementation. Thus \HOL\ satisfies the early plan to apply
the \LCF\ methodology to other logics.
The original \LCF\ was implemented at Edinburgh in the early 1970's, and is now
referred to as `Edinburgh \LCF'. Its code was ported from Stanford Lisp to
Franz Lisp by G\'erard Huet at {\small INRIA}, and was used in a French
research project called `Formel'. Huet's Franz Lisp version of \LCF\ was
further developed at Cambridge by Larry Paulson, and became known as `Cambridge
\LCF'. The \HOL\ system is implemented on top of an early version of Cambridge
\LCF\ and consequently many features of both Edinburgh and Cambridge \LCF\ were
inherited by \HOL. For example, the axiomatization of higher order logic used
is not the classical one due to Church, but an equivalent formulation
influenced by \LCF.
The language \ML\ has now achieved status as a programming language in its own
right, although it was originally designed as the proof management language for
\LCF. It is a functional language distinguished particularly for its type
inference mechanism, that gives type security without overburdening the user.
Types, and especially abstract types, are the basis for distinguishing the
theorems of a logic from arbitrary formulae, in a secure way.
A standard has now been established for \ML\ (\cite{sml}), but for historical
reasons, the \HOL\ system includes an earlier version of \ML. There are,
however, two new implementations of \HOL\ in progress that are based on
Standard \ML\ rather than Lisp (see below). The most recent version of
Cambridge \LCF, which is documented in Paulson's book \cite{new-LCF-man}, is
also based on Standard \ML.
In this document, the acronym `\HOL' refers to both the interactive theorem
proving system and to the version of higher order logic that the system
supports; where there is serious ambiguity, the former is called `the \HOL\
system' and the latter `the \HOL\ logic'.
An enhanced and rationalized version of \HOL, called \HOL 88, was released (in
1988), after the original \HOL\ system had been in use for several years. \HOL
88 Version 2.0 (\HOL 88.2.0) is the system described in this document. This
is intended to serve as a stable platform for a number of research projects and
technology transfer activities that are in progress at Cambridge, and
elsewhere, at the time of writing. It is also the supported version of the
system for the international \HOL\ community. The main differences between
Version 2.0 and earlier releases are described in Appendix~\ref{appendix}.
\section*{The future}
As mentioned above, there are two new implementations of \HOL\ nearing
completion, both based on Standard \ML\ instead of Lisp. One is a
public domain system developed at the University of Calgary
(preliminary versions of this are already available). The other, which
is being developed by ICL Secure Systems, is a `highly assured' system
for commercial verification projects in the safety and security
critical areas.
The contact address for Calgary \HOL\ is:
\begin{center}
\begin{tabular}{l}
Graham Birtwistle\\
Computer Science Department\\
University of Calgary\\
2500 University Drive\\
Calgary\\
Alberta\\
Canada T2N 1N4\\[2mm]
({\tt email:} graham@cpsc.ucalgary.ca)
\end{tabular}
\end{center}
\noindent and the contact address for ICL \HOL\ is:
\begin{center}
\begin{tabular}{l}
Roger B. Jones \\
International Computers Limited\\
Eskdale Road\\
Winnersh\\
Wokingham\\
Berkshire RG11 5TT\\
England\\[2mm]
({\tt email:} R.B.Jones@win0103.uucp
\end{tabular}
\end{center}
The Cambridge group intends to continue to support the Lisp based
version of \HOL\ at least until it is clearly superseded (which is not
expected to be for several years). The emphasis will be on improving
the existing system and documentation, rather than adding new
features. However, there is a research project in progress at Inria
(Sofia-Antipoles, France), to develop a new and experimental interface
to \HOL. This research is being done in collaboration with the
Cambridge \HOL\ group and aims to answer the question of whether \HOL\
can be made significantly easier to use with a state-of-the-art mouse
and window interface. It is also exploring the use of colour for
managing complexity. If this experiment is successful, then a
production version of the new interface may be produced for general
use. It is not expected that this will be undertaken before 1992.
|
