Introduction to the λ-calculus — From Untyped to Simply Typed
The minimal model of computation
Basic (1st–2nd year university)
Goal of this page
Understand the untyped λ-calculus, which consists only of defining and applying functions, and β-reduction; then move on to the simply typed λ-calculus, which assigns types to terms. Grasp why assigning types makes computation always terminate, and why that matters.
1. The untyped λ-calculus
The λ-calculus is a model of computation pared down to the extreme, expressing computation with only building and using functions. Terms are built from just three things.
- Variable: $x, y, z, \dots$
- Abstraction: $\lambda x.\,M$ (a function that takes $x$ and returns $M$)
- Application: $M\,N$ (apply the function $M$ to the argument $N$)
That is all, yet you can encode natural numbers, booleans, data structures, and even recursion, giving it the same computational power as a Turing machine. Variable binding follows the same idea as bound and free variables: in $\lambda x.\,M$, $x$ is a bound variable whose name can be renamed ($\alpha$-conversion).
2. β-reduction: one step of computation
The operation of rewriting a function application $(\lambda x.\,M)\,N$ into $M[x := N]$, the term obtained by replacing every free $x$ in $M$ with $N$, is called β-reduction.
$$(\lambda x.\,M)\,N \;\to_\beta\; M[x := N]$$Passing $y$ to the identity function $\mathrm{id} = \lambda x.\,x$ replaces $x$ with $y$, giving $y$.
$$(\lambda x.\,x)\,y \;\to_\beta\; y$$Passing $3$ to $\lambda x.\,(x+x+1)$, which "doubles and adds 1," reduces to $3+3+1 = 7$. β-reduction is exactly running a program.
A form that can no longer be β-reduced is a normal form, corresponding to "computation finished." But in the untyped calculus you can write terms whose reduction never ends. For example, $(\lambda x.\,x\,x)(\lambda x.\,x\,x)$ applies the function $\lambda x.\,x\,x$ (which "applies its argument to itself") to that function itself. β-reducing replaces the $x$ in the body $x\,x$ with $\lambda x.\,x\,x$, returning to the exact same form $(\lambda x.\,x\,x)(\lambda x.\,x\,x)$. Since this repeats endlessly, the computation never halts and never reaches a normal form.
3. The simply typed λ-calculus
In many situations, non-terminating computation is a problem. So we assign a type to each term and allow only well-typed applications; this is the simply typed λ-calculus. Types are built from base types and function types $A \to B$.
Notation: a colon after a term writes its type. $M : B$ reads "the type of $M$ is $B$ ($M$ has type $B$)." Likewise $x : A$ is "the type of $x$ is $A$," and $\lambda x{:}A.\,M$ denotes "a function taking an argument $x$ of type $A$." Above the line, $x:A \vdash M:B$ reads "assuming $x$ has type $A$, $M$ has type $B$" ($\vdash$ is the "derivable from" seen in Syntax and Semantics).
The rules use the same horizontal line form as the previous chapter's natural deduction, read as "if what is above the line holds, the bottom holds." There are only two rules to remember.
① Application rule (using a function): if the function $M$ has type $A \to B$ (takes type $A$, returns type $B$) and the argument $N$ has type $A$, then the application $M\,N$ has type $B$.
$$\dfrac{M : A \to B \quad N : A}{M\,N : B}$$② Abstraction rule (building a function): if, assuming the argument $x$ "has type $A$," the body $M$ has type $B$, then the function $\lambda x{:}A.\,M$ has type $A \to B$. Above the line, $x:A \vdash M:B$ represents "assuming $x:A$, then $M:B$."
$$\dfrac{x:A \;\vdash\; M:B}{\lambda x{:}A.\,M \;:\; A \to B}$$Let the type of natural numbers be $\mathbb{N}$ (replace abstract types like $A, B$ with concrete ones). As an example, use the "add-1 function" $f = \lambda x{:}\mathbb{N}.\,(x+1)$. What this function "does" is written in the $\lambda$-body $x+1$.
- Abstraction (determining the type of $f$): assuming $x : \mathbb{N}$, the body $x+1$ has type $\mathbb{N}$. Hence $f = \lambda x{:}\mathbb{N}.\,(x+1)$ has type $\mathbb{N} \to \mathbb{N}$ (rule ②, $A=B=\mathbb{N}$).
- Application (using $f$): passing $3 : \mathbb{N}$ to $f$ gives $f\;3 : \mathbb{N}$. Indeed, β-reducing $(\lambda x{:}\mathbb{N}.\,(x+1))\,3$ replaces $x$ in the body with $3$, giving $3+1 = 4$ (rule ①, $A=B=\mathbb{N}$).
Thus the function's value ($4$) is determined by the body $x+1$, whereas the typing rules look only at types, not values (if $x+1$ is $\mathbb{N}$ then the result is $\mathbb{N}$ — computing at the level of types). "The types match" means, in application rule ①, that the function's input type equals the argument's type (both $\mathbb{N}$ above). If they do not match, no type is assigned and the application is not allowed.
Strong normalization theorem (outline)
In the simply typed λ-calculus, for every well-typed term, β-reduction necessarily halts in finitely many steps, in whatever order it proceeds. Merely assigning types eliminates non-terminating computation.
Self-applications like $(\lambda x.\,x\,x)$ cannot be assigned a consistent type, so they get no type at all. The type system rejects these "dangerous terms." The mechanism of termination is treated in detail in Strong Normalization and Termination.
4. Correspondence with proof
Looking closely at the typing rules, they look just like the rules of natural deduction. The function typing rules are exactly the introduction and elimination of implication. This is the Curry–Howard correspondence.
$\lambda x{:}A.\,M : A \to B$ corresponds to "assume $A$, derive $B$, discharge to get $A \to B$" ($\to$I); $M\,N : B$ corresponds to "from $A \to B$ and $A$, $B$" ($\to$E, modus ponens). A well-typed λ-term is itself a proof, and β-reduction is the simplification (normalization) of the proof.
Thus the λ-calculus becomes, beyond a mere model of computation, a language that expresses logical proofs themselves. The simply typed λ-calculus expresses proofs of propositional logic; extending the correspondence to logic with quantifiers leads to dependent type theory.
Summary
Key points
- λ-calculus: a minimal model of computation with only variables, abstraction $\lambda x.\,M$, and application $M\,N$
- β-reduction: $(\lambda x.\,M)\,N \to M[x:=N]$. One step of computation = running a program
- Untyped, you can write non-terminating computations; simply typed, everything terminates (strong normalization)
- The typing rules match those of natural deduction: a well-typed term = a proof (Curry–Howard)
Frequently asked questions
What is the λ-calculus?
A minimal model of computation consisting only of defining and applying functions. $\lambda x.\,M$ denotes "a function that takes $x$ and returns $M$," and computation proceeds by β-reduction. It has the same power as a Turing machine and is the basis of functional programming and type theory.
What is β-reduction?
The operation of rewriting $(\lambda x.\,M)\,N$ into the term obtained by replacing every free $x$ in $M$ with $N$. This is one step of computation, corresponding to running a program. A form that can no longer be reduced is a normal form.
What is the difference between untyped and simply typed?
The untyped λ-calculus allows any application, so non-terminating terms (self-application) can be written. The simply typed λ-calculus assigns types and allows only well-typed applications; as a result every reduction terminates (strong normalization). This typed version corresponds to logical proofs via Curry–Howard.