## 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 *F**x* = *M*, but in fact there are infinitely
many. For example, if *F**x* = *M*,
then **K**F**K** also works. Church's initial understanding of
λ*x*[*M*] was existential—a solution
of *F**x* = *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 **c**_{n},
the *n*th ** Church numeral**, as
λ

*f*[λ

*x*[

*f*

^{n}

*x*]]. (‘

*f*

^{n}

*x*’ is the application of the

*n*-fold iteration of

*f*to

*x*.)

Thus **c**_{0}, the Church numeral for the natural
number 0, is λ*x*[*x*], **c**_{1} is
λ*f*[λ*x*[*f**x*]], **c**_{2}
is λ*f*[λ*x*[*f*(*f**x*)]], and
so forth.