Re: Tagged formulas

On Friday, January 15, 2016 at 2:37:02 AM UTC+2, Leslie Lamport wrote:

Hi Ron,

First of all, you are proposing to add a fundamentally new kind of
operator to TLA (and not just to TLA+). In 25 years, no one to my
knowledge has seen any need for such an operator. So, I'm not about
to add it because one user finds that it makes writing his specs more
convenient.

Not only that, but a novice user :) Which is why I'm not saying TLA+ should have the operator, only proposing that it may. In addition, there are workarounds -- e.g. instead of:

VARIABLE x, y

Foo(t) == t + x

and then

Foo(3) = 3 + x

Foo(CAPTURE y)' = y + x'

we can define:

Foo(t) == t + x

Foo1(t) == t + x'

which is what I did on several occasions.

But as to it being a new kind of operator, I think that might depend on interpretation. It could be interpreted to be no more than a syntactic form to delimit the scope of the priming operator. The motivation is that the use of the priming operator can be surprising and puzzling, and CAPTURE could possibly make the intent of the spec clearer by "taming the prime".

Also, I still don't understand the semantics of CAPTURE. Your write

    For example, suppose x is a vatiable s.t. s[[x]] = 1 and t[[x]] = 2, then

    e == x   |-   s[[e]] = 1, <<s, t>>[[e']] = 2, s[[CAPTURE e]] = 1,
    <<s, t>>[[(CAPTURE e)']] = 1, s[[CAPTURE e']] = 2

The last equality, s[[CAPTURE e']] = 2, makes no sense. How can the
value of a formula that doesn't mention t depend on the value of x in
state t? Is it because "t" is the next letter in the alphabet after "s",
so t[[CAPTURE e']] will equal the value of x in whatever state I decide
to name "u"?

Right. So it may be better to limit CAPTURE e for expressions e of level at most 1. I wasn't sure whether it was useful at all to have CAPTURE work on level-2 expressions, but I thought I could give it meaningful semantics. But it doesn't make sense.

Ron