BEGIN 16_11_10_FixPointOperatorAgain.lhs

RECURSION VIA A FIX-POINT OPERATOR (CONTINUED)
==============================================

This handout says more than the preceding 16_11_09_FixPointOperator.lhs
about how to handle recursion uniformly via a "fix point" (sometimes
called "fixed point") operator.

Once more, here is the definition of the FIX-POINT operator:

> fix :: (a -> a) -> a 
> fix f = f (fix f)

We use "fix" to eliminate recursion -- or, more precisely, to
rewrite every recursively-defined function in terms of "fix",
so that "fix" is the only explicitly recursive function in the
program.

What we say in this handout works for a lazy (or call-by-name) 
language such as Haskell, but not for an eager (or call-by-value) 
language such as SML and other functional languages.

#########################################################
BEGIN EXAMPLE 1: A simple and tail-recursive function.

> remainder :: Int -> Int -> Int
> remainder x y = if x < y then x else remainder (x - y) y

(The function 'remainder' is equivalent to the library function 
'mod' restricted to the type Int -> Int -> Int.)

The preceding can be taken as syntactic sugar for:

> remainderA :: Int -> Int -> Int
> remainderA =  \ x y -> if x < y then x else remainderA (x - y) y

To get rid of the recursive call in remainderA, we define:

> remainderB :: Int -> Int -> Int
> remainderB =  fix (\ f -> 
>                    \ x y -> if x < y then x else f (x - y) y)

Note carefully how we modified remainderA in order to obtain
remainderB. The latter is not recursively defined and uses 
"fix".

END EXAMPLE 1
#########################################################
BEGIN EXAMPLE 2: Mutual recursive functions.

The following defines simultaneously ev (for "even") and
od (for "odd"):

> ev, od :: Int -> Bool
> ev  m = if m == 0 then True  else  od (m-1)
> od  n = if n == 0 then False else  ev (n-1)

Can we write a single recursive function, instead of two?
YES. Here is one possible way of combining the two preceding
functions into a single function:

> evAndOd :: (Int,Int) -> (Bool,Bool)
> evAndOd (m,n) = (if m == 0 then True  else snd (evAndOd (m,m-1)),
>                  if n == 0 then False else fst (evAndOd (n-1,n)))

In every successful recursive definition, there is a (hidden) INVARIANT, 
i.e. a property that remains the same through every recursive call. In 
order to really understand how a recursive definition works, it is helpful
to determine the INVARIANT underlying it. So, what is the invariant for
the function evAndOd? Here is a plausible one:

  "On arbitrary input m and n, evAndOd(m,n) returns
   (False,False) iff m is odd and n is even
   (False,True)  iff m is odd and n is odd
   (True,False)  iff m is even and n is even
   (True,True)   iff m is even and n is odd"

With the preceding INVARIANT you should be able to argue for the 
correctness of the definition of the function evAndOd.

> evAndOd1 :: (Int,Int) -> (Bool,Bool)
> evAndOd1 = \ (m,n) ->
>            (if m == 0 then True  else snd (evAndOd1 (m,m-1)),
>             if n == 0 then False else fst (evAndOd1 (n-1,n)))

We can now get rid of the recursion by using the fixed-point operator
"fix":

> evAndOd2 :: (Int,Int) -> (Bool,Bool)
> evAndOd2 = fix (\ f ->
>                 \ (m,n) ->
>                 (if m == 0 then True  else snd (f (m,m-1)),
>                  if n == 0 then False else fst (f (n-1,n))))

END EXAMPLE 2
#########################################################

END 16_11_10_FixPointOperatorAgain.lhs