SEP entry on Combinatory Logic

There's a new entry on Combinatory Logic in the Stanford Encyclopedia of Philosophy.

I haven't perused it yet, so please share opinions and comments.

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Seems OK

I've just skimmed it; it seems to be a decent elementary introduction to some of the most important topics, and I expected it to be stronger on the history of the topic than it is. Section 3.1, treating HM-style typing, was solid. I saw that Scott's D_infinity model was treated, in section 4.1: while the fact of the model's existence is certainly of interest, it doesn't seem very `core' to CL, and seemed like an odd inclusion for this article. It maybe that the author's emphasis on self-application led her to want to show how a mathematical model could handle it.

Overall, there's not much here for someone who has done a thorough course on the lambda calculus, but it's probably a good reference for non-specialists who might want to get the idea of what calculi of higher-order functions are about. It falls short of being a good introduction to CL for lambda-calculus hackers: that would still be Hindley & Seldin.

I note that Barendregt & Klop are slated to write an article on the lambda calculus.

Structural rules

Shawn Standefer wrote:

The article briefly mentions Meyer's work on combinators, and it talks about the connection between combinators and non-classical logics. However, it doesn't seem to make explicit the connection between combinators and structural rules in a sequent calculus, which Meyer calls the key to the universe.

Certainly, this is an important point that the article neglects, although I'm guessing that treating the topic properly would change the tone of the article as it stands.

Small stuff

I skimmed it too.

I would find it really nice if some basic complexity results would be included at the right places (like the expansion of Shoenfinkel of FOL is O(n^3), I think. That can easily be included.)

I expected also to see an exposition of deduction styles [sequent calculi / resolution] for CL's with/and some computational results like Knuth-Bendix completion but I gather that doesn't fall into the current understanding of the CL field.

To sum it up: more computational logic results!