Lambda Calculus
July 25, 2018
These notes (unfinished, obviously) were of a course I took on lambda cal-
culus, proof, and category theory.
I Introduction 2
1. What is a function? . . . . . . . . . . . . . . . . . . . . . . . . . 2
II Untyped λ-calculus 3
1. Terms and variables . . . . . . . . . . . . . . . . . . . . . . . . . 3
2. Change of bound variables and α-congruence . . . . . . . . . . . 4
3. Equality, =, and β-equivalence . . . . . . . . . . . . . . . . . . . 5
4. Combinatory calculus . . . . . . . . . . . . . . . . . . . . . . . . 7
I Introduction
1. What is a function?
There are two main roots of the theory of functions:
(a) analytic geometry (Descartes).
(b) the development of calculus (Leibniz, 1673, in a letter to Bernoulli).
Euler and Dirichlet concerned themselves more with numerical functions, and
in the 19th century, Bolzano, Cauchy, Weierstrass, and Fourier all had the
understanding of an analytic representation of functions:
ϕ(x) = . . . ,
for some formula. It was Fourier who first broke it! The modern definition is
due to set theory, namely Dedekind and Cantor. Bourbaki’s definition is that a
function from A B is a triple (A, R, B) such that:
(i) A and B are sets.
(ii) R A × B (the “graph”).
(iii) x A!y B . (x, y) R.
Intuitively, R(x, y)” f (x) = y”. We now say that (A, R, B) = (A
, B
, R
if and only if A = A
, B = B
, and R = R
A × B. So the modern functions
are equivalence classes of such triples:
f = g x A . f(x) = g(x).
Consider the expressions:
2 + 3 = 5, 5 = 5.
The left is dynamic, however the right is tautological.
In λ-calculus, we remove A, B from the triple. So if we wrote f as:
f : A B : x 7→ f(x),
λ-calculus only concerns itself with the rule of transformation, x 7→ f(x). In
the way, we write f now as:
the λ indicating that x is the scope of the function, and that we just replace x
in the rule f(x) with whatever we apply λx.f (x) to. A few explicit examples:
, λx.2x, λx. sin x.
To apply a function f in Λ-calculus to something a, we write f a. This conven-
tion is due to Bertrand Russell. A few more examples:
)‘a = x
[a/x] = a
, (λx.2x)‘b = 2x [b/x] = 2b,
where the notation x
[a/x] says “substitute a for x in x
Since we are merely just doing substitution, we have for anything that xy
or xx even makes sense! This is the untyped λ-calculus.
II Untyped λ-calculus
1. Terms and variables
We define the untyped λ-calculus by structural induction, defining the terms.
The class of variables, x
, x
, x
, . . . , is denoted by Var (we assume it is count-
able). We define the terms as follows:
1. Every variable is a term (this is the base case of our structural induction).
2. If M, N are terms, so is MN.
3. If M is a term, x Var, then λx.M is a term.
4. Nothing else is a term.
In this way, we have defined everything we consider a “term” (a function).
In BNF (Backus-Naur Form), this is written:
MN ::= x | M N | λx.M
If you like sets a lot (I do), you can think of λx.ϕ(x) as the set {x | ϕ(x)}. In
this way, we view xy as meaning x y.
Denote by F V (M) the set of free variables of a term M, defined by in-
1. If x Var, then F V (x) := {x}.
2. F V (MN) = F V (M) F V (N).
3. F V (λx.M) = F V (M) \ {x}.
Similarly, we can define the bound variables inductively as follows:
1. If x Var, then BV (x) := .
2. BV (MN) BV (M) BV (N).
3. BV (λx.M) = BV (M) {x}.
We say that a term M is closed if and only if F V (M) = . Another name for
closed terms is combinators. Some examples of combinators:
K = λx.λy.x, S = λx.λy.λz.(xz)‘(yz), I = λx.x.
We should probably discuss some notational kinks and quirks that we will use
frequently. Firstly, we associate function application (‘) to the left, that is:
((ab)‘c = abc,
and more so, we might even drop the indicator ‘, so it further becomes:
(ab)‘c = abc = abc.
With repeated bindings λx., we act from the inside out, sometimes dropping
the consecutive lambdas to save space and eliminate (or sometimes create) con-
λx.(λy.(λz.M)) = λxyz.M.
So for example, our combinators from before with these conventions appear as:
K = λxy.x, S = λxyz.(xz)(yz), I = λx.x.
An example, we can ‘reduce’ the term SKK as follows:
SKKx = ((SK)K)x
= (Kx)(Kx)
= x
= Ix,
where we see that if we had the axiom of extensionality:
x . (fx = gx)
f = g
then we could conclude that SKK = I. Otherwise, the most we can say is that
SKKx = Ix.
2. Change of bound variables and α-congruence
The idea of α-congruence is that:
λx.t =
where y is some new/fresh variable. That is, the bound variable can be changed,
and we say that the functions are the same still—this is α-congruence. A priori,
we can’t say that these are equal without considering α-congruence as the bound
variables are different. They are not constructively the same, but we would like
to say they are the same function at the end of the day.
Define t[M/x] for x Var and terms t, M, inductively by, y Var:
1. y[M/x] =
M, x = y;
y, otherwise.
2. (M N)[y/x] = (M[y/x])‘(N[y/x]).
3. (λx.M )[y/x] =
λy.M[y/x], x = z;
λz.M[y/x], x 6= z.
If we apply α-congruence to λ-calculus, we get that terms are equivalent up
to change of bound variables.
3. Equality, =, and β-equivalence
The phenomenon of α-congruence brings to mind that we need to rigorously
define what it means to be equal.
Equality (=) is an equivalence relation, so we have the usual reflexivity,
symmetry, and transitivity:
M = M,
M = N
N = M
M = N, N = P
M = P
In addition, we have the following:
M = N
M = N
M = N
λx.M = λx.N
where the last one there is the ξ-rule. In addition, we also have the α-congruence
rule, discussed above:
λx.M = λy.M[y/x], (α)
and what is known as β-reduction:
(λx.M)‘N = M[N/x], (β)
which says that equality respects application. Finally, we have the η-rule:
λx.(fx) = f, for x 6∈ F V (f). (η)
Proposition 1. The η-rule is equivalent to extensionality.
Proof. Suppose η and note:
fx = gx =
λx.(fx) = λx.(gx) =
f = g.
Conversely, suppose EXT, and note:
(λx.(fx))‘x = fx, (β)
for some x 6∈ F V (f), and so by EXT: f = λx.(fx).
A few examples of β-reduction:
(λx.xx)‘a =
aa, (λx.xx)‘(λx.xx) =
and as my professor said after showing us this, “We’re no longer in Kansas,
Theorem 1 (Fixed point theorem). For every F there exists an X such that
F X = X.
Proof. Let W := λx.F (xx) and X := WW . Note:
X = W W = (λx.F (xx))W =
F (W W) = F (X).
This gets us close to Russell’s paradox, indeed only a little bit extra is needed.
Consider the λ-term:
R := λx.NOT(xx),
where “NOT” is just the negation function (we will see this at a later date).
Then we try β-reducing RR:
RR = (λx.NOT(xx))R = NOT(RR).
Clearly not in Kansas.
More generally, define the Y -combinator:
Y := λf.(λx.f(xx))(λx.f(xx)),
so we see that:
Y f = (λx.f(xx))(λx.f (xx))
= f(λx.f(xx))(λx.f (xx))
= f(Y f).
If we try to “type” this (by assigning domains and codomains to our function),
we get:
Y : A
A : f 7→ Y (f ).
Historical Remark 1. It was Church who first used the notation λx.f(x),
and he said this was because they initially they used ˆx.f(x) which then changed
slightly to be x.f(x), and then finally λx.f(x) in order to accommodate print-
Another story about the early years of λ-calculus is that Church and Kleene
sought to find functions for any computable functions. The issue they came
across was that they couldn’t figure out how to λ-tize the predecessor function:
n 7→ n 1.
Church had nearly almost convinced himself that it was not possible, but then
his student Kleene took a trip to the dentist. There, he had a Eureka moment,
and he figured out the trick to defining the predecessor function in λ-calculus!
Apart from silly stories, we can recant a little about the history of λ-calculus.
Both λ-calculus and combinatory logic (logic studied via combinators) sprung
to life in the 1920s. Moses Sconfinkel was probably the first to study combi-
natory logic. A Russian logician, he gave a talk to Hilbert and the gang on 7
December 1920 about combinatory logic. Heinrich Behmann revised and pub-
lished Sconfinkel’s notes in 1924 (also, Jean van Heijenoort’s “From Frege to
odel” has it). He sadly only had one other paper published, and then he re-
turned to Moscow. In 1927, he was reportedly mentally ill and in the confines
of a sanatorium. He died poor in Moscow in 1942, all his papers burned by his
neighbours for heating.
Sconfinkel wrote that:
A × B C A C
something which we will see later is a feature of a Cartesian closed category!
Interestingly, Sch¨onfinkel was a pupil of Samuel Shatunovsky, a mathemati-
cian who had correspondence with Brouwer on cosntructivist ideas. Even more
interestingly, Shatunovsky did not have a formal school certificate so he never
really had a regular research career in mathematics.
Curry dabbled in combinatory logic during 1922, and von Neumann’s thesis
on set theory had vague combinator-like structures in it (he also had close
correspondence with the logic group at ottingen who were likely to pass on
Sconfinkel’s wisdom). Curry’s invention of combinatory logic likely was entirely
a re-invention, independent to Europe, as Curry was in the USA.
Curry focused his attention on substitution, which at the time was not a well-
analysed feature of logic. Indeed, Russell and Whitehead just forgot to define
it in Principia Mathematica, and Hilbert and Ackermann’s textbook had an
incorrect statement for it concerning predicate logic. Curry studied in particular
how to break substitution up into smaller steps, currying. This lead him to
combinatory logic.
It was only in 1928 that Alonzo Church invented the λ-calculus. Church’s
untyped λ-calculus appeared in print in 1932 with unrestricted quantification, no
law of the excluded middle. However, it was found quite quickly after that it had
a contradiction. He fixed it, and at the time hoped that G¨odel’s incompleteness
theorems for Russell and Whitehead’s system did not extend to this system (see:
History of Lambda-calculus and Combinatory Logic, Cardone & Hindley).
4. Combinatory calculus
Recall that a combinator is a closed λ-term. We have the following examples of
S = λxyz.(xz)(yz), K = λxy.x, I = λx.x, B = λxyz.x(yz), C = λxyz.xzy.
We have already seen that SK = I (assuming extensionality), and indeed B
and C can also be obtained from S and K alone.
Exercise 1. Find, using only S and K, an expression equivalent to B and C.
It turns out that any lambda term can be expressed in terms of the combi-
nators S and K, and hence to any computable function (Church thesis). There
exists algorithms for determining the SK-expression, however we will not cover
that as it is fun finding your own ways.
Historical Remark 2. These days, combinatory logic is increasingly popular
with the rise of functional programming where it is actively applied.
Note that B can be seen as composition of functions if you alter the definition
a little bit:
Bfg := f g, f g = λx.f(gx).
Exercise 2. Show that The set of λ-terms with application and identity I form
a monoid. Do you need η? This might actually be for function composition
using the B combinator, not using application. Need to try.
One can make combinators into a form of logic by viewing K as “true”, and
then K
:= λxy.y as false. You are encouraged to find all your favourite boolean
Note that both Church and Curry hated η and extensionality since it has no
computational meaning.
Exercise 3. Let M be a λ-term. Associate M to a directed multigraph, possibly
with loops, called G(M), where:
(i) The vertices is the set {N | M β-reduces to N}.
(ii) The edges are each possible β-reduction.
Example 1. If Ω := (λx.xx)(λx.xx), then G(Ω) is:
while G(KxΩ) is:
Find λ-terms M so that G(M) is of the following shapes:
An equational theory is said to be inconsistent if and only if every equation
is derivable (that is, every model is a singleton).
Proposition 2. λ-calculus with K = S is inconsistent.
Proof. Suppose that K = S, so Kabc = Sabc for all a, b, c. Hence we have
ac = (ac)(bc), so in particular, II = (II)(bI), which reduces to I = bI for all
b. Let b = Kf, and then we have I = KfI I = f for any term f. If we
choose a different b = Kg, we similarly get I = g, and hence f = g for any two
Remark that there are other possible equations one might add to guarantee
inconsistency. Church gives one, forming a theory where we quotient out by
terms without a normal form (with respect to β-reduction). If we define:
T := {M = N | M, N λ-terms without normal form},
then T is inconsistent. A hint to show this is to let M = λx.((xK)Ω) and
N = λx.((xS)Ω). If M = N , show that S = K!