Free Variable Escape in Complete Laziness

Here is a section of a message I sent to Francois-Regis Sinot regarding his paper 
Complete Laziness: A Natural Semantics
http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/sinot-wrs07.pdf
---------------

I have simplified the problem down to this expression:

(\z. (\x. \y. x) (\w. z)) I I I

Where I is the identity function.  Preprocessing, this translates to (with some manual simplifications):

let Z1(z) = (let Z4(z) = \w. z in (let Z3(z,x) = \y. x in \x2. Z3(z,x2)) Z4(z)) in (\z0. Z1(z0)) I I I

The reduction sequence as I understand it follows.  Forgive the indentation style -- it differs from
your paper.  The difference is essentially tail call optimization (I didn't indent the final sub-reduction
of each rule).

|- let Z1(z) = (let Z4(z) = \w. z in (let Z3(z,x) = \y. x in \x2. Z3(z,x2)) Z4(z)) in (\z0. Z1(z0)) I I I
Z1(z) -> (let Z4(z) = \w. z in (let Z3(z,x) = \y. x in \x2. Z3(z,x2)) Z4(z)) |- (\z0. Z1(z0)) I I I
 Z1(z) -> (let Z4(z) = \w. z in (let Z3(z,x) = \y. x in \x2. Z3(z,x2)) Z4(z)) |- (\z0. Z1(z0)) I I
 Z1(z) -> (let Z4(z) = \w. z in (let Z3(z,x) = \y. x in \x2. Z3(z,x2)) Z4(z)) |- (\z0. Z1(z0)) I
 Z1(z) -> (let Z4(z) = \w. z in (let Z3(z,x) = \y. x in \x2. Z3(z,x2)) Z4(z)), z0 -> I |- Z1(z0)
  z0 -> I |- let Z4(z) = \w. z in (let Z3(z,x) = \y. x in \x2. Z3(z,x2)) Z4(z)
  z0 -> I, Z4(z) -> \w. z |- (let Z3(z,x) = \y. x in \x2. Z3(z,x2)) Z4(z)
   z0 -> I, Z4(z) -> \w. z |- let Z3(z,x) = \y. x in \x2. Z3(z,x2)
   z0 -> I, Z4(z) -> \w. z, Z3(z,x) -> \y. x |- \x2. Z3(z,x2)
  z0 -> I, Z4(z) -> \w. z, Z3(z,x) -> \y. x |- (\x2. Z3(z,x2)) Z4(z)
  z0 -> I, Z4(z) -> \w. z, Z3(z,x) -> \y. x, x2 -> Z4(z) |- Z3(z,x2)
   z0 -> I, Z4(z) -> \w. z, x2 -> Z4(z) |- \y. x
  z0 -> I, Z4(z) -> \w. z, Z3(z,x) -> \y. x, x2 -> Z4(z) |- \y. x2
**********************************************************************************
 Z1(z) -> \y. x, z0 -> I, Z4(z) -> \w. z, Z3(z,x) -> \y. x, x2 -> Z4(z) |- \y. x2
**********************************************************************************
 Z1(z) -> \y. x, z0 -> I, Z4(z) -> \w. z, Z3(z,x) -> \y. x, x2 -> Z4(z) |- (\y. x2) I
 Z1(z) -> \y. x, z0 -> I, Z4(z) -> \w. z, Z3(z,x) -> \y. x, x2 -> Z4(z), y -> I |- x2
 Z1(z) -> \y. x, z0 -> I, Z4(z) -> \w. z, Z3(z,x) -> \y. x, x2 -> Z4(z), y -> I |- Z4(z)
  Z1(z) -> \y. x, z0 -> I, Z3(z,x) -> \y. x, x2 -> Z4(z), y -> I |- \w. z
 Z1(z) -> \y. x, z0 -> I, Z4(z) -> \w. z, Z3(z,x) -> \y. x, x2 -> Z4(z), y -> I |- \w. z
 Z1(z) -> \y. x, z0 -> I, Z4(z) -> \w. z, Z3(z,x) -> \y. x, x2 -> \w. z, y -> I |- \w. z
Z1(z) -> \y. x, z0 -> I, Z4(z) -> \w. z, Z3(z,x) -> \y. x, x2 -> \w. z, y -> I |- (\w. z) I
Z1(z) -> \y. x, z0 -> I, Z4(z) -> \w. z, Z3(z,x) -> \y. x, x2 -> \w. z, y -> I, w -> I |- z

At which point the execution is stuck because there is no binding for z.

The problem becomes apparent at the marked line, when we are finished evaluating Z1
with z free, but x2 appears to the right of the turnstile, and x2 references a free z.