Finally, Modeling Lambda Calculus: Programs are Proofs!

Now that we've worked through intuitionistic logic and it's model; and we've worked from the untyped lambda calculus to the simply typed lambda calculus; we're finally ready for the model of lambda calculus. And this is where it gets really fun.

Think about the types in the simple typed language calculus. Anything which can be formed from the following grammar is a lambda calculus type:

type ::= primitive | function | ( type )
primitive ::= A | B | C | D | ...
function ::= type -> type

The catch with that grammar is that you can create type expressions which, while they are valid type definitions, you can't write a single, complete, closed expression which will actually have that type. (A closed expression is one with no free variables.) When there is an expression that has a type, we say that the expression inhabits the type; and that the type is an inhabited type. If there is no expression that can inhabit a type, we say it's uninhabitable.

So what's the difference between inhabitable type, and an uninhabitable type?

The answer comes from something called the Curry-Howard isomorphism. For a typed lambda calculus, there is a corresponding intuitionistic logic; a type expression is inhabitable if and only if the type is a theorem in the corresponding logic.

Look at the type "A -> A". Now, instead of seeing "->" as the function type constructor, try looking at it as logical implication. "A implies A" is clearly a theorem of intuitionistic logic. So the type "A -> A" is inhabitable.

Now, look at "A -> B". That's not a theorem, unless there's some other context that proves it. As a function type, that's the type of a function which, without including any context of any kind, can take a parameter of type A, and return a value of a different type B. You can't do that - there's got to be some context which provides a value of type B - and to access the context, there's got to be something to allow the function to access its context: a free variable. Same thing in the logic and the lambda calculus: you need some kind of context to establish "A->B" as a theorem (in the logic) or as an inhabitable type (in the lambda calculus).

It gets better. If there is a closed LC expression whose type is a theorem in the corresponding intuitionistic logic, then the expression that has that type is a proof of the theorem. Each beta reduction is equivalent to an inference step in the logic. The logic corresponding to the lambda calculus is it's model. In some sense, the lambda calculus and intuitionistic logic are just different reflections of the same thing.

There are two ways of demonstrating the isomorphism: there's the original way that Curry did it, using the combinator calculus; and there's something called the sequent calculus. I learned it using the combinator version, so I'll run through that quickly. Another day, probably early next week, I'll do the sequent version.

Let's recall what a model is. A model is a way of showing that every statement in the calculus is valid in some concrete universe of values - that there is a correspondence between some set of real entities and the entities in the calculus, where statements in the calculus correspond to valid statements about the real entities. So we don't actually need to do the full isomorphism; we just need to show a homomorphism from calculus to logic. (An isomorphism means you can go both ways: from calculus to logic and from logic to calculus. Homomorphism is only from calculus to logic.)

So what we need to do is explain exactly how to take any complete lambda calculus expression, and translate it into a series of valid intuitionistic logic statements. Since the intuitionistic logic itself has been proven valid, if we can translate lambda calculus to IL, then we'll have proven the validity of lambda calculus - meaning that we'll have shown that computations in the lambda calculus are valid computations, and the lambda calculus is, indeed, a fully valid, effective computing system.

How do we get from combinators (which are just a shorthand for lambda calculus without variables) to intuitionistic logic? It's actually amazingly easy.

All proofs in an intuitionistic logic come down to a series of steps, each of which is an inference using one of two fundamental axioms:

1. A implies B implies A
   
2. (A implies B implies C) implies ((A implies B) implies (A implies C))
   

Let's rewrite those using arrows, like a type: A -> B -> A; and (A -> B -> C) -> (A -> B) -> A -> C.

Do those types look familiar to you? Take a look back at the post on simple typed lambda calculus if they don't. Those are the types of the S and K combinators.

The steps to the model should be pretty obvious now. Types in a lambda calculus correspond to types of atoms in an intuitionistic logic. Functions are inference rules. Each function can be reduced to a combinator expression; and each combinator expression is an instantiation of one of the fundamental inference rules of the intuitionistic logic. The function is a constructive proof of the theorem in the corresponding logic.

Now, is that cool, or what?

(To which any normal person would respond "what". But then, I'm obviously not a normal person, I'm a math geek.)