[amluto]

It says:

> Notice also how, in some steps, lambdas were applied to arguments that appeared outside of their bodies. This is all fine, and, in the end, the result is correct.

But one of the example steps is this transformation:

    dup a b = {x0 x1}
    dup c d = {y0 y1}
    (Pair λx0(λy0(Pair a c)) λx1(λy1(Pair b d)))
    ------------------------------------------------ Dup-Sup
    dup c d = {y0 y1}
    (Pair λx0(λy0(Pair x0 c)) λx1(λy1(Pair x1 d)))

I think I’m missing a subtlety. This step substitutes the a/b superposition into the lambdas, but I don’t see how it knows the the x0 goes into the first lambda and the x1 goes into the second one. After all, in HVM bizarro-land, lambda arguments have no scope, so the reverse substitution seems equally plausible and even syntactically valid:

    (Pair λx0(λy0(Pair x1 c)) λx1(λy1(Pair x0 d)))

This substitution produces two magically entangled lambdas, which seems fascinating but not actually correct. How does the runtime (and, more generally, the computational system it implements) know in which direction to resolve a superposition?

[LightMachine]

`dup a b = {x0 x1}` will just substitute `a` by `x0` and `b` by `x1`, no matter where `a` and `b` are. So, if you apply that, verbatin, to:

    (Pair λx0(λy0(Pair a c)) λx1(λy1(Pair b d)))

You get:

    (Pair λx0(λy0(Pair x0 c)) λx1(λy1(Pair x1 d)))

Does that make sense?