Substitution and free variable capture

A tiny language of expressions

n : num

x : var ::= x,y,...

e : exp ::= n | x | (e1,e2) | e1 e2 | fn x => exp


Substitution:

   [e2/x]e1   -- substitute e2 for free occurrences of x in e1

E.g.

   [3/x](plus x 5) --> plus 3 5

   [(plus x)/y] (y 3) --> (plus x) 3

   [(plus x)/y] ((fn z => y (y z)) (y 4)) 
      --> (fn z => plus x (plus x z)) (plus x 4)
      
      if x = 2, this evaluates to: 
         [2/x](fn z => plus x (plus x z)) (plus x 4) =
         (fn z => plus 2 (plus 2 z)) (plus 2 4) ->
         (fn z => plus 2 (plus 2 z)) 6 ->
         plus 2 (plus 2 6) ->
	 plus 2 8 ->
	 10
         

   [(plus x)/y] ((fn x => y (y x)) (y 4))
      --> (fn x => plus x (plus x x) (plus x 4)
 
      if x = 2, this evaluates to: 
         (fn x => plus x (plus x x)) (plus 2 4) ->
         (fn x => plus x (plus x x)) 6 ->
         plus 6 (plus 6 6) ->
         plus 6 12 ->
         18

But we would expect 
   
   (1)  (fn z => y (y z)) and 
   (2)  (fn x => y (y x))

to be equivalent, because the name of a locally bound
variable doesn't matter.

The problem is that when we substitute "plus x" for y
in (2) we get

   (3)  (fn x => plus x (plus x x))

and the "x" in "plus x" has been captured by the binder
"fn x =>".  This "free variable capture" should not be
allowed.

To avoid it, we can, if necessary, change the name of the
bound variable in the target expression before doing the
substitution:

   (fn x => y (y x))   --->  (fn z => y (y z))

This is called "alpha-conversion", and two expressions 
that differ only in the names of their bound variables are
called "alpha-equivalent".

Here is how we would implement this in SML: 

<subst.sml>