CSE230  THURSDAY MARCH 5, 1998



RECURSION IN THE LAMBDA CALCULUS

Consider the simple (useless) recursive function
	fun f x = if (x=0) then 1 else f (x-1)

Recursion is expressed in every real programming language by giving
a name to the recursive entity, and then using this name inside
the definition of the entity.

In the lambda calculus we cannot give names to expressions.
(When we do give an expression a name using ==, this is only
for convenience at the meta-level.)

Remarkably, recursion can be achieved in the lambda calculus.
The basic idea is that lambda expressions can be "self-reproducing."
That is, beta-reduction on Z can yield Z, or even something bigger
that contains Z.

For example, Z == (\z.zz)(\z.zz) is self-reproducing since Z -> Z.



DOING RECURSION

A lambda expression F corresponding to the function above
should somehow satisfy the property	
	F X ->* (if (zero X) B1 (F (pred X)))

For generality let's ask for
	F X ->* (\f.\x.M) F X
where
	M = (if (zero x) B1 (f (pred x)))

This way we will be able to plug in other bodies in place of M
(also called matrices) to get other recursive functions.

We want	F X ->* (\f.\x.M) F X

Because of left-associativity we want F ->* G F where G == (\f.\x.M)

Remember Z == (\z.zz)(\z.zz) -> (\z.zz)(\z.zz)

Consider F == (\z.G(zz))(\z.G(zz))

Now F -> G((\z.G(zz))(\z.G(zz))) which is G F as wanted.

This is enough to allow the \-expression (Y G) that implements
a recursive function f to behave properly.  



THE Y COMBINATOR

In general consider Y == \g.(\z.g(zz))(\z.g(zz))

For any function matrix M let G == (\f.\x.M) and let F == Y G.

Now Y G == (\g.(\z.g(zz))(\z.g(zz))) G -> (\z.G(zz))(\z.G(zz))
		-> G((\z.G(zz))(\z.G(zz)))

We have	Y G ->* G H where H == (\z.G(zz))(\z.G(zz))
and G H-> G (G H) -> G (G (G H)) -> ...

This is enough to allow the \-expression (Y G) that implements
a recursive function f to behave properly.  



USING THE Y COMBINATOR

A combinator is a closed \-expression, i.e. a \-expression
with no free variables.

Y is called a "paradoxical combinator" because of its behaviour
	Y G ->* G H -> G (G H) -> G (G (G H)) -> ...

There are other paradoxical combinators with the same behaviour.

Any expression using a paradoxical combinator will have a reduction
sequence that never terminates--the sequence that always chooses to
expand the recursion and never applies a body to an argument.

But if we choose the right reduction sequence, we get termination.

For example (Y G) B2 == ((\g.(\z.g(zz))(\z.g(zz))) G) B2
                     -> (\z.G(zz))(\z.G(zz)) B2
                     -> G ((\z.G(zz))(\z.G(zz))) B2

Plugging in the matrix from our original example of a recursive function,
we get

(\f.\x.(if (zero x) B1 (f (pred x)))) ((\z.G(zz))(\z.G(zz))) B2
      -> -> if (zero B2) B1 (((\z.G(zz))(\z.G(zz))) (pred B2))
      ->* if (zero B2) B1 (((\z.G(zz))(\z.G(zz))) (pred B2))
      ->* if (zero B2) B1 (G ((\z.G(zz))(\z.G(zz))) B1)
      ->* ...



THE LAMBDA CALCULUS IS UNIVERSAL

Obtaining recursion is the tricky aspect of the argument that the
lambda calculus is a universal programming formalism, like Turing
machines, and we just did it.

                           p
Definition: A function f: N  -> N is lambda-definable iff there
is some lambda expression F such that
	(F Bn1 ... Bnp) ->* Bm
whenever f(n1 ... np) = m

Theorem: All Turing-computable functions are lambda-definable.

Proof by example:
	double == Y (\f.\x.if (zero x) B0 (succ (succ (f (pred x)))))

Defining functions with two or more arguments is an exercise
for the reader.



A LOOPHOLE THAT MUST BE PLUGGED

We know that there is a \-expression named factorial such that
	(Y factorial) B4 ->* B24

But with the wrong reduction order, reducing (Y factorial) B4 diverges.

And what if (Y factorial) B4 ->* B25 also?

Definition: an evaluation order is safe it is guaranteed to
terminate whenever termination is possible.

We need (i) an evaluation order that is safe, and
(ii) a theorem that termination always gives a unique normal form.

The so-called normal reduction order is to always reduce the redex
that starts furthest to the left.

Theorem: Normal order is safe.
Proof: Omitted.

It is an open research question whether a random reduction order
is safe with probability 1.



THE CHURCH-ROSSER THEOREM

This is the most important theorem about the lambda calculus.  It is
the theorem that we asked for above, which says that normal forms are
unique when they exist.

Definition: The relation => is confluent iff
	for all E, E1, E2 such that E =>* E1 and E =>* E2
	there exists E3 such that E1 =>* E3 and E2 =>* E3.

Confluence is also called the Church-Rosser property, or the
diamond property.

Lemma:  If beta-reduction (plus alpha-conversion) is confluent
	then normal forms are unique up to alpha-conversion.
Proof:
Let -> stand for beta-reduction or alpha-conversion.
Suppose E ->* E1 and E ->* E2 where E1 and E2 are both normal forms.
Confluence says E3 exists such that E1 ->* E3 and E2 ->* E3.
E1 and E2 cannot be beta-reduced so E3 and E2 must be identical
modulo alpha-conversion.

Theorem: Beta-reduction (plus alpha-conversion) is confluent.

Proof: (Church and Rosser) Difficult.
See pages 230--232 of "The Study of Programming Languages"
by Ryan Stansifer (Prentice Hall, 1995)



SIGNIFICANCE OF THE CHURCH-ROSSER THEOREM

This theorem is quite strong.  It says that for any two sequences
of reductions applied to the same starting expression, some other
reductions can be done that bring the two intermediate results
together again.

The final result of reducing an expression is independent of the
order in which redices are reduced inside the expression, even
though reducing one redex may create new redices.

We must be very careful when extending the lambda calculus to
preserve confluence.  For example we cannot add a non-deterministic
choice operator with the property
	c E F ->* E
	c E F ->* F



EQUALITY

So far we do not have an equality operator for the lambda calculus.
All we have is a syntactic identity operator.

Definition: Equality is the symmetric reflexive transitive closure
of beta-reduction and alpha-conversion.

Lemma: If two \-expressions have the same normal form, then they are equal.

Example: (\z.yz)y = (\x.xx)y because both beta-reduce to yy.
Note that y is free and hence cannot be alpha-converted.

Some formulas do not have normal forms and hence the converse of the
lemma is not true.



THE \-CALCULUS IS NOT TRIVIAL

The lambda calculus is trivial if all \-expressions are equal.
Luckily...

Theorem: Not all \-expressions are equal.
Proof: \x.x and \xy.x are both normal forms, and not alpha-convertible.
By the Church-Rosser theorem, there cannot exist a \-expression E
such that E ->* \x.x and E ->* \xy.x.  Hence (but not directly)
\x.x and \xy.x are not equal.