The Curry-Howard correspondence observes that logics correspond to type systems (in the sense of having the "same" inference rules). Is there some deeper explanation/justification for this? E.g. "in category theory, 'interesting' logics and type systems are both [something] and therefore isomorphisms exist between them".


I like to think of the Curry-Howard correspondence as a natural outcome of the so-called Brouwer-Heyting-Kolmogorov (BHK) interpretation of logic. The central idea of BHK is that meaning of a mathematical statement is to be specified not by telling under what circumstances the statement is true but rather by telling what one must do in order to prove the statement. As a result, the meanings of logical operations (connectives and quantifiers) are given, not by describing the truth values of compound statements in terms of the truth values of the constituents (as in Tarski's classical definition of truth), but rather by describing the possible proofs of compound statements in terms of proofs of their constituents.

For example, "and" would be explained by saying that a proof of $A\land B$ is a pair consisting of a proof of $A$ and a proof of $B$. Similarly, implication would be explained by saying that a proof of $A\to B$ is a procedure for converting any proof of $A$ into a proof of $B$.

Writing those explanations in terms of "Pfs$(A)$", meaning the set of proofs of $A$, I'd get that Pfs$(A\land B)$ is the cartesian product of Pfs$(A)$ and Pfs$(B)$, while Pfs$(A\to B)$ is the set of functions from Pfs$(A)$ to Pfs$(B)$. So this BHK viewpoint leads to at least a rudimentary form of the Curry-Howard correspondence. In particular, it should not be surprising that the logical rules governing $\land$ and $\to$ match the set-theoretic properties of cartesian products and sets of functions. (Technicality: Here "logical rules" should be understood as rules of intuitionistic logic, because that's the logic naturally supported by the BHK interpretation --- not surprising in view of the philosophy of B and H.)

  • $\begingroup$ I would describe BHK as more like saying what "proofs" look like. Except there's nothing about this that suggests the "proofs" are formal proofs, so I usually say something like "evidence". Arguably, BHK is just (partially) defining a (different) notion of semantics. It can be tweaked to be instructions on how to interpret formulas into an arbitrary bicartesian closed category (for the propositional fragment, though quantifiers can also be handled). Even when we choose $\mathbf{Set}$, the constructiveness arguably comes from choosing $+$ and $0$ as the interpretation of $\lor$ and $\bot$. $\endgroup$ – Derek Elkins left SE Jun 10 '19 at 17:44
  • $\begingroup$ In that vein, it's probably worth noting that if $A\cong 0^{0^A}$ in a bicartesian closed category, i.e. if the interpretation of double negation elimination holds, then you can prove that there is at most one arrow between any two objects in the category, i.e. the category collapses to a preordered set. $\endgroup$ – Derek Elkins left SE Jun 10 '19 at 17:55
  • $\begingroup$ @DerekElkins I think Brouwer intensely disliked the notion of formal proofs, so his notion of proof would have been like what you call evidence, except that it needs to be completely convincing evidence. Heyting, on the other hand, set up formal systems for intuitionistic reasoning, but I don't think he or Kolmogorov would have taken "proof" as described in the BHK interpretation to mean formal proof. $\endgroup$ – Andreas Blass Jun 10 '19 at 19:42
  • 1
    $\begingroup$ Well, the usual correspondence builds on the correspondence for intuitionistic logic, by observing that the type of call/cc exactly corresponds to Peirce's law. The "proof" of excluded middle from Peirce's law, if you follow it across the correspondence, then boils down to: the "function" to prove $P \vee \lnot P$ always guesses "false" with a proof of $\lnot P$ whose implementation is a synthetic function $P \to \bot$ such that if it's ever called with a proof of $P$, it rewinds execution to where the EM function was called and returns "true" with that proof of $P$. $\endgroup$ – Daniel Schepler Jun 11 '19 at 22:23
  • 1
    $\begingroup$ @rlms The (categorical form of the BHK) interpretation doesn't work for the reason I gave earlier. We can use a different type of category for the semantics called a control category and in particular a category of continuations. Unsurprisingly, the difference is in the treatment of $\bot$ and $\lor$. Instead of interpreting these using initial objects and coproducts, we use a weaker premonoidal structure. Critically, the replacement for coproducts is not bifunctorial. (If it is, the category collapses to a Boolean algebra as before.) $\endgroup$ – Derek Elkins left SE Jun 12 '19 at 0:54

The most obvious answer to questions like this is that people came up with roughly the same idea many times. This happens a lot, but people like to make a big deal about it when it comes to math and pretend it has some kind of mystical significance. Even in math you get e.g. Newton and Leibniz both inventing calculus around the same time, probably because there were other ideas available at that time that made it feasible to do so.

However, in the case of Curry-Howard, it's maybe even less surprising. Most of the examples you see have some relation to lambda calculus. However, Church seems to have invented lambda calculus for the purpose of formalizing logic. I've even seen it suggested that he initially thought of lambda terms $λx. e$ as actually just abbreviated notation for an equivalent construction in combinatory logic (which is like logic based on SK combinators, and already existed at the time). Lambda terms standing on their own may have been later.

