Filter
Top Products
50 CHAPTER 5. PRIMITIVE BASIS OF HOL LIGHT
a variable x and a term t, which may or may not contain x, one can construct
the so-called lambda-abstraction λx. t, which means ‘the function of x that yields
t’. (In HOL’s ASCII concrete syntax the backslash is used, e.g. \x. t.) For
example, λx. x + 1 is the function that adds one to its argument. Abstractions are
not often seen in informal mathematics, but they have at least two merits. First,
they allow one to write anonymous function-valued expressions without naming
them (occasionally one sees x → t[x] used for this purpose), and since our logic is
avowedly higher order, it’s desirable to place functions on an equal footing with first-
order objects in this way. Secondly, they make variable dependencies and binding
explicit; by contrast in informal mathematics one often writes f(x) in situations
where one really means λx. f(x).
We should give some idea of how ordinary mathematical and logical vocabulary
(like x + 1 above) is represented in this simple term structure. The basic idea is
quite simple. Fixed operations that one wants to use have constants corresponding
to them. For example, the negation of a real number is represented by a constant
--, and so −x is represented by the application of the constant -- to the variable
x. Exactly the same idea is used for logical operations like negation (‘not’), so ¬p
(‘not p’) is represented by the application of the logical negation constant ~ to the
term p, whatever it may be.
Application makes no special provision for functions of more than one argument,
such as addition. The trick used is known as currying, after the logician Curry
(1930). (Actually the device had previously been used by both Frege (1893) and
Sch¨onfinkel (1924), but it’s easy to understand why the corresponding appellations
haven’t caught the public imagination.) The trick is to make the operation take
its arguments ‘one at a time’. For example, rather than considering addition as a
function R × R → R, consider it as a function R → (R → R). It accepts a single
argument a, and yields a new function of one argument that adds a to its argument.
This intermediate function is applied to the second argument, say b, and yields the
final result a + b. In other words, what we write as a + b is represented by HOL
as (+ a)(b). (Certain operations like + are written infix in the concrete syntax, for
the sake of familiarity. But the use of currying is independent of this.)
This approach is used for many multiple-argument functions in HOL. However,
there is also a pairing operation ‘,’, once again written infix in the concrete syntax,
that can also be used to form pairs of terms into new terms. Of course, this itself
has to be curried, but all other functions can be written in ‘uncurried’ form to take
a tuple as its argument. Thus, what is written in the concrete syntax as f(x, y) is
actually represented in HOL as f((, x)(y)).
Operations that bind variables are common in mathematics. For example, in
lim
x→∞
1
x
, the variable x is bound by a variable-binding operation lim, and serves
merely to connect different parts of the term. It can be renamed consistently, e.g.
lim
y→∞
1
y
. By contrast, the inner term
1
x
on its own depends on the value of x, and
here x is said to be free. Some other examples of bound variables in mathematics
and logic are the variable x in the set abstraction {x | P} (‘the set of all x such that
P’), the variable n in Σ
N
n=1
n (‘the sum of all n from 1 up to N’) and the variable z in
∀z. P (‘for all z, P holds’). All these variable-binding operations are represented in
HOL using special constants but with the actual variable-binding implemented by
lambda-abstraction. For example, there is a constant liminf (‘limit at infinity’) and
one then represents lim
x→∞
1
x
by liminf(λx.
1
x
), or expanding the body completely,
liminf(λx. (/ 1)(x)). This means one should think of liminf as a function from
real functions to reals, i.e. (R → R) → R. Similarly, the logical assertion ∀x. P is
represented using the constant ! as !(λx. P).
It is well-known that there is a 1-1 correspondence between sets of elements
(drawn from some global ‘universe’ set U), and predicates or ‘characteristic func-
tions’ U → 2, where 2 is some 2-element set of truth values. In HOL, there is no