Making Sense of Lambda Calculus 0: Abstration, Reduction, Substitution?

By Artyom Bologov

I am a programmer. A Lisp programmer, in fact. I have a creeping desire to understand Lambda Calculus because it's a powerful and elegant tool and an inspiring idea underlying many functional languages and idioms. I use lambdas every day, without knowing their secret power. Might be useful to unleash this power and tame it for productivity.

All my previous attempts to approach Lambda Calculus were unsuccessful. I opened Wikipedia, read through half the page and gave up. It was too terse. The learning curve was even steeper than that of Emacs. It just leaped from the basic "Here's a lambda" to "Here's a 20-levels nested recursive computation". There was no information in between the entry level and intermediate level. Or is it that I'm too stupid to go through the transition? Either way, Lambda Calculus needs a better explanation.

This series of articles walks me, a regular programmer, through Lambda Calculus. It's mainly intended for me to make sense of what I encounter while reading. But, as a side effect, it can be useful to others. It's fun to read through what others found weird or frustrating, right? The most immediate thing is... confusing terms.

Lambda Calculus is a mathematical model. Which means: lots of Greek letters and obscure terms. Here's a short list of terms I was able to find on 2 (!) web pages about LC:

Did I say a short list? Sorry. In this post, I'll get myself (and, hopefully, you too) through these terms. Discarding the unhelpful ones and extending on the useful ones. It's better read alongside a full-blown page describing Lambda Caclulus, like this one.

Abstraction

That's the simplest one for a programmer's mind: abstraction is a function definition. Basically when you say: "this is a function that takes X and returns Y". Et voilà—you have a function now! Lambda Calculus is built around functions, so functions are all you need.

Here's a set of examples for how abstraction looks like: 

λx.x // Identity function. Takes X, returns X.
λx.42 // A function to answer anything.
λx.π // Return pi.
λxy.x+y // Summation function for X and Y.
Examples of lambda expressions—abstractions

You get the idea: λ (Greek letter lambda) means creating a new function. What follows the lambda is the list of arguments. After the list of arguments ends (a period), function body starts. Arguments name the inputs, body specifies what happens to these.

Application

That's familiar to programmer's mind too. We usually refer to it as function call. Once you have the function, you can call it with arguments. Like: 

f(x)
f x
(f x)
Different types of function application

Yes, these three are almost the same in Lambda Calculus. So pick whatever you like. I'm a Lisper, so I'm mostly going to use the (f x) syntax, at least for complex examples. Believe me, it's clearer this way. Even if you don't lisp.

The meaning is pretty simple: get the function and pass it some arguments. Taking the abstractions from above: 

(λx.x) 5 // => 5
(λx.42) 5 // => 42
(λx.π) 5 // => π
(λxy.x+y) 3 5 // => 8
Results of application for different lambdas

Currying

You can provide more arguments or less arguments when applying the function. Providing more arguments is usually an error. Because, well, it's not intended to work this way.

Providing less arguments invokes magic called currying. Currying is when you have a function with one argument. And inside it another function with one argument. And inside it... A Russian doll of functions, if you like. Once you provide a single value to this Russian doll, it uses this argument and returns you an inner function. So that you can apply this inner function to other arguments. Et cetera..

Functions in Lambda Calculus are actually single-argument, and all the multiple arguments examples are curried. I'm using the CD(λxyz) syntax as a shortcut for the λx.λy.λz doll.

That's similar to Haskell, where all function (including the multiple-argument ones) are curried: 

// Takes three a's and returns b
a -> a -> a -> b
Typical function signature in Haskell

The summation function from above works like 

(λxy.x+y) 3 5 // Function application.
(λx.λy.x+y) 3 5 // Revealing the doll.
(λy.3+y) 5 // One less layer, x = 3
3+5 // Another layer off, y = 5,
8 // Yay!
Applying a multi-layered curried function to multiple arguments

Taking the arguments one by one and getting the results. Wait, we did something new here...

Reduction (β/beta)

Reduction is kind of like running the program and getting the result. There are problems with this comparison, but we'll get to that later. For now, all we need to know about reduction is: it's the way we get values from expressions. So our summation example above is a reduction:

The reduction procedure is as simple as it appears: just take an expression and apply functions to arguments until there's nothing to apply.

Now, there are several things that they call "reduction". There's α-reduction, there's β-reduction, and η-reduction. Here's what they are:

α/alpha-reduction
is rather variable substitution. I'll try to explain it later.
β/beta-reduction
is exactly what we're aiming at here: applying the thing until done.
η/eta-reduction
is when you simplify the expression until it's as simple as it can be.

Update Jan 5 2024: I mistakenly said that η-reduction is normalization. These two are different ones, but I'm not going to elaborate on why 😛

The essence of these is simple, but they sound intimidating. Feel free to use them to scare off Rust fanboys.

subtitution (α/alpha)

If you use some fancy JetBrains IDE, you likely know of this feature: you can rename some function or class, and the IDE will rename it in all the other places it's used in. Neat!

α-substitution (also known as α-conversion) is when we rename some function argument. Starting from simple examples to more complex ones: 

λx.x // => λy.y
λx.x x // => λy.y y
λx.y // => λz.y
λx.y x // => λz.y z
(λy.y) λy.y // => (λy.y) λx.x
Examples of α-substitution

It's mostly useful when you apply functions with similar argument names. You, an ultimate Lambda Calculus IDE, auto-rename the argument for it to not collide with other arguments.

Equivalence

There are different types of equivalence that depend on what you want to compare. It's always this way with equivalence and identity. That's why Lisp has four (!) equality operators (eq, eql, equal, equalp). That's why JavaScript has == and ===. We've already covered most of the complex stuff, so nothing hard here.

α/alpha-equivalence
is when you substitute arguments until two expressions look the same.
β/beta-equivalence
is when things reduce to the same result.
η/eta-equivalence
is when one expression can be simplified to the other.

Up Next: Order of Evaluation

So these were the terms that I needed to clear up for myself. They were too hard or were inconsistent across my learning materials. Now to the actual examples and their difficulties— in part one!