Sunday, December 03, 2006

And just as hard to use...

Here's a class related post that comes out of an explanation I got recently. It is also a bit rough, so be gentle. You can simulate lambda-abstraction in combinatory logic. You want to do this to get some of the lambda-abstraction flexibility without leaving a first-order (with types) framework. Lambda calculus is not first-order because terms (lambdas) can bind variables, which you can't do in FOL. How are lambdas different than quantifiers? One's a term and the other isn't, maybe? I'm not completely clear on that. But, the combinators are first order. The simulated abstraction doesn't work in all cases. It can't with the resources of just combinatory logic. One case it fails is (\lambda x.t)[s/z]=\lambda x(t[s/z]) (From Jeremy Avigad). Why might one want to do simulate the abstraction at all? There is a result that shows there is an isomorphism between proofs and programs, and so types (and categories, apparently). This means that one can think of a proof as a program, which is definable via the lambda calculus. This in turn means that one can think of proofs as terms (formulas? I think terms) in the lambda calculus. What sort of proof though? The terms are natural deduction proofs, with the abstracted terms viewed as undischarged hypotheses. Application is discharging a hypothesis. So, one gets that lambda calculus is the type theoretic analog of natural deduction. What are combinators then? Combinators are the type theoretic analog of axiomatic proofs. The route to seeing this is by looking at the types that make up the combinators. K is p->(q->p) and S is (p->q->r)->((p->q)->(p->r)). These types are structurally the same as the first two axoims of propositional logic (as usually presented; they'll be in there somewhere). The punchline: combinators are the type theoretic analog of axiomatic proofs, and they are just as hard to use. Now, the question is: what is the type theoretic analog of the sequent calculus?


Richard Zach said...

Hm? In FOL, quantifiers also bind variables. λ-calculus is quite a bit easier to use--what do you want to use it for and why is the fact that abstraction binds variables an obstacle?

Shawn said...

I think I was not as clear as I should have been. That probably stems from a bit of confusion about a key point. What I had meant was that you can simulate lambda abstraction in FOL if you use combinators. If I understand it correctly, the lambda calculus does some things that you can't do in FOL w/combinators, namely bind variables with terms (lambda abstraction). You can bind variables in FOL with quantifiers. However, if I understand correctly, there is a difference between quantifiers binding and lambdas binding variables. Maybe the former is at the formula level while the latter is at the term level? I will check on this ASAP and put up a correction note.

Looking at my post, I don't think I ever directly answered the question about why you'd want to simluate lambda abstraction with combinators. I'll do that later.

However, as was pointed out, working with lambdas is quite easy. Natural deduction proofs are (comparatively) quite easy too, which is nice since that's the way I wanted to say the correspondence ran. Combinators are hard to work with (at least based on personal experience); axiomatic proofs are similiarly difficult. So, if the correspondence (from the howard-curry isomorphism?) is between combinators and axiom proofs, then the combinators also possess the comparative unintuitiveness of axiomatic proofs.

So, give me lambdas and natural deduction any day. Unless we're proving cut elimination; in that case pass the sequent calculus.