Go backward to Quantification over Flexible Variables
Go up to Top
Go forward to Quantification in TLA

Quantification over Flexible Variables

"Obvious" definition:
- sigma[[exists $x$ : $F$ ]] $<=>$ exists tau in St^infinity: (sigma =_x tau) and tau[[F]]
- Not correct since not necessarily invaraint under stuttering!
Remove stuttering steps:
- < $s$ ₀, $s$ ₁, ...> $<=>$
     if forall $n$ in Nat: $s$ _n = $s$ ₀
        then < $s$ ₀, $s$ ₀, ...>
        else if $s$ ₁ = $s$ ₀ then < $s$ ₁, $s$ ₂, ...>
           else < $s$ ₀> o < $s$ ₁, ...>
TLA = STLA + quantification.
- Existential quantifier over flexible and rigid variables.
- All TLA formulas are invariant under stuttering:
  sigma = tau $=>$ sigma[[ $F$ ]] = tau[[ $F$ ]]

Id: tla2.tex,v 1.2 96/05/06 10:48:53 schreine Exp Locker: schreine