Chapter 3: Simply Typed Lambda Calculus

Here is how you were taught to prove an implication. To prove “if $A$ then $B$”, you write suppose $A$, you reason until you reach $B$, and you write therefore $A$ implies $B$, at which point the supposition is spent: it may not be used again, and the conclusion does not depend on it. To use an implication you already have, you write we have $A\to B$, and we have $A$, so $B$. And a supposition in force may be written down wherever it is wanted. Three moves, and every proof you have read in a mathematics lecture is built from them and their cousins for the other connectives.

Now take the rule for parameters that Chapter 2 licensed, write it beside (var) and (app), and rub out the programs:

A supposition in force may be written down. From $A\to B$ and $A$, conclude $B$. If $B$ follows on the supposition $A$, conclude $A\to B$ and drop the supposition. They are the same three moves. The checker that reads your definition f x = ... is checking a proof written the way mathematicians write proofs, and this chapter is about the logic that makes that exact.

3.1 The λ-calculus

In Chapter 1 a definition $fx:=M$ had a name, $f$, and the name had to be declared before it could be used. Church’s notation does away with the name: it writes the function that takes $x$ and returns $M$ as $\mathit{𝜆𝑥}.M$, a term in its own right, which can be written wherever a term can be written and applied without ever being named.

You have written the third form many times. It is \x -> M in Haskell, lambda x: M in Python, x => M in JavaScript; every def f(x): return M is one with a name attached, and every method in Java is one with a name and a class attached. A definition $f{x}_1\cdots x_n:=M$ of Chapter 1 is the term $\lambda x_1.\cdots \lambda x_n.M$, and the two constants are the two terms

which is why they need no longer be taken as given.

Where the notation comes from. The calculus is Alonzo Church’s. He introduced the notation at Princeton in the paper §1.3 described (1932): the $\lambda$ was there to write the functions of a logic meant to carry the whole of mathematics. The logic did not survive and the notation did. Church used it to exhibit a question no procedure can settle (1936), Turing proved in the same year that it computes exactly what his machines compute, and Church repaired it with types (1940) — the repair your compiler inherited. Schönfinkel’s two combinators had been published in 1924 with the same object in view, and Curry spent the 1930s on them, which is why one language has two origins: the combinatory algebra of Chapter 1 is this calculus with the variables compiled away, and Theorem 3.3 below says that nothing is lost either way. That the calculus is also the heart of every programming language was noticed twenty years later.

Free, bound, and substitution. The $x$ in $\mathit{𝜆𝑥}.M$ is the function’s parameter: the $\lambda$ binds it, and its scope is the body $M$. An occurrence of a variable is bound if it lies in the scope of a $\lambda$ on that variable and free otherwise. In $(\mathit{𝜆𝑥}.xy)x$ the first two occurrences of $x$ are bound and the last, like the $y$, is free. The set $\mathrm{FV}(M)$ of free variables of $M$ is defined by recursion on the shape of $M$, one clause for each of the three forms:

1.

$M$ is a variable $x$: $\mathrm{FV}(x)=\{x\}$.

2.

$M$ is an application $M_1{M}_2$: $\mathrm{FV}(M_1{M}_2)=\mathrm{FV}(M_1)\cup \mathrm{FV}(M_2)$.

3.

$M$ is an abstraction $\mathit{𝜆𝑥}.M_1$: $\mathrm{FV}(\mathit{𝜆𝑥}.M_1)=\mathrm{FV}(M_1)\setminus \{x\}$.

The first two clauses only collect; the third is the one that does anything. Only a $\lambda$ removes a variable from the list, and it removes only its own parameter. A term with no free variables is closed: a whole program rather than a fragment of one. Two terms that differ only in the names of their bound variables, like $\mathit{𝜆𝑥}.x$ and $\mathit{𝜆𝑦}.y$, describe the same function, and we treat them as the same term: a bound variable may be renamed whenever that is convenient.

Substitution $M(N∕x)$ replaces the free occurrences of $x$ in $M$ by $N$, and nothing else. In Chapter 1 this was simply replacement, because nothing in that language bound a variable; now it has to step around binders, and it too is defined by recursion on the shape of $M$, one clause per form, except that the variable and abstraction cases each split according to whether the variable met is the very one being replaced:

1.

$M$ is the variable $x$ itself: $x(N∕x)=N$.

2.

