Re: [tlaplus] Re: Subtraction has higher precedence than addition?

> 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

On Fri, Apr 11, 2025 at 8:07 AM Andrew Helwer <andrew.helwer@xxxxxxxxx> wrote:

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

On Thu, Apr 10, 2025 at 1:13 PM Andrew Helwer <andrew.helwer@xxxxxxxxx> wrote:
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

--
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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/CABj%3DxUU0z5Cym4JkzbwLDF44Fn8%2Br958nxerP-35d%3DDZyB%3DfdA%40mail.gmail.com.