Anyhow, his initial try yielded an inconsistent logic, so types were added to rule that out. If you look at this stuff, it's surprisingly similar to Martin-löf's logical framework, just much earlier. But also around that time, Church and Turing realized that you could also use lambda-definability as a criterion for whether functions are computable. I don't know why the typed version got picked up in this branch of things, but one possible reason is that it rules out weird looping terms. That is the source of logical paradoxes, though, so it would be adding types for similar reasons.

So, in some sense, it's not even a Newton-Leibniz case for Curry-Howard. It's Church coming up with one tool that was good for two (seemingly) different things, and then variations made by independent lines of development ended up being essentially the same as one another. If you forget they were related in the first place, it might seem mystical that they relate to one another, but maybe it isn't that surprising.

(I found out most of the Church stuff by skimming his early papers linked on Wikipedia, by the way. They're not easy to read, since the notation for things is rather different than what is used now, but they're interesting to look at.)


To make a long answer short, the part of the history I am best aware of is that Curry stumbled onto it when devising a system of types for combinatory logic and found - by a most remarkable coincidence - that the types of the basic combinators just so happen to have the same form as the basic axioms of implicational logic; that the rule for forming types for function application in combinatory logic happen to match the modus ponens rule; and that the process of abstracting out a free variable to find the combinator that gives you a lambda expression happens to match the rule for discharging an hypothesis in a proof conditioned on hypotheses.

The deeper this correspondence was delved into, the more that was found to line up; e.g. if combinatory logic is extended to allow for tuples, then one can add conjunctions to its scope.

The best explanation that I can think of is that in discovering that things lined up this way, it's not so much that anyone discovered that one can be accounted for or explained in terms of the other or vice versa, but that one just happened onto two instances of an elaborate structure that later came to be recognized to occur elsewhere in other - often unrelated - contexts, and that this was the structure that eventually came to be known and formalized in Category Theory as various types of categories: Cartesian closed, bi-Cartesian closed, etc.

Good account is provided for the "and" and "if-then" connectives and of the "true" and even "false" predicate constants. To some degree, the "all" quantifier can also be treated within this framework.

But there is always such a thing as pushing an analogy too far; and I think that those who are imbued with the notion that one can be explained or accounted for in terms of the other are guilty of doing this. The weak spot is - and has always been - the dual operators, "or" (the dual of "all"), "unless" (the dual of "if-then"), "some" (the dual of "all"), and the correspondence starts to become a bit forced and awkward ... or non-existent (i.e. there's no Curry-Howard rendition of "unless" that I'm aware of).

Within Category theory, propositions correspond to objects, while the inference relation between propositions corresponds to the arrows of morphisms, with the morphisms themselves being the proofs that bear witness to the inference. This is not just a "correspondence": they are the elements for the structure of an actual category, for logic; since we always have reflexivity and transitivity amongst our basic rules for inferrability (i.e. the relation is a pre-order for predicates) and the ability to chain up proofs made of two or more inferences in sequence.

Inferences are (1,1) sequents: sequents that have one statement on each side. A general sequent $A₀,A₁,⋯ ⊢ B₀,B₁,⋯$ may permit 0, 1, 2 or any finite number of statements on each side. It is always reducible, equivalently, to (1,1) form as $A₀∧A₁∧⋯ ⊢ B₀∨B₁∨⋯$, where $∧$ is the "and" connective, $∨$ is the "or" connective and $⊢$ is the "infers" relation.

When trying to draw analogy to type theory, what we're actually trying to do is extend the correspondence to also be able to account for "assertions": or (0,1) sequents $⊢ B$. There is nothing in category theory that directly corresponds to this, but we'd like to think of a proof that witnesses this sequent $b: ⊢ B$ as somehow being a "member" of a "type" which $B$ corresponds to. Types are then populated by members, in some sense.

I'm always a fan of symmetry, so I feel uneasy when I see this treatment, while a similar treatment remains absent - for the dual notion of a "query" or counter-factual "is it so?" question: the (1,0) sequent $a: A ⊢$. A language, like Prolog, actually has something that corresponds to both, the notations being respectively $b.$ and $?- a$.

The process of starting with a purely category-theoretic starting point and then trying to populate the objects so that they can be treated as types is what we now call creating an "internal language". There is no dual notion of "co-language" that I am aware of.

So, when it comes time to try and relate types and propositions, there is an asymmetry in the Curry-Howard correspondence reflected by the absence of full duality. This speaks more to the "the two analogues are the first two instances of a general as-yet-discovered phenomenon" view that I just relayed, rather than to the more prevalent "one can be explained by or account for in terms of the other" view.

So, I think it just comes down to this: that the correspondence was the discovery of the first two examples of a category-theoretic structure and that it is actually category theory that lies beneath everything.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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