The Correspondence

The correspondence pairs the two halves of the foundations exactly. A proposition corresponds to a type; a proof of the proposition corresponds to a program — a term — of that type. Implication A→B corresponds to the function type A→B, and the pairing is not loose: a proof of A→B is a method turning any proof of A into a proof of B, which is precisely a function from the type A to the type B — a program of type A→B. Conjunction is the product type, a proof being a pair; disjunction is the sum type, a proof being a tagged choice; the rules of intuitionistic natural deduction are, inference by inference, the typing rules of the simply-typed λ-calculus. The proposition “is provable” and the type “is inhabited” are one predicate.

And then the dynamic half — the part that makes it astonishing. Proofs can be simplified: a detour, where one proves A→B by assuming A and deriving B and then immediately feeds it a proof of A, can be cut out, the proof of A substituted directly. This simplification is normalization. Under the correspondence, normalizing a proof is evaluating a program — β-reduction, the substitution of an argument into a function body, the single computational step of the λ-calculus. To run a program is to simplify a proof; the normal form of the proof is the value of the program. So the correspondence is no static dictionary between vocabularies; it is a live identification of two processes — proving-and-simplifying, and computing — that turn out to be one process. Curry saw the static pairing in the 1930s and 40s; Howard made the dynamic identification explicit in 1969; and Lambek added a third vertex, the cartesian closed categories, completing a three-way identity to which we return.

The upshot is what the rest of the volume exploits. Because logic and computation are one system, every object in one has an exact counterpart in the other, with all its properties intact. A consistent logic is a type theory in which some type is uninhabited; an inconsistent logic is one in which every type has a program. A logic that proves everything corresponds to a language in which every type — the empty one included — has an inhabitant. Hold that correspondence fixed and ask the collection's question: what is the diagonal, here? What is the fixed point, when a proof and a program are the same thing? The answer is a single notorious object, and it bears two names, depending on which side you read it from.

The diagonal, in the λ-calculus, is the fixed-point combinator. The untyped λ-calculus contains a term Y such that for any f, Yf reduces to f(Yf): Y hands every function a fixed point. This is the engine of recursion — how a function is made to call itself, the basis of every recursive definition, the λ-calculus's form of Kleene's recursion theorem and the obverse volume's reflexive object. Read as a program, Y is pure generative power: the diagonal's positive face, the thing that makes self-reference a tool.

Now read Y across the correspondence, as a proof, and watch the face turn. Were the fixed-point combinator assigned a type, it would have the type (A→A)→A for every proposition A: given a function from A to A, it returns an A. But A→A is trivially provable — it is the identity, “assume A, conclude A.” So Y, fed that trivial proof, would yield a proof of A — and A was arbitrary. Y proves every proposition; in particular it proves ⊥, falsehood. The untyped λ-calculus, read as a logic, derives everything: it is inconsistent. This is Curry's paradox, shown in 1942 — write D = λx.(xx → A) and U = DD; then U reduces to (U → A), so U is equivalent to “U implies A,” and from a sentence equivalent to its own implication of A, minimal logic derives A itself, for any A at all. The fixed-point combinator is the machine that builds the self-referential U. The very object that is recursion is, read as a proof, the collapse of the logic.

This is the diagonal's two faces, the obverse and reverse the collection has followed throughout — but here they are not two readings of one theorem, joined by contraposition. They are one term, the same string of symbols, read once as a program and once as a proof. As a program it is recursion, the generative face, the engine; as a proof it is ⊢ ⊥, the catastrophic face, the inconsistency. The poison and the antidote of the threshold volume, the wall and the power of the obverse, have collapsed into a single object whose meaning flips entirely with the question you put to it — “what does this compute?” or “what does this prove?” The fixed point is recursion when you want to compute and contradiction when you want to prove, and it is numerically the same fixed point.

