<p>Referencing to the comment of John Tromp, I want to remark that combinatory logic <em>feels</em> very different from lambda calculus. Since your interest stems from functional programming, you really do not want to know that much about combinatory logic.</p>

<p>My favorite tutorial on combinatory logic is in <a href="http://www.cl.cam.ac.uk/teaching/Lectures/founds-fp/Founds-FP.ps.gz" rel="nofollow">these lecture notes</a> from the Cambridge University.</p>

<p>However, they are introduced to explain implementation of so-called lazy (or applicative) languages; as mentioned in my previous comment, such techniques are now outdated.</p>

CC BY-SA 4.0
2018-11-14T13:16:02.947Z
Since combinatory languages are no longer used to implement lazy/applicative languages, what are the state of the art techniques now? And is there a name/category to classify these techniques?
CMCDragonkai
CC BY-SA 4.0
2018-11-15T10:18:49.593Z
@CMCDragonkai See comments to https://cstheory.stackexchange.com/a/306/989 for discussion. The short practical answer is "see papers on what GHC does": there is a variety of different techniques (including both the STG machine and optimizations such as strictness analysis) that are combined together to make lazy programs fast.
Blaisorblade
CC BY-SA 2.5
2010-09-08T22:07:12.273Z
2010-09-08T22:07:12.273Z
Blaisorblade
<p>What distinguishes combinatory logic is that it is variable free.  This is sometimes useful in metamathematics and philosophical logic, where the status of variables is tricky.</p>

<p>It may also be useful in implementations, since managing variables can be a headache.  Cf., e.g., Hughes, 1982, <em>Super-combinators: A new implementation method for applicative languages</em></p>

CC BY-SA 2.5
2010-09-08T21:34:18.963Z
Combinatory logic is _no more_ considered useful in implementations, and it was never used because "managing variables can be a headache". Combinators and variants were used to implement graph reduction for lazy languages, but nowadays Haskell (the most prominent lazy language) uses much more reasonable techniques to implement graph reduction.
Blaisorblade
CC BY-SA 2.5
2010-09-08T21:42:24.443Z
See e.g. S. Peyton Jones, 1992, "Implementing lazy functional languages on stock hardware: the Spineless Tagless G-machine" - http://research.microsoft.com/copyright/accept.asp?path=/users/simonpj/papers/spineless-tagless-gmachine.ps.gz&pub=34
Blaisorblade
CC BY-SA 2.5
2010-09-09T07:55:05.650Z
@Blaisorblade: *Combinators and variants were used to implement graph reduction for lazy languages* - Be careful: Haskell and ghc aren't the same, and the literature contains several supercombinator-based Haskells.  But it's true, the state-of-the art in functional programming has found the efficiency advantages of handling environments that outweigh its complexity.  You still see supercombinators used, e.g., in higher-order logic programming, where this is not true.    Supercombinators remain part of the inventory of techniques used in implementing higher-order programming.
Charles Stewart
CC BY-SA 2.5
2010-09-10T18:31:17.243Z
Supercombinators avoid only free variables, not bound ones, so IMHO they can't be considered uses of combinatory logic per se. They are mostly special lambda terms.

