HiveBrain v1.2.0
Get Started
← Back to all entries
patternMinor

Why are combinators important in lambda calculus?

Submitted by: @import:stackexchange-cs··
0
Viewed 0 times
whycalculusarecombinatorsimportantlambda

Problem

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?

Solution

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.

Context

StackExchange Computer Science Q#68969, answer score: 8

Revisions (0)

No revisions yet.