$M$ is a variable $y$ other than $x$: $y(N∕x)=y$.

3.

$M$ is an application $M_1{M}_2$: $(M_1{M}_2)(N∕x)=M_1(N∕x)M_2(N∕x)$.

4.

$M$ is an abstraction on $x$ itself: $(\mathit{𝜆𝑥}.M_1)(N∕x)=\mathit{𝜆𝑥}.M_1$.

5.

$M$ is an abstraction on some other variable $y$:

$$(\mathit{𝜆𝑦}.M_1)(N∕x)=\mathit{𝜆𝑦}.M_1(N∕x),\text{provided }y\notin \mathrm{FV}(N).$$

Clauses 1 to 3 do what you would expect: replace the variable when you meet it, and otherwise pass the substitution down. Clause 4 stops at a $\mathit{𝜆𝑥}$ because every $x$ inside it is bound: there is nothing to replace. The side condition on clause 5 is the one subtlety. Pushing $N$ under a $\mathit{𝜆𝑦}$ when $y$ is free in $N$ would turn that free $y$ into a bound one and change what $N$ means, so the clause declines; the remedy is to rename the $y$ of $\mathit{𝜆𝑦}.M_1$ to a letter that occurs nowhere else, and then substitute. Rename first. Chapter 4 shows what goes wrong when a substitution skips that step, and shows the same bug on the logic side, where it has been known for a century.

Running. There is one rule of computation. To apply a function to an argument, substitute the argument for the parameter:

anywhere inside a term; the pair on the left is a redex, and the step is called $\beta$. That is what a function call does, and it is all a function call does. The three steps of Definition 1.3 are all instances of it: the $𝖪$ step is two $\beta$ steps on $(\mathit{𝜆𝑥}.\mathit{𝜆𝑦}.x)MN$, the $𝖲$ step is three, and a definition step is one for each parameter.

3.2 Typing

The types are those of Definition 1.9 and the contexts and judgements those of Definition 1.10. Two of the rules are Chapter 1’s, for variables and for applications. The third is the one the Deduction Theorem licensed — if $B$ follows from the hypothesis $A$, then $A\to B$ follows without it (Theorem 2.7) — which we may now adopt outright, since adopting it lets nothing new be typed:

Read (abs) as the checker reads a function definition: to check $\mathit{𝜆𝑥}.M$, add the parameter to the context with the type it is to have, check the body, and the function has the arrow type. If $\mathrm{\Gamma }$ already declares an $x$, rename the parameter first, since a context lists each variable once. Rule (abs) is the first rule we have met that changes the context: above the line there is one more variable in scope than below it. The constants are gone — $𝖪$ and $𝖲$ are now terms, and they get their types by (abs), which Exercise 3.1 asks you to check gives exactly (1.1) and (1.2). A typing is a finite list of judgements as before, with the conventions for justifications as before; the one difference from Definition 1.11 is that the lines of a single typing no longer all carry the same context.

So nothing is lost by the change of notation, and the checker of Chapter 1 and the checker of (3.2) accept the same programs at the same types. What is gained is that the compiler no longer has to compile anything to decide whether to say yes: it reads the definition as written.

A worked typing. Here is the typing of a program you have written in one form or another, \f -> \g -> \x -> f (g x), in the context $\mathrm{\Gamma }=f:B\to C,g:A\to B,x:A$.

1.

$\mathrm{\Gamma }⊢g:A\to B$ (var): $g:A\to B$ is in $\mathrm{\Gamma }$

2.

$\mathrm{\Gamma }⊢x:A$ (var): $x:A$ is in $\mathrm{\Gamma }$

3.

$\mathrm{\Gamma }⊢gx:B$ (app) 1, 2

4.

$\mathrm{\Gamma }⊢f:B\to C$ (var): $f:B\to C$ is in $\mathrm{\Gamma }$

5.

$\mathrm{\Gamma }⊢f(gx):C$ (app) 4, 3

6.

$f:B\to C,g:A\to B⊢\mathit{𝜆𝑥}.f(gx):A\to C$ (abs) 5

7.

$f:B\to C⊢\mathit{𝜆𝑔}.\mathit{𝜆𝑥}.f(gx):(A\to B)\to A\to C$ (abs) 6

8.

$⊢\mathit{𝜆𝑓}.\mathit{𝜆𝑔}.\mathit{𝜆𝑥}.f(gx):(B\to C)\to (A\to B)\to A\to C$ (abs) 7

