Quick and dirty intro to Lambda Calculus – Post #2

This is a continuatin of my previous post.

In this post and all the following posts I write, all -calculus expressions are left-associative, ie..

In this post I will expound upon some of the things I glossed over in the last post.

Variable Bindings

The operator binds a variable. If a variable occurs in the body of an abstraction but is not bound, then it is called free. In the case of name clashes, variable is bound to the inner most .

-conversion

The easiest way to ensure that variable names don’t have scope issues is to simply rename all bound variables to a unique name:

-reduction

What I referred to as simplifying in the last post was actually a -reduction. -reduction is the act of making all the applications in an expression that do not use any bound variables. If all bound variables in expression have unique names, then a beta-reduction is very simple:

reduces to

The -conversion described above is very important because if variable names clash, then a -reduction is much more complicated. Take the following term:

Without first applying an -conversion we might end up with something like this:

wrong:

Now our free variable in is incorrectly bound. Instead we should get this:

correct:

Now our newly renamed is still a free variable.

That’s it for this post, in an upcoming post I will explain how to encode some basic datatypes using pure -calculus.