Why are combinators important in lambda calculus?

Question

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?

Answer 1

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.

Answer 2

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.