Discarded prototype TLA+ syntax: using @ inside proofs?

[Andrew Helwer]

This is probably just another episode of me stumbling across and exhuming some long-discarded prototype syntax, but I wanted to make sure:

There are several places in the tools where there is a reference to use of the @ symbol in a proof context. We are all familiar with @ as used in [f EXCEPT ![n] = @ + 1], for example. Another place where you can use @, not as familiar, is in subexpressions like op!<<!@. If you don't know what subexpressions are then worry not, Lamport views them as a mistake and hopes they get removed from the language. My understanding of the meaning of @ in subexpressions is that they let you turn an unbound quantifier like op == \A x : f[x] into the operator op(x) == f[x] by going op!@. Turn unbound quantifiers into LAMBDAs, basically. But anyway, back on topic - is there yet another (deprecated?) use of @ in the language?

The first place I noticed this was in the TLAPM parser; the "At" expression variant takes a boolean parameter, with the curious comment:

`true` means `@` from `EXCEPT`, and
`false` means `@` from a proof step.

I didn't understand what this was about, thinking perhaps EXCEPT statements require special handling when used inside proofs. As far as I can tell the only attempt to construct an "At true" variant in the TLAPM parser is commented out, so the boolean parameter might just be some zombie thing.

Then I was looking at how subexpressions are implemented in SANY, and found this curious comment:

An assertion or ASSUME/PROVE step is represented as an
ordinary theorem, so the object's getTheorem() node
returns the ExprNode or AssumeProveNode that is the
assertion made by the step.  The object's isSuffices()
method returns false.

As a special case, a step of the form "@ infixop expression"
has as its theorem an OpApplNode whose first argument is an
OpApplNode with operator $Nop and argument (a reference to)
the right-hand-side expression of the previous step.

So here's another hint about something involving @ and proofs, this time having to do with the rather complicated ASSUME/PROVE construct. ASSUME/PROVE blocks can include nested ASSUME/PROVEs which can be labelled, and labels are types of subexpressions, so @ having some meaning in the context of ASSUME/PROVE blocks is not unthinkable (also, "$Nop" is what SANY uses as the subexpression opcode, don't ask why).

Does anybody know more about this topic? Is this some deprecated syntax like temporal ASSUME/PROVE or does it still exist in some form in the language?

Thanks!

Andrew Helwer

[Stephan Merz]

Hi Andrew,

the uses of @ (mainly) in proofs are described in the TLA+2 document [1].

(i) Section 6.5 (p.16) is about using subexpression names as operators (the construction that you allude to).

(ii) Section 7.4.3 (p.24) is about using @ to name the right-hand side of the expression on the right-hand side of the previous proof step. This allows you to write chains of (in)equations such as

<X>1. a <= b

<X>2. @ = c

<X>3. @ < d

<X>4. a < d    BY <X>1, <X>2, <X>3

Personally, I never use (i) but I find (ii) quite useful.

Stephan

[1] https://lamport.azurewebsites.net/tla/tla2-guide.pdf

--
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 visit https://groups.google.com/d/msgid/tlaplus/CABj%3DxUVfndQ5OYzaUi7VZnT_KBhQLSAZTo7YJnMOyhPs1kFoxQ%40mail.gmail.com.

[Andrew Helwer]

Thanks, Stephan! Wow, after all these years parsing TLA+ I am still learning about new corners of the language.

Andrew

To view this discussion visit https://groups.google.com/d/msgid/tlaplus/87F3F9EA-FE7A-4425-9C4F-E0FC4C5159FD%40gmail.com.