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.
I’m very surprised to see people think the lambda calculus is unreadable–I write it every day!
\x -> x + x. (in Haskell)
fun x -> x + x (ML)
(fun (x) (+ x x)) (lisps)
all seem pretty straightforward.
About the only thing you need to really simplify things to useful form is let-expressions, which are quite simple syntactic sugar:
let x = expr in rhs
->
(fun x -> rhs) expr
Seems to me, like that is not pure lambda calculus, Andrew. you cannot apply some preknown function like addition. All you can do is apply one argument `f` to a single other argument `x` or to some nested lambda term.
In programming practice functions are generally typed. You have simple functions and second order functions, which take the simple functions as arguments. But anything higher order is just too hard to understand, let alone functions that have arguments which are functions which can be applied to themselves, as the Y-combinator.
To follow up on Bodo’s comment, here’s how you’d write addition in lambda calculus, assuming m and n are Church-encoded numbers:
λm n f x. m f (n f x)
I doubt very many people would look at that and immediately recognize it as addition.
The Wikipedia article seems inconsistent. The part you quote, “…denotes the number of binders that are in scope *between* that occurrence and its corresponding binder.” would lead to counting from 0, just as Loup Vaillant does. λx. x translates to λ. 0 since there are zero binders *between* x and its corresponding binder. However, later in the Wikipedia article, in the formal definition, it says “The binding site for a variable n is the nth binder it is in the scope of”, which leads to counting from 1 instead of 0. Historically, de Bruijn’s original paper does count from 1; but every other presentation of de Bruijn indices I have ever seen (both in theory and in practice) counts from 0.