# Re: [tlaplus] How to determine an Action execution.

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.

On Fri, Nov 9, 2018 at 10:09 AM Stephan Merz <stepha...@xxxxxxxxx> wrote:
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/

On 8 Nov 2018, at 21:06, Apostolis Xekoukoulotakis <apostolis.xe...@xxxxxxxxx> wrote:

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.

On Thu, Nov 8, 2018 at 9:15 PM Leslie Lamport <tlapl...@xxxxxxxxx> wrote:
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.

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