<p>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).</p>

<p>However, CL seems to be presented <em>in the language of</em> <span class="math-container">$\lambda$</span>-calculus. This seems to have been a general progression AFAIK where <span class="math-container">$\lambda$</span> superseded CL and the latter seems to have fallen off to the wayside.</p>

<p>My understanding is that although one can "define" a combinator like so in CL, the only way to "implement" it is via <span class="math-container">$\lambda$</span>? 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 <span class="math-container">$\lambda$</span> and thus it's not relevant by itself per se. </p>

<p>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 <em>seems</em> irrelevant as of today (2019-20). Almost everything in CL can be translated to <span class="math-container">$\lambda$</span> and vice versa. So is there any "insight" to be gained by studying CL? Is it now just a "simpler alternative" than <span class="math-container">$\lambda$</span> when trying to understand something that could get messy when analyzing with <span class="math-container">$\lambda$</span>? Or is there more to it than meets the eye?</p>

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

CC BY-SA 4.0
2019-04-17T00:31:16.537Z
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. https://www.cambridge.org/core/journals/journal-of-symbolic-logic/article/combinatory-account-of-internal-structure/3A92F27DDD53CE4FA05E41C571A78949
James Koppel
CC BY-SA 4.0
2019-04-17T15:06:21.437Z
[Physics,Topology, Logic and Computation: A Rosetta Stone](http://math.ucr.edu/home/baez/rosetta.pdf) seems to indicate that combinatory logic is useful for modelling linear logic and quantum computation.
Joey Eremondi
CC BY-SA 4.0
2019-04-18T06:34:15.930Z
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](http://www.madore.org/~david/programs/unlambda/)?
Andrej Bauer
CC BY-SA 4.0
2019-04-18T07:20:37.813Z
@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.
PhD
CC BY-SA 4.0
2019-04-18T12:37:06.337Z
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](https://doi.org/10.1017/CBO97805116263640, although that book came before he invented separation logic.
Andrej Bauer
<soft-question><lambda-calculus><big-picture><combinatory-logic>
Is Combinatory Logic (CL) still relevant for programming language theory?
PhD
# Is Combinatory Logic (CL) still relevant for programming language theory?

(Asked by: username_0 on 2019-04-17)

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)?

**Tags:** soft-question, lambda-calculus, big-picture, combinatory-logic

> **Comments:**
> **username_1**: 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. https://www.cambridge.org/core/journals/journal-of-symbolic-logic/article/combinatory-account-of-internal-structure/3A92F27DDD53CE4FA05E41C571A78949  
> **username_2**: [Physics,Topology, Logic and Computation: A Rosetta Stone](http://math.ucr.edu/home/baez/rosetta.pdf) seems to indicate that combinatory logic is useful for modelling linear logic and quantum computation.  
> **username_3**: 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](http://www.madore.org/~david/programs/unlambda/)?  
> **username_0**: @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.  
> **username_3**: 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](https://doi.org/10.1017/CBO97805116263640, although that book came before he invented separation logic.  

---

## 0 answers

