[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*From*: Calvin Loncaric <c.a.loncaric@xxxxxxxxx>*Date*: Mon, 11 Mar 2024 17:01:52 -0700*References*: <29ec994d-bb29-4b4b-9925-fde5aca2de73n@googlegroups.com> <e873813f-b854-40e2-b65a-e76bcaf33b65n@googlegroups.com> <CABf5HMj4sWzphzEuLvr_cYOjah520-Exh7hROU7eySSszf7XBQ@mail.gmail.com> <d03c3da3-43b8-4745-a52f-bc8707577b97n@googlegroups.com>

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

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

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 : Fillegal just as it makes\A \in S : Fillegal.Leslie--On Monday, March 11, 2024 at 4:32:57 PM UTC-7 Calvin Loncaric wrote: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`

--CalvinOn Mon, Mar 11, 2024 at 3:50 PM Leslie Lamport <tlapl...@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 : Fto 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.LeslieOn 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 NaturalsASSUME \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/888As 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+u...@xxxxxxxxxxxxxxxx.

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/e873813f-b854-40e2-b65a-e76bcaf33b65n%40googlegroups.com.

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/d03c3da3-43b8-4745-a52f-bc8707577b97n%40googlegroups.com.

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/CABf5HMjYNnrD%3DAxpz_42eQAKr7TXovcbMbimAW75Tohm%3DU1p0w%40mail.gmail.com.

**References**:**[tlaplus] Minor issue with TLA+ semantics to resolve***From:*Andrew Helwer

**[tlaplus] Re: Minor issue with TLA+ semantics to resolve***From:*Leslie Lamport

**Re: [tlaplus] Re: Minor issue with TLA+ semantics to resolve***From:*Calvin Loncaric

**Re: [tlaplus] Re: Minor issue with TLA+ semantics to resolve***From:*Leslie Lamport

- Prev by Date:
**Re: [tlaplus] Re: Minor issue with TLA+ semantics to resolve** - Next by Date:
**[tlaplus] Strong fairness** - Previous by thread:
**Re: [tlaplus] Re: Minor issue with TLA+ semantics to resolve** - Next by thread:
**[tlaplus] PlusCal issue** - Index(es):