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)