Semantics of the Lambda Calculus

The semantics of the Lambda Calculus is defined by three
basic operatorins called conversions.

1.  Alpha Conversion

	\V. E  -->  \V'. E [V'/V]  (using the full substitution rules)

This is just saying we can rename any binder and all of the occurences
it binds, and still have an equivalent expression.  That is, the
names of the bound variables have no meaning except to associate them
with their binder.

2.  Beta Conversion

	(\V. E1) E2 --> E1[E2/V]  (again, full substitution rules)

This just says that the key step in applying a function is substituting
the values for the formal parameters.  It turns out to be the key
part of the meaning of the lambda calculus.

3.  Eta Conversion

	(\V. (E V)) --> E          (if V not free in E)

This just says that if you wrap a binder around a function and apply
the function to the parameter, that means the same things as the
function.  For example, the "sqr" function is the same thing
as the (\x. sqr x) function.

For each of the above rules, the arrow says the former (alpha/beta/eta)
converts to the latter.  Any lambda expression which can be reduced
using one of these rules is called an (alpha/beta/eta)-redex or
reducible expression.

We extend the definition of the conversions to apply to subexpressions
of a lambda expression (and call them generalized conversions).

If you look back at the definition, you'll see that alpha and eta 
conversions are just kinds of renaming; the basic work of calculation
is done by (carefully) seleting beta-redexes and applying the
generalized beta conversion rule.

For example:

	(\x y. y) a b --> (\y. y) b --> b

since application associates left.