Curry–Howard correspondence

In programming language theory and proof theory, the Curry–Howard correspondence is the direct relationship between computer programs and mathematical proofs. It is also known as the Curry–Howard isomorphism or equivalence, or the proofs-as-programs and propositions- or formulae-as-types interpretation.
It is a generalization of a syntactic analogy between systems of formal logic and computational calculi that was first discovered by the American mathematician Haskell Curry and the logician William Alvin Howard. It is the link between logic and computation that is usually attributed to Curry and Howard, although the idea is related to the operational interpretation of intuitionistic logic given in various formulations by L. E. J. Brouwer, Arend Heyting and Andrey Kolmogorov and Stephen Kleene. The relationship has been extended to include category theory as the three-way Curry–Howard–Lambek correspondence.

Origin, scope, and consequences

The beginnings of the Curry–Howard correspondence lie in several observations:

In 1934, Curry observes that the types of the combinators could be seen as axiom-schemes for intuitionistic implicational logic.
In 1958, he observes that a certain kind of proof system, referred to as Hilbert-style deduction systems, coincides on some fragment with the typed fragment of a standard model of computation known as combinatory logic.
In 1969 Howard observes that another, more "high-level" proof system, referred to as natural deduction, can be directly interpreted in its intuitionistic version as a typed variant of the model of computation known as lambda calculus.

Actually, Howard's first formulation of the isomorphism was referred to Gentzen's sequent calculus. The observation that the isomorphism is best understood with natural deduction, as well as the current formulation of the isomorphism itself, are due to Per Martin-Löf. The Curry–Howard correspondence is the observation that there is an isomorphism between the proof systems, and the models of computation. It is the statement that these two families of formalisms can be considered as identical.
If one abstracts on the peculiarities of either formalism, the following generalization arises: a proof is a program, and the formula it proves is the type for the program. More informally, this can be seen as an analogy that states that the return type of a function is analogous to a logical theorem, subject to hypotheses corresponding to the types of the argument values passed to the function; and that the program to compute that function is analogous to a proof of that theorem. This sets a form of logic programming on a rigorous foundation: proofs can be represented as programs, and especially as lambda terms, or proofs can be run.
The correspondence has been the starting point of a large range of new research after its discovery, leading to a new class of formal systems designed to act both as a proof system and as a typed programming language based on functional programming. This includes Martin-Löf's intuitionistic type theory and Coquand's calculus of constructions, two calculi in which proofs are regular objects of the discourse and in which one can state properties of proofs the same way as of any program. This field of research is usually referred to as modern type theory.
Such typed lambda calculi derived from the Curry–Howard paradigm led to software like Rocq in which proofs seen as programs can be formalized, checked, and run.
A converse direction is to use a program to extract a proof, given its correctness, an area of research closely related to proof-carrying code. This is only feasible if the programming language the program is written for is very richly typed: the development of such type systems has been partly motivated by the wish to make the Curry–Howard correspondence practically relevant.
The Curry–Howard correspondence also raised new questions regarding the computational content of proof concepts that were not covered by the original works of Curry and Howard. In particular, classical logic has been shown to correspond to the ability to manipulate the continuation of programs and the symmetry of sequent calculus to express the duality between the two evaluation strategies known as call-by-name and call-by-value.
Because of the possibility of writing non-terminating programs, Turing-complete models of computation must be interpreted with care, as naive application of the correspondence leads to an inconsistent logic. The best way of dealing with arbitrary computation from a logical point of view is still an actively debated research question, but one popular approach is based on using monads to segregate provably terminating from potentially non-terminating code. A more radical approach, advocated by total functional programming, is to eliminate unrestricted recursion, using more controlled corecursion wherever non-terminating behavior is actually desired.

General formulation

