[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.