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 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 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:
  1. In 1934 Curry observes that the types of the combinators could be seen as axiom-schemes for intuitionistic implicational logic.
  2. In 1958 he observes that a certain kind of proof system, referred to as Hilbert-style deduction systems, coincides on some fragment to the typed fragment of a standard model of computation known as combinatory logic.
  3. 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.
In other words, the Curry–Howard correspondence is the observation that two families of seemingly unrelated formalisms—namely, the proof systems on one hand, and the models of computation on the other—are in fact the same kind of mathematical objects.
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 spectrum of new research after its discovery, leading in particular to a new class of formal systems designed to act both as a proof system and as a typed functional programming language. 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 Coq 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.
Speculatively, the Curry–Howard correspondence might be expected to lead to a substantial unification between mathematical logic and foundational computer science:
Hilbert-style logic and natural deduction are but two kinds of proof systems among a large family of formalisms. Alternative syntaxes include sequent calculus, proof nets, calculus of structures, etc. If one admits the Curry–Howard correspondence as the general principle that any proof system hides a model of computation, a theory of the underlying untyped computational structure of these kinds of proof system should be possible. Then, a natural question is whether something mathematically interesting can be said about these underlying computational calculi.
Conversely, combinatory logic and simply typed lambda calculus are not the only models of computation, either. Girard's linear logic was developed from the fine analysis of the use of resources in some models of lambda calculus; is there typed version of Turing's machine that would behave as a proof system? Typed assembly languages are such an instance of "low-level" models of computation that carry types.
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 the singleton type. Quantifiers correspond to dependent function space or products.
This is summarized in the following table:
Logic sideProgramming side
universal quantificationgeneralised product type
existential quantificationgeneralised sum type
implicationfunction type
conjunctionproduct type
disjunctionsum type
true formulaunit type
false formulabottom 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 sideProgramming side
Hilbert-style deduction systemtype system for combinatory logic
natural deductiontype system for lambda calculus

Between the natural deduction system and the lambda calculus there are the following correspondences:
Logic sideProgramming side
hypothesesfree variables
implication elimination application
implication introductionabstraction

Corresponding systems

Hilbert-style deduction systems and 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:
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:
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 logicSimply 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 sideProgramming side
assumptionvariable
axiomscombinators
modus ponensapplication
deduction theoremabstraction 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

Natural deduction and lambda calculus

After Curry emphasized the syntactic correspondence between Hilbert-style deduction and combinatory logic, Howard made explicit in 1969 a syntactic analogy between the programs of simply typed lambda calculus and the proofs of natural deduction. Below, the left-hand side formalizes intuitionistic implicational natural deduction as a calculus of sequents with implicit weakening and the right-hand side shows the typing rules of lambda calculus. In the left-hand side, Γ, Γ1 and Γ2 denote ordered sequences of formulas while in the right-hand side, they denote sequences of named formulas with all names different.
Intuitionistic implicational natural deductionLambda calculus type assignment rules

To paraphrase the correspondence, proving Γ ⊢ α means having a program that, given values with the types listed in Γ, manufactures an object of type α. An axiom corresponds to the introduction of a new variable with a new, unconstrained type, the rule corresponds to function abstraction and the rule corresponds to function application. Observe that the correspondence is not exact if the context Γ is taken to be a set of formulas as, e.g., the λ-terms λx.λy.x and λx.λy.y of type would not be distinguished in the correspondence. Examples are given below.
Howard showed that the correspondence extends to other connectives of the logic and other constructions of simply typed lambda calculus. Seen at an abstract level, the correspondence can then be summarized as shown in the following table. Especially, it also shows that the notion of normal forms in lambda calculus matches Prawitz's notion of normal deduction in natural deduction, from which it follows that the algorithms for the type inhabitation problem can be turned into algorithms for deciding intuitionistic provability.
Logic sideProgramming side
axiomvariable
introduction ruleconstructor
elimination ruledestructor
normal deductionnormal form
normalisation of deductionsweak normalisation
provabilitytype inhabitation problem
intuitionistic tautologyinhabited type

