Curry-Howard correspondence

The Curry-Howard correspondence is the direct relationship between computer programs and mathematical proofs. Also known as Curry-Howard isomorphism, proofs-as-programs correspondence and formulae-as-types correspondence, it refers to the 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.

Origin, scope and consequences of the correspondence

At the very beginning, the Curry–Howard correspondence is
# the observation in 1934 by Curry that the types of the combinators could be seen as axiom-schemes for intuitionistic implicational logic,
# the observation in 1958 by Curry 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,
# the observation in 1969 by Howard 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 simple observation that two at-the-time-seemingly-unrelated families of formalisms, the proof systems on one side and the models of computation on the other side, were, on the two examples considered by Curry and Howard, in fact structurally the same kind of objects.

If one now abstracts on the peculiarities of this or that formalism, the immediate generalization is the following claim: "a proof is a program, the formula it proves is a type for the program". Most informally, this can be seen as an analogy which 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 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. 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 which were not covered by the original works of Curry and Howard. In particular, classical logic has been shown to correspond to the ability to manipulating 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 may 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 untyped underlying 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; can we imagine a typed version of Turing machine that would behave as a proof system? Typed assembly languages are such an instance of "low-level" model of computation that carries types.

General formulation of the Curry-Howard correspondence

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. If quantification comes in two flavors, it is because there are two ways to think about the Curry-Howard correspondence. If one considers that every single proof step has to be computational, then universal quantification is interpreted as dependent product and existential quantification as a dependent sum (this corresponds to interpreting a proof as a term typed à la Church). If otherwise one considers that some trivial computational step can be omitted, then universal quantification is interpreted as an intersection type and existential quantification as a union type (this corresponds to interpreting a proof as a term typed à la Curry, which was actually the approach taken by Howard). This is summarized in the following table:

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.

Howard's correspondence naturally extends to other extensions of natural deduction and simply-typed lambda calculus. Here is a non exhaustive list:

* Girard-Reynolds System F as a common language for both second-order propositional logic and polymorphic lambda calculus,
* higher-order logic and Girard's System F_ω
* inductive types as algebraic data type
* ...

Correspondence between classical logic and control operators

At the time of Curry, and so was at the time of Howard, the proof-as-program correspondence was only concerning 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.

Finally, the equations of the category are
* $id\; circ\; t\; =\; t$, $t\; circ\; id\; =\; t$, $(v\; circ\; u)\; circ\; t\; =\; v\; circ\; (u\; circ\; t)$
* $star\; circ\; t\; =\; star$
* $pi\_1\; circ\; (t,\; u)\; =\; t,\; pi\_2\; circ\; (t,u)\; =\; u,\; (pi\_1\; circ\; t,\; pi\_2\; circ\; t)\; =\; t$
* $eval\; circ\; (lambda\; t,\; id)\; =\; t,\; lambda\; eval\; =\; id$

Now, there exists $t$ 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 a simple example, we construct 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" twice to K. That is, we have I = ((S K) K). As a description of a proof, this says that to prove α → α, we can proceed as follows:

* instantiate the second axiom scheme with the formulas α, β → α and α, so that to obtain a proof of (α → ((β → α) → α)) → ((α → (β → α)) → (α → α)),
* instantiate the first axiom scheme once with α and β → α, so that to obtain a proof of α → ((β → α) → α),
* instantiate the first axiom scheme a second time with α and β, so that to obtain a proof of α → (β → α),
* apply modus ponens twice so that to obtain a proof of α → α

In general, the procedure is that whenever the program contains an application of the form ("P" "Q"), we should first prove theorems corresponding to the types of "P" and "Q". 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 β. We can then 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 (S (K S) K). This is our roadmap for the proof of the theorem (β → α) → (γ → β) → γ → α.

First we need to construct (K S). We make the antecedent of the K axiom look like the S axiom by setting α equal to (α → β → γ) → (α → β) → α → γ, and β equal to δ:

: α → β → α: ((α → β → γ) → (α → β) → α → γ) → δ → (α → β → γ) → (α → β) → α → γ

Since the antecedent here is just S, we can detach the consequent:

: δ → (α → β → γ) → (α → β) → α → γ

This is the theorem that corresponds to the type of (K S). We now apply S to this expression. Taking S

: (α → β → γ) → (α → β) → α → γ

we put α = δ, β = α → β → γ, and γ = (α → β) → α → γ, yielding

: (δ → (α → β → γ) → (α → β) → α → γ) → (δ → (α → β → γ)) → δ → (α → β) → α → γ

and we then detach the consequent:

: (δ → α → β → γ) → δ → (α → β) → α → γ

This is the formula for the type of (S (K S)). A specialcase of this theorem has δ = (β → γ):

: ((β → γ) → α → β → γ) → (β → γ) → (α → β) → α → γ

