10
$\begingroup$

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.

Improve this question
$\endgroup$

2 Answers 2

Reset to default
14
$\begingroup$

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.

Improve this answer
$\endgroup$
2
  • 3
    $\begingroup$ 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. $\endgroup$
    – Dan Doel
    Commented Nov 10, 2021 at 19:15
  • 3
    $\begingroup$ @DanDoel it turns out "a calculus of first-class substitutions" is a really useful idea! $\endgroup$
    – cody
    Commented Nov 12, 2021 at 19:14
7
$\begingroup$

Someone wanted a deep category-theoretic insight?

A Heyting algebra is a cartesian-closed category.

Improve this answer
$\endgroup$
6
  • 5
    $\begingroup$ I was guessing you would say “a topology is a Heyting algebra!” $\endgroup$
    – Neel Krishnaswami
    Commented Nov 12, 2021 at 5:50
  • 2
    $\begingroup$ What has topology got to do with $\lambda$-calculus? $\endgroup$
    – Andrej Bauer
    Commented Nov 13, 2021 at 19:59
  • 1
    $\begingroup$ (a) the topology via logic view, where termination/nontermination gets modelled by the Sierpinksi space, and computable functions are modelled by continuous ones, $\endgroup$
    – Neel Krishnaswami
    Commented Nov 15, 2021 at 9:51
  • 1
    $\begingroup$ (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. $\endgroup$
    – Neel Krishnaswami
    Commented Nov 15, 2021 at 9:55
  • 1
    $\begingroup$ 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? $\endgroup$
    – Andrej Bauer
    Commented Nov 15, 2021 at 10:47

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.