Lambda Calculus and the Curry–Howard Correspondence

A proof of an implication explains how to obtain its conclusion from its hypothesis. A function explains how to obtain an output from an input. Making this resemblance precise required a language of functions, a discipline of types, and a detailed analysis of proof rules.

The result is usually called the Curry–Howard correspondence. It is a family of exact relationships between particular calculi. Understanding one small correspondence is more informative than memorizing a table of slogans.

Functions without unnecessary notation

Moses Schönfinkel's 1924 paper developed combinators: operations designed to express combinations of functions without bound variables. Haskell Curry extended combinatory logic and investigated its connections with logic.

Alonzo Church developed lambda calculus in the early 1930s, initially within a larger foundational project. Inconsistency results affected that original logical system, while lambda calculus continued as a mathematical account of functions and computation.

The untyped lambda calculus has three basic forms:

A term is a variable, an abstraction, or an application. In $\lambda x.t$, the variable $x$ is bound in $t$. Application associates to the left, so $f\,a\,b$ means $(f\,a)\,b$.

The expression $\lambda x.x$ represents the identity function. Applying it to $u$ gives

The general computation rule is beta reduction:

Substitution must avoid capturing free variables. For example, substituting $y$ for $x$ in $\lambda y.x$ requires renaming the bound variable first. The result can be $\lambda z.y$; writing $\lambda y.y$ would change the meaning.

Computation without guaranteed termination

Lambda terms can represent arithmetic and general effective computation. The computability note placed Church's results alongside recursive functions and Turing machines.

This expressive power includes divergence. Let

A beta step returns exactly the same term. There is no normal form.

The Church–Rosser theorem establishes confluence of beta reduction: if a term reduces along two finite paths, the resulting terms have a common reduct. Consequently, a normal form, when it exists, is unique up to the usual renaming of bound variables.

Confluence does not say that every term terminates. It does not even say that every reduction strategy reaches a normal form whenever one exists. An evaluator can spend forever reducing $\Omega$ inside an argument that another evaluation strategy would discard.

These distinctions become central when a calculus is used both to execute programs and to represent proofs.

Adding simple types

In the simply typed lambda calculus, types can be built from atomic types using the function constructor $A\to B$.

A context records variable assumptions, such as $x:A,y:B$. The judgment

says that $t$ has type $A$ under the assumptions in $\Gamma$.

Two rules expose the connection with implication:

Abstraction discharges an input assumption. Application uses a function together with a suitable input.

Church's 1940 simple type theory belongs to this history, although its full logical setting includes choices different from the purely intuitionistic correspondence developed below. “Typed” does not by itself determine whether a logic is classical or constructive.

Constructing a proof and a term together

Consider the proposition

Assume $A$. Under that assumption, also assume $B$. The original assumption already supplies $A$. Discharge the assumption $B$ to obtain $B\to A$, then discharge $A$ to obtain the whole proposition.

Attach names to the assumptions. Let $x:A$ and $y:B$. The proof of $A$ is represented by $x$. Discharging $y$ creates $\lambda y.x$, and discharging $x$ creates

The type of $k$ is $A\to(B\to A)$.

Now give it a term $a:A$ and a term $b:B$:

On the proof side, introducing an implication and then immediately eliminating it creates a detour. Removing that detour substitutes the supplied proof for the discharged assumption.

Beta reduction is therefore the computational counterpart of this proof normalization step. The correspondence concerns the internal structure and transformation of derivations, not just a resemblance between the words “proof” and “program.”

The example also depends on permitting an unused assumption $B$. In a strictly linear fragment, that use of weakening would need justification, connecting this note with the preceding discussion of structural rules.

From Curry's observation to Howard's formulation

Curry had recognized relationships between types of combinators and implicational logic. William Howard's 1969 manuscript, published in 1980 as “The Formulae-as-Types Notion of Construction,” developed the connection with natural deduction and constructive arithmetic.

Related ideas appeared in work by de Bruijn on Automath and by Martin-Löf on constructive type theory. The modern name joins some of these threads without exhausting their history.

Wadler's historical presentation is useful for tracing the contributions and explaining why several discoveries and rediscoveries belong to the account.

Extending the correspondence

For an appropriate intuitionistic calculus, the connection extends beyond implication.

For conjunction, a pair $\langle a,b\rangle$ represents the combined proof. Projecting its first component reduces to $a$, matching the elimination of a conjunction-introduction detour.

For disjunction, a tag records which alternative has been supplied. Eliminating it requires a construction for each case. The tag is part of the evidence; an unstructured claim that one of two propositions holds does not yet explain the elimination rule.

Dependent products and sums extend the account to quantifiers. Their additional structure belongs in the next note.

Functions and products provide enough structure to inspect the correspondence directly. The lab checks each typed reduction against its original judgment; its separate untyped examples prepare the question of termination that follows.

Why an arbitrary program is not a proof

The simply typed lambda calculus, with its standard rules and without unrestricted recursion, is strongly normalizing: every reduction sequence terminates.

This matters logically. Under the intended empty-type interpretation, a closed term of the empty type would represent a proof of falsehood. A sound normalization argument helps exclude such a term by analyzing possible normal forms.

Now add an unrestricted fixed-point operator at every type. A recursive definition can diverge while being assigned a type whose logical reading would be absurd. General-purpose type safety may ensure that a program does not perform certain invalid operations, while leaving termination unproved.

Thus a language can be well typed and still fail to support the direct interpretation “every program of this type is a terminating proof of this proposition.”

Effects, exceptions, control operators, and evaluation strategy introduce further distinctions. Some have sophisticated logical interpretations, including connections with classical logic, but each interpretation needs its own formal account.

What the correspondence made possible

The correspondence gave proof checking a computational organization. A proposition could be represented by a type, a proof by a term, and a basic proof transformation by reduction.

It also gave programming languages a logical vocabulary for abstraction, composition, and specification. Those consequences developed along different paths: richer foundational type theories, categorical semantics, and executable functional languages.

We follow those paths separately so that the history does not jump directly from Church to a modern proof assistant without explaining the intervening mathematics.

Sources and further reading

• Moses Schönfinkel, “Über die Bausteine der mathematischen Logik” (1924).
• Alonzo Church, “A Set of Postulates for the Foundation of Logic” (1932–1933); Church and J. Barkley Rosser, “Some Properties of Conversion” (1936).
• Alonzo Church, “A Formulation of the Simple Theory of Types” (1940).
• Haskell B. Curry and Robert Feys, Combinatory Logic, volume I (1958).
• William A. Howard, “The Formulae-as-Types Notion of Construction,” manuscript of 1969, published in To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism (1980).
• Philip Wadler, “Propositions as Types” (2015).