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 - E_{1} and E_{2}. E_{1} = λy.xy and E_{2} is λx.x. And E = E_{2}.E_{1}

Vaguely speaking, a lambda function can thought of as a 'c'-ish function. In our example both expressions are lambda functions. Here E_{1} is fed as a "parameter" to E_{2}. In pseudo code it might look like this.

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

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 E_{1}E_{2}E_{3} is evaluated as ((E_{1}E_{2})E_{3}). Evaluating E gives us E_{1} since E_{2} 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_E_{1} 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

E_{2} ⇒ λy.xy

E_{1} ⇒ λx.E_{2}

E ⇒ E_{1}z

Lets try writing it out in our pseudo code style

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

So evaluating E gives us E_{2}z ⇒ λy.zy. Lets break down a slightly more complicated expression:

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

E_{1} = λz.zx = λt.tx

E_{2} = λy.yzE_{1} = λa.azE_{1}

E_{3} = λxyz.xE_{2}
E = E_{3}mno

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

func_E_{1}(var t) { subst t•x // substitute all t by 'var t' } func_E_{2}(var a) { subst a•z•func_E_{1}// subst all a by 'var a' } func_E_{3}(var x, var y, var z) { subst x•func_E_{2}// substitute all x,y,z by var x var y and var z } func_E() { func_E_{3}(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.