A free variable occurs in a rule definition of a residual program

[hirrolot]

I've tried to supercompile the following code (with spsc-lite-js):

g1(C(x)) = B();
g2(B(), x) = x;

g2(g1(x), x)

And got the following output:

g21(C(v_1)) = x;

g21(x)

As you can see, the variable x occurs in the definition of g21, while being unbound. If I remember correctly, the SLL language this project attempts to implement prohibits this kind of situation.

Is this is a bug or a "feature"?

[sergei-romanenko]

Certainly, this is a bug... Perhaps, the process tree generated is correct, and the bug is in residuator?

[hirrolot]

The initial reason why I wrote this code is that I doubted the implementation of drive. In spsc-lite-js/spsc.js, when we're unfolding a g-function call with a variable x as the first argument, we're essentially performing a substitution on x with a freshly generated constructor. But this is not quite how normal-order reduction is presented by Gluck & Sorensen. From "A Roadmap to Metacomputation by Supercompilation":

Here, we're interested in the rule (5). The substitution happens for the whole expression, not just a g-function call. This means that, in my code snippet, we're substituting the first x when unfolding g1(x), but we're ignoring the second x (the second argument of g2).

This might be the reason for the bug.

[hirrolot]

One interesting fix would be to implement variables as mutable cells.

Each variable would hold a reference to a mutable memory location. Whenever we need to perform substitution on a variable, we just mutate its contents, and it's automatically "updated" in all places.

However, one caveat is that we would need to perform deep cloning whenever we return multiple items from drive. For SLL, this is only rule (5). This is to ensure that if we mutate a variable from some term, this wouldn't affect the other terms (erroneous sharing).

But in our case, probably it would be easier to just ~maintain a map~ in drive. After we recursively call drive on the first argument (the default case), we need to perform accumulated substitution for the rest of the arguments. EDIT: it might make sense to just use a returned contraction for the substitution.

[hirrolot]

Alright! It seems I've fixed the bug for the JS implementation. Now the code supercompiles to:

g21(C(v_1)) = C(v_1);

g21(x)

Leaving this issue open as the bug might be present in other implementations as well.

[sergei-romanenko]

And got the following output:

g21(C(v_1)) = x;

g21(x)

Is this is a bug or a "feature"?

Oh! I've found this wonderful "feature" also in spsc-lite-julia!