I've been reading up on R. Smullyan's "To Mock a Mockingbird" and Hindley's "Lambda-Calculus and Combinators: An Introduction". I've even read Schonfinkel's 1924 paper introducing the idea of combinators and followed up with some Curry. "After" reading Hindley I can say that I "get" CL to some extent (and perhaps is the reason for this question).

However, CL seems to be presented in the language of $\lambda$-calculus. This seems to have been a general progression AFAIK where $\lambda$ superseded CL and the latter seems to have fallen off to the wayside.

My understanding is that although one can "define" a combinator like so in CL, the only way to "implement" it is via $\lambda$? Is this a valid inference? A satisfactory mathematical definition of a combinator may not be possible and thus it's described in the language of $\lambda$ and thus it's not relevant by itself per se.

The "concept" of combinators may still be useful (although I can't yet say how/where) for gaining some insight owing to it being "variable free" but for the most part it seems irrelevant as of today (2019-20). Almost everything in CL can be translated to $\lambda$ and vice versa. So is there any "insight" to be gained by studying CL? Is it now just a "simpler alternative" than $\lambda$ when trying to understand something that could get messy when analyzing with $\lambda$? Or is there more to it than meets the eye?

Is my understanding/assumption correct? What are the other reasons for it to not be "mainstream PLT" (or is that just my POV)?

  • 3
    $\begingroup$ The pattern calculus of TG Wilson and Barry Jay, and its successor, the SF calculus, are both recent combinatory logics that (to my knowledge) have no lambda analogues. cambridge.org/core/journals/journal-of-symbolic-logic/article/… $\endgroup$ – James Koppel Apr 17 '19 at 0:31
  • $\begingroup$ Physics,Topology, Logic and Computation: A Rosetta Stone seems to indicate that combinatory logic is useful for modelling linear logic and quantum computation. $\endgroup$ – jmite Apr 17 '19 at 15:06
  • 1
    $\begingroup$ Your impression about inevitabilty of $\lambda$-calculus in relation to CL is mistaken. It's perfectly possible to define CL, and implement it, without any reference to the $\lambda$-calculus. Have you not hear of unlambda? $\endgroup$ – Andrej Bauer Apr 18 '19 at 6:34
  • $\begingroup$ @AndrejBauer - I have never heard of it. Great link. Time to read up. As you can see, my understanding is limited and flawed in many places. I’m craving to find a book (or books) that put things in perspective and help me understand the various topics and their interrelationships better along with their “theoretical” applications. I’ll be indebted to gain some references. Do you have a “syllabus” for PLT where you teach along with recommended texts? I could use that as a study plan template to help fill in the gaps to my understanding of these wonderful topics. $\endgroup$ – PhD Apr 18 '19 at 7:20
  • $\begingroup$ Hmm, it's difficult to teach "all of PLT" and even to have a textbook on "all of PLT". I can tell you what to read about programming language design and type theory, but it seems you already know those. Maybe a book which isn't so much about type theory, like John Reynold's [Theories of Programming Languages](doi.org/10.1017/CBO97805116263640, although that book came before he invented separation logic. $\endgroup$ – Andrej Bauer Apr 18 '19 at 12:37

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.