Lines 1 to 5 are routine: three look-ups and two uses of (app), each matching an argument’s type against the type a function expects. Lines 6 to 8 are (abs) three times, each taking the last variable out of the context and putting a $\lambda$ on the front of the program: watch the context shrink as you read down, until at line 8 it is empty and the program is closed. This is what the compiler did, in a few microseconds, when it accepted your composition function.

Rub out the programs. Lines 1–5 are a proof of $C$ from the three hypotheses $B\to C$, $A\to B$ and $A$: three hypothesis lines and two uses of modus ponens. That is hypothetical syllogism — from $A\to B$ and $B\to C$, conclude $A\to C$ — which Chapter 2 proved from hypotheses in seven lines. Lines 6–8 discharge $A$, then $A\to B$, then $B\to C$, and the formula on the last line,

is hypothetical syllogism as a theorem, with nothing assumed. That formula cost Chapter 2 seven lines of which the first was an instance of (II) with twenty letters and nineteen arrows; here it is found and checked in three discharges. The compiler read your program as that proof.

3.3 Conjunction, disjunction, and negation

The arrow is one connective, and a logic needs and, or and not as well. Each is a type you have used — a pair, a tagged union, the empty type — and each comes with its rules the way $\to$ did. A rule that introduces a connective is one whose conclusion has that connective on the outside; on the program side it builds a value of the type, so it is a constructor. A rule that eliminates one has it on the outside of a premise; on the program side it takes a value apart, so it is a pattern match. Those two words, introduction and elimination, will organise everything that follows.

To establish $A\wedge B$ you establish both; to use it you take whichever half you need. A proof of a conjunction is a pair of proofs, and the two eliminations are the two projections.

To establish $A\vee B$ you establish one of them and say which. To use it you argue by cases: if you can reach $C$ supposing $A$, and reach $C$ supposing $B$, then you have $C$ — and both suppositions are discharged, like the supposition in ($\to$I). A proof of a disjunction is a proof of one side with a tag saying which, and the elimination is a case expression with one branch per tag.

There is no way to establish $\perp$ outright, and that is the point of it. If you ever have $\perp$ in hand you may conclude anything, which is what “from a contradiction, anything follows” means and what absurd :: Void -> a says; and $\neg A$ is the claim that from $A$ you could reach $\perp$, a function from $A$ to the empty type. Everything in this part that looks like a negation is an implication into $\perp$, and the rules for $\neg$ are the rules for $\to$. (Whether $\perp$ can be established from some set of hypotheses is a different question, and it is the question of §3.6.) Here is the whole language in one table: each connective, the type it is, how a value of that type is built, and how it is taken apart.

That is the table of the part, and the thing to carry away from it: the connectives of logic are the data types of a programming language, the introduction rules are their constructors, and the elimination rules are the pattern matches that take them apart. A proof is a program that builds and takes apart values of these types, and nothing else.

3.4 Natural deduction

Everything so far has been about programs. Now rub the programs out. Take the rules of (3.2) and §3.3, delete every term, and keep what is left: judgements $\mathrm{\Gamma }⊢A$ relating a set of formulas to a formula. Ten rules survive, and here they are.

Every one of those rules is a rule you have already used, with the program deleted: ($\to$I) is a $\lambda$, ($\to$E) an application, ($\wedge$I) a pair, ($\vee$E) a case, ($\perp$E) the function absurd. Nothing has been added. What has changed is only what we are looking at.

And what we are looking at is not a system invented for this book, nor one that came out of computing at all. It is Gerhard Gentzen’s, published in his doctoral thesis (1934), two years before Turing’s machine and before there was a program in the world to type. He called it natural deduction because he built it by watching: he took proofs as mathematicians actually write them and wrote down the moves they actually make. To prove an implication, suppose the antecedent. To use one, apply it. To prove a conjunction, prove both halves. To use a disjunction, argue by cases. Each connective gets rules that say how to prove a statement with that connective on the outside and how to use one — and nothing else. That is the whole design, and the rules of (3.3) are the record of it.

So the two systems are one logic in two notations, and the Deduction Theorem is precisely the thing that makes them so: it is the ($\to$I) rule of natural deduction, proved admissible for the Hilbert system. From here on I write $⊢$ for both.

