| I was referring to "intensional logics" [1]. Just as standard mathematical logic and as pointed out by Leslie, TLA+ is extensional, i.e. the meaning of TLA+ formulas is defined by the interpretations ("designations") of symbols.
Stephan
[1] https://plato.stanford.edu/entries/logic-intensional/
Functional extensionality is the property of being able to prove that two functions f , g are equal if for every x in their "domain" , f x = g x . In current dependent type languages, this is not possible to prove. There might be other more general uses of the term "extensional" and "intensional".
By "Inheritance" I meant that a property P is true for A if and only if P is true for B. I was a bit lazy.
I'm not a logician, so I don't know what Stephan means by
"extensionally" and "intensional" here. Also, I don't know what you
mean by your statement that "fairness properties on action A will also
be inherited by action B".
The meaning of any _expression_ exp in a TLA+ module is the _expression_
obtained by (recursively) replacing all defined operators in exp by
their definitions. This implies that the meaning of exp is a formula
containing only the constants and variables declared in the module and
the primitive TLA+ operators. If you define
A == defA
B == defB
where defA and defB are equivalent expressions, then replacing "A" by "B"
in any _expression_ does not change the meaning of that _expression_.
"Leslie Lamport" and "the inventor of TLA" are two different names for
me. Would you say that properties of Leslie Lamport are inherited by
the inventor of TLA? It's not how I would use the term "inherited",
but I don't claim to be an expert on the meaning of English words.
The Inventor of TLA
On Thursday, November 8, 2018 at 9:50:20 AM UTC-8, Stephan Merz wrote: TLA+ actions are defined "extensionally" by formulas evaluated over pairs of states. If two action formulas A and B are equivalent, then so are WF_v(A) and WF_v(B), and any execution satisfying one of these formulas also satisfies the other one. There is no "intensional" notion of actions that would differentiate between two equivalent action formulas.
If the distinction is important, for example for identifying the server executing the action, you will have to make the distinction explicit in your specification, for example by including the server identity as a parameter of the action.
Regards,
Stephan
> On 8 Nov 2018, at 15:30, apostolis.xekoukoulotakis wrote:
>
> Consider the case that we have two actions which are identical, they have the same conditions for triggering them and the same restrictions on the "next" step in case we don't have stuttering.
>
> From what I understand, any fairness properties on action A will also be inherited by action B. In other words, either both actions are triggered or none.
>
> Which means that from a meta-theoretic point of view, you can not attach a specific action to a specific entity, like a program, or a specific server etc.
>
> --
> You received this message because you are subscribed to the Google Groups "tlaplus" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe at googlegroups.com.
> To post to this group, send email to tlaplus at googlegroups.com.
> Visit this group at https://groups.google.com/group/tlaplus.
> For more options, visit https://groups.google.com/d/optout.
--
You received this message because you are subscribed to a topic in the Google Groups "tlaplus" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/tlaplus/TJBMk1TJ0IU/unsubscribe.
To unsubscribe from this group and all its topics, send an email to tlaplus+u...@xxxxxxxxxxxxxxxx.
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.
--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@xxxxxxxxxxxxxxxx.
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.
|