The Untyped Lambda Calculus
In 1936 Alonzo Church published a formal system he
was using to attack the foundations of logic. Stripped of its logical apparatus, what remained was a
language so small it fits on a napkin — yet powerful enough to express every computable
function. It has no numbers, no booleans, no data structures, no assignment, no control flow. It has
three syntactic forms and one computation rule. This is the
untyped lambda calculus, and it is the theoretical bedrock on which the entire study
of programming languages is built.
Why should a graduate student in programming-language theory care about a formalism older than the
transistor? Because the lambda calculus is the lingua franca of the field. When we reason
about evaluation order, scoping, higher-order functions, type systems, continuations or effects, we do
it in the lambda calculus first and translate to Haskell, OCaml or Scala afterwards. Every core
calculus in Pierce's Types and Programming Languages is the untyped lambda calculus plus
annotations. Master its syntax and its one rule, and the rest of the course is elaboration.
The grammar: three productions and nothing else
Fix a countably infinite set V = \{x, y, z, \dots\} of
variables. The set \Lambda of lambda terms
is defined inductively by the abstract grammar
M, N \;::=\; x \;\mid\; \lambda x.\, M \;\mid\; M\ N
Read the three productions as the three things you can do with functions:
-
A variable x — a placeholder standing for a value to be
supplied later. This is the only primitive; there are no constants.
-
An abstraction \lambda x.\, M — the act of
building a function. It denotes "the function that, given x,
returns the body M." The \lambda is a binder;
the variable immediately after it is the formal parameter.
-
An application M\ N — the act of using a
function. It denotes "call M on the argument N,"
written simply by juxtaposition, operator first.
That is the complete syntax. Because the definition is inductive, every term is a finite tree whose
leaves are variables and whose internal nodes are abstractions (one child, the body) and applications
(two children, operator and operand). Structural induction over exactly these three cases is the proof
technique we will lean on for the rest of the module — see
induction
on derivations.
Two conventions that banish the brackets
Fully parenthesised terms are unreadable, so we adopt two universal conventions. Internalise them now;
misreading a term is the single most common source of confusion for beginners.
-
Application associates to the left. A bare
M\ N\ P means (M\ N)\ P, never
M\ (N\ P).
-
Abstraction bodies extend as far right as possible. In
\lambda x.\, M\ N the body is the whole application
M\ N, i.e. \lambda x.\, (M\ N), not
(\lambda x.\, M)\ N.
A third convenience is nested abstraction: we abbreviate
\lambda x.\, \lambda y.\, \lambda z.\, M as
\lambda x\, y\, z.\, M. Under these conventions,
\lambda f.\, \lambda x.\, f\ (f\ x) parses unambiguously as the tree we are
about to draw.
Currying: many arguments from one
The grammar gives every abstraction exactly one parameter, so how do we write a two-argument function?
We curry: a function of two arguments becomes a function that takes the first argument
and returns a function that takes the second. The
transformation (named after Haskell Curry, though Moses Schönfinkel had it first) is the isomorphism
(A \times B) \to C \;\;\cong\;\; A \to (B \to C).
So the "constant function returning its first of two arguments" is
\lambda x.\, \lambda y.\, x. Feeding it two arguments,
(\lambda x.\, \lambda y.\, x)\ a\ b, peels off one
\lambda per argument. Currying is not a mere trick: it is why a
one-parameter grammar loses no expressive power, and it is the reason Haskell and ML type every
function as a chain of single-argument arrows.
The abstract syntax tree
A term is its parse tree. Here is the AST of the Church numeral two,
\overline{2} = \lambda f.\, \lambda x.\, f\ (f\ x). Application nodes are
drawn as @; abstraction nodes carry their bound variable. Step through the
build-up to see how the two reading conventions resolve the term into a unique tree.
Notice the shape: two abstraction nodes form a "spine" (\lambda f then
\lambda x), below which sits the body — an application
f\ (f\ x) whose left child is the bare variable
f and whose right child is the parenthesised inner application
(f\ x). The parentheses in the source are gone; the tree records the
structure directly. Every question we ask about a term — its free variables, its redexes, how it
reduces — is answered by walking this tree.
Working with terms as data
Since a term is a tree over three constructors, it maps cleanly onto an algebraic data type. Below we
model \Lambda in TypeScript, write a pretty-printer that honours the two
parsing conventions (inserting parentheses only where they are needed), and measure the size
and depth of a term by structural recursion. Press Run.
// The three constructors of Λ, as a tagged union.
type Term =
| { tag: "var"; name: string }
| { tag: "abs"; param: string; body: Term }
| { tag: "app"; fn: Term; arg: Term };
const v = (name: string): Term => ({ tag: "var", name });
const lam = (param: string, body: Term): Term => ({ tag: "abs", param, body });
const app = (fn: Term, arg: Term): Term => ({ tag: "app", fn, arg });
// Pretty-print with minimal parentheses.
// ctx: "top" | "fn" (left of an application) | "arg" (right of an application)
function show(t: Term, ctx: "top" | "fn" | "arg" = "top"): string {
switch (t.tag) {
case "var":
return t.name;
case "abs": {
const s = `λ${t.param}. ${show(t.body, "top")}`;
// an abstraction must be bracketed unless its body may run to the right edge
return ctx === "top" ? s : `(${s})`;
}
case "app": {
const s = `${show(t.fn, "fn")} ${show(t.arg, "arg")}`;
// application must be bracketed when it sits in argument position
return ctx === "arg" ? `(${s})` : s;
}
}
}
// Size = number of nodes; depth = longest root-to-leaf path.
function size(t: Term): number {
switch (t.tag) {
case "var": return 1;
case "abs": return 1 + size(t.body);
case "app": return 1 + size(t.fn) + size(t.arg);
}
}
function depth(t: Term): number {
switch (t.tag) {
case "var": return 1;
case "abs": return 1 + depth(t.body);
case "app": return 1 + Math.max(depth(t.fn), depth(t.arg));
}
}
// two = \f. \x. f (f x)
const two = lam("f", lam("x", app(v("f"), app(v("f"), v("x")))));
console.log("term =", show(two)); // \f. \x. f (f x)
console.log("size =", size(two)); // 7 nodes
console.log("depth =", depth(two)); // 5
// Left-association survives a round trip: f a b == (f a) b
const fab = app(app(v("f"), v("a")), v("b"));
console.log("fab =", show(fab)); // f a b (no brackets needed)
// Argument on the right needs brackets: f (a b)
const fAB = app(v("f"), app(v("a"), v("b")));
console.log("fAB =", show(fAB)); // f (a b)
The pretty-printer is the parsing conventions run in reverse: it emits a bracket exactly when
re-parsing without it would change the tree. That the round trip is faithful is a small but genuine
theorem about the grammar.
Why three constructs suffice
It is astonishing that a language with no primitive data can be Turing-complete. The
result is due to Church and Turing, working independently in 1936; Turing later proved his machines and
Church's calculus define exactly the same class of computable functions.
-
A numeric function f : \mathbb{N}^k \to \mathbb{N} is
computable if and only if it is lambda-definable: there is a
closed term F with
F\ \overline{n_1}\cdots\overline{n_k} reducing to
\overline{f(n_1,\dots,n_k)} on the Church numerals.
-
The lambda-definable functions coincide with the partial recursive functions and
with the Turing-computable functions.
The engine that supplies unbounded computation is self-application: because a term may be
applied to itself (x\ x is perfectly legal), we can build fixed-point
combinators and, through them, arbitrary recursion — the subject of the last lesson in this module.
Data (numbers, pairs, trees) is encoded as behaviour, a technique we develop in
Church
encodings. The whole of computation, from three productions.
Hilbert's Entscheidungsproblem (1928) asked for a mechanical procedure that, given any
first-order logical statement, decides whether it is universally valid. To prove no such
procedure exists, one first has to pin down what "mechanical procedure" even means — and in 1936 there
was no accepted definition. Church invented the lambda calculus partly as that definition: a function
is effectively calculable, he proposed, exactly when it is lambda-definable. He then exhibited a
lambda-definable predicate that no lambda term can decide, settling the Entscheidungsproblem in the
negative. A few months later Turing reached the same conclusion with his machines and, crucially,
proved the two models equivalent. That equivalence is the empirical content of the
Church–Turing thesis — and the reason a language of three symbols sits at the origin
of computer science.
The commonest parsing error is to stop an abstraction's body too early. Because a
\lambda's body extends as far right as it can, the term
\lambda x.\, f\ x is the abstraction whose body is the application
f\ x — a single function. It is not
(\lambda x.\, f)\ x, which is an application of the constant function
\lambda x.\, f to the argument x. These have
different trees and reduce differently.
The dual error is misreading left-association. \lambda x.\, x\ x\ x is
\lambda x.\, ((x\ x)\ x), and a\ b\ c\ d is
((a\ b)\ c)\ d. When in doubt, fully parenthesise on paper before you
reduce: nearly every "the answer came out wrong" story begins with a bracket placed by intuition rather
than by the two rules.