So I wrote a lengthy blog post about functional programming [1] and in it I have a segment where I praise lambda calculus as the best thing ever [2], link a couple of books, and leave you to your own devices. One of the nice things about lambda calculus (elaborated upon below) is that it is very simple. This makes it easy to use because there’s not a lot to keep track of. One of the frustrating things about lambda calculus is that it is very simple. This makes it hard to get the hang of it because it takes forever to decide how it can actually be used for anything. So instead of just saying that lambda calculus is awesome and then letting you take care of reading multiple books and figuring out how to use what you learn, I’m going to try and give you a crash course and some ideas as to how you can apply lambda calculus. But first, here’s some books [3] [4] [5].
Lambda calculus is turing complete language. This means that any function that can be computed in a different turing complete language (like C# for example) can also be computed in lambda calculus. Lambda calculus is also a simple language. Its syntax can be described with three recursive rules.
λ-TERM ::=
x, y, z, … (VAR)
| λ VAR . λ-TERM (ABS)
| λ-TERM λ-TERM (APP)
Of course parentheses are allowed (and/or required) to eliminate any ambiguity. The VAR simply stands for variable, ABS indicates an abstraction (this is very much like using an anonymous function), and APP just means application or apply (like calling a function).
There are two types of variables in lambda calculus. Bound variables and free variables. Bound variables are straight-forward. Consider an anonymous function in C#.
( int a ) => a + 5;
In this C# example, the ‘a’ variable is bound. So you already have a good intuition as to what a bound variable is. It’s a variable that exists in the parameter list of a function.
λ a . a
That’s a lambda term where ‘a’ is also a bound variable.
Free variables are a little bit harder to talk about. Technically there are no valid lambda calculus programs that contain free variables. However, sometimes you want to consider a sub-term that contains variables that are not bound in any lambda abstractions that are currently visible.
λ n . λ f . λ v .
n ( λ a . λ b . b ( a f ) )
( λ k . v )
( λ i . i )
In this rather complex example every variable is bound, but maybe you want to just look at a small part of it.
n ( λ a . λ b . b ( a f ) )
In that example, ‘a’ and ‘b’ are both bound, but ‘n’ and ‘f’ are free variables.
Now that you’ve got bound and free variables down, there’re two rules that you have to remember.
α-conversion
( λ a . a ) <=> ( λ b . b )
That is you can rename a variable without changing the meaning of the lambda term. This is important because sometimes you need to change the name of a variable in order to avoid naming clashes.
β-reduction
This is a single computation step in lambda calculus. Roughly analogous to executing a single instruction in the CPU. The name of the game is substitution. A lambda abstraction is just like an anonymous function with a single input parameter. Instead of executing assembly instructions when you apply a value to the lambda abstraction you substitute the value into the lambda abstraction at every instance of the bound variable of that abstraction.
A simple example with a free variable ‘z’.
( λ a . a a ) z
=> z z
Just replacing the bound variable ‘a’ with the free variable ‘z’. Of course you can also use bound variables as input parameters and even entire lambda terms as input parameters.
( λ b . λ c . c b ) z ( λ a . a )
=> ( λ c . c z ) ( λ a . a ) // z replaces b
=> ( λ a . a ) z // ( λ a . a ) replaces c
=> z // z replaces a
That’s really about all there is in lambda calculus. And that does raise the question, “how exactly is lambda calculus turing complete?” Fortunately, I don’t think I have to answer that question for lambda calculus to be useful (although there is an answer if you’re really interested). It’s simple. This means that there aren’t a lot of complex rules to memorize. Once you internalize how to encode algorithms in lambda calculus you’re going to be able to use it without checking tables of precomputed values or constantly looking up an endless set of unintuitive formulas. Additionally, you’re not going to get stuck because the language is turing complete. Well, you might get stuck, but that will be because you’re having problems and not because lambda calculus is having problems.
And this is the best part. With a language so simple, sometimes it’s really hard to do things that ought to be simple, sometimes it’s too slow, sometimes it’s confusing, and sometimes you just don’t feel like it. But the entire language is based around function abstraction and function application. If you can’t write your algorithm in lambda calculus, just write it in C#, use a loop and if-statements, and then abstract it inside of a function. Use it just like it was any other function. This process isn’t exactly formal (although there are techniques that can make it formal if you really want to go down that road), but it is very convincing. Any function you can write in another turing complete language like C# can also be expressed in the turing complete lambda calculus. Convince yourself that what you want to do is possible in a turing complete language (any turing complete language) and then just pretend that your definition is really replaced with an equivalent definition in lambda calculus.
The next question is, “why go through all of this trouble when we have perfectly good languages like C/C++, C#, and Java?” And my opinion is that we don’t have perfectly good languages. Don’t get me wrong. These languages, especially C#, are a lot better than they have to be. And they are all improving constantly. However, key concepts from mainstream programming languages, like global mutable state, mutable references, flimsy type systems, and dynamic stack effects, conspire together to make the ever increasing complexity of modern software increasingly hard for software engineers to build successfully.
I’m not quite ready to give an exhaustive argument as to why the way things are done today stands in the way of bigger and better software systems. But I also don’t want to argue that everyone needs to jump ship to exotic languages like Haskell. Type theory and category theory are complicated things; it takes time to transition to using them. I think changing paradigms without taking a lot of time to figure out how things are different is a recipe for failure. However, lambda calculus is simple and surprisingly compatible with modern software development. It can help you avoid problematic programming constructs, and you can start using it today.
[1] – 2014/03/11/functional-programming/
[2] – Not actually the best thing ever. However, it is very useful.
[3] – https://rubymanor.org/3/videos/programming_with_nothing/
Not actually a book, but a really good talk that shows you what is doable with lambda calculus.
[4] – https://research.microsoft.com/en-us/um/people/simonpj/papers/slpj-book-1987/
[5] – https://www.cis.upenn.edu/~bcpierce/tapl/
