More readable lambda calculus
Lambda calculus is simple. The definitions and rules of lambda calculus would easily fit on an index card.
But you can't really read" lambda calculus so much as you can mentally execute it. Not many people can look at more than a few characters of lambda calculus and have any idea what it represents, though it's not hard to mechanically manipulate it. I suppose in hindsight that's what you'd expect from a theoretical model for computing.
The post The Programmer's Ring by Loup Vaillant gives a notation for lambda calculus that I hadn't seen before, notation that in my opinion is easier to understand. The author combines two ideas: de Bruijn indices (which I'd seen before), and replacing lambdas with brackets (which I had not seen).
The idea of de Bruijn indices is to replace variables with numbers. Vaillant describes De Bruijn indices saying
... variables are not referenced by name, but by stack offset: the last variable is accessed with the number 0, the second last with the number 1, and so on ...
This would be a terrible idea in an ordinary programming language, but in lambda calculus it actually helps. Lambda calculus is so low-level that the variables aren't meaningful anyway. It's not like you can look at a few lines of lambda calculus and say Oh, this is calculating net present value, so this variable must be the interest rate. It would be easier to read if they just called it interest_rate instead of 42 because it's the 42nd variable."
Wikipedia describes de Bruijn indices differently than Vaillant:
Each De Bruijn index is a natural number that represents an occurrence of a variable in a -term, and denotes the number of binders that are in scope between that occurrence and its corresponding binder.
It's not immediately obvious that these two definitions of a de Bruijn index are the same, and in fact they're not. But the only difference is that the first definition numbers from 0 and the second numbers from 1. This post will count from 0 with Vaillant.
After rewriting lambda calculus expressions to use de Bruijn indices, Vaillant fully parenthesizes the expressions (using braces, saving parentheses for grouping, as Mathematica does) then deletes the s: every bracketed expression starts with a , so the itself is redundant. Also, you can delete the name of the variable that the takes since the variable numbering takes care of that.
OK, so what does all this buy us? As Vaillant points out, this notation is more concise, and it makes some patterns easier to recognize. For example, the famous Y combinator
Y = f. (x. f (x x)) x. f (x x)
becomes
Y = [ [1 (0 0)] [1 (0 0)] ]
The latter makes the repetition inside more apparent.
As another example, let's look at Church encoding for numerals:
0 f. x. x 1 f. x. f x 2 f. x. f (f x) 3 f. x. f (f (f x)) ...
Here's what Church numerals would look like in the notation described above.
0 [[ 0 ]] 1 [[ 1 0 ]] 2 [[ 1 (1 0) ]] 3 [[ 1 (1 (1 0)) ]] ...
You can convert a Church numeral to its corresponding integer by adding all the numbers in the lambda calculus expression.
Vaillant's notation is more formal than traditional lambda calculus notation, but lambda calculus is formal anyway, so you might as well carry the formality a step further if it makes things easier.
Related postsThe post More readable lambda calculus first appeared on John D. Cook.