Filter
Top Products
Chapter 5
Primitive basis of HOL Light
The introductory chapter gave a brief introduction to the key ideas behind HOL and
simple interaction with the system. Here we explain more systematically how math-
ematical and logical assertions are represented in HOL, and list all the primitive
ways of producing theorems.
We should distinguish carefully between abstract and concrete syntax. The ab-
stract syntax of a term, which HOL deals with internally, is a tree-like CAML data
structure indicating how the term is built up from its components. While this is
convenient to manipulate, humans are more used to representing terms by a linear
sequence of characters, the concrete syntax. HOL’s quotation parser automatically
translates the concrete syntax into the abstract syntax, and its prettyprinter per-
forms an inverse mapping back to concrete syntax. For simple use of HOL, it is not
necessary to think much about the distinction, still less to understand details of the
abstract syntax. However, we think it is best to cover this early, since it shows how
simple the underlying structures really are. The present chapter can be read as an
abstract description of the HOL logic, without considering the actual implementa-
tion in CAML. However when we discuss concrete syntax, we are implicitly talking
about that accepted by HOL’s parser.
5.1 Terms
HOL’s logic is based on λ-calculus, a formalism invented by Alonzo Church. In HOL,
as in λ-calculus, terms are built up starting just from constants and variables using
application and abstraction. All mathematical and logical assertions are represented
in this uniform way.
Constants and variables are probably familiar to the reader from an informal
understanding of mathematics. They are used as the building-blocks of terms.
Variables can have any name, e.g. n, x, p. Constants, e.g. [] (the empty list),
(true) and ⊥ (false), are intended to be abbreviations for other terms, and except
for a couple of primitive ones such as equality itself, need to have been defined
before they can be used in terms. We will see below how the user can define new
constants.
Application is application of a function to an argument, an operation used con-
stantly in mathematics. The customary concrete syntax for the application of a
function f to an argument t is f(t). HOL, following lambda-calculus convention,
allows the parentheses to be omitted, unless they are needed because t is itself a
compound term. For example, f(g(x)) needs at least the outer pair of parentheses,
as HOL’s parser interprets f g x to mean (f(g))(x), for reasons explained shortly.
Abstraction is in a precise sense a converse operation to application. Given
49