Re: [tlaplus] Rigid and flexible variables

[Stephan Merz <stepha...@xxxxxxxxx>]

> On 27 Nov 2016, at 19:09, 'fl' via tlaplus <tla...@xxxxxxxxxxxxxxxx> wrote:
> 
> 
> I've just read Leslie Lamport's "Temporal Logic of Actions" ACM Transactions on Programming Languages and Systems, 1994:
> 
> http://dl.acm.org/citation.cfm?id=177726
> 
> http://research.microsoft.com/en-us/um/people/lamport/pubs/lamport-actions.pdf
> 
> (I suppose this article is an exact description of what is implemented currently by TLA+ and TLAPS).
> 

The TOPLAS paper describes the temporal logic TLA, whereas the specification language TLA+, supported by TLC and TLAPS, combines (Zermelo-Fraenkel) set theory for data structures and TLA for specifying behavior. 

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

Yes, variables introduced by TAKE are rigid. TLAPS has no support so far for the quantifiers \AA and \EE.

Best regards,

Stephan