Subtraction has higher precedence than addition?

[Andrew Helwer]

While writing a parsing tutorial for TLA+ I came across something weird. Per page 271 of Specifying Systems, the addition operator in TLA+ has precedence 10 and the subtraction operator has precedence 11. This means that the expression a + b - c is parsed (a + (b - c)) instead of the usual PEMDAS-style ((a + b) - c) we learned in grade school. I looked in SANY and confirmed the relative precedence is there as well. Oddly, multiplication and division have the same precedence (although only multiplication is associative; a / b / c will be a parse error).

Does anybody know why this design decision was made? Over fields like integers and reals a - b is the same as a + -b, so a + b - c becomes (a + (b + -c)), a kind of weird right-associative addition. Since addition is commutative over the integers and reals this should never matter (as in the final value of all ways of parsing the expression should all be the same), but we can actually redefine addition and subtraction in TLA+ so it's possible they could be defined over a non-abelian group where this leads to unexpected behavior. I can't think of an example off the top of my head though.

Andrew Helwer

[Andrew Helwer]

Consulted with a math friend about this and they said that by convention + and - are only used over abelian groups; if you're doing non-abelian things you probably use different operator symbols. So it's unlikely for this to lead to unexpected behavior.

Andrew Helwer

[Calvin Loncaric]

> it's possible they could be defined over a non-abelian group where this leads to unexpected behavior. I can't think of an example off the top of my head though.

TLC's implementation of integers might qualify, since it uses 32-bit integers with overflow checking. You might expect this would work:

2^30 + (-2^30) - (2^30 + 1)

because (2^30 + (-2^30) = 0). But TLC reports an error because it evaluates the subtraction first:

(tla+) 2^30 + (-2^30) - (2^30 + 1)

Error evaluating expression: '2^30 + (-2^30) - (2^30 + 1)'
tlc2.tool.EvalException: Overflow when computing -1073741824-1073741825

Adding parentheses around the first addition silences the error:

(tla+) (2^30 + (-2^30)) - (2^30 + 1)
-1073741825

...but even so, I think I agree with your friend that this doesn't matter in practice. The overflow behavior is a limitation/quirk of TLC, and not a property of true TLA+ integers.

--

Calvin

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/CABj%3DxUU0z5Cym4JkzbwLDF44Fn8%2Br958nxerP-35d%3DDZyB%3DfdA%40mail.gmail.com.