Luis Ziliani, a.k.a. Beta

This new post is intended to summarize all what is written in this page.

First of all, an errata from the previous post: I encourage the reader to define other functions, like the predecesor of a number… Well, I can’t remember if I planned to be that evil, or if I was just too drunk or what, but the fact is that that was an open question for many years. So if you made it (without cheating), you can say out-loud “I’m a Master in lambda calculus!!!”. But nobody will care, to be honest.

The λ-calculus formalism

I’ve learned how to write lambda in the posts! I will present the λ-calculus in a more formal way. Let V be a (countable) set of variables. The terms T in the calculus are defined in a semantic way as:

T :== x | (T T’) | (λx.T)

(A term is a variable, or an application, or an abstraction. Recall to the 3rd post.)

The β-reduction is the rule

(λx.T) R → T[x/R]

where the substitution T[x/R] is defined as:

1. x[x/R] = R
2. y[x/R] = y
3. (T T’)[x/R] = T[x/R] T’[x/R]
4. (λy.T)[x/R] = (λy.T[x/R])

The idea is quite simple: we iterate through the terms until we find a variable. If the variable is what we are looking for, then we replace the variable for the new term we want in that place. This works the same as the find/replace function of any text processor. A little tricky thing is that we are assuming that the variable names are different in each abstraction. This is like what we’ve done in the previous post by coloring the variables in order to distinguish them. If not additional rules are needed, and a condition is required in rule 4 (do not pay too much attention to this):

4. (λy.T)[x/R] = (λy.T[x/R]) if y does not appear in R
5. (λx.T)[x/R] = (λx.T)
6. (λy.T)[x/R] = (λz.T[y/z][x/R]) if y does appears in R and z does not appear in any of the terms.

Rule 6 makes a name change to avoid a variable capture (we don’t want the y variable in R to be “captured” by the new λ).

Examples

I was being criticized for the lack of examples. So here are a few. Maybe I add some others later. Again, I highly recommend to follow them in paper.

1) A function (let’s call it ‘K’) that given two parameters, returns the first one:

K = (λx.(λy.x))

K u v = (λx.(λy.x)) u v → (λy.x)[x/u] v = (λy.x[x/u]) v = (λy.u) v → u[y/v] = u

Note: I’ve to explain the different use of ‘=’, and the difference with ‘→’ in this example. The first ‘=’ in the definition of K, is a way of saying “whenever I say ‘K’, I’m meaning the term (λx.(λy.x)))”. So in ‘K u v = …’ I’m just using the definition of K. Then we have the → for the β-reduction. Then we have ‘=’ for the substitution. Why ‘=’? Because it is an operation that have to take the first term to the subtituted term “in one step”. I mean, I can write (λy.x)[x/u] = (λy.u). It is an atomic operation.

2) A function (let’s call it ‘S’) that given three parameters, distributes the third parameters into the other two. That is, “f(x,y,z) = x(z) y(z)”

S = (λx.(λy.(λz. (x z) (y z))))

S u v w = (λx.(λy.(λz. (x z) (y z)))) u v w → (λy.(λz. (x z) (y z)))[x/u] v w = … = (λy.(λz. (u z) (y z))) v w → (λz. (u z) (y z))[y/v] w = … = (λz. (u z) (v z)) w → ((u z) (v z))[z/w] = … = (u w) (v w)

One simple way to make arithmetic expressions in lambda calculus, is just to extend the calculus with the arithmetic rules:

(λx.(λy. x+y)) 2 3 → (λy. 2+y) 3 → 2+3 = 5

But that’s pretty easy for us, and (as you problably have already noticed) we like to complicate what’s easy. So let’s try to make the sum with the base lambda calculus. Why? Because it’s fun!

First of all, a bit of notation: let’s say that we can write the expression (λx.(λy. T)) (i.e. the function that takes a parameter and returns the function that takes another parameter and returns the generalized term T) as λx y. T

Secondly, I highly recomend you to follow the examples in paper, trying to see why one step lead to another.

In the beginning there was a Beta reduction… But He (Alonso Church) says “Let there be the numerals”, and the numerals appears:

0: (λf x.x)

1: (λf x. f x)

2: (λf x. f (f x))

…

N: (λf x.f (… f (f x))

This is just a way of doing this. You can say “for me, the 0 is (λx.x), the 1 is (λx y. y), …”. Or “for me, all this stuff is pure crap. Got a life, you punk!”. I choose this way for one simple reason: it is in the wikipedia, and it looks good and easy to use.

So the numerals are functions. Why? What’s the meaning of that? Let’s try to answer. The 1 is saying “given two parameters, we apply the first one to the second one”. And the N says: “given two parameters, we apply N times the first one to the second one”. So it’s looks like a for loop expression in a normal programming language. In order to answer to the first question, let’s show how to sum:

SUM: (λn1 n2 f x. n1 f (n2 f x))

Note: because all the numerals takes two parameters, it is expected that the Sum function returns some numeral that also takes two numbers. That’s why we receive the two numerals (n1 and n2) and the two parameters every numeral needs (f and x). Let’s make a simple sum:

SUM 2 1: (λn1 n2 f x. n1 f (n2 f x)) (λf x. f (f x)) (λf x. f x) → we replace n1 by the first numeral: (λn2 f x. (λf x. f (f x)) f (n2 f x)) (λf x. f x) → we replace n2 by the second numeral → (λf x. (λf x. f (f x)) f ((λf x. f x) f x))

This is a mess of f and x, so let’s try to make a difference between them. I will put gay colors in it.

(λf x. (λf x. f (f x)) f ((λf x. f x) f x))

We can reduce the orange numeral with the fucsia variables:

(λf x. (λf x. f (f x)) f ((λf x. f x) f x)) → (λf x. (λf x. f (f x)) f ((λx. f x) x)) → (λf x. (λf x. f (f x)) f (f x))

Now we can reduce the green numeral with the fucsia f (we have to change f by f), and then we can replace the green x by the fucsia (f x) expression:

(λf x. (λf x. f (f x)) f (f x)) → (λf x. (λx. f (f x)) (f x)) → (λf x. f (f (f x)))

And now everything is girly fucsia! And what does this expression means? The numeral 3 of course!

If you want to play more with this arithmetic way of computations, you can try to define the other functions (multipication, predecesor, etc). Or you can take a look at

http://en.wikipedia.org/wiki/Lambda_calculus