The Curry-Howard Correspondence

Probably interesting if you like: philosophy, math, language, programming, or arguing.

Introduction

Logic studies the structure of reasoned argument.
Programming studies the structure of reasoned action.
Games present a forum for taking various paths of reasoned action in a form of reasoned argument (or competition).

Perhaps hearing logic, programming and games explained in this way makes it seem that they are almost the same thing. In fact, they are. Exactly. The Same. Thing.

These fields have all been studied extensively by theoreticians, to the point of reducing some of the systems' behavior to symbolic manipulation. Many, though certainly not all, proofs, programs and games can be encoded in simple languages designed by theoreticians for this purpose. These languages are "simple" to the extent that they are fully described by a few rules for how to arrange and move around symbols.

It is the point of the Curry-Howard Isomorphism that the languages describing certain large classes of proofs, programs and games are in fact one and the same language. These languages may differ historically in how people think about them and what notation to write them, but their RULES ARE EXACTLY THE SAME.

To be reader-friendly, below we will give examples in plain English, sometimes with a number or two. Rest assured that there are much more concrete ways (not English!) of encoding mathematical and programming expressions into symbols.

What corresponds to what?

Note: It is a relatively recent idea that the correspondence extends to game theory. For now, I will leave this part out of the explanation below, instead comparing only proofs and programs.

Mathematics deals with propositions -- claims, like theorems, lemmas, patently false statements, conjectures, you name it. Examples:

