Previous: Part 3: Evaluation Strategies, Next: Part 5: Church Numerals, Up: Contents

Part 4: Reductions

Goals

Understand the usefulness of reductions in the lambda calculus.
Understand and use alpha-, beta-, and eta-reductions.
Be able to find the simplest form of a given expression.

Prerequisites

Understanding of the syntax of the lambda calculus.
Understand the concept of scope with respect to functions.

Notation

In this tutorial, all expressions will use the symbol "\" for "lambda". This shorthand saves space and time.

What are reductions?

Reductions are used in the lambda calculus to reduce a statement to its simplest possible form. This is, essentially, what a computation in lambda calculus does. If you were to give a lambda calculus expression to "lambda calculus" calculator, it would use a combination of alpha, beta, and eta reductions to find the simplest reduction of your expression.

Beta reductions

The beta reduction is perhaps the most intuitive reduction, but is also the most important in analyzing lambda expressions. It is, in essence, a direct substitution, and it goes something like this:

	((\ (x) . BODY) a)	->_β	BODY [x\a]	= BODY

Lets look at this step by step.

	((\ (x) . BODY) a)

As you should already know, this first part defines a function which takes an argument 'x' and puts it into 'BODY'. In this instance, we are looking to pass 'a' to that function. This is the expression on which we want to perform our beta reduction.

	->_β	BODY [x\a]	= BODY

Here is our beta reduction. First we explicit say we are doing a beta reduction, then the BODY [x\a] part means "In 'BODY', I am substituting all instances of 'x' with 'a'". Because there is no 'x' in BODY, no substitution is actually made. After this (or on the next line) you write the result.

Exercise

Here are three examples of beta reductions. The first two are one step reductions, while the third is a two step reduction. Make sure you understand them before we continue.

(\ z. f z) b    ->_β  (f z)[b\z]  = (f b)
       (\ z.y) c       ->_β     y [c\z]  =  y
       (\ y . c)((\ z. f z) b)
                            ->_β  (\ y . c)( (f z)[b\z])
                             =    (\ y.c) (f b) 
                            ->_β  c [(f b)\y]
                             =    c

The third one could be written as (\ y . c)((\ z. f z) b) ->* c.

Quiz

select_first is defined as \x.\y. x, or:

	select_first = \x.\y. x

Apply beta reductions to the following expression until they cannot be further reduced:

	select_first u v

Alpha Reductions

An alpha reduction is hardly a reduction at all. It could be otherwise called, "renaming," but must be done with some care to make sure that one does not alter the scope of a variable when renaming it. Lets look at an example:

	(\(x) (+ x y))

In this expression, x is used as part of a function. It can be said that x is bound to the scope of the lambda expression, but y is free. You should agree that this is equivalent to:

	(\z.(+ z y))

If you wanted to do this formally, it would be called an alpha reduction, and would be written as:

	(\x.(+ x y))	->_α	(\ (z) (+ z y))

Like I said earlier, you must be aware of the scope of the variable. If you cause a name conflict, then the reduction is not valid. Consider the following:

	(\x.(+ x y))	->_α	(\ (y) (+ y y))

Because y was initially unbound (sort of like a global variable), the meaning of y is changed when you substitute it. This is referred to as a name conflict. Before the reduction, the scope of y is global, but after the reduction, the scope is changed to local. This is illegal in lambda calculus.

Name conflicts can be avoided in alpha (and beta) reductions by using new variable names. By using alpha-reductions in conjunction with beta reductions, you can avoid name conflicts reducing a more complicated statement. Here is an example of such a case:

	((\x.(\y.(x y))) y)

In order to have a proper beta reduction, you must first use an alpha reduction to change the second x to an alternate variable, like z:

	((\x.(\y.(x y))) y)	->_α				=
	((\x.(\z.(x z))) y)	->_β	(\z. (x z)) [x\y]	=
	(\z.(y z))

Eta Reductions

Eta reductions are used to eliminate useless variables in abstractions. Let's look at an example:

	(\x.(BODY x)) 	->_η	= BODY

In this abstraction, whenever the function is to be used, any argument will simply be passed to BODY. Hence, this function is, in essence, equal to BODY. One caveat of eta abstraction is that a name conflict must be avoided. What this means is if x is a free variable (i.e., not scoped in a function abstraction) in BODY itself, then this eta reduction is not valid, as it would be changing the scope of x. In order to avoid this, an alpha reduction must be performed before the eta reduction.

Eta reductions are very rarely used, and in most applications of the lambda calculus, it can be avoided completely.

References

http://www.cs.unr.edu/~sushil/class/326/notes/wk7.1.html
http://www.cs.rpi.edu/~schupp/entries/COURSES/pl/notes/theory1.html
http://www.cs.ualberta.ca/~you/courses/325/Mynotes/Fun/lambda.html

Previous: Part 3: Evaluation Strategies, Next: Part 5: Church Numerals, Up: Contents