Editing Curry–Howard correspondence (section)

===Intuitionistic Natural deduction and typed lambda calculus===
After [[Haskell Curry|Curry]] emphasized the syntactic correspondence between intuitionistic [[Hilbert-style deduction system|Hilbert-style deduction]] and typed [[combinatory logic]], [[William Alvin Howard|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 [[sequent]]s (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]]. In the left-hand side, Γ, Γ<sub>1</sub> and Γ<sub>2</sub> denote ordered sequences of formulas while in the right-hand side, they denote sequences of named (i.e., typed) formulas with all names different.

{| class="wikitable" style="text-align:center; margin: 0 auto;" cellpadding="10"
! width="200px"| Intuitionistic implicational natural deduction
! width="200px"| Lambda calculus type assignment rules 
|- style="height:70px" valign=bottom
| <math>\frac{}{\Gamma_1, \alpha, \Gamma_2 \vdash \alpha} \text{Ax}</math>
| <math>\frac{}{\Gamma_1, x:\alpha, \Gamma_2 \vdash x:\alpha}</math>
|- style="height:70px" valign=bottom
| <math>\frac{\Gamma, \alpha \vdash \beta}{\Gamma \vdash \alpha \rightarrow \beta} \rightarrow I</math>
| <math>\frac{\Gamma, x:\alpha \vdash t:\beta}{\Gamma \vdash (\lambda x\!:\!\alpha.~t) : \alpha \rightarrow \beta}</math>
|- style="height:70px" valign=bottom
| <math>\frac{\Gamma \vdash \alpha \rightarrow \beta \qquad \Gamma \vdash \alpha}{\Gamma \vdash \beta} \rightarrow E</math>
| <math>\frac{\Gamma \vdash t:\alpha \rightarrow \beta \qquad \Gamma \vdash u:\alpha}{\Gamma \vdash t\;u:\beta} </math>
|}

To paraphrase the correspondence, proving Γ ⊢ ''α'' means having a program that, given values with the types listed in Γ, manufactures an object of type ''α''. An axiom/hypothesis corresponds to the introduction of a new variable with a new, unconstrained type, the {{math|→&nbsp;''I''}} rule corresponds to function abstraction and the {{math|→&nbsp;''E''}} 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 {{math|''α'' → ''α'' → ''α''}} would not be distinguished in the correspondence. Examples are given [[#Examples|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 [[Dag Prawitz|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.

{| class="wikitable" style="margin: 0 auto; text-align: center;"
! style="width:200px" | Logic side
! style="width:200px" | Programming side
|- 
| axiom/hypothesis || variable
|- 
| introduction rule || constructor
|- 
| elimination rule || destructor
|- 
| normal deduction || normal form
|- 
| normalisation of deductions || [[Normalization property (lambda-calculus)|weak normalisation]]
|- 
| provability  || [[type inhabitation problem]]
|-
| intuitionistic tautology || universally inhabited type
|}

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|System F<sub>ω</sub>]]
* inductive types as [[algebraic data type]]
* necessity <math>\Box</math> in [[modal logic]] and staged computation<ref name=DaviesPfenningStaged group=ext>{{Citation|doi=10.1145/382780.382785|first1=Rowan|last1=Davies|first2=Frank|last2=Pfenning|year=2001|title=A Modal Analysis of Staged Computation|journal=Journal of the ACM |volume=48|issue=3|pages=555–604|url=https://www.cs.cmu.edu/~fp/papers/jacm00.pdf|citeseerx=10.1.1.3.5442|s2cid=52148006}}</ref>
* possibility <math>\Diamond</math> in [[modal logic]] and monadic types for effects<ref name=PfenningDaviesJudgmental group=ext/>
* The {{mvar|λ<sub>I</sub>}} calculus (where abstraction is restricted to ''λx''.''E'' where ''x'' has at least one free occurrence in ''E)'' and '''CL'''<sub>I</sub> calculus correspond to [[relevant logic]].<ref>{{Citation|first1=Morten|last1=Sørenson|first2=Paweł|last2=Urzyczyn|title=Lectures on the Curry-Howard Isomorphism|citeseerx = 10.1.1.17.7385 |year=1998}}</ref>
* The local truth (∇) modality in [[Grothendieck topology]] or the equivalent "lax" modality (◯)<!-- should be a large circle --> of Benton, Bierman, and de Paiva (1998) correspond to CL-logic describing "computation types".<ref>{{Citation|last=Goldblatt|title=Mathematical Modal Logic: A Model of its Evolution|chapter=7.6 Grothendieck Topology as Intuitionistic Modality|pages=76–81|chapter-url=http://homepages.mcs.vuw.ac.nz/~rob/papers/modalhist.pdf}}. The "lax" modality referred to is from {{Citation|last1=Benton|last2=Bierman|last3=de Paiva|title=Computational types from a logical perspective|journal=Journal of Functional Programming|volume=8|issue=2|pages=177–193|year=1998|doi=10.1017/s0956796898002998|citeseerx=10.1.1.258.6004|s2cid=6149614 }}</ref>