Lambda my beloved

2023-08-14 — Jahan Rashidi

I love lambda calculus. These itty bitty λ can do so much with so little.


Lambda calculus was created by Alonzo Church in the 1930s as a way of writing out any computation in simple terms. All lambda functions are written as just λarg.body and functions are applied by writing the argument after the function like so: λx.x 10, which would be 10. If this sounds at all similar to LISP to you, that's because lambda calculus heavily influenced LISP (and computer science in general). If it doesn't remind you LISP, it'll start to sound more familiar once some abstraction is added.

When I wrote λx.x 10, it's important to note that 10 is just a symbol here. Lambda calculus by default lacks some of the things we take for granted, like numbers. Anything can be represented however if we chose a way to encode them. A common way of writing numbers is with the function λf.λx.x representing 0, λf.λx.f x being 1, λf.λx.f (f x) being 2, and so on. But we'll come back to that in a little bit.

λx.x is the simplest function you can write, and it's normally called the identity function, since it returns whatever is passed to it. Instead of writing out the function each time, it's common to give functions names in the notation name := function, so we could write identity := λx.x and then identity hello would return hello. A function can also be passed as a parameter, so identity identity would return identity. (identity identity) identity would first do (identity identity) returning identity and then the rightmost identity would be applied to the returned identity giving the final result of identity. This is all pretty pointless, but it's just to show how it works.

Logic
To start actually doing something, let's try doing some basic logic using lambdas. The function λa.λb.a will return a function which will return the argument originally passed to the function. This really just means a function with two arguments, a and b, so from now on I'll write functions like this in the notation λargs.body, so this would be λab.a. To try it out, λab.a 10 3 will return 10, the first argument. Alternatively to that, λab.b will return the second argument, so λab.b 10 3 will return 3. What does this have to do with logic you're wondering? Well, if we say true := λab.a and false := λab.b, writing something similar to a predicate in many programming languages (bool ? if_true : if_false), true 10 3 returns 10 and false 10 3 returns 3. To make this a bit more readable lets also say that if := λctf.ctf, the argument c being short for condition, t for if true, and f for if false.

Now we can write if true 42 24, which becomes
λctf.ctf true 42 24, which becomes
true 42 24, which becomes
λab.a 42 24, which becomes
42. Cool huh?

Before we move on let's add a few more basic logic functions, and, or, and not. and should accept two arguments and return true if both arguments are true. We can write this and := λab.if a b false, saying that if a is true, return b since it now determines the result of and, otherwise just return false. However since if a b false is equivalent to a b false, let's just write that. or should accept two arguments and return if either are true. This can be written or := λab.if a true b, and simplified to or := λab.a true b. What we're saying here is that if a is true, we just return true since one of the arguments is true. Otherwise, we just return the result of b since now that determines whether one of the arguments is true or not. Lastly, not should return true if given a false argument, and false if given a true argument. We can write this not := λa.if a false true, simplified to not := λa.a false true.

Now that we have all these functions we can write something like λab.if (or a b) (not a) true, which will return true as long as a is not. Still, it doesn't seem like much if we can only compare true and false, so let's add a bit more.

Numbers and arithmetic
I previously mentioned that numbers were represented (in Church encoding at least) as λfx.x, λfx.fx, λfx.f(fx), λfx.f(f(fx)), and so on. As you might have noticed, the number of f's in the body of the function is what determines the value of the number (check out base 1). This means to add one to a number, we just need to add an f to it. We can write a function like this as inc := λnfx.f(nfx), where inc stands for increase, n stands for number, and f and x correlate to how we write numbers (λfx.x). This might make no sense, but to demonstrate, let's say that 0 := λfx.x, and 1 := λfx.fx.

If we write inc 0 this becomes
λnfx.f(nfx) 0 which becomes (since 0 is passed to n)
λfx.f(0fx) which becomes
λfx.f(λfx.x fx) which becomes
λfx.fx which is equal to 1.

If we say 2 := λfx.f(fx) and write inc 1 this becomes
λnfx.f(nfx) 1 which becomes
λfx.f(1fx) which becomes
λfx.f(λfx.fx fx) which becomes
λfx.f(fx) which is equal to 2.

