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

Re: Tagged formulas

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.