CSE230  THURSDAY FEBRUARY 26, 1998



THE LAMBDA CALCULUS

A "calculus" is a notation that can be manipulated mechanically.
A "calculus" is a foundation for formal, hence rigorous, reasoning.

The lambda calculus is a Turing-complete calculus for programming,
i.e. any program for calculating with integers has a lambda calculus
version.  We will show this.

The lambda calculus is the core functional programming language
in the same way that Turing machines are the core imperative
language.

There are interesting contrasts between Turing machines and the
lambda calculus:
	TMs are too low-level: memory access is not constant-time.
	The lambda calculus is too high-level: a single reduction
	is the primitive operation in the lambda calculus, but cannot
	be implemented in constant time in general.

The lambda calculus was first formalized by Alonzo Church of Princeton 
and later UCLA, in 1941.  Church died in 1995.

	Alonzo Church, 92, theorist of the limits of mathematics.(Obituary)
	New York Times v144 (Tue, Sept 5, 1995):A11(N), B6(L), col 5.

Paradoxically, the lambda calculus is an American invention and TMs
are European, but the theory of the lambda calculus is a European
specialty now, whereas TM-based computational complexity is more
active in America.



LAMBDA CALCULUS SYNTAX

A lambda expression is either 
	(1) an identifier, or
	(2) an abstraction of the form \x.E where x is an identifier
            and E is a lambda expression, or
	(3) an application of the form EF where E and F are
            lambda expressions.

\ is the closest Ascii symbol to the Greek letter lambda.
We assume a countable set of identifiers.
Parentheses are used to indicate grouping, e.g. (\x.(\y.x))(\z.z)

Think of \x.E as a shorter notation for (fn x => E).



BOUND AND FREE VARIABLES

(\x.E) is a scope or block inside which the name x is bound.

More formally, every appearance of a name in an expression is "bound"
or "free".  If x appears in E, and the appearance is inside some
subexpression F of the form (\x.G) then the appearance is bound;
otherwise it is free.

For example x is free in (\y.x) but x is bound in (\x.(\y.x)).



BETA-REDUCTION

Beta-reduction is the name of the fundamental \-calculus operation
that corresponds to function invocation.

Intuitively, (\x.E)F may be reduced to a copy of E where each
appearance of x is replaced textually by F.

For example, (\u.(u^2 + 2u + 1))(3x) -> (3x)^2 + 2(3x) + 1

                          beta
Formally we write (\x.E)F ----> E [x |-> F]

The definition of the substitution E [x |-> F] must avoid capture.
The formal definition is by cases, following the abstract syntax
of \-expressions:

	     x [x |-> F] = F
	     y [x |-> F] = y
	  (MN) [x |-> F] = M[x |-> F] N[x |-> F]
	(\x.B) [x |-> F] = \x.B
	(\y.B) [x |-> F] = \y.(B[x |-> F]) if y is NOT free in F
                         = (\z.(B[y |-> z]) [x |-> F] if y is free in F,
                                               where z is a fresh variable


ALPHA-CONVERSION

This is the most basic rule for manipulating \-expressions.
One expression may be reduced to another by changing a bound identifier
throughout its scope to any other identifier that does not occur
already in the scope.

When we write (\z.(B[y |-> z]) above, we are doing an alpha-conversion
because z is a fresh variable.

Alpha-conversion is two-way but beta-reduction is (usually) one-way.

     alpha           alpha             beta           beta
If E -----> F then F -----> E but if E ----> F then F --/-> E typically.