We need to apply this last formula to K. Again, we specialize K, this time by replacing α with (β → γ) and β with α:

: α → β → α: (β → γ) → α → (β → γ)

This is the same as the antecedent of the prior formula, so we detach the consequent:

: (β → γ) → (α → β) → α → γ

Switching the names of the variables α and γ gives us

: (β → α) → (γ → β) → γ → α

which was what we had to prove.

The normal proof of (β → α) → (γ → β) → γ → α in natural deduction seen as a λ-term

We give below a proof of (β → α) → (γ → β) → γ → α in natural deduction and show how it can be interpreted as the λ-expression λ "a". λ"b". λ "g".("a" ("b" "g")) of type (β → α) → (γ → β) → γ → α.

a:β → α, b:γ → β, g:γ Unicode|⊢ b : γ → β a:β → α, b:γ → β, g:γ Unicode|⊢ g : γ ——————————————————————————————————— ———————————————————————————————————————————————————————————————————— a:β → α, b:γ → β, g:γ Unicode|⊢ a : β → α a:β → α, b:γ → β, g:γ Unicode|⊢ b g : β ———————————————————————————————————————————————————————————————————————— a:β → α, b:γ → β Unicode|⊢ a (b g) : α ———————————————————————————————————— a:β → α, b:γ → β Unicode|⊢ λ g. a (b g) : α ———————————————————————————————————————— a:β → α Unicode|⊢ λ b. λ g. a (b g) : α ———————————————————————————————————— Unicode|⊢ λ a. λ b. λ g. a (b g) : α

External links

* [http://www.thenewsh.com/~newsham/formal/curryhoward/ The Curry-Howard Correspondence in Haskell]
* [http://www.haskell.org/sitewiki/images/1/14/TMR-Issue6.pdf The Monad Reader 6: Adventures in Classical-Land] : Curry-Howard in Haskell, Pierce's law.

References

Seminal references

*.

* Citation | last1=Curry | first1=Haskell B. | last2=Feys | first2=Robert | other1-last=Craig | other1-first=William | title=Combinatory Logic Vol. I | publisher=North-Holland | location=Amsterdam | year=1958, with 2 sections by William Craig, see paragraph 9E.

* De Bruijn, Nicolaas (1968), "Automath, a language for mathematics", Department of Mathematics, Eindhoven University of Technology, TH-report 68-WSK-05. Reprinted in revised form, with two pages commentary, in: "Automation and Reasoning, vol 2, Classical papers on computational logic 1967-1970", Springer Verlag, 1983, pp. 159-200.

* (original manuscript from 1969).

*

Extensions of the correspondence

*.

*.

*.

*. (Full version of the paper presented at "Logic Colloquium '90", Helsinki. Abstract in "JSL" 56(3):1139-1140, 1991.)

*.

*. (Full version of a paper presented at "Logic Colloquium '91", Uppsala. Abstract in "JSL" 58(2):753-754, 1993.)

*.

*. (Full version of a paper presented at "2nd WoLLIC'95", Recife. Abstract in "Journal of the Interest Group in Pure and Applied Logics" 4(2):330-332, 1996.)

Synthetic papers

*, the contribution of de Bruijn by himself.

*Citation | last1=Geuvers | first1=Herman | editor1-last=Groote | editor1-first=Philippe de | title=The Curry-Howard isomorphism | publisher=Academia-Bruyland | series=Cahiers du Centre de logique (Université catholique de Louvain) | isbn=978-2-87209-363-2 | volume=8 | chapter=The Calculus of Constructions and Higher Order Logic | pages=139–191, contains a synthetic introduction to the Curry-Howard correspondence.

*, contains a synthetic introduction to the Curry-Howard correspondence.

Books

*Citation | editor1-last=De Groote | editor1-first=Philippe | title=The Curry-Howard Isomorphism | publisher=Academia-Bruylant | series=Cahiers du Centre de Logique (Université catholique de Louvain) | isbn=978-2-87209-363-2 | year=1995 | volume=8, reproduces the seminal papers of Curry-Feys and Howard, a paper by de Bruijn and a few other papers.

*, notes on proof theory and type theory, that includes a presentation of the Curry-Howard correspondence, with a focus on the formulae-as-types correspondence

* Girard, Jean-Yves (1987-90). " [http://www.monad.me.uk/stable/Proofs+Types.html Proof and Types] ". Translated by and with appendices by Lafont, Yves and Taylor, Paul. Cambridge University Press (Cambridge Tracts in Theoretical Computer Science, 7), ISBN 0 521 37181 3, notes on proof theory with a presentation of the Curry-Howard correspondence.

* Thompson, Simon (1991). " [http://www.cs.kent.ac.uk/people/staff/sjt/TTFP/ Type Theory and Functional Programming] " Addison-Wesley. ISBN 0-201-41667-0.