We begin our reassessment of the constructions needed in mathematics by considering the function-type and sum. The system of types which is freely generated by the binary symbols x, ® and + from Æ, 1 and a given collection of base types or sorts will be called simple type theory. Applied to sets, Æ, 1, x, + and ® refer to the constructions of Section 2.1. Recall that these were accompanied by operations such as pi, ni and ev, which we shall now discuss. Later we shall show how certain other mathematical objects admit directly analogous structures.
Function (l) abstraction Sections 1.1-1.3 discussed how functions act, but they must also be considered as entities in themselves. Early in the history of the integral calculus problems arose in which the unknown was a function as a whole, rather than its value at particular or even all points: the Sun's light takes that path through the variable density of the atmosphere which minimises the time of travel; the motion of a stretched string depends on its initial displacement along its whole length.
REMARK 2.3.1 In order to consider a function per se, we must first identify which of the unknowns in an expression p are inputs. Lambda abstraction, l[(x)\vec], does this, thereby binding these variables (Definition 1.1.6). Sometimes the function already has a name, such as sin or sine, but the squaring function can only be written as 2 or, now, as lx.x2. Since l is clearer than the informal notation p(x) of Remark 1.1.2 as a way of distinguishing the inputs from other variables, we treat all variables, whether free or bound, as part of the expression p.
Given a function f and an argument a, the one may be applied to the other and evaluated to a result. This is usually written fa without brackets, in which the juxtaposition denotes a formal operation of application; as we shall need to study this operation in its own right, we shall sometimes write ev(f,a) instead. The result of the evaluation, which was written p(a) informally, is p[x: = a]. The passage (using substitution)
from (lx.p)a to p[x: = a]
is called b-reduction. See Definition 1.2.2 for related terminology.
We also identify lx.sinx with sin, and more generally
|
Besides the type-theoretic rules, we also intend that the constants may have their own laws, or d-rules, as they are known in the l- calculus.
For us, all terms are typed: if x and p have types X and Y, the abstraction lx.p has type X® Y º YX. Notice that the two reduction rules preserve type, ie they obey subject reduction, Definition 1.2.12.
The type X® (Y® Z) or (ZY)X º Z(XxY) is that of a function of two arguments. This trick - of using l-abstraction to supply multiple arguments one by one to a function - is called Currying, though it had been observed by Moses Schönfinkel and was implicit in Frege's work.
CONVENTION 2.3.2 It is customary to omit the brackets as follows:
omitted eqnarray* environment
The notation is further abbreviated to [(X)\vec]® Y, f[(a)\vec] and l[(x)\vec].p respectively. As this deals with many-argument functions (in fact in a rather useful way), many authors omit pairing from the calculus. By contrast, the type (X® Y)® Z is that of what is sometimes called a function al, ie a function whose argument is itself a function, and so is more complex.
Normalisation A distinction is made between (lx.p)a and p[x: = a], and between application and evaluation, since the result of a b-reduction is frequently a longer expression than the first: it may contain more ls and so more opportunities for further reduction than the original term. So strategies for b-reduction are an important topic of study in themselves.
FACT 2.3.3 The Church-Rosser Theorem says that the pure l-calculus (without d-rules) is confluent (Definition 1.2.5). The simply typed pure l-calculus is also strongly normalising (Definition 1.2.8). []
The Church-Rosser Theorem relies too much on intricacies of syntax to be appropriate for this book: see, eg , [Bar81], [LS86] and [Bar92] for a detailed treatment. The result is valid in many different calculi - including the untyped l-calculus, in which the normalisation theorems fail - but unfortunately breaks down in some variations which seem semantically benign, such as the untyped calculus with surjective pairing. Without the type discipline (Notation 1.3.3) there need be no normal form to which a term reduces. For example the term (lx.xx)(lx.xx) reduces to itself, and there are much worse phenomena.
The depth of bracket nesting, with the above Convention for omitting them, considered as a notion of type complexity, can be used to prove weak normalisation : see Example 2.6.4. It follows from Fact 2.3.3 and Theorem 1.2.9 that normal forms exist and are unique. They are characterised in Exercise 2.23, and used in Theorem 7.6.15. Section 7.7 shows in another way that every term is provably equal to a normal form.
REMARK 2.3.4 When the l-calculus is used as a programming language [ Plo77], it is usual to forbid b-reduction under l, as lx.p is regarded as an as yet passive fragment of code, which is only activated when it is applied to some argument. Then there is a choice whether
Contexts for the l-calculus The variable governed by l-abstraction, like that bound by the quantifiers $ and ", is generic, so we use boxes to delimit it. As in Section 1.5, the variable cannot be used outside the box, because to do so would restrict its generality and prejudice the question of whether its type is empty.
DEFINITION 2.3.5 The box rules for l-abstraction and application are
|
NOTATION 2.3.6 As for the predicate calculus (Definition 1.5.3), the abstract study of the l-calculus needs a sequent form in which
|
DEFINITION 2.3.7 The sequent forms of the rules for l-terms are
|
|
|
|
REMARK 2.3.8 We need structural rules for terms as well as formulae (Definition 1.4.8). In fact these ought to have been given for the ("Á )- and ($E )-boxes (Definition 1.5.1), in order to import terms.
|
REMARK 2.3.9 There is a superficial similarity between the b- and cut rules. To see the b-rule in action in a symbolic idiom we need to use general expressions for the body p and argument a of the function, cf the various ways of expressing conjunction as a sequent rule in Remark 1.4.9; Example 7.2.7 gives a diagrammatic version with variables instead. Cut makes these substitutions, and this explains the likeness.
The substitution rule (Definition 1.1.10(d)) relates cut to (® Á ):
|
The sum type The rules for sum largely mirror those for product. The pair a,b for the product is supplied by the data, and the program uses pi to extract what it needs. For the sum, the program provides a pair [f,g] of options, from which the input makes a selection using ni. There is an ultimate result type Q to mirror the context of parameters G. This symmetry is much more (arguably too) obvious in the categorical presentation (Sections 5.3-5.5); it is really spoilt by the asymmetry of the term calculus, in which the input but not the output may involve parameters. The defects require new variable-binding operations, and rules to handle substitution and its dual notion of continuation.
These rules are rather technical and will not be relevant until Section 5.3, so you should skip the rest of this section unless you are already very familiar with the typed l-calculus expressed in a contextual style.
REMARK 2.3.10 The sum type has inclusions n0 and n1,
|
|
|
|
omitted eqnarray* environment
The h-rule says that if the two branches contain the same code p then the switch is redundant: [\Case 0 x.p(n0(x)), \Case 1 y.p(n1(y))](c) = p(c).
There is also an equality rule similar to (l = ) in Definition 2.3.7.
REMARK 2.3.11 Just as pairing handles many-argument operations uniformly, so l- abstraction avoids the need for other variable binders. Thus (+E) can be put in a form which doesn't itself alter the context:
|
|
REMARK 2.3.12 Terms may be imported into the boxes, with the effect of substituting for free variables within the binding. The rule for this is exactly analogous to that in Definition 1.1.10(d),
|
|
REMARK 2.3.13 Remark 1.6.5 showed that the ($E )- box is essentially open-ended below: any phrase of proof not involving the bound variable can be moved in or out. The (+E)-rule has the same property, but now that we are discussing significant terms rather than anonymous proofs, we must state another law, called a continuation rule or commuting conversion. This says that moving the continuation z into or out of the box has no effect,
|
As for the function-type, these reduction rules interact, and questions of confluence and normalisation have to be studied. For example we would like to know that every definable closed term of sum type is provably equal to either n0(a) or n1(b). This will be considered in Section 7.7.
REMARK 2.3.14 Since there are two binary introduction rules, there is no nullary one (and so no b-rule either), and as the binary elimination rule has two cases (premises), the nullary one has none.
|
Contexts will be developed in Section 4.3 and Chapter VIII. Sections 4.5- 4.7 give a categorical account of products and function-types , applying the former to universal algebra. We discuss the binary sum further in Section 5.3ff, along with the if then else fi programming construct. Section 9.3 treats the infinitary (dependent type) analogue, Sx.Y[x].