On Friday, January 15, 2016 at 3:06:47 AM UTC+2, Leslie Lamport wrote:
Hi Ron,
I should point out another problematic part of what you wrote--namely:
<<s, t>>[[(CAPTURE e)']] = 1
The semantics of prime is that
<<s, t>>[[exp']] = t[[exp]].
Therefore, your equality implies that t[[CAPTURE e]] = 1. Why does
t[[x]] = 2 imply that t[[CAPTURE x]] = 1?
I think that this, too, is a matter of interpretation. If you interpret CAPTURE to be a state-level (or even a transition-level, although I see that the latter doesn't make sense) _expression_, then this is indeed problematic. But if you see CAPTURE as a syntactic operation it makes sense. So I'd like to revise my specification a bit (although it doesn't change any semantics, I believe, only interpretation), and say that: (CAPTURE e)' is a syntax which is semantically equivalent to e. As such, even though the _expression_ (CAPTURE e)' is primed, it is not a transition level _expression_ at all. So <<s, t>>[[(CAPTURE e)']] does not exist. It is s[[(CAPTURE e)']].
Perhaps it is best, then, to not describe CAPTURE as an operator at all, but as a part of the definition of the priming operator:
e' == e with all its variables primed, except those enclosed in a CAPTURE block.
Ron