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
And
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.
Ron
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
.
.
.