Curry-Howard correspondence

I read that the Curry-Howard correspondence introduces an isomorphism between typed functions and logical statements. For example, supposedly the function

$$\begin{array}{l} I : \forall a. a \to a\\ I = \lambda x. x \end{array}$$

can be interpreted as:

$$p \implies p \text{ for any proposition } p$$

Is that correct? How might I interpret a function $K : \forall ab. a \to (b \to a)$? What about $\text{succ} : \mathbb{N} \to \mathbb{N}$, where $\text{succ} = \lambda x. x + 1$?

If the scope of this question is too large, can someone recommend an introductory book that would cover this? A proof of the isomorphism would probably be enlightening, too: can someone point me to one?

-

Have a look at Girard, Lafont and Taylor, Proofs and Types. It's available online in its entirety.

We can state the Curry–Howard correspondence in general terms as a correspondence between proof systems and type theories. Two ways of stating it as that proofs are programs and propositions are types. Your question looks like it's focused on the connection which Howard drew between natural deduction and the simply-typed $\lambda$-calculus.

You ask how to interpret a function $K : \forall{a, b} . a \rightarrow (b \rightarrow a)$, which is not precisely the right question to ask, because it misses the intensional aspect of the correspondence. Let $t$ be a term of type $\forall{a, b} . a \rightarrow (b \rightarrow a)$ whose extension is the function $K$. (In general there will be many such $t$ for any given $K$.) What does $t$ correspond to, then? A proof of the proposition which its type corresponds to: the proposition that for arbitrary propositions $a$ and $b$, $a \rightarrow (b \rightarrow a)$.

What might $t$ look like? We can figure this out to some extent because of its type. Start with $r : b \rightarrow a$. Let $v : a$ and $x : b$. Then let $r := \lambda x. v$. Then $t := \lambda y. (\lambda x. v)$.

Of course this isn't terribly informative: to figure out anything substantial we'd need to know what $v$ is. There are lots of things it might be: here's one which fits. Let $v := y$. Then $t := \lambda y. (\lambda x. y)$. In other words, provide terms $u : a$ and $s: b$ (which, remember, are proofs of $a$ and $b$ respectively), so then $(t[u / y])[s / x]$ reduces to just $u$, which is a proof of $b$.

-
Thanks! I have a couple questions about your explanation: (1) When you refer to the extension of $t$ in paragraph 2, are you talking about this? I.e., extension $\approx\,$ black box and intension $\approx\,$ white box? (2) In paragraph 3, did you mean $r : b \to a$, or am I misunderstanding something? –  Snowball Jul 4 '12 at 22:27
(1) Yes. Two different terms may define the same function. For example we can define the successor function as $\lambda x. x + 1$ or as $\lambda x. x + 2 - 1$. Extensionally they are the same: they define the function $\left\{ \langle x, x + 1 \rangle : x \in \mathbb{N} \right\}$. But intensionally they are different. The phrases "Everyone in this room" and "Everyone in this room wearing a hat" appear to pick out two different properties. But suppose everyone in the room is wearing a hat. Then the two properties are co-extensive, despite going by different descriptions. –  Benedict Eastaugh Jul 5 '12 at 5:08
(2) is indeed a typo. I've now fixed it, thanks for pointing it out. –  Benedict Eastaugh Jul 5 '12 at 5:08
Thank you! I'll read the book you mentioned at the top. That was an exceptional explanation, by the way. –  Snowball Jul 5 '12 at 5:24

The short version of the Curry-Howard correspondence is: to interpret a type as a proposition, interpret the function type $a\to b$ as "$a$ implies $b$". Interpret the product type $a\times b$ as "Both $a$ and $b$". Interpret the disjoint union type $a \sqcup b$ as "Either $a$ or $b$ (or both)".

Then for example the type of the $K$ combinator, $a\to(b\to a)$, is interpreted as the proposition that if we know $a$, then if we know $b$ we can conclude $a$. Or the type of the program which gets a pair $(a,b)$ and returns $b$ is $a\times b\to b$, and this is the theorem that says that if you can prove $a$ and $b$, then you have a proof of $b$, usually written $a\land b\to b$.

(In the Haskell language, $a\times b$ is notated (a,b) and $a\sqcup b$ is notated Either a b.)

The successor function is a bit silly, because its type is a trivial theorem. The type $\Bbb N$ is known to be inhabited, because it contains constants like 0. Such types correspond to propositions that are known to be true. For example, there is a program, written 0, with type $\Bbb N$, and this is indeed a theorem. So the successor function's type, ${\Bbb N}\to{\Bbb N}$, just says that $\Bbb N$ implies $\Bbb N$, which is not very interesting. Perhaps slightly more interesting is the theorem $a\to \Bbb N$, which corresponds to the program $\lambda a. 13$.

There is more to the correspondence than that types are theorems of logic. More important is that a program with a certain type corresponds to a proof of the corresponding theorem. Evaluation of the program corresponds to elimination of the "cut" rule from the proof. Purely functional programs correspond to theorems of intuitionistic logic, but imperative programs correspond to theorems of classical logic, which is stronger. Double-negation corresponds to exception handling. Glivenko's theorem, which says that any theorem of classical logic has an intuitionistic analogue, corresponds to the implementation of an imperative program in a functional language in continuation-passing style.

I recommend that you read Morten Heine Sørensen and Paweł Urzyczyn's Lectures on the Curry-Howard Isomorphism for complete details.

Also potentially interesting: this answer constructs a program with type $\lnot\lnot(P\lor\lnot P)$.

-
The intuitionistic/classical distinction does not correspond to pure/imperative programming. If we introduce imperative features with something like ML's ref type, removing all of the ref and ! operators and replacing every assignment with () will still yield a well-typed program. So being imperative does not increase the number of inhabited (ref-less) types. One programming feature that does produce classical logic, however, is a call/cc primitive (whose type $\forall \alpha.\forall \beta.((\alpha\to\beta)\to\alpha)\to\alpha$ corresponds to Peirce's law in logic). –  Henning Makholm Jul 4 '12 at 17:20
@HenningMakholm Thanks for this clarification. I was thinking of control flow primitives such as call/cc and threw-catch, not of references, and I made my statement too broad. –  MJD Jul 4 '12 at 20:48