Re: [tlaplus] Re: Minor issue with TLA+ semantics to resolve

It always feels a little unsatisfying to me when the empty case has special rules.

Leslie, do you think it would be reasonable to define the empty-tuple case this way?

\A <<>> \in S: P ==
    (<<>> \in S) => P

\E <<>> \in S: P ==
    (<<>> \in S) /\ P

I believe that is consistent with the semantics given in Specifying Systems, and it seems relatively sane:

\A <<x, y>> \in S: P == \A x : \A y : (<<x, y>> \in S) => P
\A <<x>>    \in S: P == \A x :        (<<x>>    \in S) => P
\A <<>>     \in S: P ==               (<<>>     \in S) => P

Calvin

On Mon, Mar 11, 2024 at 3:50 PM Leslie Lamport <tlaplus.ll@xxxxxxxxx> wrote:

According to the grammar in section 15.1 of "Specifying Systems", \A << >> ... is syntactically incorrect. The fact that SANY accepts it is therefore a bug. If one considers

\A x_1, ... , x_n : F

to equal F if n=0, then TLC seems to correctly evaluate an _expression_ \A << >> \in S : F according to the semantics on page 294 of the book.

So, this should be reported as a very low priority SANY bug. I don't know if other parsers have the same bug.

Leslie
On Saturday, March 9, 2024 at 5:41:05 AM UTC-8 andrew...@xxxxxxxxx wrote:
Here is a very minor issue with TLA+ semantics that I think is a good exercise for the community/foundation to work to resolve if we are taking ownership of the language. I encourage everybody to read and think about this then we can have a brief discussion about it on the community meeting on Tuesday, March 12th.

The question: should this be valid TLA+ syntax?

---- MODULE Test ----
ASSUME \A <<>> \in {<<>>} : TRUE
====

Currently SANY allows the empty tuple <<>> when destructuring tuples in a quantifier. Usually the tuple is not empty and is used as follows:

---- MODULE Test ----
EXTENDS Naturals
ASSUME \A <<x, y>> \in Nat \X Nat : TRUE
====

Should SANY allow the empty tuple? To my mind it seems nonsensical, as the purpose of quantifiers is to introduce at least one new bound variable into scope. However, whether something is sensical or not depends on whether you can define a formal semantics for it. Calvin Loncaric gave a good shot at defining the semantics of the empty tuple quantifier in the original bug report thread: https://github.com/tlaplus/tlaplus/issues/888

As I understand it ideally the TLA+ syntax could be decomposed into the specific set of operations allowed by the ZFC axioms, which would constitute a full formal semantics of the language. I guess a way to do this would be translate TLA+ syntax into metamath? Perhaps a fun project for when I have a spare entire year.

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 on the web visit https://groups.google.com/d/msgid/tlaplus/e873813f-b854-40e2-b65a-e76bcaf33b65n%40googlegroups.com.