26
$\begingroup$

I am currently reading "Lambda-Calculus and Combinators" 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", John 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 instead of lambda calculus?

Any references would be appreciated.

$\endgroup$
  • $\begingroup$ Take a look at "Lambda calculus: its syntax and semantics" by H.P. Barendregt. $\endgroup$ – Kaveh Aug 19 '10 at 21:54
16
$\begingroup$

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

$\endgroup$
  • 3
    $\begingroup$ 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. $\endgroup$ – Blaisorblade Sep 8 '10 at 21:34
  • $\begingroup$ See e.g. S. Peyton Jones, 1992, "Implementing lazy functional languages on stock hardware: the Spineless Tagless G-machine" - research.microsoft.com/copyright/accept.asp?path=/users/simonpj/… $\endgroup$ – Blaisorblade Sep 8 '10 at 21:42
  • 2
    $\begingroup$ @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. $\endgroup$ – Charles Stewart Sep 9 '10 at 7:55
  • $\begingroup$ 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. $\endgroup$ – Blaisorblade Sep 10 '10 at 18:31
  • $\begingroup$ I didn't know of higher-order logic programming - I found this paper on it: springerlink.com/content/t68777w270713p5n. Unfortunately, it's unlikely I will have time to read it. $\endgroup$ – Blaisorblade Sep 10 '10 at 18:39
4
$\begingroup$

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 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.

$\endgroup$
  • $\begingroup$ 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? $\endgroup$ – CMCDragonkai Nov 14 '18 at 13:16
  • $\begingroup$ @CMCDragonkai See comments to 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. $\endgroup$ – Blaisorblade Nov 15 '18 at 10:18

Your Answer

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

Not the answer you're looking for? Browse other questions tagged or ask your own question.