In its more general formulation, the Curry–Howard correspondence is a correspondence between formal proof calculi and type systems for models of computation. In particular, it splits into two correspondences. One at the level of formulas and types that is independent of which particular proof system or model of computation is considered, and one at the level of proofs and programs which, this time, is specific to the particular choice of proof system and model of computation considered.
At the level of formulas and types, the correspondence says that implication behaves the same as a function type, conjunction as a "product" type, disjunction as a sum type, the false formula as the empty type and the true formula as a unit type. Quantifiers correspond to dependent function space or products.
This is summarized in the following table:

Logic side	Programming side
formula	type
proof	term
formula is true	type has an element
formula is false	type does not have an element
logical constant ⊤	unit type
logical constant ⊥	empty type
implication	function type
conjunction	product type
disjunction	sum type
universal quantification	dependent product type
existential quantification	dependent sum type

At the level of proof systems and models of computations, the correspondence mainly shows the identity of structure, first, between some particular formulations of systems known as Hilbert-style deduction system and combinatory logic, and, secondly, between some particular formulations of systems known as natural deduction and lambda calculus.

Logic side	Programming side
Hilbert-style deduction system	type system for combinatory logic
natural deduction	type system for lambda calculus

Between the natural deduction system and the lambda calculus there are the following correspondences:

Logic side	Programming side
hypotheses	free variables
implication elimination	application
implication introduction	abstraction

Corresponding systems

Intuitionistic Hilbert-style deduction systems and typed combinatory logic

It was at the beginning a simple remark in Curry and Feys's 1958 book on combinatory logic: the simplest types for the basic combinators K and S of combinatory logic surprisingly corresponded to the respective axiom schemes α → and → → ) used in Hilbert-style deduction systems. For this reason, these schemes are now often called axioms K and S. Examples of programs seen as proofs in a Hilbert-style logic are given [|below].
If one restricts to the implicational intuitionistic fragment, a simple way to formalize logic in Hilbert's style is as follows. Let Γ be a finite collection of formulas, considered as hypotheses. Then δ is derivable from Γ, denoted Γ ⊢ δ, in the following cases:

δ is an hypothesis, i.e. it is a formula of Γ,
δ is an instance of an axiom scheme; i.e., under the most common axiom system:
* δ has the form α →, or
* δ has the form → → ),
δ follows by deduction, i.e., for some α, both α → δ and α are already derivable from Γ

This can be formalized using inference rules, as in the left column of the following table.
Typed combinatory logic can be formulated using a similar syntax: let Γ be a finite collection of variables, annotated with their types. A term T will depend on these variables when:

T is one of the variables in Γ,
T is a basic combinator; i.e., under the most common combinator basis:
* T is K:α → , or
* T is S: → → ),
T is the composition of two subterms which depend on the variables in Γ.

The generation rules defined here are given in the right-column below. Curry's remark simply states that both columns are in one-to-one correspondence. The restriction of the correspondence to intuitionistic logic means that some classical tautologies, such as Peirce's law → α, are excluded from the correspondence.

Hilbert-style intuitionistic implicational logic	Typed combinatory logic

Seen at a more abstract level, the correspondence can be restated as shown in the following table. Especially, the deduction theorem specific to Hilbert-style logic matches the process of abstraction elimination of combinatory logic.

Logic side	Programming side
assumption	variable
axiom schemes	combinators
modus ponens	application
deduction theorem	abstraction elimination

Thanks to the correspondence, results from combinatory logic can be transferred to Hilbert-style logic and vice versa. For instance, the notion of reduction of terms in combinatory logic can be transferred to Hilbert-style logic and it provides a way to canonically transform proofs into other proofs of the same statement. One can also transfer the notion of normal terms to a notion of normal proofs, expressing that the hypotheses of the axioms never need to be all detached.
Conversely, the non provability in intuitionistic logic of Peirce's law can be transferred back to combinatory logic: there is no typed term of combinatory logic that is typable with type
Results on the completeness of some sets of combinators or axioms can also be transferred. For instance, the fact that the combinator X constitutes a one-point basis of combinatory logic implies that the single axiom scheme
which is the principal type of X, is an adequate replacement to the combination of the axiom schemes