Haskell Curry noticed in the 1950s that the types of his combinators were the axioms of a Hilbert system (Curry and Feys, 1958); William Howard, in a manuscript of 1969, saw that the same held of the $\lambda$-calculus and natural deduction, rule for rule, and that running a program corresponded to something Gentzen had already studied (Howard, 1980). The observation is called the Curry–Howard correspondence. It is the reason this chapter could be written twice over without saying anything twice, and §3.6 takes up the last part of it: what Gentzen had studied, and why he cared.

3.5 Derivations as trees

Definition 3.8 writes a derivation as a list, and carries the set $\mathrm{\Gamma }$ along on every line. That is the right thing for a checker: each line can be checked on its own, because everything it depends on is written on it, and the programs of §3.2 can be written beside the lines. It is the wrong thing for a reader. The hypotheses are copied onto every line whether they are used there or not, and the shape of the argument — which step feeds which — has to be reconstructed from the justifications on the right. Gentzen wrote derivations the other way, as trees, and so does every book since. The hypotheses sit at the leaves, at the top, written once each. Each rule is a horizontal bar with its premises above and its conclusion below, labelled on the right with the rule used. The conclusion of the whole derivation is the single formula at the root, at the bottom. You read a tree downwards, and the shape of the tree is the shape of the argument.

The one thing a tree must record that the list records in its contexts is discharge. The rule ($\to$I) proves $A\to B$ by using $A$ as a hypothesis and then giving it up: after the rule has fired, the conclusion no longer depends on $A$. So a leaf of a tree is in one of two states. It is open, and the conclusion rests on it; or it has been discharged by some rule below it, and the conclusion does not. A discharged leaf is written in square brackets. Which hypotheses are open is not decoration: it is the whole content of the turnstile, and the definition has to track it.

Three remarks on reading that definition, each about a place where students expect something other than what it says.

Discharge takes every open leaf at once. Clause 2 removes $A$ from a set. Every open leaf labelled $A$ in $𝒟$ is therefore discharged together, which is why the second tree below can close two copies of $A\wedge B$ with one bracket. Some books let a rule discharge a chosen subset of the occurrences instead; nothing provable changes, because an undischarged copy can always be discharged by a later ($\to$I) that reintroduces the same formula.

Discharge may be vacuous. Clause 2 does not require $A$ to occur in $𝒟$ at all. If it does not, $\mathrm{OH}(𝒟)\setminus \{A\}$ is just $\mathrm{OH}(𝒟)$, and the rule has proved $A\to B$ from a proof of $B$ that never looked at $A$. That is schema (I) of Chapter 2, and on the program side it is $𝖪$: a function that ignores its argument.

The numbers are bookkeeping. The definition says which leaves a clause discharges, so it needs no numbers. They appear in practice because a drawn tree may contain several rules that discharge, and the reader needs to see which bracket belongs to which bar. Writing ${[A]}^1$ at the leaf and $\to I,1$ at the bar is a labelling of the same information, not more of it.

Three trees. Here is hypothetical syllogism, which §3.4 gave as a six-line list with $\mathrm{\Gamma }=\{p\to q,q\to r\}$ repeated on every line. As a tree it is three bars, and the two hypotheses are written once each; they stay open, because the conclusion depends on them.

Read it from the leaves down: suppose $p$; with $p\to q$, get $q$; with $q\to r$, get $r$; discharge the supposition and conclude $p\to r$. Its open hypotheses are $\{p\to q,q\to r\}$, computed by clause 3 twice and clause 2 once, so the tree witnesses $\{p\to q,q\to r\}⊢p\to r$.

Next, one hypothesis discharged at two leaves at once, which is clause 2 working on a set. The conclusion is $⊢(A\wedge B)\to (B\wedge A)$, with no open hypotheses at all.

On the program side that derivation is $\mathit{𝜆𝑥}.(\mathrm{𝑠𝑛𝑑}x,\mathrm{𝑓𝑠𝑡}x)$, and the two bracketed leaves are the two occurrences of the variable $x$ in its body. A variable used twice is a hypothesis discharged at two leaves; a variable used once, at one; and a parameter never used at all is a vacuous discharge.

Last, clause 7, which discharges two different hypotheses, one in each branch — the case where the bracket notation earns its keep. The conclusion is $⊢(A\vee B)\to (B\vee A)$.