Howard's correspondence naturally extends to other extensions of natural deduction and simply typed lambda calculus. Here is a non-exhaustive list:
At the time of Curry, and also at the time of Howard, the proofs-as-programs correspondence concerned only intuitionistic logic, i.e. a logic in which, in particular, Peirce's law was not deducible. The extension of the correspondence to Peirce's law and hence to classical logic became clear from the work of Griffin on typing operators that capture the evaluation context of a given program execution so that this evaluation context can be later on reinstalled. The basic Curry–Howard-style correspondence for classical logic is given below. Note the correspondence between the double-negation translation used to map classical proofs to intuitionistic logic and the continuation-passing-style translation used to map lambda terms involving control to pure lambda terms. More particularly, call-by-name continuation-passing-style translations relates to Kolmogorov's double negation translation and call-by-value continuation-passing-style translations relates to a kind of double-negation translation due to Kuroda.
Logic sideProgramming side
Peirce's law: → αcall-with-current-continuation
double-negation translationcontinuation-passing-style translation

A finer Curry–Howard correspondence exists for classical logic if one defines classical logic not by adding an axiom such as Peirce's law, but by allowing several conclusions in sequents. In the case of classical natural deduction, there exists a proofs-as-programs correspondence with the typed programs of Parigot's λμ-calculus.

Sequent calculus

A proofs-as-programs correspondence can be settled for the formalism known as Gentzen's sequent calculus but it is not a correspondence with a well-defined pre-existing model of computation as it was for Hilbert-style and natural deductions.
Sequent calculus is characterized by the presence of left introduction rules, right introduction rule and a cut rule that can be eliminated. The structure of sequent calculus relates to a calculus whose structure is close to the one of some abstract machines. The informal correspondence is as follows:
Logic sideProgramming side
cut eliminationreduction in a form of abstract machine
right introduction rulesconstructors of code
left introduction rulesconstructors of evaluation stacks
priority to right-hand side in cut-eliminationcall-by-name reduction
priority to left-hand side in cut-eliminationcall-by-value reduction

Related proofs-as-programs correspondences

The role of de Bruijn

used the lambda notation for representing proofs of the theorem checker Automath, and represented propositions as "categories" of their proofs. It was in the late 1960s at the same period of time Howard wrote his manuscript; de Bruijn was likely unaware of Howard's work, and stated the correspondence independently. Some researchers tend to use the term Curry–Howard–de Bruijn correspondence in place of Curry–Howard correspondence.

BHK interpretation

The BHK interpretation interprets intuitionistic proofs as functions but it does not specify the class of functions relevant for the interpretation. If one takes lambda calculus for this class of function, then the BHK interpretation tells the same as Howard's correspondence between natural deduction and lambda calculus.

Realizability

's recursive realizability splits proofs of intuitionistic arithmetic into the pair of a recursive function and of
a proof of a formula expressing that the recursive function "realizes", i.e. correctly instantiates the disjunctions and existential quantifiers of the initial formula so that the formula gets true.
Kreisel's modified realizability applies to intuitionistic higher-order predicate logic and shows that the simply typed lambda term inductively extracted from the proof realizes the initial formula. In the case of propositional logic, it coincides with Howard's statement: the extracted lambda term is the proof itself and the realizability statement is a paraphrase of the fact that the extracted lambda term has the type that the formula means.
Gödel's dialectica interpretation realizes intuitionistic arithmetic with computable functions. The connection with lambda calculus is unclear, even in the case of natural deduction.

Curry–Howard–Lambek correspondence

showed in the early 1970s that the proofs of intuitionistic propositional logic and the combinators of typed combinatory logic share a common equational theory which is the one of cartesian closed categories. The expression Curry–Howard–Lambek correspondence is now used by some people to refer to the three way isomorphism between intuitionistic logic, typed lambda calculus and cartesian closed categories, with objects being interpreted as types or propositions and morphisms as terms or proofs. The correspondence works at the equational level and is not the expression of a syntactic identity of structures as it is the case for each of Curry's and Howard's correspondences: i.e. the structure of a well-defined morphism in a cartesian-closed category is not comparable to the structure of a proof of the corresponding judgment in either Hilbert-style logic or natural deduction. To clarify this distinction, the underlying syntactic structure of cartesian closed categories is rephrased below.
Objects are defined by
Morphisms are defined by
Well-defined morphisms are defined by the following typing rules.
Identity:
Composition:
Unit type :
Cartesian product:
Left and right projection:
Currying:
Application:
Finally, the equations of the category are
These equations imply the following -laws:
Now, there exists such that iff is provable in implicational intuitionistic logic,.

