Filter
Top Products
5.2. TYPES 51
separate notion of ‘set’: they are identified with predicates, i.e. Boolean-valued
functions. Thus, one can simply write s x instead of x ∈ s, though the latter is
also possible using the infix constant IN, e.g. x IN s. It is thus normal and often
convenient to slip between thinking of truth-functions as predicates or as sets, even
within the same term.
5.2 Types
Application and abstraction are converse in the precise sense that (λx. t)(x) is
equal to t, and there is a primitive HOL rule to make this inference and produce
the theorem (λx. t)(x) = t. More generally, HOL is capable of proving that
(λx. t)(s) = t[s/x] where the right-hand side denotes the appropriate (see later)
replacement of each instance of x in t by s. For example, (λx. 1 + x)(y) = 1 + y.
Unfortunately, even these banalities would allow one to get inconsistencies without
further restrictions. For example, using the logical negation operation, we can derive
the Russell paradox about the set of all sets that do not contain themselves (think
of P x as x ∈ P if preferred):
(λx. ¬(x x))(λx. ¬(x x)) = ¬((λx. ¬(x x))(λx. ¬(x x)))
In other words, something is equal to its own logical negation! The problem
seems to arise because no proper distinction of levels is made: x is treated both as
a predicate and the argument to a predicate. Even if it didn’t lead to inconsistency,
one might argue that it looks a bit strange. Normally one likes to have a clear idea of
what sort of mathematical object a term denotes — our explanation of currying, for
example, leaned on the idea that addition is thought of as a function R → (R → R).
Accordingly, Church (1940) augmented λ-calculus with a theory of types, simpli-
fying Russell’s system from Principia Mathematica (Whitehead and Russell 1910)
and giving what is often called ‘simple type theory’. HOL follows this system quite
closely. Every term has a unique type which is either one of the basic types or the
result of applying a type constructor to other types. The only basic type in HOL
is initially the type of booleans bool and the only type operator is the function
space constructor →. (Many others are added later, as we shall see.) HOL extends
Church’s system by allowing also ‘type variables’ which give a form of polymor-
phism. Constants with polymorphic type are generic, and can have various types
resulting from fixing the names of the type variables. For example, the equality
relation has type α → α → bool where α is a type variable. This means it can be
used with any types, even if they themselves involve type variables, replacing α.
Just as in typed programming languages, functions may only be applied to
arguments of the right type; only a function of type f : γ → . .. may be applied to
an argument of type γ.
For familiarity, types are written in a concrete syntax with some type construc-
tors like → written infix. Just as with constant and variable terms, type variables
and type constants are not distinguished syntactically: HOL’s parser assumes that
everything whose name corresponds to a constant is a constant, and every other
identifier is a variable. However, it’s customary to use names beginning with an
uppercase letter for type variables, e.g. A and State. Examples of HOL types then,
include bool and A → bool (where A is a type variable). We write t : γ to indicate
that a term t has type γ. Readers familiar with set theory may like to think of types
as sets within which the objects denoted by the terms live, so t : γ can be read as
t ∈ γ. Note that the use of the colon is already standard in set theory when used
for function spaces, i.e. one typically writes f : A → B rather than f ∈ A → B.