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

Rigid and flexible variables

I've just read Leslie Lamport's "Temporal Logic of Actions" ACM Transactions on Programming Languages and Systems, 1994:



(I suppose this article is an exact description of what is implemented currently by TLA+ and TLAPS).

And I just wonder: when in a proof the goal is:

   \A x \in A : P (A a set, P an action),

and then you have the step:

   TAKE x \in A,

what is the status of x?

I bet for a rigid variable (see p. 6). (The other possibility would be a variable neither rigid nor flexible but I don't think so.)

I think the "only" difference between a flexible and a rigid variable only consists in their semantic interpretation (p. 34)
"sequences of state functions" versus "elements of Val" and in the way of quantifying them: \AA \EE versus \A \E.