Hacker News Reader

Comment by oh_my_goodness | Hacker News Reader

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.

View on HN

Sorry, 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

Could 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.

I believe this is exactly what OP meant, so likewise I don’t think ordering is a problem in his proposal.

You can allow mingling as long as you don't produce an evaluation loop. The existence of evaluation loops can be detected by the compiler (Metron does this already).

Author 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.

Right. That’s what I meant by imposing synaptic constraints getting you back to well trodden ground.

Reply on news.ycombinator.com