How to determine an Action execution.

[apostolis.xe...@gmail.com]

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.

[Stephan Merz]

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

> --
> 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...@googlegroups.com.
> Visit this group at https://groups.google.com/group/tlaplus.
> For more options, visit https://groups.google.com/d/optout.

[Leslie Lamport]

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.

[Apostolis Xekoukoulotakis]

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

https://ncatlab.org/nlab/show/function+extensionality

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.

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...@googlegroups.com.

[Stephan Merz]

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/

To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com.

[Apostolis Xekoukoulotakis]

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.

1. http://www.jimpryor.net/teaching/courses/mind/notes/scientificIDs.html

[Jorge Adriano Branco Aires]

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.

[Leslie Lamport]

This discussion of intension and extension may be fine, but I'm
concerned that an engineer reading it might get the idea that 
TLA+ has subtle problems and is difficult to understand.  So, I
will explain the issue being discussed in simple terms that an

engineer will understand.

TLA+ is a precise, formal mathematical language.  As far as I can

tell, mathematicians have no standard way of formalizing the concept
of a definition.  Some logicians formalize the definition A == 2 by
saying that it adds the axiom A = 2.  I found it simpler to make
definition a syntactic concept in TLA+, so a defined operator is
essentially a macro.  This implies that the definition A == 2 means
that one can replace A by 2 or vice versa in any expression without
changing the meaning of that expression.  Thus,

(1) if A == 2 and B == 2, then A = B is true and any A appearing

    in an expression can be changed to B (and vice-versa) without
    changing the meaning of the expression.

Similarly, 

(2) If A(x) == 2*x and B(x) == 2*x, then for any expression exp,
    A(exp) can be replaced by B(exp) (and vice versa) in any
    expression without changing the meaning of that expression.

Note that in (2), I did not write A = B because that's not a legal
TLA+ expression.  To keep TLA+ as simple as possible, equality of
operators is not expressible in it.

Also, A(x) == 2*x and A(y) == 2*y define the same operator A,
so (2) is true if the definition of A is replaced by A(y) = 2*y.

Note: A TLA+ recursive definition is shorthand for its actual
definition.  For example, the recursive function definition

   f[n \in Nat] == IF n = 0 THEN 1 ELSE n * f[n-1]

is shorthand for the actual definition

   f == CHOOSE f : f = [n \in Nat |-> IF n = 0 THEN 1 ELSE n * f[n-1]]

The actual definition of a recursively defined operator is quite
complicated, but it defines the operator to have the expected meaning
on values of its arguments for which the recursion terminates.

-------

Let me give the name "definitional equivalence" to the general
property of definitions illustrated by (1) and (2).  Definitional
equivalence is similar to the property of equality called
"substitutivity".  Substitutivity asserts that exp1 = exp2 implies
that replacing exp1 by exp2 (or vice versa) in any expression leaves
the value of the expression unchanged.  Definitional equivalence holds
for all definitions and expressions of TLA+.  However, substitutivity
holds only for ordinary mathematics, which is formalized by the subset
of TLA+ obtained by eliminating the action operators and temporal
operators in Tables 3 and 4 (page 269) of "Specifying Systems".  The
full TLA+ language expresses a temporal logic, and substitutivity does
not hold in temporal logic.  This complicates writing proofs of
liveness properties, but it is of no concern to users of TLA+ who
don't write proofs.

Leslie