So how is consistency recovered? By typing. Look at the heart of the fixed-point combinator: the self-application xx, a variable applied to itself — the subterm that appears inside Y and in the looping term Ω = (λx.xx)(λx.xx). For xx to make sense in a type system, x must carry some type τ and, since it is applied to itself, also the type τ→σ of a function on τ — so τ and τ→σ must be one and the same type, τ = τ→σ. The simply-typed λ-calculus forbids exactly this: a type is a finite tree built from base types by the arrow, and no finite tree equals a function type formed from itself. So λx.xx is untypable; Y is untypable; the fixed-point combinator cannot be written. Self-application is banned at the level of syntax.

And this ban is no side effect — it is the whole point of types. Church introduced the simply-typed λ-calculus in 1940 precisely to exclude the paradoxical self-applications of his earlier untyped system, which Kleene and Rosser had shown inconsistent in 1935 and which Curry's paradox pinned down. The maneuver is exactly Russell's, a generation before: Russell's theory of types forbade a set from belonging to itself, breaking the diagonal of set theory; Church's theory of types forbids a function from applying to itself, breaking the diagonal of computation. Both are the same defensive move against the same construction — stratify, so that the self-application the diagonal requires can no longer be formed. Typing is the diagonal's prohibition rendered as a discipline of syntax: the rule that a thing may not be applied to, or contain, or quantify over, itself.

This is the entry on the threshold volume's menu that the correspondence makes exact. That volume laid out the prices a system must pay to host self-reference and survive — surrender expressiveness, or bivalence, or a universal truth predicate, or consistency. Typing is the surrender of expressiveness in its most precise form: the expressiveness given up is, exactly, self-application. Where the threshold named the price in general terms, the correspondence prices it in the hard currency of computation — and the next section reads the receipt to the last computable function.

The ban works, with a precise and beautiful payoff: the simply-typed λ-calculus is strongly normalizing. Every well-typed term reduces to a normal form — a finished value, no reductions left — in finitely many steps, and no matter the order in which the reductions are taken. There is no looping; every typed program halts. This is not obvious; it is a real theorem, proved by Tait in 1967 by the method of “reducibility.” The naive induction on terms fails — applying a function can produce a larger term — so Tait defines, by recursion on types, a predicate of “reducible” terms strong enough to carry the induction through: a strengthening of the goal, indexed by the structure of types, that is itself a quiet instance of the very move the collection studies. Strong normalization is the ban's dividend. Where the untyped calculus had Ω looping forever and a fixed point for every function, the typed calculus has neither.

And strong normalization is consistency, by the correspondence, in a single step. Consider the empty type — the type with no values, which under Curry–Howard is the proposition ⊥, falsehood. Is it inhabited? Suppose it were, by a closed term M : ⊥. By strong normalization M reduces to a closed normal form; but the shape of a closed normal term is fixed by its type, and ⊥ has no introduction rule and so no normal inhabitant at all. Hence there is no closed normal term of type ⊥, and — everything normalizing — no closed term of type ⊥ whatsoever. The empty type is empty; ⊥ is unprovable; the logic is consistent. Typing bought consistency, and termination is the receipt — they are one fact read on the two sides of the correspondence. A language in which every program halts is a logic in which falsehood has no proof.

So the situation has exactly inverted from the combinator section. There, the untyped calculus had the fixed point and was, as a logic, inconsistent — falsehood provable, every type inhabited. Here, the typed calculus lacks the fixed point and is consistent — falsehood unprovable, the empty type empty. The single difference between the two states is the presence or absence of the fixed point, and that one difference governs everything: with it, looping and inconsistency; without it, termination and consistency. We have bought a great deal by typing. The next section is the bill.

Consistency is not free, and the bill is exact: it is Turing-completeness. The strongly-normalizing typed calculus, by halting always, cannot express every computable function — and the reason is the halting problem, run backwards. A Turing-complete language expresses every computable function, including ones whose termination is undecidable; and since no algorithm decides halting, no Turing-complete language can guarantee that all its programs halt — it must admit possibly-non-terminating ones. The typed calculus guarantees that all its programs halt. Therefore it is not Turing-complete: there are computable functions it cannot define. The very property that gave consistency — every program terminates — is the property that forbids universality. Termination and Turing-completeness are incompatible, and the typed calculus chose termination.

