2
$\begingroup$

I'm trying to wrap my head around the understanding of lambda-calculus, from a math/computing/logic standpoint and am reading more about its very genesis. This has taken me to 1924 - Schonfinkel's introduction of combinatory logic that seems to have started it all. On Wikipedia it says:

Combinatory logic is a notation to eliminate the need for quantified variables in mathematical logic. It was introduced by Moses Schönfinkel and Haskell Curry...

I understand the need for quantified variables like $\forall$ and $\exists$ in mathematical logic and it seems useful. But I fail to understand the reason to eliminate them. Why was this important? What does one attain with this elimination? Does it become more expressive? How so?

$\endgroup$
3
$\begingroup$

First, I'm not sure I agree that combinatory logic primarily aims to eliminate variables bound by $\forall$ and $\exists$. The basic formulation of combinatory logic works at the propositional level, where there are no quantifiers to eliminate in the first place. Instead, what it eliminates is $\lambda$-bound variables, but in a terms-as-proofs setting through the Curry-Howard isomorphism. We the have the correspondence

$$ \frac{\text{combinatory logic}}{\lambda\text{-calculus}} : \frac{\text{Hilbert-style formal proofs}}{\text{natural deduction}} $$

There's a natural correspondence between terms in the simply-typed $\lambda$-calculus and proofs in natural deduction for intuitionistic propositional logic. Through this correspondend, the combinators in combinatory logic correspond to the basic axioms of a Hilbert-style system.

There are various ways to extend this correspondence to predicate logic (and these may well have come first, historically), but they are not nearly as well-known or commonly encountered as the propositional setting. So you should probably not think of it as primarily having to do with $\forall$ and/or $\exists$ -- at least if you're trying to gain a contemporary understanding of how things fit together.

Now, what is this good for? As a practical way of writing down proofs it is a disaster -- it is well known that terms in the $\lambda$-calculus can increase in size exponentially when one tries to express them in combinatory logic.

However, there are some theoretical benefits -- because there are no variables, there is no need to define a notion of substitution either, and we don't need to worry about capturing variables during substitution and develop a machinery for avoiding this. This can often simplify proofs about the system.

$\endgroup$
  • $\begingroup$ Given my understanding of $\lambda$ calculus is still rudimentary and I'm struggling with associating it with logic and computing, could you please "dum down" your explanation for the non-mathematically inclined? I'm not sure I understood the answer well enough. $\endgroup$ – PhD Feb 11 '15 at 22:18
  • $\begingroup$ Comment 1: on the history: Curry undoubtedly was interested in illative combinatory logic encyclopediaofmath.org/index.php/Illative_combinatory_logic which aims to capture the logical quantifiers as primitives. $\endgroup$ – Rob Arthan Feb 12 '15 at 22:46
  • $\begingroup$ Comment 2: on the practicalities of combinatory logic: combinators are not disastrous (unless you tie your hands behind your back and only allow $S$ and $K$). The theory of combinators is very important for implementors and users of functional programming languages. E.g., see dl.acm.org/citation.cfm?id=802129 for a seminal reference on the use of combinators in compilers. $\endgroup$ – Rob Arthan Feb 12 '15 at 22:55
  • $\begingroup$ @RobArthan: I must admit I never read the supercombinator stuff back when I had a way through the paywall (and I even did some joint work with the author :p) but isn't that under an assumption where you can design which combinators to use based on the program you want to compile? $\endgroup$ – Henning Makholm Feb 12 '15 at 23:06
  • $\begingroup$ @Henning Makholm: you can still compile functional programs quite efficiently with a fixed repertoire of combinators. See David Turner's seminal reference on bracket abstraction jstor.org/discover/10.2307/… $\endgroup$ – Rob Arthan Feb 12 '15 at 23:14

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.