Making Sense of Lambda Calculus 1: Ignorant, Lazy, and Greedy Evaluation
By Artyom Bologov
Lambda Calculus is not hard, but some parts of it are confusing. While I've sorted out the confusing terms, I'm still getting tripped over
- missing parentheses,
- unclear lambda scope,
- and general computation/definition order.
This post is me trying to clear up Lambda Calculus evaluation properties.
Being Ignorant
My programmer background doesn't make it easier. I'm used to the fact that arguments are evaluated before the function call.
Lambda Calculus is working the other way around. Arguments are evaluated only when the function is applied to them. And the function is evaluated before the arguments. You can have a looped computation as argument to your function. And that doesn't necessarily makes your function stuck. Depends on what is the order of computation. Here's an example:
So there actually is computation in between argument evaluation. Scary, right? But that's how it works.
Being Lazy
It's often the case with LC examples that they omit parentheses. Some of these are uncertain in what to do first.
This one first applies f
to g
and then applies the result of that to h
.
Spelling that out doesn't make it clearer for me.
But here's the point: the argument are lazily collected.
So you only take an argument when you need one.
And, again, you don't evaluate arguments until you need to use them.
Being Greedy
Okay, so the order of application is lazy and minimalist. It only takes arguments when it needs them. If a function needs only one argument, it only takes one.
What's extremely inconsistent is that abstraction is greedy. It extends as far to the right as possible. The previous example would be a single lambda if we remove parentheses
That's why most examples you see out in the wild parenthesize the function: they need to restrict the abstraction from eating up too much expressions.
Up next: Numerous Quirks of Numbers
Lambda Calculus might seem really nasty at this point: it's Ignorant, Lazy, and Greedy. But I'm being misleading here: LC is still a powerful idea. And my negative impressions might be a consequence of getting repulsed by its specificities. So let's bear with it and get to appreciate it while diving deeper.
We've established the order of typical Lambda Calculus operations and understood basic terms used in Lambda Calculus. Now to the actual practice: Church Numerals encoding numbers! Arithmetic, numbers as function applications, elegant multiplication and exponentiation, and... ugly subtraction.