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

[tlaplus] Minor issue with TLA+ semantics to resolve

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/29ec994d-bb29-4b4b-9925-fde5aca2de73n%40googlegroups.com.