Your face has a green spot on it.
My cat is hairy. (Let's say, "has at least one hair.")
Every man on earth has an umbrella.
There exists a number bigger than a million.
Every even number greater than three is the sum of two prime numbers.

(I am aware that these examples are absurd and not all clear-cut yes-or-no. If you don't like those then ignore them.)

Some of these propositions have proofs; others do not. For some that don't, you may be able to prove the opposite of the statement. Again, examples:

Two scenarios: If you do have a green spot on your face, then you could point it out. That's proof. If you don't have a spot, then no proof exists.
Here's my cat. Here's a hair, on my cat. Done.
No proof exists. (I challenge you!) Here's a proof of the opposite: Here's my friend Bob. He doesn't have an umbrella.
How 'bout this one: One million and twenty.
Nobody yet knows whether this last one is true or false! No one has yet found a proof of the opposite, though. This is called "Goldbach's conjecture."

What exactly is going on here? For each one of the proofs above, we proved the statement (or its negative) by giving an example.

Type	Example
Green spots on your face	This green spot on your face
Hairs on my cat	This hair on my cat
Men on Earth that DON'T have an umbrella	My friend Bob
Numbers bigger than a million	A million and twenty

(I left out Goldbach's Conjecture since we don't have a proof of it or its opposite. :-( )

Every one of these "types" or "sets" of things corresponds to one of the propositions above. Every one of these examples corresponds to one of the proofs above. And notice how similar they look, too!

This is the Curry-Howard Correspondence: Propositions are types and a proof of a proposition corresponds to an example of the associated type of objects. A proposition has a proof (is "true," in a certain sense) if and only if the corresponding type has an example. If there are no examples, there are no proofs. Every example is a proof. Every proof is an example.

The technical part

Those examples above looked kind of like proofs, even though they were about my cat and things like that, instead of about mathematical objects. They certainly weren't written in any special language, but I assure you, there is a way to encode many mathematical statements (the above weren't quite mathematical) into a formal language of symbols, though some complicated ones no one knows how to do.

Where's the programming side of this? We gave "examples" and claimed they were like proofs, but then we said that proofs were like programs. This comes down to the fact that in some programming languages, programs have "datatypes," or just "types" for short. These types basically say what you're allowed to do to these programs, with them, etc. With more advanced type systems, you can even specify in great detail what a program does -- what goes in, and how what comes out relates to what goes in.

The "lambda calculus" (nothing to do with the derivative and integral stuff you might have learned in school) is one of the simplest programming languages. It was invented by Alonzo Church in 1936 (here) in response to a challenge to find a formal system with "complex" behavior. (This is a sort of euphemism for something much more specific. We will not deal with it here.) There was an even more general question of making a language for describing "processes" and "procedures," what we now call programs, and the lambda calculus answered it nobly. Expressions in the lambda calculus represent procedures in their purest form: rules for what goes in and how it gets transformed to output. These transformation rules can be fed various inputs, including other rules. (Let's just call these "rules" functions, because functions also take inputs and change them according to some scheme.) The type of a lambda expression just specifies what sorts of expressions you're allowed to feed into it (if it's a function), e.g. integers, strings, frogs, cheese, and what it can be fed into, e.g. only an animal that eats cheese-eating animals! I don't have time to make a much clearer explanation right now, but I hope I'll finish later. In the meantime, see Wikipedia's entry on the lambda calculus if you're interested. Also, read the definition of "type theory" at the bottom of my DIMACS home page.

And if I can't give an example?

Note that you can prove something without giving an example -- Let me prove that with an example. (That was a joke.)

Suppose you go to work (or class), and there's an empty cup on a table, and you know you didn't leave it there. You can still say with pretty good confidence that someone left the cup there. You can say that and be sure of it without having any clue who that person was.

This is called a non-constructive proof (because you don't construct an example), and it shows up a lot in mathematics. For a famous example, see The Banach-Tarski Paradox . (Beware, what you read there is not supposed to work in the real world but only in certain mathematical models that permit more than we can actually do with a knife and an orange.)

Non-constructive proofs include proof by contradiction: Suppose no one left the cup on the table, then the cup must have ended up on the table somehow, then bladi-bladi-bla, then... your pants are on fire... is that a flying giraffe?... okay, this is absurd. Someone must have left the cup on the table.

What does this correspond to in a program or procedure? Say we're running along, doing our computation, making assumptions, proving our assumptions, etc. Then we realize that we've proved nonsense, absurdity. At this point, we throw up our arms and say our assumptions must have been ridiculous; the opposite must be true. We interrupt whatever is left of this computation and just go back to the point that we started with the bad assumption. Now we know that the opposite is true and since we've proved it, we can use that in further computation if we wish.

This is known as the correspondence between proof by contradiction (in "classical" mathematical logic) and control operators (in programming languages, e.g. throwing exceptions, as in Java, or jumping with continuations, as in Lisp). This is a relatively recent discovery (1990). The technical part of this is actually pretty tricky, so I'll leave you with these intuitive examples for now. You can read more about proof by contradiction and the Curry-Howard correspondence in the references below (esp. Chapter 6 of Lectures on the Curry-Howard Isomorphism).

How much further does it go?

The Curry-Howard correspondence extends to more and more complicated logics and functional programming languages, though still, there are lots of unsolved problems about what things correspond to in complicated logics and programming languages. There is hot work being done on making analogous systems in games or graphs, thereby extending the Curry-Howard isomorphism to new realms.

Knowledge of the Curry-Howard correspondence has enabled the development of programming languages in which you can actually type up and then automatically check mathematical proofs -- the computer will tell you if your proof has any errors. Many mathematical results have been formalized in this way, but it is still a pitiful small fraction of the mathematical literature. (See references for the language Coq below.) Encoding these theorems and proofs in these languages has helped in understanding the structure of proofs and reasoned arguments.

Stuff to Read

The Wikipedia article on the Curry-Howard correspondence.

The Wikipedia article on the lambda calculus

My homepage at DIMACS.

A Wikibooks treatment.

Putting Curry-Howard to Work at Lambda the Ultimate.

Lectures on the Curry-Howard Isomorphism (See description below.)

This last one is so awesome that it deserves a section of its own.

Here is a summary: The Curry-Howard isomorphism is a correspondence between systems of mathematical logic (proof systems) and programming languages (lambda calculi). The correspondence also extends to a third realm, that of two-player games (prover-skeptic dialogues). The book's discussion of the correspondence illuminates both programming and mathematics (and even game theory) to the reader by explaining each on its own and then in relation to the others. Ideally, there are no prerequisites, since most things are explained from the beginning. However, a strong interest and preferably prior knowledge in either mathematics (esp. logic) or (functional) programming is very helpful, since a lot of the book is presented in a formal, mathematical way, and is easier to understand if the reader has an intuition based on experience in programming or in writing mathematical or philosophical arguments.

This book is available, currently, used for about $100 at Amazon.
If you're cheap, also see (slightly less organized) free draft versions at 1, 2, or 3.
I like the book better than these notes, but since the book is priced at a hundred dollars, I'd go for one of these if it's not in your library.
There are also previews on Google Books.

If you would like me to change something about this page, or write more, or write less, or if you liked it, or if you didn't, please let me know. My address is my first name (avi) dot my last name (rashin) on gmail.

Home at DIMACS Home at Rutgers