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

*From*: Stephan Merz <stepha...@xxxxxxxxx>*Date*: Sun, 4 Sep 2016 09:38:56 +0200*References*: <b4f7d7bf-7fe5-44c3-a034-f8eca4d3a5be@googlegroups.com> <36514f56-6c98-443a-8254-3df839772bb3@googlegroups.com> <06725555-9ECB-45E5-828C-55B38453F3A5@gmail.com> <33fdac88-641b-49cf-806c-9b45b5e6a0cf@googlegroups.com>

Dear Frédéric,
In order to interpret a formula of temporal logic, you have to know which symbols are flexible (assigned values by states) and which are rigid (assigned values by the underlying first-order interpretation, independently of states). That's why in TLA+ you declare every parameter to be either a CONSTANT or a VARIABLE. If this bothers you, you are not alone, but people seem to prefer writing, say, [](x > 0) where x is a state variable rather than \A t \in Nat : x(t) > 0 as you would have to do if you expressed temporal properties in a purely first-order language. As for quantification, many modal logics only have quantification over rigid variables, such that you can write, for example, \A n \in Nat : []<>(x = n) but in TLA there is also quantification over state variables (\AA and \EE), used in particular in connection with refinement. In quantifier contexts, the kind of the bound symbol is indicated by the quantifier. Regards, Stephan [1] In theory, rigid variables can be avoided in TLA+: if all variables are assumed to be flexible, one can express that a particular variable x is rigid by writing [][FALSE]_x. However, including such a formula in every statement would be exceedingly clumsy. |

**Follow-Ups**:**Re: [tlaplus] Curious oddity***From:*fl

**References**:**Curious oddity***From:*fl

**Re: Curious oddity***From:*fl

**Re: [tlaplus] Curious oddity***From:*Stephan Merz

**Re: [tlaplus] Curious oddity***From:*fl

- Prev by Date:
**Re: [tlaplus] Curious oddity** - Next by Date:
**Re: [tlaplus] Curious oddity** - Previous by thread:
**Re: [tlaplus] Curious oddity** - Next by thread:
**Re: [tlaplus] Curious oddity** - Index(es):