SANY incorrectly allows an empty tuple of identifiers in quantifier bounds

[ahelwer]

This passes both syntactic & semantic checks:

---- MODULE Test ----
op == \A <<>> \in STRING : TRUE
====

This seems inherently nonsensical and should be disallowed at the syntax level.

Discovered during work on #882.

[lemmy]

Why is this nonsensical?

[ahelwer]

Quantifier bounds allow two types of things:

1. comma-separated lists of identifiers ex. a, b, c \in Nat
2. destructured tuple of identifiers ex. <<a, b>> \in Nat \X Nat

The purpose is to introduce at least one bound identifier into scope; an empty tuple does not do that. I also don't know what kind of set could even produce empty tuples to quantify over and destructure. Maybe {<<>>}? TLC fails on that:

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

produces:

Starting... (2024-03-08 11:44:20)
Error: Evaluating assumption line 2, col 8 to line 2, col 32 of module Test failed.
Argument mismatch in operator application.%1
Finished in 00s at (2024-03-08 11:44:20)

I guess it's possible this is a valid sentence in the language, it's hard to say. Might be a Leslie question, or fall under "silly expressions".

[ahelwer]

I just used STRING as a random plausible expression placeholder to get it to pass parsing, you can put anything there if you want. What do you think, is it a problem with SANY that it allows empty tuples of identifiers in quantifier bounds, or is it a problem with TLC that it can't evaluate \A <<>> \in {<<>>} : TRUE?

[lemmy]

Couldn't one argue that the following should then also be rejected?

\A <<i>> \in {1} \X {2} : TRUE

or

\A <<a,b,c,d>> \in {}: TRUE

[ahelwer]

I would say no, because those examples cross the line to runtime/evaluation/semantic errors instead of parse errors. The set from which the elements are drawn can be an arbitrarily complicated expression which is intractable to statically analyze, especially at the syntax/parser level. Whereas if we focus on the syntactic purpose of the quantifier bound - to introduce additional named variables into scope - it could make sense to disallow the empty tuple.

Also your second example would just be true by vacuous truth.

[lemmy]

Also your second example would just be true by vacuous truth.

Exactly, and the same can be argued for \A <<>> \in {}: TRUE.

[ahelwer]

Okay so your vote is in favor of this being a TLC bug and not a SANY bug?

[lemmy]

I suggest to bring this up at one of the monthly community calls.

[lemmy]

Also, how does TLAPS handle it?

[Calvin-L]

Let me know if I missed something, but...

I think the empty-tuple destructuring binder actually does make sense, with semantics

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

This is based on a simple "desugaring" rule. Ignoring problems with name-capture and abusing syntax:

\A <<a, ...rest...>> \in set:
  P(a, ...rest...)

is the same as

\A a \in {Head(x) : x \in set}:
  \A <<...rest...>> \in {Tail(x) : x \in set /\ Head(x) = a}:
    P(a, ...rest...)

The desugaring rule should still hold even when ...rest... is empty. That is,

\A <<a>> \in set: P(a)
<=>
\A a \in {Head(x) : x \in set}: \A <<>> \in {Tail(x) : x \in set /\ Head(x) = a}: P(a)
<=>
\A a \in {Head(x) : x \in set}: P(a)

EDIT: looking at it again, I don't think the desugaring rule I proposed is quite right. But I think it's close, and I believe we should be able to assign some meaning to \A <<>> \in set: P.

[quicquid]

I would define pattern matching a tuple as \A <<x,y>> \in S : P as \A x,y,z : (z = <<x,y>> /\ z \in S) => P. In the case of the tuple being empty, I'd end up with \A z \in S : (z = <<>> /\ z \in S) => P then. For <<>> \in S that would simplify the premise of the implication to TRUE s.t. the formula simplifies to just P. For ~(<<>> \in S) the premise would simplify to FALSE and the whole formula to TRUE.

I've tried evaluating some of these expressions in TLC. It accepts \A <<>> \in {} : FALSE and ealuates it to TRUE (which is consistent with my definition above. The expressions \A <<>> \in {1,2,3} : FALSE and \A <<>> \in {<<>>} : FALSE are accepted but not evaluated with error message The Evaluate Constant Expression� section�s evaluation failed. Argument mismatch in operator application.%1

My SANY installation is about a year old though.

P.S. I just realized the additional variable is not necessary, one could use \A x,y : (<<x,y>> \in S) => P which is much simpler.

[Calvin-L]

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

Yes, this feels right. :)

Indeed, Lamport's tech report The Operators of TLA+ (unfortunately offline at the moment) spells out essentially that same rule by example.

He gives this example on page 6:

\E <<x, y>> \in S, z, w \in T : p ==
    \E x, y, z, w : (<<x, y>> \in S) /\ (z \in T) /\ (w \in T) /\ p

So, I would infer that a 0-element tuple is just one that introduces no binders:

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

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

[Calvin-L]

Also, how does TLAPS handle it?

It looks like TLAPS does not support tuple-binding syntax with any number of arguments.

[ahelwer]

Per discussion with Lamport in the google group thread and then later in the March community call, this is being defined as a SANY bug.