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

Re: [tlaplus] Tagged formulas

Sorry for being late to this discussion. I think that basically what you want is

Capture(e) == CHOOSE x : x = e

with the additional effect that the _expression_ Capture(e) is considered as a level-0 _expression_ by SANY. (If you try writing Capture(x')' for the above definition where x is a state variable, SANY will complain about level-incorrectness.)

It seems to me that this wouldn't cause problems semantically. In fact, the more general solution would be to consider any _expression_

  CHOOSE x : P

to be of level 0, whatever the level of P (currently, P must be of level <= 2, but even an extension to CHOOSE expressions for temporal formulas should be acceptable).


On 14 Jan 2016, at 11:07, Ron Pressler <r...@xxxxxxxxxxxxxxxxxxx> wrote:

On Thursday, January 14, 2016 at 1:56:03 AM UTC+2, Leslie Lamport wrote:
If you can precisely specify the meaning of Capture, we might consider it.  That is, for any _expression_ e, define the meaning of Capture(e) in terms of the meaning of e.  The meaning of an action-level _expression_ e is a mapping from pairs of states to values.  I have no idea how to do that. 

I'll try:
Given _expression_ e of level 0, 1, or 2, CAPTURE e is level-0 _expression_ having the same value as e.
In other words, CAPTURE e is always equal to e, except that (CAPTURE e)' is also equal to e.

So (CAPTURE e)' is level correct and has level 2 iff e is level-correct and has level at most 2.

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


    e == x + x'   |-   <<s, t>>[[e]] = 3, e' is illegal, <<s, t>>[[CAPTURE e]] = 3 and <<s, t>>[[(CAPTURE e)']] = 3

If that somehow poses a problem, e could be limited to levels 0 and 1 only (undefined for 2 and up, so that CAPTURE e could be made level-incorrect if e has level 2 and up).

This operator adds symmetry: Currently, any level-0 _expression_ e could be made level 1 with (e \cup es) where [](es = {}), but there's no way of turning a level-1 _expression_ back to a level-0.


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...@xxxxxxxxxxxxxxxx.
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.