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:
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 CurryHoward 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:
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.)
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 CurryHoward 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:

A implies B implies A

(A implies B implies C) implies ((A implies B) implies (A implies C))
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.)
6 Comments:
This is an interesting series of posts. Lambda calculus is often referred to so an overview is appreciated. Though I must admit that I will have to restudy this later in order to assimilate it sufficiently.
The coupling to intuitionistic logic raises a question for me that I hope somebody has an answer for.
(long and vague intro) I'm currently trying to grasp the treatment of facts in science. Coming from science into philosophical discussions on science I have trouble to find a reasonable treatment.
Philosophy assumes truth/false values about nature. This is all good and well in the usual science realistic view, but facts from observations behave differently and should have a natural model instead.
Coming from the other direction, knowledge representation or usual formal theories doesn't seem to describe the behaviour of facts. Both assumes truth/false values.
Most generally the use of frames describes cases when we not yet know about phenomena.
Abstracting that we have cases when the knowledge changes due to better observations or theories. That could be a temporal logic, and here intuitionistic logic comes in.
Abstracting yet again we have the usual ideal cases of the simplest facts as "not yet known", "true", "false". This could be intuitionistic logic. (/long and vague intro)
Q: Has intuitionistic logic been used to describe the behaviour of science facts, or is there a similar logic tried?
(long and vague ending) The quote "in regular predicate logic, we can infer that a forall statement is false if we know that there must be some value for which it's false; in intuitionist logic, we need to be able to show a specific example for which it's false"´, though describing the logic itself, is enticingly similar to the need for observational evidence to conclude facts suggested by formal theories.
If intuitionistic logic is usable I find it interesting to see a true three value logic of observed nature mapping between the unobservable "true nature" of philosophers and the idealised "known facts" of knowledge bases or "proposed facts" from formal theories.
It is also interesting that it would be based on the nature of functions. Functions seems so natural. (/long and vague ending)
By Torbjörn Larsson, at 11:15 PM
torbjorn:
In fact, the original motivation for intuitionistic logic was exactly what you're talking about. The idea of intuitionistic logic was to try to capture our intuitive reasoning facilities  the kinds of reasoning that we use when we're doing science  in a formal framework. It's not entirely successful I think, but it's a good approach.
There are a range of logics that try to capture different kinds of reasoning; IL is great for a particular kind of constructivist deduction. I'd also suggest looking at fuzzy logics, where instead of things being true of false, there's a concept of "degrees" of truth: something can be "mostly" true, or "a little bit" true, etc.
By MarkCC, at 11:07 AM
markcc,
Thank you for the information!
I didn't think there was a worthwile connection between everyday commonsense intuitive logic and science before, but I will pursue this. Fuzzy logic or Bayesian beliefs may be too detailed compared to the simpler 'natural' epistemic model for facts I'm looking for. In any case I will start looking on the simplest approach of course.
By Torbjörn Larsson, at 4:43 PM
BTW, it hit me that what I've seen of both fuzzy logic and bayesian beliefs are fairly linear applications, though I believe both can be modified here.
The qualitative switch between theories or observations "don't know" and "verified beyond reasonable doubt" is sharp by construction. (Though with arbitrary limits, for example 5 sigma for physics.) So my intuition is to look at what people has done with intuitionistic logic first. ;)
By Torbjörn Larsson, at 4:55 PM
Very interesting article, and an interesting conference too, about this subject:
http://www.pps.jussieu.fr/~krivine/articles/Geocal06.pdf
By boubou, at 2:05 PM
nice story..
hope you excelencet in your job..
nice blog..
All The Best.
Cheers,
diabetic diets
murad skin care
By fbtry, at 1:31 PM
Post a Comment
<< Home