Filter
Top Products
2 CHAPTER 1. INTRODUCTION
calculators and CASs are often open to doubt — even for something as trivial
as explicit calculation involving approximations like sin(0.7) = 0.6442176872.
Moreover, CASs often leave out essential sideconditions such as denominators
of fractions being nonzero.
Needless to say, this greater power and reliability comes at a price.
• Only in limited problem domains can HOL Light produce its theorems com-
pletely automatically. In general, the user needs to describe a suitable math-
ematical proof in reasonable detail — HOL Light merely fills in some of the
simpler gaps and checks that the user doesn’t make mistakes.
• Whereas calculators and CASs are highly efficient and optimized for the typi-
cal problems, HOL Light derives its theorems via a uniform mechanism which
tends to be less efficient in particular cases.
Like good calculators and CASs, HOL Light is programmable. This means that
one can start with the available functions for proving certain theorems automat-
ically, and produce new ones for particular tasks by implementing them in terms
of the original ones. Similarly, a simple scientific calculator might have a built-in
function to approximate sin, but none for evaluating, say, areas under the normal
distribution curve — the user has to program the latter. Once this has been done,
it can itself become a subroutine in more complex operations.
The majority of the HOL Light system is a tower of such functions. Right at the
bottom, a very small set of primitive operations ultimately produce all theorems.
In terms of these, more convenient higher-level functions are defined, these are
themselves used to build up additional layers, and so on. Any user can build up
this tower further. Because theorems are ultimately produced by the primitive rules,
errors in higher-level functions cannot lead to false ‘theorems’ being produced; this
explains the claim that HOL Light is relatively reliable. (A similar claim cannot
be made for ordinary calculators since the answers are often approximate, and it’s
hard to analyze how the inaccuracy builds up.)
This approach to theorem proving, using programmability to build up from a
small and reliable logical core, originated with the Edinburgh LCF project (Gordon,
Milner, and Wadsworth 1979). For the approach to be palatable, the programming
language must be well suited to the task, and as part of the LCF project a completely
new programming language called ML
3
was developed. ML has since taken on a life
of its own and is currently being widely touted as a general-purpose language. It
is a higher-order functional programming language, featuring a novel polymorphic
type system (Milner 1978) and a simple but useful exception mechanism as well as
some traditional imperative features.
The version of ML used in HOL Light is CAML Light (Weis and Leroy 1993).
This language and an excellent lightweight interpreter for it have been developed
by a team at INRIA Rocquencourt in Paris. HOL Light has no separate user
interface: the user actually works inside the CAML interpreter with all the HOL
Light infrastructure loaded in.
HOL Light is the latest in a line of theorem provers going back to the mid-
eighties, using the LCF approach to implement a theorem prover for classical Higher
Order Logic (hence the name HOL). Previous versions have included HOL88, hol90,
ICL ProofPower, and more recently hol98. HOL Light is intended to be a more
simple and elegant version targeted at users who really want to understand how the
3
ML for metalanguage; following Tarski (1936) and Carnap (1937), it has become usual to en-
force a strict separation between the ‘object language’ under consideration and the ‘metalanguage’
used to talk about it. For example in a course in Russian given in English, Russian is the object
language and English the metalanguage.