# Why is the Curry-Howard isomorphism?

The Curry-Howard isomorphism is the correspondence between type systems (like for the simply typed lambda calculus) and proof systems (like natural deduction). More precisely, types resemble propositions, terms resemble proofs, reduction resembles cut elimination etc.

The isomorphism becomes obvious because there is a 1-to-1 correspondence between the inference rules of Curry typing and the inference rules of predicate logic ND systems, for example.

However, what is not obvious (to me) is why this happens. Is there a deeper reason that proofs and typing are just two facets of the same system?

Merely noting that this is possible because the basic definitions are isomorphic is not really satisfactory, because this just shifts the question towards asking why the definitions of these systems end up isomorphic.

I suspect someone is going to come along with a deep category-theoretic reason for the connection, but in the meantime, here is my insight.

Both logic and programming with functions are built around the notion of hypotheticals. The proposition $$A \to B$$ says "If I had an $$A$$, I could prove $$B$$." A function of type $$A \to B$$ says "If I had a value of type $$A$$, I could compute a value of type $$B$$. So these logics/languages are really systems for hypothetical reasoning, which we need for both programming and proving.

Whether we say "prove" or "compute" really just depends on whether we only care about the existence of an $$B$$, or whether we care about which $$B$$ we get. But this isn't a change in the system, it's just a change in its use.

In some sense, the Curry-Howard isomorphism isn't an isomorphism at all, and some people prefer the word "correspondence". But depending on your view, it's not "two things that are isomorphic" but "two different views of the same thing." You don't have to view it as there being two systems, logic and programming, that are separate but connected.

Instead, I view it as "here is a single system for reasoning about abstraction and hypotheticals, and it turns out we can view this system as either a logic or as a programming language." It's not a connection between two things, but two uses of a single thing.

• I think it's also worth noting that Church's earliest papers on lambda calculus were attempting to create a formal system for logic, similar to a modern "logical framework." Lambda terms for computation was (publication-wise at least) slightly later. Nov 10 '21 at 19:15
• @DanDoel it turns out "a calculus of first-class substitutions" is a really useful idea!
– cody
Nov 12 '21 at 19:14

Someone wanted a deep category-theoretic insight?

A Heyting algebra is a cartesian-closed category.

• I was guessing you would say “a topology is a Heyting algebra!” Nov 12 '21 at 5:50
• What has topology got to do with $\lambda$-calculus? Nov 13 '21 at 19:59
• (a) the topology via logic view, where termination/nontermination gets modelled by the Sierpinksi space, and computable functions are modelled by continuous ones, Nov 15 '21 at 9:51
• (b) the ability to do finite observations of data structures corresponds to be able to answer questions in geometric logic about them. E.g, see Balat et al, POPL 2004, Extensional normalisation and type-directed partial evaluation for typed lambda calculus with sums, which formed a Grothendieck topology using the branches of pattern matches. Nov 15 '21 at 9:55
• Ok, but how does this explain why the $\lambda$-calculus and propositional calculus are related? For instance, what do question of termination have to do with anything when we explain the Curry-Howard correspondence? Nov 15 '21 at 10:47