That is argument by cases, written out: we have $A\vee B$; in the case $A$ we reach $B\vee A$, in the case $B$ we reach $B\vee A$; so we have it either way. The program is $\mathit{𝜆𝑥}.\mathrm{𝐜𝐚𝐬𝐞}x\mathrm{𝐨𝐟}\mathrm{𝐿𝑒𝑓𝑡}a\Rightarrow \mathrm{𝑅𝑖𝑔h𝑡}a\mid \mathrm{𝑅𝑖𝑔h𝑡}b\Rightarrow \mathrm{𝐿𝑒𝑓𝑡}b$, and the two discharged leaves are the two branch variables $a$ and $b$, each in scope only in its own branch — which is exactly what “one in each branch” means.

Induction over derivations. The definition buys more than a notation. Because it is inductive — nine clauses and a “nothing else”, exactly as Definition 1.1 built terms — it comes with a principle of proof, and it is the principle every theorem in the rest of this chapter uses.

To show that every derivation has a property $P$, it is enough to show that each one-node derivation has $P$, and that for each of clauses 2–8, if the subderivations the clause uses have $P$ then so does the derivation the clause builds.

That is rule induction, and it is the same move as induction on the natural numbers with the clauses in place of zero and successor. It is how Theorem 3.15 will show that running a program preserves its type, and how Lemma 3.18 will show that a stopped program is a constructor: in each case one checks the base and then walks once through the list of clauses. When you meet “by induction on the derivation” in any book on proof theory, this is what is meant.

We shall go on writing lists, because the checker does and because the programs can be written beside them, and we shall draw trees when the shape of an argument is the point. They are the same object described twice, and Theorem 3.13 is the licence to move between them without comment.

3.6 Normalisation

What Gentzen had studied, and what Howard saw running a program corresponded to, is this. A proof can take a detour: it can establish $A\wedge B$ by ($\wedge$I) from proofs of $A$ and $B$, and then at once take $A$ back out by ($\wedge$E${}_1$); or establish $A\to B$ by ($\to$I), discharging a supposition, and at once use it on a proof of $A$ by ($\to$E). In each case an introduction is met by its own elimination, and the proof would have been shorter without the pair. On the program side the pair is a redex, and removing it is a step of computation.

These are the steps your interpreter takes: call a function, project a pair, branch on a tag. That they are also the removal of detours from proofs is the content of the correspondence, and the two theorems of Chapter 1 say the same two things about them, now for the whole language.

The program-side proof is Tait’s (1967) and the proof-side proof is Prawitz’s (1965); the two are the same proof, and Girard et al. (1989, chapter 4) give it in a form readable at the level of these notes, for $\to$ and $\wedge$, with $\vee$ and $\perp$ needing a little more. We take it on trust, as we did in Chapter 1.

It is worth saying why Gentzen wanted this theorem, because he did not want it in order to run anything. He wanted consistency. In the 1920s Hilbert had set the programme of proving, by arguments so elementary that no one could doubt them, that mathematics could never derive a contradiction; and the elementary arguments allowed were arguments about the shapes of written symbols — no appeal to infinite collections, no appeal to what the symbols were about. A normalisation theorem is exactly such an argument, and it pays off at once. A proof with no detours in it never invents material: every formula appearing in it is a piece of the formulas at its two ends. So if you want to know whether $\perp$ can be proved from nothing, you need only ask what a detour-free proof of $\perp$ from nothing could possibly look like, and the answer is that there is no shape available for it. Consistency becomes a statement about the grammar of proofs rather than about mathematics, which is why Gentzen proved his version of this theorem — the Hauptsatz, the main theorem of his thesis — before he proved anything with it, and why Theorem 3.19 below costs us a page rather than a book.

How far that method can be pushed is the question of Chapter 11, where it meets a limit that Hilbert did not expect. For now we collect what normalisation buys here, which is a great deal, because a program that has stopped has a very particular shape.

The “exactly when” is a small induction on the term, and the one thing it needs is types: a normal-form application $MN$ has an $M$ of arrow type that is not a $\lambda$, and the only normal-form terms of arrow type that are not $\lambda$s are neutral ones; likewise a projection of a non-pair, a case on a non-tag, and an $\mathrm{𝑎𝑏𝑠𝑢𝑟𝑑}$ of anything, since $\perp$ has no introduction form at all. Exercise 3.8 asks for the cases in full. What matters is this: a neutral term is a chain of eliminations hanging off a variable, and that variable is free in it, since nothing in the chain binds it.

