In programming language theory and proof theory, the Curry–Howard correspondence is a 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.The correspondence was first made explicit in . See, for example section 4.6, p.53 Gert Smolka and Jan Schwinghammer (2007-8), Lecture Notes in Semantics 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 (see Brouwer–Heyting–Kolmogorov interpretation)The Brouwer–Heyting–Kolmogorov interpretation is also called the 'proof interpretation': and Stephen Kleene (see Realizability). 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 (a variant of) 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 (i.e., the type of values returned by 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 (CoC), 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 (such as languages with arbitrary recursive functions) 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 (an approach that also generalizes to much richer models of computation, and is itself related to modal logic by a natural extension of the Curry–Howard isomorphism). A more radical approach, advocated by total functional programming, is to eliminate unrestricted recursion (and forgo Turing completeness, although still retaining high computational complexity), 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 (this may be called a tuple, a struct, a list, or some other term depending on the language), disjunction as a sum type (this type may be called a union), the false formula as the empty type and the true formula as a unit type (whose sole member is the null object). Quantifiers correspond to dependent function space or products (as appropriate).
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 ⊤ (truth) unit type logical constant ⊥ (falsehood) 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 (modus ponens) 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 is the rule of modus ponens)
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 (also annotated with its type) will depend on these variables [Γ ⊢ T:δ] when:
T is one of the variables in Γ, T is a basic combinator; i.e., under the most common combinator basis: T is K:α → (β → α) [where α and β denote the types of its arguments], 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 (since otherwise a simplification can happen).
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 (extensional) 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 α → (β → α) and (α → (β → γ)) → ((α → β) → (α → γ)).
Intuitionistic natural deduction and typed lambda calculus