7
$\begingroup$

I've been reading Lectures on the Curry-Howard Isomorphism and it talks about intuitionistic/constructive logic (IL) , combinatory logic (CL) and lambda calculus ($\lambda$c) before moving on to the Curry-Howard correspondence.

In fact, almost every text I've come across when trying to understand the "history and theory of functional programming", I've almost found these 3 topics interlinked. However, I'm unable to grasp how exactly are they connected?

From what I understand, IL predates CL which predates $\lambda$c.I believe $\lambda$c incorporates the principles of IL and CL in some form but I can't seem to put a finger on it. It seems this some form has something to do with Curry-Howard Isomorphism (CHI), but I'm unable to find a "non-abstract" example that relates everything together. Most texts have proofs with letters A, B, C and the like and it takes a while to figure out exactly what's going on.

So, how are they related? If its CHI, then what's a good example to hit the point home, intuitively speaking? Perhaps a constructive example for the proof of CHI could be helpful.

$\endgroup$
  • $\begingroup$ A nice bowtie on all these concepts is the Categorical Abstract Machine, that ties together concepts of category theory, $\lambda$c with explicit substitution, and combinatory logic. $\endgroup$ – cody Feb 18 '15 at 22:15
  • $\begingroup$ have always thought, it seems that maybe writing code & what was historically known as "constructive logic" may be linked.... working code must be "compilable" which seems to have strong parallels to "constructive"... $\endgroup$ – vzn Feb 19 '15 at 22:28
6
$\begingroup$

I don't understand exactly what you are looking for, I'll try to explain the Curry-Howard correspondence in a nutshell, you'll let me know if it helps.

The Curry-Howard correspondence (or isomorphism, if you wish) definitely links the three objects you mention: it actually tells that two of them, IL and $\lambda$c, are the same thing. The term is used today in a broad sense and often without referring to a specific technical statement, but it can be formulated precisely in at least two frameworks:

  1. Hilbert-style deduction for intuitionistic logic and SK combinators;
  2. Gentzen's natural deduction and the $\lambda$-calculus.

The first is actually the "original" correspondence, dating back to the late 50s when Curry observed that the types you would give to the SK combinators $$ \begin{align*} S &:(A\rightarrow B\rightarrow C)\rightarrow(A\rightarrow B)\rightarrow A\rightarrow C \\ K &:A\rightarrow B\rightarrow A \end{align*} $$ are exactly the axioms of implicational propositional intuitionistic logic in Hilbert-style deduction. Note that this latter has only modus ponens as a rule for building proofs; accordingly, terms in combinatory logic are built using only application.

That's it for the combinatory logic side. It took another decade before Howard fully formulated the correspondence in the second guise, which I think looks best:

  • on the logical side, you have $\mathbf{NJ}^{\Rightarrow,\land}$, Gentzen's natural deduction system for the negative fragment of propositional intuitionistic logic. You have propositional formulas defined by $A,B::=\alpha\mathrel{|} A\Rightarrow B\mathrel{|} A\land B$ (atom, implication and conjunction), proofs built from introduction and elimination rules for each connective, and you have proof normalization, which consists in 2 rewriting rules replacing what Prawitz calls "detours" (an introduction of a connective immediately followed by its elimination) with more explicit pieces of proof. This rewriting procedure closely corresponds to cut-elimination in sequent calculus, also introduced by Gentzen.
  • On the computational side, you have the simply-typed $\lambda$-calculus $\Lambda^{\rightarrow,\times}$, with types defined by $T,U::=o\mathrel{|}T\rightarrow U\mathrel{|} T\times U$ (base, function space and pairs), terms built from constructors ($\lambda$ for $\rightarrow$ and pairing for $\times$) and destructors (application for $\rightarrow$ and projections for $\times$), and $\beta$-reduction, which consists of 2 rewriting rules: the usual one and one for handling projections acting on a pair.

The Curry-Howard correspondence, which is the subject of the book you are reading, has three levels:

  1. formulas = types: just change the notation swapping $\alpha/o$, $\Rightarrow/\rightarrow$ and $\land/\times$;
  2. proofs = terms: more precisely, introduction rule=constructor, elimination rule=destructor;
  3. normalization = reduction: this is harder to write inline, but it's obvious once you write the rewriting rules of the two systems side by side. The correspondence is one-to-one, i.e., one step in $\mathbf{NJ}^{\Rightarrow,\land}$ corresponds to exactly one step in $\Lambda^{\rightarrow,\times}$ and vice versa.

At this level, I hesitate to call this an "isomorphism" because it is not entirely clear what structures are being preserved. Here's where category theory may be of help: if you formulate $\mathbf{NJ}^{\Rightarrow,\land}$ and $\Lambda^{\rightarrow,\times}$ as categories (without being too precise: formulas/types as objects and normal proofs/normal terms as morphisms), then they are isomorphic as Cartesian-closed categories (CCC). Indeed, as I defined them, they both are the free CCC on one object ($\alpha$ if you are a logician or $o$ if you are a computer scientist). So, there you go, you now have a third object into the picture and you get what Robert Harper calls the Holy Trinity (logic, programming languages and categories).

Actually, the above categorical view hides a bit what I think is the most important aspect of the Curry-Howard correspondence, which is normalization = reduction. Somewhat annoyingly, this is left out in current alternative terminologies for the correspondence: people say "proofs as programs" or "formulae as types", nobody says "cut-elimination as computation". To properly accommodate the third level, you'd have to climb a bit up on the higher-dimensional ladder and make $\mathbf{NJ}^{\Rightarrow,\land}$ and $\Lambda^{\rightarrow,\times}$ into 2-categories, or even more (things make sense up to dimension 3 at least).