Read what has been shown. The logic of this chapter does not prove everything. It does not prove $\perp$, and it does not prove any bare claim $p$: whatever it proves has an arrow, an and or an or on the outside, which is to say that it proves things about the relationships between claims and never a claim out of nothing. The disaster of §1.3 — a logic in which every statement had a proof — cannot happen here, and the reason it cannot is that every program stops and a stopped program is a constructor. The argument used nothing about what the letters mean, no table, no notion of a formula being the case. It is an argument about the shapes of strings, and it was available to Gentzen in 1934. The same question — does this system prove everything? — asked of arithmetic rather than of the bare connectives, is the subject of Chapter 11, and the answer there is of a different kind.

One more thing falls out of the shape lemma, and it is worth having now.

In this logic you cannot establish “$A$ or $B$” without establishing one of them and saying which, because a proof of a disjunction is a value with a tag on it. Hold on to that; Part 2 has a use for it.

3.7 Curry’s paradox

Now the argument that closes §1.3, written out exactly, with the programs on. It needs one thing the rules do not allow, and seeing where the rules refuse is the point.

The $\lambda$-calculus with pairs, sums and the empty type is a proof system — Gentzen’s natural deduction — with the programs written beside the lines: a hypothesis is a variable, ($\to$I) is $\lambda$, ($\to$E) is application, and the other connectives are your data types, their introduction rules the constructors and their elimination rules the pattern matches. It proves exactly what the Hilbert system proves, and the Deduction Theorem is its ($\to$I). Running a program is removing detours from a proof, and what the checker says survives it (subject reduction). Every typed program stops (on loan), and a stopped closed program is a constructor; so the logic proves no letter and no $\perp$ — it does not prove everything — and a proof of or always says which. Curry’s paradox and $\mathrm{\Omega }$ are one term, refused by one fact: a type is not a part of itself.

Safe is not correct. Nothing we care about — a sorted list, a transitive order, a discount on every day of the sale — is proved from no hypotheses; by Theorem 3.19 nothing with a bare claim at the top ever is. Such things are proved from a specification, a set of sentences about lists, orders or sales taken as hypotheses. And a specification says for all — for all $x$, for all $y$ — which no formula of this chapter can say.

3.8 From pseudocode to combinators

This part has three languages in it: the two constants of Chapter 1, the $\lambda$-calculus of this one, and the proofs that both turned out to be. They are one language, and the way to believe that is to watch something ordinary travel the whole distance. Here is factorial, as you would write it on a whiteboard.

fact(n): 
    if n = 0 then return 1 
    else return n * fact(n - 1)

Four things in it are not in the language of Definition 1.1: a parameter, a name that calls itself, a conditional, and arithmetic. Take them away one at a time.

The parameter becomes a $\lambda$. A definition with a parameter is an abstraction, which is what §3.1 was for. Writing $\mathrm{𝑖𝑠𝑍𝑒𝑟𝑜}$, $\mathrm{𝑚𝑢𝑙𝑡}$ and $\mathrm{𝑝𝑟𝑒𝑑}$ for the test, the product and the predecessor, and using a boolean as its own conditional in the manner of Example 1.5, so that “if $b$ then $M$ else $N$” is written $bMN$:

Nothing has really happened yet, because $\mathrm{𝑓𝑎𝑐𝑡}$ still occurs on the right-hand side, and a term may not refer to itself.

The self-reference becomes a parameter. So make it one. Abstract over the recursive call as well, and the self-reference disappears:

The term $F$ mentions nothing but its own two parameters: give it the function to call and a number, and it does one layer of the work. What we want is a term $\mathrm{𝑓𝑎𝑐𝑡}$ with $\mathrm{𝑓𝑎𝑐𝑡}=F\mathrm{𝑓𝑎𝑐𝑡}$ — a fixed point of $F$ — and that is exactly what the constant $\mathrm{𝑓𝑖𝑥}$ of Exercise 1.6 delivers, since $\mathrm{𝑓𝑖𝑥}F⇝F(\mathrm{𝑓𝑖𝑥}F)$. So

and one step shows why that is the right definition: $\mathrm{𝑓𝑖𝑥}F\overline{3}⇝F(\mathrm{𝑓𝑖𝑥}F)\overline{3}$, whose $r$ is $\mathrm{𝑓𝑖𝑥}F$ again — the recursive call is the fixed point unfolding once more, on demand and no sooner.

