Minor issue with TLA+ semantics to resolve

[Andrew Helwer]

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

[Leslie Lamport]

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

[Calvin Loncaric]

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

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

[Leslie Lamport]

What you propose is exactly what I believe I was interpreting "Specifying Systems" to state the semantics to be.  I'm sorry if I didn't make it clear.  However, it's moot because those expressions are syntactically illegal.  The grammar makes 

     \A << >> \in S : F 

illegal just as it makes 

     \A \in S : F  

illegal.

Leslie

[Calvin Loncaric]

I'm glad my understanding is correct. :)

The \A \in S : F example is a good one, and I think it has convinced me that it is not useful to allow \A << >> \in S : F, even if the semantics do give it a sensible meaning.

--

Calvin

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/d03c3da3-43b8-4745-a52f-bc8707577b97n%40googlegroups.com.