3 ms·
I don't think the ordering matters. In both a' = a + b + 1 and b' = a + b + 1 the new values are on the left and the old values are on the right.
by oh_my_goodness 4y ago
I don't think the ordering matters. In both
a' = a + b + 1
and
b' = a + b + 1
the new values are on the left and the old values are on the right.
- thwayunion 4y agoSorry, I edited a bunch and the point was that the ordering can matter due to references to the new value on the rhs or due to a loop. So a' = a + b + 1 and b' = a + b + 1 should be a' = a + b' + 1 and b' = a' + b + 1 Or alternatively they can have non-primed right hand sides but occur in a loop and you have the same problem even though the rhs's are at-free. A syntactic constraint won't work unless it includes "and also no loops in at-mentioning blocks" which... well, yeah, we know how to reason about NFAs :) Sorry again, trying to make too many points with a single example
- woutervdb 4y agoCould you not tackle this problem by not allowing this mingling of 'next' and 'current' variables? You would only allow a next variable to be a computation of current variables. Not sure to what extent this would limit the application of the paradigm, though.
- aappleby 4y agoAuthor here, you are both correct and not correct - in your example the two equations represent an impossible constraint (there's an evaluation loop), thus a program (or TLA proof) containing those two statements would be invalid.
- thwayunion 4y agoRight. That’s what I meant by imposing synaptic constraints getting you back to well trodden ground.