The arithmetic was combinators already. The three operations and the numerals are the ready-made constants of Chapter 1, and Theorem 1.8 says each of them is a term in $𝖪$ and $𝖲$: Example 1.6 builds the numerals and addition, Exercise 1.1 multiplication, and the predecessor is a famous enough puzzle to have its own anecdote. Nothing is being smuggled in; we keep them as names only to keep the term on the page.

The $\lambda$s become $𝖪$ and $𝖲$. One construction remains, and we already have it. The proof of the Deduction Theorem, run with the programs left on rather than rubbed out, takes a term with a parameter and returns one without (Theorem 3.3). Written as a recipe, it eliminates a single $\lambda$ from a term $M$ containing no other, producing a term $[x]M$ in which $x$ does not occur:

The three clauses are the three cases of that proof wearing programs: the first is the case of a line that does not use the hypothesis, and writes the $𝖪$ that weakens it in; the second is the case of the hypothesis itself, whose proof of $A\to A$ is $𝖲𝖪𝖪$; the third is the case of a modus ponens, and writes the $𝖲$ that pushes the hypothesis through it. The recipe works because of the guarantee that comes with it: $([x]M)N$ runs to $M$ with $N$ in place of $x$, for every $N$.

Apply it to $F$, innermost parameter first. Write $B$ for the body, so that $F=\mathit{𝜆𝑟}.\mathit{𝜆𝑛}.B$, and read $B$ as the application $(\mathrm{𝑖𝑠𝑍𝑒𝑟𝑜}n1)(\mathrm{𝑚𝑢𝑙𝑡}n(r(\mathrm{𝑝𝑟𝑒𝑑}n)))$. The third clause splits it, the first and second finish each half, and with $𝖨$ written for $𝖲𝖪𝖪$ the result is

twenty-six symbols, with $r$ still free in it. Eliminate $r$ from that by the same three clauses and every variable is gone:

where $A=𝖲(𝖲(𝖪\mathrm{𝑖𝑠𝑍𝑒𝑟𝑜})𝖨)(𝖪1)$, $C=𝖲(𝖪\mathrm{𝑚𝑢𝑙𝑡})𝖨$ and $E=𝖲(𝖪\mathrm{𝑝𝑟𝑒𝑑})𝖨$. Thirty-eight symbols, counting $𝖨$ as its three. There is not a variable, a parameter, a conditional or a recursive call anywhere in it — only $𝖪$, $𝖲$, three arithmetic constants and juxtaposition — and $\mathrm{𝑓𝑖𝑥}F$ applied to $\overline{4}$ runs, by the two rules of Definition 1.3, to $24$.

That is the whole of this part in one object. A program you could have written in your first week is a closed term in two constants (Chapter 1); it has a type, $\mathrm{𝐼𝑛𝑡}\to \mathrm{𝐼𝑛𝑡}$, and the typing that proves so is a proof (Chapter 2); the proof is the one a mathematician would write, in Gentzen’s rules, with the terms rubbed out (§3.4). Every well-typed thing you compile sits on $𝖪$ and $𝖲$ in exactly this way.

With one exception, and it is the one Chapter 1 warned of. The two constants did not supply the loop: $\mathrm{𝑓𝑖𝑥}$ had to be added, and Remark 3.22 has just said what adding it costs. Normalisation goes, so $\mathrm{𝑓𝑖𝑥}F$ is a typed term with no normal form; and read as a proof, $\mathrm{𝑓𝑖𝑥}$ proves everything, $\perp$ included. The price of factorial is the consistency of the logic. Every language you use pays it, and pays it knowingly: the loop is worth more to a programmer than consistency is, and a programmer who wants both must say in the type where the recursion is allowed to go — which is a question for a logic with more to say than this one has.

Exercises

Reading

Girard et al. (1989, chapters 2–4) is the text behind §§3.4–3.6: natural deduction, the identification of proofs with programs, conversions as the removal of detours, and the normalisation theorem proved in full for $\to$ and $\wedge$; it is short, free online, and the right next thing to read. Gentzen (1934) is the original, and Prawitz (1965) the book that made normal proofs a subject. Howard (1980) is the correspondence as Howard wrote it down in 1969; Wadler (2015) is the story told to programmers. Next, Chapter 4: for all, and proving from a specification. References.