Alpha renaming lambda expressions
=================================

Alpha renaming the variable of an arbitary lambda expresssion is
remarkably similar to the problem of alpha renaming a program with
let expressions .....

When a function is declared it introduces some bound variables whose scope
is that function body ... thus it is just like a lambda expression.

When a lambda expressions is entered it introduces a variable:  in the alpha
renaming process we shall associate with that variable a (new) number.   This is done by simply
keeping a counter which we increment each time wehave to rename a variable.  Now
that variable name may have already been used so we shall keep a stack (a.k.a. list)
of variables and their assigned numbers.  When we seach for a variable we shall always
take the first variable of that name that we find  ... in this way we will always use
the variable occurrence which is intended.

However, this does mean that we need to remove variables from our stack
of variables and assigned numbers once we have completed the renaming
process for a scope.

Here is a little example illustrating what we want to happen:

          Expression                      Variable/number        Counter   action
           \x. (\x.x) x (\x.x)                  []                              0         push (x,0)
	    (\x.x) x (\x.x)                     [(x,0)]                         1
	    (\x.x) x                            [(x,0)]                         1   
	    (\x x)                              [(x,0)]                         1         push (x,1)
	    x                                   [(x,1),(x_0)]                   2         lookup x
	    x1                                  [(x,1),(x_0)]                   2         pop x1 and rebind
	    \x1.x1                              [(x,0)]                         2         
	    x                                   [(x,0)]                         2         lookup x
	    x0                                  [(x,0)]                         2 
            (\x1.x1) x0                         [(x,0)]                         2         rebuild application
	    (\x.x)                              [(x,0)]                         2         push (x,2)
	    x                                   [(x,2),(x,0)]                   3         lookup x
	    x2                                  [(x,2),(x,0)]                   3         pop x2 and rebind
	    \x2.x2                              [(x,0)]                         3         rebuild application
	    (\x1.x1) x0 (\x2.x2)                [(x,0)]                         3         pop x0 and rebind
	    \x0. (\x1.x1) x0 (\x2.x2)           []                              3         done

OK so lets turn this into Haskell!!  First we need a datatype for lambda expressions:

> data Lambda v = Var v
>               | App (Lambda v) (Lambda v)
>               | Abst v (Lambda v)
>    deriving (Show,Eq)

The next problem is to walk over the expression carrying a state which is a list of
variable/integer pairs and a counter and take take the appropriate renaming action at
each stage.

First we set up the state monad:

> data SM s a = Sm (s -> (a,s))

Here we runs the state monad on a state

> runSM:: (SM s a) -> s -> (a,s)
> runSM (Sm h) s = h s

To get a monad going we need to introduce its curried kind
as a functor (recall SM:: * -> * -> * is a type constructor with two
arguments and the functor class wants a type constructor with just one
argument (SM s):: * -> *):

> instance Functor (SM s) where
>     fmap f (Sm h) = Sm (\s -> (\(a,s') -> (f a, s')) (h s))

Next one needs to define (SM s) as an applicative:

> instance Applicative (SM s) where
> --    pure:: a -> (SM s a)
>     pure a = Sm (\s -> (a,s))
> --    (<*>) ::(SM s (a->b)) -> (SM s a) -> (SM s b)
>     u <*> v
>           = Sm (\s -> (\(f,s') -> (\(a,s'') -> (f a, s'')
>                                   ) (runSM v s')
>                       )(runSM u s))

The applicative here is the state change given by running the
state change mandated by u to obtain a function, f, and a new state, s',
then one uses this state, s', to run the state change mandated by , v,
to obtain the value, a, and a new state, s''.  One returns
the state s'' paired with the evaluation of f a.

Once you have the monad this can be expressed as
       u <*> v =  do f <- u
                     a <- v
                     return (f a)

Finally, we can declare this state changing device as a monad:

> instance Monad (SM s) where
>     return a = Sm (\s -> (a,s))
>     (Sm f) >>= g = Sm (\s -> (\(a,s') -> runSM (g a) s') (f s))

At last we are ready to alpha-rename a lambda expression:

> alpha_rename:: Lambda String -> (SM ([(String,Int)],Int) (Lambda String))
> alpha_rename (Var x)
>         = do y <- Sm( \(stack,counter) -> (look_up x stack,(stack,counter)))
>              return (Var y)
> alpha_rename (App t1 t2)
>         = do t1' <- alpha_rename t1
>              t2' <- alpha_rename t2
>              return (App t1' t2')
> alpha_rename (Abst z t)
>           = do counter <- Sm(\(stack,counter) -> (counter,((z,counter):stack,counter+1))) -- pushing the variable
>                t' <- alpha_rename t
>                () <- Sm(\(stack,counter) -> ((),(mytail stack,counter))) -- popping the variable
>                return (Abst (z++(show counter)) t')

Notice the steps in which we are just changing the state in the lambda abstraction:
we have to first push a variable, use the new stack to translate the body, then pop the variable!

We need some supporting code:

> mytail:: [a] -> [a]
> mytail (x:xs) = xs
> mytail [] = []

> look_up:: String -> [(String,Int)] -> String
> look_up v [] = error "Look up on empty stack!"
> look_up v ((w,i):rest) | v==w = v++(show i)
>                        | otherwise = look_up v rest

Now let us try things out:

> t1 = runSM (alpha_rename
>          (Abst "x" (App (App (Abst "x" (Var "x")) (Var "x")) (Abst "x" (Var "x")))))
>          ([],0)