If you're looking for concrete examples, the above framework isn't very rich but already gives you an idea. Take the second-order definition of natural number: $$\mathsf{Nat}(x):=\forall\alpha.(\forall y.\alpha(y)\Rightarrow\alpha(\mathsf{s}y))\Rightarrow\alpha(0)\Rightarrow\alpha(x)$$ ($x$ is an integer if it satisfies every property $\alpha$ which is true for $0$ and is true for $y+1$ as soon as it is true for $y$). Now, erase all first-order information and second-order quantification. You get $$(\alpha\Rightarrow\alpha)\Rightarrow\alpha\Rightarrow\alpha$$ Translated in types, this is $$\mathsf{N}:=(o\rightarrow o)\rightarrow o\rightarrow o.$$ Guess who are the normal forms of type $\mathsf N$? Exactly the (typed version of the) Church numerals. So every term $\mathsf{N}\rightarrow\mathsf{N}$ is a function on integers. If you keep the first and second order information, you get much more. For instance, the proof in second-order Peano arithmetic that addition is total, i.e., that $$\vdash\forall x.\forall y.\mathsf{Nat}(x)\land\mathsf{Nat}(y)\Rightarrow\mathsf{Nat}(x+y)$$ gives you a $\lambda$-term of type $\mathsf{N}\times\mathsf{N}\rightarrow\mathsf{N}$. Guess what functions it computes? Well, addition, of course (see Krivine's book "Lambda-calculus: Types and Models"). Cool, isn't it?

Another classical source to learn about Curry-Howard is Girard, Lafont and Taylor's book "Proofs and Types" (but you may already know that, it's in the bibliography of the book you are reading).

$\endgroup$
  • $\begingroup$ This a great explanation. Although I'm weak on the category theory side, but most of it does make sense! A question though: How/why did $\alpha$ change to $o$ when translating in types? $\endgroup$ – PhD Feb 19 '15 at 19:52
  • 1
    $\begingroup$ Well, the notation did not "change", different people use different notations, none stands out as standard. For simple types, you do see a lot $o$ being used as the basic type, I think it's just a distortion of the number $0$, which stands for the order in the type hierarchy: $1:=0\rightarrow 0$, $2=1\rightarrow 0$ and generally $n+1:=n\rightarrow 0$. This numerical notation is used often in the context of the simply-typed $\lambda$-calculus, especially in early papers. (This is just my personal interpretation, I don't know if it is historically accurate). $\endgroup$ – Damiano Mazza Feb 19 '15 at 21:44
  • 1
    $\begingroup$ By the way, you don't have to know category theory to appreciate the "isomorphism": informally, you can simply consider IC and $\lambda c$ as two freely generated structures endowed with a rewriting relation. The "iso" is a mapping $[\cdot]$ from formulas to types and proofs to terms preserving the whole structure: a proof $\pi$ of $A$ is sent to a term $[\pi]:[A]$, each construct being sent to the corresponding construct, and commuting with rewriting, i.e., $\pi$ rewrites to $\pi'$ iff $[\pi]$ rewrites to $[\pi']$. So IC and $\lambda c$ are the same structure, just written in different ways. $\endgroup$ – Damiano Mazza Feb 19 '15 at 21:54
  • $\begingroup$ Why last term computes addition only but not multiplication if NxN -> N holds also for mutiplication $\endgroup$ – Trismegistos Mar 6 '15 at 19:55
  • $\begingroup$ @Trismegistos: Because it comes from a proof of totality of addition. If it came from a proof of totality of multiplication, i.e. $\vdash\forall x.\forall y.\mathsf{Nat}(x)\land\mathsf{Nat}\rightarrow\mathsf{Nat}(x\cdot y)$, then it would compute multilication. This is true in general of any function whose recursive definition is provably total in second order Peano arithmetic. See the book by Krivine I meantion in the answer. $\endgroup$ – Damiano Mazza Mar 7 '15 at 7:23
4
$\begingroup$

Simple summary:

  • Typed $\lambda$-calculi are a way of presenting intuitionistic logics.

  • Combinatory logic is a presentation of logic (propositional, first-order, higher-order, intuitionistic or otherwise) without binders.

  • Typed $\lambda$-calculi can easily be translated into combinatory logic. Some combinatory logics can easily be translated to typed $\lambda$-calculi.

Not sure that answers your question.

$\endgroup$
  • $\begingroup$ It doesn't answer my question directly. BUT...it does provide interesting insight into their inter-relationships! +1 :) $\endgroup$ – PhD Feb 19 '15 at 0:32
3
$\begingroup$

Let me offer the simple, intuitive way that I think about this.

If you restrict yourself to closed lambda expressions, you have an equivalent of the combinatory logic. In fact with just a few simple closed lambda expressions you can generate all the others.

Closed lambda expressions give you the equivalent of implications where any conclusion/output you reach is either something you put in as an input, or something that you built by combining your inputs (in the general case, possibly recursively).

This means that you can't pull a result "out of thin air" the way you can with non-constructive logics / mathematics.

The only tricky bit left is how you handle negation / non-termination, which is a whole area by itself, but hopefully I've already given you the simple, but deep, correspondence between the three that you are asking for.

$\endgroup$

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.