while_correction behavior

[nkrusch]

We should discuss the behavior of this method:

https://github.com/seiller/pymwp/blob/4250ab22bab7d7057c4949712ca35b9e76b50fd5/pymwp/relation.py#L130-L136

This is the only place where i may be introduced. It is run on each while loop node during the analysis (after computing fixpoint).

Some open questions:

• What I don't get is that it seems that we are applying that correction to all the coef., and not only to the ones on the diagonal. What am I missing?

• I think that if the coefficient is not m (meaning it is either 0, w, p or i), then we need to change it to i: as of now, I don't think that's what we do.

• this expression is totally different if you change parentheses:

if mon.scalar == "p" or (mon.scalar == "w" and i == j)

to

if (mon.scalar == "p" or mon.scalar == "w") and i == j

the latter checks for diagonal scalars only.

[aubertc]

Remember, the original rules are

which seems to imply that "anything that isn't m" is problematic.

[nkrusch]

"anything that isn't m" is problematic

Seems to me W says "diagonal all m" and "for all i,j cannot have p"?

That would be "no p anywhere" which matches the expression in the code.

But can we not apply L if there is p somewhere? Or when we analyze while we must always use rule W? When we analyze by hand we use rule L for loops. Implementation always uses W.

[aubertc]

"anything that isn't m" is problematic

Seems to me W says "diagonal all m" and "for all i,j cannot have p"?

Sorry, I meant on the diagonal. You are correct that p can be problematic anywhere (and so is i, but I guess we won't replace i with itself if it occurs somewhere) when applying W.

[seiller]

I think while loops should be analysed with W each time, and for loops can be analyzed with L. I think the implicit difference is that when entering a for we know from the start how many iterations we will do, so we can accept more behaviors than in a while.

[aubertc]

Briefly, the condition if mon.scalar == "p" or (mon.scalar == "w" and i == j) actually covers all the cases we need for the W rule:

• M^* is defined as 1 ⊕ M ⊕ M^2 ⊕ …, so there cannot be any 0 on the diagonal,
• The W rule says that a p anywhere (including but not limited to the diagonal) is problematic,
• Hence, the only thing that remains to check on the diagonal only is the presence of w.

(Taking into account the fact that replacing an i with an i is useless…)