## Recursion ##

## Basic fixed points ##

1. Recall that `ω := \f.ff`, and `Ω := ω ω`.
Is Ω a fixed point for ω?  Find a fixed point for ω,
and prove that it is a fixed point.

## Arithmetic infinity? ##

The next few questions involve reasoning about Church arithmetic and
infinity.  Let's choose some arithmetic functions:

    succ = \nfz.f(nfz)
    add = \m n. m succ n in
    mult = \m n. m (add n) 0 in
    exp = \m n . m (mult n) 1 in

There is a pleasing pattern here: addition is defined in terms of
the successor function, multiplication is defined in terms of
addition, and exponentiation is defined in terms of multiplication.
   
1. Find a fixed point `X` for the succ function.  Prove it's a fixed
point, i.e., demonstrate that `succ X <~~> succ (succ X)`.  

We've had surprising success embedding normal arithmetic in the lambda
calculus, modeling the natural numbers, addition, multiplication, and
so on.  But one thing that some versions of arithmetic supply is a
notion of infinity, which we'll write as `inf`.  This object usually
satisfies the following constraints, for any (finite) natural number `n`:

    n + inf == inf
    n * inf == inf
    n ^ inf == inf
    n leq inf == True

2. Prove that `add 1 X <~~> X`, where `X` is the fixed
point you found in (1).  What about `add 2 X <~~> X`?  

Comment: a fixed point for the succ function is an object such that it
is unchanged after adding 1 to it.  It make a certain amount of sense
to use this object to model arithmetic infinity.  For instance,
depending on implementation details, it might happen that `leq n X` is
true for all (finite) natural numbers `n`.  However, the fixed point
you found for succ is unlikely to be a fixed point for `mult n` or for
`exp n`.


#Mutually-recursive functions#

<OL start=5>
<LI>(Challenging.) One way to define the function `even` is to have it hand off
part of the work to another function `odd`:

	let even = \x. iszero x
					; if x == 0 then result is
					true
					; else result turns on whether x's pred is odd
					(odd (pred x))

At the same tme, though, it's natural to define `odd` in such a way that it
hands off part of the work to `even`:

	let odd = \x. iszero x
					; if x == 0 then result is
					false
					; else result turns on whether x's pred is even
					(even (pred x))

Such a definition of `even` and `odd` is called **mutually recursive**. If you
trace through the evaluation of some sample numerical arguments, you can see
that eventually we'll always reach a base step. So the recursion should be
perfectly well-grounded:

	even 3
	~~> iszero 3 true (odd (pred 3))
	~~> odd 2
	~~> iszero 2 false (even (pred 2))
	~~> even 1
	~~> iszero 1 true (odd (pred 1))
	~~> odd 0
	~~> iszero 0 false (even (pred 0))
	~~> false

But we don't yet know how to implement this kind of recursion in the lambda
calculus.

The fixed point operators we've been working with so far worked like this:

	let X = Y T in
	X <~~> T X

Suppose we had a pair of fixed point operators, `Y1` and `Y2`, that operated on
a *pair* of functions `T1` and `T2`, as follows:

	let X1 = Y1 T1 T2 in
	let X2 = Y2 T1 T2 in
	X1 <~~> T1 X1 X2 and
	X2 <~~> T2 X1 X2

If we gave you such a `Y1` and `Y2`, how would you implement the above
definitions of `even` and `odd`?

					
<LI>(More challenging.) Using our derivation of Y from the [Week3
notes](/week3/#index4h2) as a model, construct a pair `Y1` and `Y2` that behave
in the way described.

(See [[hints/Assignment 4 hint 3]] if you need some hints.)