Sunday, December 10, 2006

And just as hard to use (II)

In the previous post on combinators and lambdas, I had said that the lambda calculus is not first-order cause of variable binding. This was hopelessly vague (nod to Richard Zach for pointing this out), so I'm going to clarify. First-order logic has variable binding in the form of quantifiers. The lambda calculus has variable binding by lambdas. What's the difference? The lambdas are in terms, so in the lambda calculus, there is variable binding at the term level. The quantifiers of, e.g., FOL are only in formulas, not terms. They bind at the formula level. The reason that FOL+Combinators can't fully simulate lambda abstraction is because it can't have binding at the term level. There are extensions of FOL that allow this, but they were not what I was talking about. I hope that clears up what I was trying to say: a joke that required too much set up.

No comments: