Notes to The Lambda Calculus
1. When laying out the early principles of λ-calculus, Church restricted β-reduction to only those cases where variable capture does not occur. As an illustration of the kinds of difficulties that can arise if one is too casual about free and bound variables, one can formulate a sequent calculus for first-order logic where cut elimination fails if one views first-order formulas as concrete objects rather than as an equivalence class of α-convertible formulas.
2. Other definitions of substitution are available. One can, for example, modify clause (5) by requiring that all free occurrences of y in M are rewritten so that they do not become bound after substitution. In this way the variable capture that we are trying to avoid is built in to the definition of substitution and thereby does not need to be laid down as a separate convention.
There is a small price to pay for such an approach, though: the definition of substitution is somewhat more complicated than the straightforward definition given here. There is even some nondeterminism in such an approach to substitution: if we need to rewrite free occurrences of y in M before substituting M for free occurrences of x in λy[A], how should we do it? Which of the infinitely many variables should we choose? One can get around this difficulty by using a predefined enumeration of the set of variables, or by other syntactic measures such as the so-called de Bruijn representation of terms (which this entry does not treat). Our straightforward approach suffices for this entry's introductory purposes.
3. The theorem says given M one can find at least one F that Fx = M, but in fact there are infinitely many. For example, if Fx = M, then KFK also works. Church's initial understanding of λx[M] was existential—a solution of Fx = M for F—though nowadays one understands λx[M] as a unique object, namely, the function that, given x, produces M.
4. This is not to say that no sense whasotever can be made of adding 5 and the identity function. The intention of this example is to motivate the differentiation of a domain of discourse into kinds or types.
Indeed, if one wanted, one possible strategy for interpreting such a combination would be to ‘promote’ the number 5 by reading it as the constant function λx[5]; we then need to understand addition of unary functions. One can can naturally understand (λx[5]) + (λx[x]) as (λx[5 + x]).
5. If an untyped λ-term M can be assigned one type, then it can be assigned infinitely many types: for any type variable a occurs in the type σ assigned to M, one can substitute any type τ, and the result is still a type for M. For example, the combinator I can be assigned the type a → a. Thus, it can be assigned the types:
- a → a
- a → (a → a)
- (a → a) → a
- (a → a) → (a → a)
- …
It is thus not correct to talk about the type of a typable term.
Nonetheless, a result known as the principal type theorem assures us that the situation with I just illustrated is typical: if a term M can be assigned a type at all, then there is a type τ such that all types that can be assigned to M are instances of τ. Such a type is called a principal type of M. Even though it is improper to talk about the principal type of a typable term—if a and b are distinct type variables, then a → a and b → b are distinct principal types of I—there is still a precise sense in which there is one and only one principal type of a typable term: a → a and b → b are simply (uniform) substitution instances of each other.
There is an algorithm for computing principal types; see (Hindley, 1997, chapter 3).
6. Definition: For a natural number n, define cn, the nth Church numeral, as λf[λx[fnx]]. (‘fnx’ is the application of the n-fold iteration of f to x.)
Thus c0, the Church numeral for the natural number 0, is λx[x], c1 is λf[λx[fx]], c2 is λf[λx[f(fx)]], and so forth.
