I think this is getting unnecessarily complicated. The terms "extensional" and "intensional" in the answers above refer to a property of the language, not of sentences (yes your source does it, it can be done, but it's just complicating things here).
Simply put, an action is defined by the results it provides for particular instances of its primed and unprimed variables. That's it. There is no other property that matters. Two actions are the same if they provide the same results for the same "inputs" (instantiations of primed and unprimed variables). It doesn't matter how you express these actions, it doesn't matter if you gave them a name in a definition or what name you used, it doesn't matter if your computer takes longer to evaluate on action then the other.
So if you want two write two actions A and B that are different, then there has to be some pair of states (current state and next state) for which both actions provide a different result.
So for instance, if A and B represent actions by different servers, maybe you should have
A == some_formula /\ server' = "A"
B == some_formula /\ server' = "B"
Or perhaps more sensibly, maybe you want parametrisation over servers,
Action(s) == some_formula /\ server' = s
Not saying this necessarily is how you want to proceed. Just making it explicit that you need to model the difference you want to observe.
PS:
Regarding the generic concept of extensionality / intensionality. To talk about it you need to have some function like objects that can be applied to things, and what matters is if those objects are fully defined by the results of such applications, or if they have some other inherent properties that distinguish them.
This notion of "function like objects" that you apply to things, can show up in different "flavours".
- Usual function syntax. A function "f(x) = 2*(x+3)" is applied to "a" via "f(a)"
- Context holes. An _expression_ with holes "C = 2* ( _ + 3)" can have its hole filled with "a" via "C[a]"
- Substitution. An _expression_ "e = 2*x+3" can have its free variable substituted with "a" via a "e[x/a]"
In this discussion it's useful to think of the 3rd kind. The extensional nature of actions has to do with the results said actions return under specific "current state" and "next state". These states provide you with an instantiation via substitution of values for primed and unprimed variables.
I think this observation might be useful because I got the impression your answer seemed a bit confused by different notions of "application".
J.A.
On Sunday, 11 November 2018 06:45:59 UTC, Apostolis Xekoukoulotakis wrote:
Ok, let me try to learn something.
According to Jim Pryor(1) ,
"The extension of a term is the set of things which it picks out in the world, as the world actually is."
The terms "Leslie Lamport" and "the inventor of TLA" have the same extension , because both of them refer to the same person.
"A sentence fragment "___ is such-and-such" counts as extensional
just in case filling in the blank with different terms having the same
extension will always result in sentences with the same truth-value."
In our case, the sentence " __ is the winner of the 2013 Turing award." is extensional. Both "Leslie Lamport" and "the inventor of TLA" have the same truth value.
On the other hand, the sentence "It is necessary that __ is a man." is intensional becuase the inventor of TLA could have been a woman.
Now, to do the same for TLA, I would say that the extension of a tla _expression_ is the one we get by replacing all defined operators by their definitions.
Since the truth value of an _expression_ is determined by the truth value of the primitive operators and variables , constants , two expressions with the same extension have the same truth value.
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...@googlegroups.com.
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...@googlegroups.com.
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 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...@googlegroups.com.
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.