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

Re: Tagged formulas

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.