5
$\begingroup$

I just recently learned a little about the lambda calculus, from the brief intro in the text Programming Language Pragmatics and this outstanding 4-video sequence from Adam Doupé. Basically I learned the gist of lambda calculus, $\alpha$-conversion and $\beta$-reduction, a bit of Church numerals, addition/subtraction, and the $Y$ combinator.

In this I learned the concept of a combinator, i.e. that it is an abstraction with no free variables. Simple concept. And there seemed to be this idea I kept reading between the lines, that we can/should turn non-combinator abstractions into combinators by wrapping them in abstractions that bind the free variables. For example, we can take the abstraction $(\lambda x. xy)$ and wrap it in $(\lambda y. \lambda x. xy)$ to bind the $y$.

But it was never really explained why it is important or useful to prefer combinators.

I'm assuming its because combinators allow us to easily combine expressions (surprise surprise) without the need of any externally-supplied variables. So in other words we could evaluate an arbitrary-length series of combinator applications without having to provide any initial conditions ahead of time. Which to me sounds like the equivalent in programming of avoiding global variables so as to avoid looking up values outside the current scope, in order to make it easier to understand the program and reduce errors. It also seems to align with the idea of a "pure functional" language that has no variables and no side-effects, which would imply such a language is effectively a series of combinator applications.

Is that correct?

$\endgroup$
7
$\begingroup$

The word "combinator" has some connotations that you don't seem to be intending here and sometimes a stricter definition. Another term for the definition you gave is a closed term. The opposite is an open term. The programming language equivalent of an open term would be an expression referring to a variable that's simply not in scope. Not just not in the current scope, but not in any containing scopes either. Most languages simply don't allow this. We can model let expressions that locally bind a name with lambda abstraction and application. In particular, let x = E in B becomes $(\lambda x.B)E$. The top-level, or global, scope can then be thought of conceptually as just a short-hand for wrapping your program in a bunch of let expressions. The point being, even global names are bound. The analogy to an open term, in this context, would be a term with one or more completely undefined variables in it.

Now clearly a closed term is self-contained which is useful. Further, for the purposes of computation, we never need to consider anything other than closed terms (assuming we start with nothing but closed terms). More precisely, for computation we usually care about weak (head) normal form which is the normal form for call-by-value(/name) reduction. An important aspect of these reduction strategies is they never reduce under a lambda. As such, any instance of $\beta$-reduction using these reduction strategies will only involve closed terms and will only ever produce a closed term assuming the initial term was closed. So, for the purposes of programming and computation closed terms are all that matters. Optimizing compilers, though, manipulate programs and often do perform reduction under a lambda and as such do need to deal with open terms. Proof assistants also need to deal with open terms as they usually need to reduce to normal form to compare lambda terms for equality. (Actually, they can often avoid going all the way to normal form.)

The focus on "combinators" isn't driven by software engineering concerns. It's simply a fact that for many purposes you only need to consider closed terms. The theory and formal manipulation of open terms is quite a bit hairier than for closed terms, so it is useful to limit to closed terms when possible.

$\endgroup$
  • $\begingroup$ Great answer thanks. This is along the lines of what I was trying to get at but I couldn't word it as clearly as you did. Is it useful to study lambda calculus for purposes other than influencing functional programming? $\endgroup$ – Dave Jan 20 '17 at 0:35
  • $\begingroup$ I should clarify my question but I can't edit it -- I'm sure it is useful to study it for other reasons, but I'm not sure what reasons there are for studying it. $\endgroup$ – Dave Jan 20 '17 at 0:42
  • $\begingroup$ @Dave The original purpose for the lambda calculus in the 1930s was understanding mathematical logic. There are deep connections various typed lambda calculi and category theory, and from there to physics as covered in Physics, Topology, Logic and Computation: A Rosetta Stone. There are applications to linguistics. I'm sure there are more. The connection to category theory allows it to be transplanted into many other fields, e.g. graph theory, though the significance isn't always clear. $\endgroup$ – Derek Elkins Jan 20 '17 at 1:29
  • $\begingroup$ Ok great. I knew about the basic origins and that it theoretically can be a math foundation, but not how far it reaches into theory today. Thanks. $\endgroup$ – Dave Jan 20 '17 at 1:40
2
$\begingroup$

A combinator is a lambda expression with no free variables.

So, λx.x is a combinator but λx.y is not a combinator.

Consider the following:

(λxy.xy)(λx.y) = (λy.xy)[x := λx.y] = (λy.(λx.y)y)

Notice how the final lambda expression is incorrect because the previously free variable y in λx.y has become bound. That's why when you're combining lambda expressions with free variables you have to follow renaming rules to ensure that the expression that results has the same meaning it had at the start.

Hence, this seems to me to be one of the reasons combinators are important:

When substituting with combinators your reduced expression will never change in meaning.

P.S. I'm now learning this stuff so I could be wrong.

$\endgroup$
  • $\begingroup$ Someone on IRC freenode in the #haskell-beginners channel (Cale) had this to say: "The more important thing is that combinators, having no remaining free variables, are the terms which are in some sense intrinsically meaningful -- there's nothing left to be determined from context about what is being expressed. It's the same as the difference between a proof following from assumptions, and a proof of something which follows entirely from the rules of the logic.". $\endgroup$ – Dwayne Crooks Jan 19 '17 at 22:12
  • 1
    $\begingroup$ This is essentially what I would have answered if you hadn't, with the minor difference that I would have said "renaming" rather than "disambiguation". Different perspective on the same idea. $\endgroup$ – Peter Taylor Jan 19 '17 at 22:37
  • $\begingroup$ I came across the disambiguation term in the Wikipedia article on lambda calculus but renaming is definitely a clearer term. $\endgroup$ – Dwayne Crooks Jan 19 '17 at 22:43
  • $\begingroup$ Right, I understood that you have to rename before substituting, to avoid free variable capture. Really good summary insight -- I like the focus on meaning there and in your comment. It seems to sum up the importance. Thanks. $\endgroup$ – Dave Jan 20 '17 at 1:20
  • 2
    $\begingroup$ You've basically got it, in that one of the key problems with lambda calculus is that a naive implementation of beta reduction can suffer from name capture. (By the way, this is also a problem in real-world compilers, where "inlining" a function may require renaming all variables inside it depending on how the compiler represents variables.) It's also interesting to know that a programming language doesn't need variables! By the way, it also has practical applications. See research.microsoft.com/en-us/um/people/simonpj/papers/… $\endgroup$ – Pseudonym Jan 20 '17 at 3:34

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.