Examples

Thanks to the Curry–Howard correspondence, a typed expression whose type corresponds to a logical formula is analogous to a proof of that formula. Here are examples.

The identity combinator seen as a proof of in Hilbert-style logic

As an example, consider a proof of the theorem. In lambda calculus, this is the type of the identity function I = λx.x and in combinatory logic, the identity function is obtained by applying S = λfgx.fx twice to K = λxy.x. That is, I =. As a description of a proof, this says that the following steps can be used to prove :
In general, the procedure is that whenever the program contains an application of the form, these steps should be followed:
  1. First prove theorems corresponding to the types of P and Q.
  2. Since P is being applied to Q, the type of P must have the form α → β and the type of Q must have the form α for some and. Therefore, it is possible to detach the conclusion,, via the modus ponens rule.

    The composition combinator seen as a proof of in Hilbert-style logic

As a more complicated example, let's look at the theorem that corresponds to the B function. The type of B is → → Γ → α. B is equivalent to. This is our roadmap for the proof of the theorem → → Γ → α.
The first step is to construct. To make the antecedent of the K axiom look like the S axiom, set α equal to, and equal to :
Since the antecedent here is just S, the consequent can be detached using Modus Ponens:
This is the theorem that corresponds to the type of. Now apply S to this expression. Taking S as follows
put,, and, yielding
and then detach the consequent:
This is the formula for the type of. A special case of this theorem has :
This last formula must be applied to K. Specialize K again, this time by replacing with and with :
This is the same as the antecedent of the prior formula so, detaching the consequent:
Switching the names of the variables and gives us
which was what remained to prove.

The normal proof of in natural deduction seen as a λ-term

The diagram below gives proof of in natural deduction and shows how it can be interpreted as the λ-expression λ a. λ b. λ g. of type.
a:β → α, b:γ → β, g:γ ⊢ b : γ → β a:β → α, b:γ → β, g:γ ⊢ g : γ
——————————————————————————————————— ————————————————————————————————————————————————————————————————————
a:β → α, b:γ → β, g:γ ⊢ a : β → α a:β → α, b:γ → β, g:γ ⊢ b g : β
————————————————————————————————————————————————————————————————————————
a:β → α, b:γ → β, g:γ ⊢ a : α
————————————————————————————————————
a:β → α, b:γ → β ⊢ λ g. a : γ → α
————————————————————————————————————————
a:β → α ⊢ λ b. λ g. a : -> γ → α
————————————————————————————————————
⊢ λ a. λ b. λ g. a : -> -> γ → α

Other applications

Recently, the isomorphism has been proposed as a way to define search space partition in genetic programming. The method indexes sets of genotypes by their Curry–Howard isomorphic proof.
As noted by INRIA research director Bernard Lang, the Curry-Howard correspondence constitutes an argument against the patentability of software: since algorithms are mathematical proofs, patentability of the former would imply patentability the latter. A theorem could be private property, a mathematician would have to pay for using it, and to trust the company that sells it but keeps its proof secret and rejects responsibility for any errors.

Generalizations

The correspondences listed here go much farther and deeper. For example, cartesian closed categories are generalized by closed monoidal categories. The internal language of these categories is the linear type system, which generalizes simply-typed lambda calculus as the internal language of cartesian closed categories. Moreover, these can be shown to correspond to cobordisms, which play a vital role in string theory.
An extended set of equivalences is also explored in homotopy type theory, which became a very active area of research around 2013 and as of 2018 still is. Here, type theory is extended by the univalence axiom which permits homotopy type theory to be used as a foundation for all of mathematics. That is, the Curry–Howard correspondence that proofs are elements of inhabited types is generalized to the notion homotopic equivalence of proofs.

Seminal references