Lambda calculus : Part 2
Kapil Kapre | Thursday, Oct 10, 2013

Continuing from Part 1, in Part 2, I'll cover some examples.

E ⇒(λx.x)(λy.xy)

First lets break it down into two lambda expressions - E1 and E2. E1 = λy.xy and E2 is λx.x. And E = E2.E1
Vaguely speaking, a lambda function can thought of as a 'c'-ish function. In our example both expressions are lambda functions. Here E1 is fed as a "parameter" to E2. In pseudo code it might look like this.


func_E1(var y)
{
    subst x•y   // replace 'y' with whatever 'var y' points to and return result
}
func_E2(var x)
{
    subst x;   // replace 'x' with whatever 'var x' points to and return result
}
func_E()
{
    get func_E2(func_E1);   // evaluate and get result
}
(Note: The • does not have any special meaning, I'm just using it to separate the two names)

I think this is a very intuitive way to look at things. For most procedural programmers what becomes obvious looking at the above pseudo code is that the variable names 'var x' and 'var y' are completely irrelevant - same as with lambda calculus. Note that the analogy to c-ish functions is not perfect as functions are not first class types in C. And subst is not really a C operation. One thing to note here is that expressions associate from the left. So E1E2E3 is evaluated as ((E1E2)E3). Evaluating E gives us E1 since E2 just 'returns' whatever parameter was passed to it. (λx.x) is formally referred to as an Identity function.

I briefly mentioned free vs bound variables in Part 1. Take a look at the above pseudo-code. The bound 'names' are the ones contained in the parameter and the free ones are the ones contained in the body of the functions. So in func_E1 y is bound and x is free. This is important to note as confusing the two can cause problems evaluating expressions where a name occurs both as bound and as free, but in different sub-expressions for e.g. (λx.(λz.xz)zx).

Another example:

E ⇒ (λx.(λy.xy))z
E2 ⇒ λy.xy
E1 ⇒ λx.E2
E ⇒ E1z

Lets try writing it out in our pseudo code style


func_E2(var y)
{
    subst x•y;    // replace 'y' with whatever 'var y' points to and return result
}
func_E1(var x)
{
    subst func_E2  // replace 'x' in body of func_E2 with 'var x' and return result
}
func_E()
{
    get func_E1(z)   // evaluate and get result
}

So evaluating E gives us E2z ⇒ λy.zy. Lets break down a slightly more complicated expression:

E ⇒(λxyz.x(λy.yz(λz.zx)))mno

E1 = λz.zx = λt.tx
E2 = λy.yzE1 = λa.azE1
E3 = λxyz.xE2 E = E3mno

Here we see something new. E3takes in 3 'parameters'. But again, if we write it in our pseudo code style, it becomes fairly easy to reason about.


func_E1(var t)
{
    subst t•x        // substitute all t by 'var t'
}
func_E2(var a)
{
    subst a•z•func_E1      // subst all a by 'var a'
}
func_E3(var x, var y, var z)
{
    subst x•func_E2        // substitute all x,y,z by var x var y and var z
}
func_E()
{
    func_E3(m,n,o)
}

So evaluating the above expression with var x = m, var y = n and var z = o gives us
m(λa.ao(λt.tm))

There is a lot more to understand about lambda calculus but my aim here is just to cover the basics. I might go into further detail in the future.