Re: Documentation Lacking for Multivar Set Comprehension

Apologies, my bad. Indeed you're right, I missed that. I have however to respectfully disagree when you say,

"the fact that one would have to look at documentation to find the order in which the bound variable declarations should be applied for set constructors suggests that the restriction in that case was a good idea"

As I mentioned, in Chapter 1 it is stated:

\A x \in S, y \in T : F means \A x \in S : (\A y \in T : F)

But it doesn't really. And I think that is the surprising fact here.

I personally looked up formal semantics (obviously not as carefully as I should have, sorry about that again) just to make sure my bug report got the right semantics. I was surprised that set comprehensions appeared to define a right to left scooping order. This is why in this post I argued it seemed unintuitive and in need of documentation. I think that a left to right scope is standard and intuitive enough that people wouldn't be having to look it up.

Indeed I agree. My point there was precisely that the latter example, for set comprehensions written with all the unions, was terrible. Much more of a pain to read and write than the one with quantifiers which by comparison is OK.

J.A.

On Wednesday, 5 September 2018 19:00:13 UTC+1, Leslie Lamport wrote:

Neither this nor the issue reported in GitHub are bugs. The semantics of quantifiers and set construction in Specifying Systems in these instances clearly state (in the phrase "the S_i lie outside the scope of the bound identifiers") that the bound variables cannot appear in the bounding set expressions. I don't find the right-hand side in the example with \E so terrible. The fact that one would have to look at documentation to find the order in which the bound variable declarations should be applied for set constructors suggests that the restriction in that case was a good idea.

Leslie

On Wednesday, September 5, 2018 at 9:16:20 AM UTC-7, Jorge Adriano Branco Aires wrote:

It appears to me that documentation for multivariable set comprehensions should be more easily accessible and detailed. My initial question was whether I could write something like:
{<<x,y>> : x \in 1..2, y \in 1..x}

The answer can of course be found in the operator semantics chapter of "Specifying Systems" (chapter, 16 page 301). But I think this feature is basic and useful enough, and the answer unintuitive enough I'd argue, that it should be, informally but clearly, documented elsewhere easily accessible, for instance Summary of TLA+.

And the answer is that rather than,
   {e : x \in X, y \in Y} == UNION {{e : y \in Y} : x \in X}
which would make the above _expression_ legal, it actually unfolds to,
   {e : x \in X, y \in Y} == UNION {{e : x \in X} : y \in Y}

The scope of variables is therefore defined from right to left. So the above should instead be written as,
{<<x,y>> : y \in 1..x, x \in 1..2}

NOTE: While this should work, it does not. The same bug affects multivar quantifiers. I reported it here https://github.com/tlaplus/tlaplus/issues/186

Back to the issue with the documentation though, other than the formal semantics in chapter 16 the only other references I found to multivar set comprehensions were:

* Summary of TLA+ (page 4):

https://lamport.azurewebsites.net/tla/summary-standalone.pdf

There's a reference to multivar in the footnotes, but doesn't clarify anything about scope.

* Specifying Systems, page 66

The semantics of multivar set comprehension are said to allow for the same generalisations as quantifiers do, without further detail. For quantifiers, "Specifying Systems", pag 14, informally defines:

\A x \in X, y \in Y : F == \A x in X : (\E y \in Y : F)

The semantics is quite clear in this case. But it is the opposite of set comprehensions with regards to scope. With quantifiers the scope is defined to from left to write. So in the above _expression_ x should be in the scope of Y.

NOTE: Again this should work but doesn't, see the above bug report.

\A x \in 1..2, y \in 1..x : TRUE

Let me end by noting that working without multivar can be a pain, more so with sets than quantifiers. Just compare the right-hand sides here,
\E x \in X, y \in Y, z \in Z : F == \E x \in X : \E y \in Y : \E z \in Z : F
and here,
{e : x \in X, y \in Y, z \in Z} == UNION {UNION {{e : x \in X} : y \in Y} : z \in Z}

The latter is quite horrible to both write and read.

So back to the point, I'd like to suggest that maybe the semantics of set comprehensions with multiple variables (and those of quantifiers for consistency) should be presented with more detail at least in the Summary of TLA+. Possibly also in the hyperbook. It should suffice to present the unfolding of a generic set comprehension with two variables, as done for quantifiers in page 14 of "Specifying Systems".