Making Sense of Lambda Calculus 0: Abstration, Reduction, Substitution?
By Artyom BologovI 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:
- Abstraction.
- Application.
- Composition.
- Currying.
- Normalization.
- α-conversion.
- α-, β-, and η-reduction.
- α-, β-, and η-equivalence.
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.
You get the idea: λ (Greek letter lambda) means creating a new function.
What follows the lambda is its argument(s).
(It's a notational problem that
λxy might mean either of (1) a one xy argument function,
or (2) a two-argument function.
Most (simple) examples of LC expressions (including mine) usually go with (2).)
After the arguments end (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)
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
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 LC are actually single-argument, and all the multiple arguments examples are curried.
I'm using the λ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
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!
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:
- We take an expression.
- We apply the function to the argument.
- We apply another function to another argument.
- ...
- Profit!
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.
- δ/delta-reduction
- No one knows exactly what that means, but the general idea is that it's something about expanding primitives/vars to their definitions/effects.
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.
Substitution (α/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
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!