A Theory Independent Curry-De Bruijn-Howard Correspondence

Abstract

Brouwer, Heyting, and Kolmogorov have proposed to define constructive proofs as algorithms, for instance, a proof of A ⇒B as an algorithm taking proofs of A as input and returning proofs of B as output. Curry, De Bruijn, and Howard have developed this idea further. First, they have proposed to express these algorithms in the lambda-calculus, writing for instance λf ^{A ⇒A ⇒B} λx ^A (f x x) for the proof of the proposition (A ⇒A ⇒B) ⇒A ⇒B taking a proof f of A ⇒A ⇒B and a proof x of A as input and returning the proof of B obtained by applying f to x twice. Then, they have remarked that, as proofs of A ⇒B map proofs of A to proofs of B, their type $\mbox{\em proof}(A \Rightarrow B)$ is $\mbox{\em proof}(A) \rightarrow \mbox{\em proof}(B)$. Thus the function proof mapping propositions to the type of their proofs is a morphism transforming the operation ⇒ into the operation →. In the same way, this morphism transforms cut-reduction in proofs into beta-reduction in lambda-terms.