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.
[1] 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)[2] and Stephen Kleene (see Realizability).
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.
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.
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,[9] and is itself related to modal logic by a natural extension of the Curry–Howard isomorphism[ext 1]).
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.
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.
A term T (also annotated with its type) will depend on these variables [Γ ⊢ T:δ] when: The generation rules defined here are given in the right-column below.
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 After Curry emphasized the syntactic correspondence between intuitionistic Hilbert-style deduction and typed 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 (the use of sequents is standard in discussions of the Curry–Howard isomorphism as it allows the deduction rules to be stated more cleanly) with implicit weakening and the right-hand side shows the typing rules of lambda calculus.
Howard showed that the correspondence extends to other connectives of the logic and other constructions of simply typed lambda calculus.
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.
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.
In the case of classical natural deduction, there exists a proofs-as-programs correspondence with the typed programs of Parigot's λμ-calculus.
Gödel's dialectica interpretation realizes (an extension of) intuitionistic arithmetic with computable functions.
Joachim Lambek showed in the early 1970s that the proofs of intuitionistic propositional logic and the combinators of typed combinatory logic share a common equational theory, the theory of cartesian closed categories.
to refer to the relationships between intuitionistic logic, typed lambda calculus and cartesian closed categories.
To clarify this distinction, the underlying syntactic structure of cartesian closed categories is rephrased below.
Recently, the isomorphism has been proposed as a way to define search space partition in genetic programming.
[13] The method indexes sets of genotypes (the program trees evolved by the GP system) by their Curry–Howard isomorphic proof (referred to as a species).
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.
Moreover, these can be shown to correspond to cobordisms,[15] which play a vital role in string theory.