The Curry-Howard Correspondence

The BHK reading says that a proof of $\varphi \rightarrow \psi$ is a construction taking any proof of $\varphi$ to a proof of $\psi$. Read casually that is an explanation. Read exactly it is a definition of a function, and the observation that turns it into a theorem is that the rules of natural deduction for implication are, symbol for symbol, the rules of the typed lambda calculus.

The correspondence is not an analogy between two subjects. It is the same structure described twice.

The calculus

Set beside the implication rules of natural deduction, the two typing rules are the same rule. Introduction discharges an assumption of $\varphi$ to conclude $\varphi \rightarrow \psi$; abstraction binds a variable of type $A$ to build a term of type $A \rightarrow B$. Elimination applies a proof of $\varphi \rightarrow \psi$ to a proof of $\varphi$; application applies a term of type $A \rightarrow B$ to a term of type $A$. Discharging an assumption is binding a variable. An undischarged assumption is a free variable.

The correspondence covers the whole of intuitionistic propositional logic once the types are enriched. A proof of a conjunction is a pair, matching the BHK clause exactly. A proof of a disjunction is a tagged value, and the tag is the BHK requirement that the disjunct be indicated. The empty type has no closed terms, which is the statement that a contradiction has no proof. Negation is the function type into the empty type, matching the definition of $\neg \varphi$ as $\varphi \rightarrow \bot$.

Excluded middle is where the reading pays its way. A term of type $A + (A \rightarrow \bot)$, for a variable $A$, would be a uniform procedure returning either a value of an arbitrary type or a function refuting it, and no such procedure exists. The intuitionistic rejection is recovered as a fact about programs rather than as a philosophical stipulation.

Normalisation

The correspondence would be a curiosity if it stopped at syntax. Its substance is that the dynamics match.

The case of implication shows the whole pattern. A proof that introduces $\varphi \rightarrow \psi$ by discharging an assumption, and then immediately eliminates it against a proof of $\varphi$, contains a detour: the proof of $\psi$ was already there, with $\varphi$ assumed, and the proof of $\varphi$ can be substituted for the assumption. The corresponding term is $(\lambda x.\, t)\,u$, and the corresponding operation is substituting $u$ for $x$ in $t$, which is the beta rule.

Prawitz proved in 1965 that every natural deduction proof normalises, and the same statement in the other vocabulary is that every typed term reduces to a normal form. Strong normalisation, that every reduction sequence terminates, holds too, and the significance is worth pausing on: a typed lambda calculus cannot express a non-terminating computation, so the price of the correspondence is that the programs are not all the programs. Adding a fixed point operator makes the language Turing complete and makes the logic inconsistent, since the fixed point operator inhabits every type, and these are the same fact.

The relation to cut elimination is the expected one. Natural deduction normalisation and sequent calculus cut elimination correspond to one another, so the result proved in the article on sequent calculus is a theorem about the termination of a computation. The subformula property becomes the statement that a normal term's subterms have types occurring in its own, which is why type checking is decidable.

What the correspondence became

The scope has widened three times since Howard's manuscript, and each widening was a discovery rather than a generalisation for its own sake.

Girard and Reynolds independently found the second-order case in 1972 and 1974, the polymorphic lambda calculus, where quantification over types matches second-order propositional quantification. Martin-Löf's dependent type theory, developed through the 1970s, extended it to predicate logic, with the dependent function type matching the universal quantifier and the dependent pair type matching the existential. That system is the basis of the proof assistants now in use, Coq and Agda and Lean, in which a formal proof is literally a program and checking it is type checking. Griffin observed in 1990 that control operators such as call with current continuation can be typed by classical principles, so that Peirce's law and double negation elimination correspond to non-local control flow, which extended the correspondence past the intuitionistic boundary that had seemed constitutive of it.

Next

The structural rules of the sequent calculus have been in the background of both this article and the one on cut elimination, treated as bookkeeping. They are not. Dropping them yields logics in which a premise is a resource that is consumed, and the next article takes up what that buys.