There are much smaller differences between supercombinators, lambda-lifted programs (if there's any, not sure) and GHC's implementation (where pointers from a closure to its free variables can be copied from the host function, thanks to purity).
Having said that, I was also thinking to the recent Utrecht Haskell Compiler, which is very similar to GHC, but IIRC uses lambda-lifting; still, that's not CL.
Blaisorblade
CC BY-SA 2.5
2010-09-10T18:39:48.720Z
I didn't know of higher-order logic programming - I found this paper on it: http://www.springerlink.com/content/t68777w270713p5n/. Unfortunately, it's unlikely I will have time to read it.
Blaisorblade
CC BY-SA 2.5
2010-09-10T19:41:28.620Z
@Blaisorblade: You can read off the output of the lamba-lifting algorithm as the specification of a set of combinators. Look at Johnsson, 1985, [Lambda lifting: transforming programs to recursive equations](http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.48.4346): he stresses how the result is lambda free (the only bound variables are variables on the lhs of a definition, i.e., in the place variables are bound in the definition of a combinator).  GHC is different - the STG-machine represents passed environments directly.
Charles Stewart
CC BY-SA 2.5
2010-09-10T19:48:13.473Z
@Blaisorblade: That paper isn't higher-order logic programming, it's an embedding of first-order logic programming into a combinatory logic.  Look at Miller, Nadathan, Pfenning & Scedrov (1991) [Uniform proofs as a foundation for logic programming](http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.105.9987) - which doesn't use combinators, fwiw.
Charles Stewart
CC BY-SA 2.5
2010-08-19T11:18:48.657Z
2010-08-19T11:18:48.657Z
Charles Stewart
<p>I am currently reading "<a href="http://www.cambridge.org/catalogue/catalogue.asp?isbn=9780521898850">Lambda-Calculus and Combinators</a>" by Hindley and Seldin.  I'm not an expert, but have always taken an interest in lambda calculus because of involvement with functional programming (starting with Lisp and SICP, and now with R and Haskell).  </p>

<p>In "<a href="http://homepages.cwi.nl/~tromp/cl/LC.pdf">Binary Lambda Calculus and Combinatory Logic"</a>, <a href="http://homepages.cwi.nl/~tromp/">John Tromp</a> states:</p>

<blockquote>
  <p>CL may be viewed as a subset of lambda calculus...the theories are largely the same,
  becoming equivalent in the presence of the rule of extensionality.</p>
</blockquote>

<p>Under what conditions would one use <a href="http://en.wikipedia.org/wiki/Combinatory_logic">combinatory logic</a> instead of <a href="http://en.wikipedia.org/wiki/Lambda_calculus">lambda calculus</a>?</p>

<p>Any references would be appreciated.</p>

CC BY-SA 2.5
2010-08-19T21:54:15.550Z
Take a look at "Lambda calculus: its syntax and semantics" by H.P. Barendregt.
Kaveh
<combinatory-logic><functional-programming><lambda-calculus>
Are lambda calculus and combinatory logic the same?
Shane
# Are lambda calculus and combinatory logic the same?

(Asked by: username_0 on 2010-08-18)

I am currently reading "[Lambda-Calculus and Combinators](http://www.cambridge.org/catalogue/catalogue.asp?isbn=9780521898850)" by Hindley and Seldin. I'm not an expert, but have always taken an interest in lambda calculus because of involvement with functional programming (starting with Lisp and SICP, and now with R and Haskell).

In "[Binary Lambda Calculus and Combinatory Logic"](http://homepages.cwi.nl/~tromp/cl/LC.pdf), [John Tromp](http://homepages.cwi.nl/~tromp/) states:

> CL may be viewed as a subset of lambda calculus...the theories are largely the same,
> becoming equivalent in the presence of the rule of extensionality.

Under what conditions would one use [combinatory logic](http://en.wikipedia.org/wiki/Combinatory_logic) instead of [lambda calculus](http://en.wikipedia.org/wiki/Lambda_calculus)?

Any references would be appreciated.

**Tags:** combinatory-logic, functional-programming, lambda-calculus

> **Comments:**
> **username_1**: Take a look at "Lambda calculus: its syntax and semantics" by H.P. Barendregt.  

---

## 2 answers

### Answer by username_4 on 2010-08-19. Score: 17 | Accepted answer

What distinguishes combinatory logic is that it is variable free. This is sometimes useful in metamathematics and philosophical logic, where the status of variables is tricky.

It may also be useful in implementations, since managing variables can be a headache. Cf., e.g., Hughes, 1982, *Super-combinators: A new implementation method for applicative languages*

> **Comments:**
> **username_2**: Combinatory logic is _no more_ considered useful in implementations, and it was never used because "managing variables can be a headache". Combinators and variants were used to implement graph reduction for lazy languages, but nowadays Haskell (the most prominent lazy language) uses much more reasonable techniques to implement graph reduction.  
> **username_2**: See e.g. S. Peyton Jones, 1992, "Implementing lazy functional languages on stock hardware: the Spineless Tagless G-machine" - http://research.microsoft.com/copyright/accept.asp?path=/users/simonpj/papers/spineless-tagless-gmachine.ps.gz&pub=34  
> **username_4**: @username_2: *Combinators and variants were used to implement graph reduction for lazy languages* - Be careful: Haskell and ghc aren't the same, and the literature contains several supercombinator-based Haskells.  But it's true, the state-of-the art in functional programming has found the efficiency advantages of handling environments that outweigh its complexity.  You still see supercombinators used, e.g., in higher-order logic programming, where this is not true.    Supercombinators remain part of the inventory of techniques used in implementing higher-order programming.  
> **username_2**: Supercombinators avoid only free variables, not bound ones, so IMHO they can't be considered uses of combinatory logic per se. They are mostly special lambda terms.  There are much smaller differences between supercombinators, lambda-lifted programs (if there's any, not sure) and GHC's implementation (where pointers from a closure to its free variables can be copied from the host function, thanks to purity). Having said that, I was also thinking to the recent Utrecht Haskell Compiler, which is very similar to GHC, but IIRC uses lambda-lifting; still, that's not CL.  
> **username_2**: I didn't know of higher-order logic programming - I found this paper on it: http://www.springerlink.com/content/t68777w270713p5n/. Unfortunately, it's unlikely I will have time to read it.  
> **username_4**: @username_2: You can read off the output of the lamba-lifting algorithm as the specification of a set of combinators. Look at Johnsson, 1985, [Lambda lifting: transforming programs to recursive equations](http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.48.4346): he stresses how the result is lambda free (the only bound variables are variables on the lhs of a definition, i.e., in the place variables are bound in the definition of a combinator).  GHC is different - the STG-machine represents passed environments directly.  
> **username_4**: @username_2: That paper isn't higher-order logic programming, it's an embedding of first-order logic programming into a combinatory logic.  Look at Miller, Nadathan, Pfenning & Scedrov (1991) [Uniform proofs as a foundation for logic programming](http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.105.9987) - which doesn't use combinators, fwiw.  

---

### Answer by username_2 on 2010-09-08. Score: 4

Referencing to the comment of John Tromp, I want to remark that combinatory logic *feels* very different from lambda calculus. Since your interest stems from functional programming, you really do not want to know that much about combinatory logic.

My favorite tutorial on combinatory logic is in [these lecture notes](http://www.cl.cam.ac.uk/teaching/Lectures/founds-fp/Founds-FP.ps.gz) from the Cambridge University.

However, they are introduced to explain implementation of so-called lazy (or applicative) languages; as mentioned in my previous comment, such techniques are now outdated.

> **Comments:**
> **username_3**: Since combinatory languages are no longer used to implement lazy/applicative languages, what are the state of the art techniques now? And is there a name/category to classify these techniques?  
> **username_2**: @username_3 See comments to https://cstheory.stackexchange.com/a/306/989 for discussion. The short practical answer is "see papers on what GHC does": there is a variety of different techniques (including both the STG machine and optimizations such as strictness analysis) that are combined together to make lazy programs fast.  

---