So the choice is forced, and a single object governs it. Lay the two regimes side by side. With the fixed point — the untyped calculus, or a typed calculus given a general-recursion operator — you have Turing-completeness, you have programs that loop, and, as a logic, you have inconsistency, the fixed point inhabiting every type. Without it — the simply-typed calculus and the consistent calculi above it — you have termination, you have consistency, and you have a strict cap below Turing-completeness. There is no third regime keeping Turing-completeness and termination and consistency, because all three turn on the one object the first demands and the others forbid. The diagonal is the master switch between two possible worlds of computation, and it throws all three levers at once.

And the cap on the consistent side is not a low one — which sharpens the point rather than softening it. One can climb a long way in expressive power while staying terminating and consistent. System F, the polymorphic λ-calculus, is strongly normalizing (Girard, 1972) and consistent, yet it expresses an enormous class of functions — every one whose totality is provable in second-order arithmetic, very nearly everything anyone writes — and above it stand the stronger systems on which modern proof assistants are built, all terminating, all consistent, all able to formalize the deepest mathematics. Yet none of them is Turing-complete, and the single thing each lacks is the fixed point. The price is not the loss of power in general; it is the loss of one specific thing — unrestricted self-application — and the climb up the consistent hierarchy, however high it reaches, never crosses the line the fixed point alone can cross. The cap is precise, and the fixed point is exactly what lies beyond it.

First, the bridge back to the obverse. You can recover Turing-completeness inside a typed calculus, without abandoning types altogether, by admitting one new kind of type — a recursive type. The type τ = μX.(X→X) is, by definition, a type equal to its own function space: τ ≅ τ→τ. With it, a term of type τ may be applied to itself — being at once a function τ→τ and an argument τ — so the self-application xx typechecks once more, Y returns, recursion returns, and strong normalization is lost. But look at what μX.(X→X) is: a type D with D ≅ D→D. That is the reflexive object of the obverse volume — Scott's D∞, the object isomorphic to its own function space, the thing Set forbids and the domains permit — here in purely syntactic dress. The recursive type is the reflexive object; to admit it is to admit the diagonal's positive face; and its price, the loss of normalization, is the very price the obverse charged for that face in Set. Three volumes have met on one object: the reflexive object in categories, the recursive type in computation, and the fixed-point combinator in programs are one thing under three descriptions.

Which opens onto the deepest unity the collection can state. The correspondence has a third vertex. Curry–Howard pairs logic with computation; Lambek's theorem adds categories — the simply-typed λ-calculus, intuitionistic logic, and the cartesian closed categories are, all three, the same structure, a fact sometimes called computational trinitarianism. A proposition, a type, and an object; a proof, a program, and a morphism; normalization, evaluation, and the equations of a category: three vocabularies for one mathematics. And the diagonal appears in each, as the same thing seen three ways — in categories, Lawvere's theorem, the construction this collection is built upon; in logic, Curry's paradox and Löb and Gödel, self-reference as inconsistency and incompleteness; in computation, the Y-combinator, self-reference as recursion.

So the place of it all is clear. The collection's thesis was that one construction lies behind six famous results. The trinity says something larger — that the three great frameworks in which those results live, category theory and logic and computation, are themselves one framework, and that the diagonal is the precise point at which the three coincide. The fixed point is not a theorem that happens to recur across fields, nor even a construction that happens to unify six results. It is the single place where structure, proof, and computation are revealed to be one thing — and in each of the three it is at once the source of all generative power and the seed of all paradox. Lawvere's morphism, Curry's proof, and Church's program are the same fixed point; and that fixed point is where mathematics, asked to speak of itself, both gains its deepest tool and meets its hardest limit. The collection found the one construction behind the results. The correspondence finds the one construction behind the frameworks — and it is the diagonal, all the way down.