Addition is simply increasing a by one b times (or vice versa) where a + b. You might not have noticed, but our numbers aren't just numbers, they are useful functions as well. If we try applying identity to f and some symbol like xylophone to x in the function 2, this will result in the expression 2 identity xylophone, which expands to
λfx.f(fx) identity xylophone which becomes
identity(identity xylophone) which means identity will be applied to xylophone twice.

This means that a number n used as a function in our encoding will result in the second parameter being applied to the first parameter n times. That means to write an addition function, we just need to write + := λab.a inc b. Now if we write
+ 2 3 where 3 := λfx.f(f(fx)), the expression will expand to
λab.a inc b 2 3 which becomes
2 inc 3 which becomes
λfx.f(fx) inc 3 which becomes
inc(inc 3), and if you want you can work out inc increasing 3 by adding f's, but since we know that's what'll happen I'll skip past the evaluation and just say that inc(inc 3) will increase 3 twice resulting in 5, where 5 := λfx.f(f(f(f(fx)))).

Multiplication is simply repeating a number a b times, where a * b. This can also be thought as adding a to 0 b times. We can write this as * := λab.a (+ b) 0. In this function (+ b) is one argument and 0 is the other, and we can think of (+ b) as its own function that increments an argument by whatever b was. There are some simpler ways to write multiplication functions in lambda calculus, but they're less intuitive in my option so we'll stick with this. To try it out, let's write
* 2 3 (I'm going to leave out "which becomes" from now on)
λab.a (+ b) 0 2 3
2 (+ 3) 0
λfx.f(fx) (+ 3) 0
(+ 3) (+ 3 0)
+ 3 3
6, where 6 := λfx.f(f(f(f(f(fx))))) (tell me if I missed a parenthesis).

Subtraction is decrementing a by one b times where a - b. That will be very similar to our + function, but first we need a function to decrease a number by one. A decrease function will have to remove one f from a number. On top of that, since we have no way to represent negative numbers (there are ways, we just currently aren't using one), what should we do if someone tries to decrement 0? We'll just say that if they try to do that, we'll return 0. Before diving into the horrors of subtraction, let's quickly make a function to check if a number is 0. Since number n applies x to f n times, 0 will never run f and simply return x. So if we apply two arguments to a number, a function that accepts a parameter and returns true to f, and false to x, we will receive false if the number is 0 and true otherwise. We can now turn this into a function: zero? := λn.n (λx.true) false.

Now, let's make a function to remove one f from a number. The only issue is, we don't really have any way to do that, so instead of trying to remove an f, let's try adding an f to 0 n - 1 times. We can do that by writing the function dec := λnfx.n (λgh.h(gf)) (λu.x) identity. dec stands for decrement, and n f and x correspond to their values in the inc function. The part (λgh.h(gf)) is for incrementing the number we're creating by 1. We apply it to n along with (λu.x), and (λu.x) when applied to (λgh.h(gf)) will end up wasting one iteration. At the end identity will be applied to what's left, turning it into a number. Note that 0 (0 := λfx.x == λf.identity). We'll end up with a number that was incremented n - 1 times.
dec 3
λnfx.n (λgh.h(gf)) (λu.x) identity 3
λfx.3 (λgh.h(gf)) (λu.x) identity
λfx.λab.a(a(ab)) (λgh.h(gf)) (λu.x) identity (since there were now two functions with an arguments named f and x, I renamed the ones in the number to a and b)
λfx.(λgh.h(g)) ((λgh.h(gf)) ((λgh.h(gf)) (λu.x))) identity
λfx.(λgh.h(g)) ((λgh.h(gf)) (λh.h((λu.x)f))) identity
λfx.(λgh.h(g)) (λh.h((λi.i((λu.x)f))f)) identity (I changed the h to i as double again)
λfx.(λk.k((λh.h((λi.i((λu.x)f))f))f)) identity
λfx.identity((λh.h((λi.i((λu.x)f))f))f)
λfx.((λh.h((λi.i((λu.x)f))f))f)
λfx.((λh.h((λi.i(x))f))f)
λfx.(f((λi.i(x))f))
λfx.(f(f(x)))
λfx.f(fx)

Phew. That was a lot of work, but the result is 2, which we expected. To make subtraction we just have to do - := λab.b dec a.

Lastly for arithmetic is division, but division is a bit more complicated, so we'll come back to it after checking out our next topic:

Comparisons
Currently we have no way of knowing if 3 > 2, or if 12 - 3 < 1, or even if 2 = 2.

Let's first make a less-than-or-equal-to function. This might seem like a strange first step to take, but it's easy using our zero? function we made earlier. Given two parameters, we should subtract the second parameter from the first. If the result is zero (since our numbers never go under zero) that means the first parameter is either less than or equal to the first. We write that as <= := λab.zero? (- a b). The opposite of <= would be >, so we can say > := λab.not (<= a b)

We can also make a greater-than-or-equal-to function similarly, by simply switching around a and b when subtracting: >= := λab.zero? (- b a). And since the opposite of >= is < we can say < := λab.not (>= a b).

Now that we have functions for comparing if something is bigger or smaller, we can check if two numbers are equal if they fulfil both >= and <=. So we can say = := λab.and (>= a b) (<= a b). Let's now finish up arithmetic.

Division and Recursion
To divide two numbers we have to count how many times we can subtract one number from the other. In order to do this, we'll have to write a recursive function. Recursion deserves a whole other article, but it basically just means that we're going to be calling our function from inside our function. What'd we like to do is write something like / := λab.if (< a b) 0 (inc (/ (- a b) b)), where we would subtract b from a until a < b and return the amount of times that happened. Unfortunately however this wouldn't work, as we would end up expanding / infinitely as (- a b) is evaluated after /.

The fix for this is writing a second function with the bulk of the function in one and giving it a parameter for which another function will pass that function to itself. This will stop it from being endlessly evaluated. For division, let's make one function, divhelper := λrab.if (< a b) 0 (inc (r (- a b) b r)) where r stands for reference and will be itself. Now we can make our division function / := λab.divhelper divhelper a b. My understanding of creating recursive functions in lambda calculus is quite thin, so I can't explain it well. I recommend doing more research on it yourself if you are interested.

Pairs
I mentioned at the start how LISP took a great deal of influence from lambda calculus. This is probably most noticeable from the fact that functions in LISP are created using the lambda keyword. Another thing LISP shares with lambda calculus however is pairs.

A pair is two connected values. We should be able to retrieve either value in the pair. We should also want to chain together pairs in order to make lists. Also, since we were just talking about LISP, and its staple is lists (ListProcessing) we'll use some LISP terminology for our functions.

To create a pair, we will make a cons function, short for construct. All that's needed for this is cons := λhtf.fht, where h stands for head, t stands for tail, and f stands for function. If we do cons 3 5 we will be returned the function λf.f 3 5. Remember how our true and false functions return the first and second argument applied to them respectively? We can use these for our pairs as well. For example
λf.f 3 5 true
true 3 5
3


To make this more intuitive, let's say car := λp.p true and cdr := λp.p false. If you don't know any LISP, then this is probably even less intuitive than before, but car stands for "contents of the address register" and cdr stands for "contents of the decrement register". I doubt that helps much, but just know car will get the first element, and cdr will get the second.

To make a list, we simply have to chain together pairs, like so: pair 1 (pair 2 (pair 3 4)). This will create something looking like this (1 (2 (3 4))). To get the third element in a list like this, we would first apply cdr to it twice and then car. We can write a function to do that for us: nth: λpi.car (i cdr p). Lets assign the list we made earlier to a variable: list := pair 1 (pair 2 (pair 3 4)) and try out our nth function on it:
nth list 2
λpi.car (i cdr p) list 2
car (2 cdr list)
car λfx.f(fx) cdr list
car cdr(cdr list)
3


To finish this off, here are a few more lambda-focused things I've stumbled upon. Enjoy