Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
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.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.