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

*From*: Ioannis Filippidis <jfili...@xxxxxxxxx>*Date*: Tue, 1 Nov 2016 17:24:39 -0700 (PDT)*References*: <28f8d422-17ee-4394-86c1-b9741cda838b@googlegroups.com> <013E753A-A292-4ED6-A2A4-5D9F8356B6E2@gmail.com>

Thank you for the comments, Stephan.

Indeed, the TOPLAS paper [3] does not define the operator `\sim_x`,

which is what I intended to allude to with

"using the notation \sim_x to encapsulate the first two conjuncts from Eq.(49)".

Eq.(49) reads:

sigma[[ \EE x : F ]] ==

\E rho, tau \in St^\infty :

/\ Natural(sigma) = Natural(rho)

/\ rho =_x tau

/\ tau[[F]]

Using the predicate `IsABehavior`, the above can be written as:

sigma[[ \EE x : F ]] ==

\E tau:

/\ IsABehavior(tau)

/\ \E rho:

/\ IsABehavior(rho)

/\ Natural(rho) = Natural(sigma)

/\ rho =_x tau

/\ tau[[F]]

The older "definition" of `\sim_x` was extracted from Eq.(49),

by comparing to [1, p.316]:

sigma |= \EE : F ==

\E_{behavior} tau:

/\ sigma \sim_x tau

/\ tau |= F

The conjunct:

/\ \E rho:

/\ IsABehavior(rho)

/\ Natural(rho) = Natural(sigma)

/\ rho =_x tau

serves the purpose of the conjunct `sigma \sim_x tau`.

Depending on how `\sim_x` is defined, these two expressions can

be equal or not, even though what `\EE` means can remain unaffected.

This note started as an observation about how `\EE` is defined.

In the updated errata, it seems to me that `\sigma[[ \EE x: F ]]` is

defined equivalently to TOPLAS. So, I described the remaining comments

as related to the "definition" of `\sim_x`.

The two definitions of `\EE` appear to be equisatisfiable with respect to `tau`,

but satisfied by possibly different collections of behaviors `tau`.

So, which of the two expressions is used as conjunct above does not

appear to affect `\EE`.

(Sketch: A behavior `tau` that satisfies the old definition satisfies the new one,

and a `tau` that satisfies the new definition may be too short for the old one,

but can always be elongated by stuttering,

in order to obtain another `tauhat` that satisfies the old definition.)

In words (based on Stephan's phrasing):

The old definition "squeezes, stretches, overwrites x" to obtain tau from sigma.

The new definition "overwrites x, squeezes, stretches, overwrites x" to

obtain tau from sigma.

If the operator `\sim_x` is used elsewhere in place of

`(Natural(sigma) = Natural(rho)) /\ (rho =_x tau)`,

then there could be a change in meaning.

I do not know whether `\sim_x` has been used in this way.

Remark: The attached TLA+ file says "The _expression_ $\rho \sim \sigma$ from [3]".

No `\sim` appears in [3]. The symbol `\sim` refers to stuttering as defined

on p.904 "... invariant under stuttering, which means formally that

Natural(sigma) = Natural(tau) implies ...", i.e., `\sim` stands for stutter

equivalence, defined as `Natural(sigma) = Natural(tau)`.

An earlier definition of stutter equivalence [7, p.7 in DEC report] used `\simeq`.

Thank you for mentioning [6]. The definition of `\simeq_x` appears

to me equivalent to the updated `\sim_x`. A rough comparison:

`sigma \simeq_x tau == \E_{behavior} sigma', tau': sigma ~ sigma' =_x tau' ~ tau`,

and the updated definition of `\sim_x` is "close" to (but different from):

`\E_{behavior} sigma', tau': sigma =_x sigma' ~ tau' =_x tau`.

Remark: Some names I've used for operators in the attached TLA+ file

almost coincide with the terminology used in [6],

for example `SimUpToVar` and "similar up to v" [6, p.417].

[1] Leslie Lamport,

"Specifying systems",

Addison-Wesley, 2002

https://research.microsoft.com/en-us/um/people/lamport/tla/book-02-08-08.pdf

[3] Leslie Lamport,

"The temporal logic of actions",

TOPLAS, Vol.16, No.3, pp.872--923, 1994

https://dx.doi.org/10.1145/177492.177726

https://research.microsoft.com/en-us/um/people/lamport/pubs/lamport-actions.pdf

[6] Stephan Merz,

"The specification language TLA+",

Logics of specification languages, Springer, 2008

https://dx.doi.org/10.1007/978-3-540-74107-7_8

https://members.loria.fr/SMerz/papers/tla+logic2008.html

[7] Martín Abadi, Leslie Lamport,

"The existence of refinement mappings",

TCS, Vol.82, No.2, pp.253--284, 1991

https://dx.doi.org/doi:10.1016/0304-3975(91)90224-P

https://research.microsoft.com/en-us/um/people/lamport/pubs/abadi-existence.pdf

Best regards,

ioannis

On Tuesday, November 1, 2016 at 4:21:30 AM UTC-7, Stephan Merz wrote:

Indeed, the TOPLAS paper [3] does not define the operator `\sim_x`,

which is what I intended to allude to with

"using the notation \sim_x to encapsulate the first two conjuncts from Eq.(49)".

Eq.(49) reads:

sigma[[ \EE x : F ]] ==

\E rho, tau \in St^\infty :

/\ Natural(sigma) = Natural(rho)

/\ rho =_x tau

/\ tau[[F]]

Using the predicate `IsABehavior`, the above can be written as:

sigma[[ \EE x : F ]] ==

\E tau:

/\ IsABehavior(tau)

/\ \E rho:

/\ IsABehavior(rho)

/\ Natural(rho) = Natural(sigma)

/\ rho =_x tau

/\ tau[[F]]

The older "definition" of `\sim_x` was extracted from Eq.(49),

by comparing to [1, p.316]:

sigma |= \EE : F ==

\E_{behavior} tau:

/\ sigma \sim_x tau

/\ tau |= F

The conjunct:

/\ \E rho:

/\ IsABehavior(rho)

/\ Natural(rho) = Natural(sigma)

/\ rho =_x tau

serves the purpose of the conjunct `sigma \sim_x tau`.

Depending on how `\sim_x` is defined, these two expressions can

be equal or not, even though what `\EE` means can remain unaffected.

This note started as an observation about how `\EE` is defined.

In the updated errata, it seems to me that `\sigma[[ \EE x: F ]]` is

defined equivalently to TOPLAS. So, I described the remaining comments

as related to the "definition" of `\sim_x`.

The two definitions of `\EE` appear to be equisatisfiable with respect to `tau`,

but satisfied by possibly different collections of behaviors `tau`.

So, which of the two expressions is used as conjunct above does not

appear to affect `\EE`.

(Sketch: A behavior `tau` that satisfies the old definition satisfies the new one,

and a `tau` that satisfies the new definition may be too short for the old one,

but can always be elongated by stuttering,

in order to obtain another `tauhat` that satisfies the old definition.)

In words (based on Stephan's phrasing):

The old definition "squeezes, stretches, overwrites x" to obtain tau from sigma.

The new definition "overwrites x, squeezes, stretches, overwrites x" to

obtain tau from sigma.

If the operator `\sim_x` is used elsewhere in place of

`(Natural(sigma) = Natural(rho)) /\ (rho =_x tau)`,

then there could be a change in meaning.

I do not know whether `\sim_x` has been used in this way.

Remark: The attached TLA+ file says "The _expression_ $\rho \sim \sigma$ from [3]".

No `\sim` appears in [3]. The symbol `\sim` refers to stuttering as defined

on p.904 "... invariant under stuttering, which means formally that

Natural(sigma) = Natural(tau) implies ...", i.e., `\sim` stands for stutter

equivalence, defined as `Natural(sigma) = Natural(tau)`.

An earlier definition of stutter equivalence [7, p.7 in DEC report] used `\simeq`.

Thank you for mentioning [6]. The definition of `\simeq_x` appears

to me equivalent to the updated `\sim_x`. A rough comparison:

`sigma \simeq_x tau == \E_{behavior} sigma', tau': sigma ~ sigma' =_x tau' ~ tau`,

and the updated definition of `\sim_x` is "close" to (but different from):

`\E_{behavior} sigma', tau': sigma =_x sigma' ~ tau' =_x tau`.

Remark: Some names I've used for operators in the attached TLA+ file

almost coincide with the terminology used in [6],

for example `SimUpToVar` and "similar up to v" [6, p.417].

[1] Leslie Lamport,

"Specifying systems",

Addison-Wesley, 2002

https://research.microsoft.com/en-us/um/people/lamport/tla/book-02-08-08.pdf

[3] Leslie Lamport,

"The temporal logic of actions",

TOPLAS, Vol.16, No.3, pp.872--923, 1994

https://dx.doi.org/10.1145/177492.177726

https://research.microsoft.com/en-us/um/people/lamport/pubs/lamport-actions.pdf

[6] Stephan Merz,

"The specification language TLA+",

Logics of specification languages, Springer, 2008

https://dx.doi.org/10.1007/978-3-540-74107-7_8

https://members.loria.fr/SMerz/papers/tla+logic2008.html

[7] Martín Abadi, Leslie Lamport,

"The existence of refinement mappings",

TCS, Vol.82, No.2, pp.253--284, 1991

https://dx.doi.org/doi:10.1016/0304-3975(91)90224-P

https://research.microsoft.com/en-us/um/people/lamport/pubs/abadi-existence.pdf

Best regards,

ioannis

On Tuesday, November 1, 2016 at 4:21:30 AM UTC-7, Stephan Merz wrote:

Thank you for your observation. However, looking back at the TOPLAS paper (in the version available from Leslie's home page), I do not see where it defines the relation \sim_x. In particular, equation (49) that you refer to defines the value of\sigma[[ \EE x : F ]]without introducing an auxiliary relation \sim_x, so I think that your comparison is somewhat moot. It is still an interesting observation that for the definition of the flexible quantifier, it is enough to "squeeze and stretch" the original behavior sigma first and then change the values of the bound variable (but I believe this observation was known to Leslie and Martín when the TOPLAS paper was written).In my paper on the TLA+ semantics [1], I define a relation \simeq_x by (adapting your notation)sigma \simeq_x tau ==

\E sigma', tau':

/\ IsABehavior(sigma') /\ IsABehavior(tau')

/\ Natural(sigma') = Natural(sigma)/\ Natural(tau') = Natural(tau)

/\ sigma' =_x tau'and I believe this definition is equivalent to the definition in the new errata sheet to the book; in particular, both are symmetric relations.Best regards,Stephan[1] https://members.loria.fr/SMerz/papers/tla+logic2008. html On 1 Nov 2016, at 08:52, Ioannis Filippidis <jfil...@xxxxxxxxx> wrote:Dear Dr. Lamport, TLA+ Users Group,

The operator `\sim_x' appears to be defined differently in the book's errata (version of 28 Oct 2016)

than in the 1994 TOPLAS paper "The temporal logic of actions".

--------------------------------------- EXAMPLE ------------------------------ ---------

For example, in ZF, let

sigma == [

n \in Nat |->

IF n = 0

THEN [ x |-> 1, y |-> "a" ]

ELSE IF n = 1

THEN [ x |-> 2, y |-> "a" ]

ELSE [ x |-> 2, y |-> "b" ] ]

tau == [

n \in Nat |->

IF n = 0

THEN [ x |-> 999, y |-> "a" ]

ELSE [ x |-> 999, y |-> "b" ] ]

------------------------------------------------------------ ------------------------------ -----

Using TOPLAS (with Natural defined as in the book, and using the notation

\sim_x to encapsulate the first two conjuncts from Eq.(49)):

sigma \sim_x tau ==

\E rho:

/\ IsABehavior(rho)

/\ Natural(rho) = Natural(sigma)

/\ rho =_x tau

Natural(sigma) = [

0 |-> [ x |-> 1, y |-> "a" ],

1 |-> [ x |-> 2, y |-> "a" ],

2 |-> [ x |-> 2, y |-> "b" ] ]

PROPOSITION Rho1 ==

\A rho:

/\ IsABehavior(rho)

/\ rho =_x tau

=> rho[1]["y"] = "b"

PROOF SKETCH:

BY axiom about function equality,

DOMAIN tau = Nat,

DEF IsABehavior,

\A n \in Nat: DOMAIN rho[n] = VarNames,

"y" \in VarNames,

DEF tau,

DEF =_x.

PROPOSITION NaturalRho1 ==

\A rho:

/\ IsABehavior(rho)

/\ rho =_x tau

=> Natural(rho)[1]["y"] = "b"

PROOF SKETCH:

BY Rho1,

DEF Natural,

DEF =_x,

DEF tau,

"a" # "b".

PROPOSITION Unequal ==

\A rho:

/\ IsABehavior(rho)

/\ rho =_x tau

=> Natural(rho) # Natural(sigma)

PROOF SKETCH:

BY NaturalRho1,

DEF Natural,

axiom about function equality.

THEOREM ~ (sigma \sim_x \tau)

PROOF SKETCH:

BY Unequal, DEF \sim_x.

------------------------------------------------------------ ------------------------------ -----

Using the erratum from 28 Oct 2016:

Overwrite(p, var, value) == [

n \in Nat |->

[ p[n] EXCEPT ![var] = value ] ]

sigma \sim_x tau ==

\E value:

Natural(Overwrite(sigma, "x", value)) =

Natural(Overwrite(tau, "x", value))

PROPOSITION Misc ==

/\ Overwrite(sigma, "x", 999) = [

n \in Nat |->

IF n = 0

THEN [ x |-> 999, y |-> "a" ]

ELSE IF n = 1

THEN [ x |-> 999, y |-> "a" ]

ELSE [ x |-> 999, y |-> "b" ] ]

/\ Overwrite(tau, "x", 999) = tau

/\ Natural(Overwrite(sigma, "x", 999)) = [

0 |-> [ x |-> 999, y |-> "a" ],

1 |-> [ x |-> 999, y |-> "b" ] ]

/\ Natural(Overwrite(tau, "x", 999)) = [

0 |-> [ x |-> 999, y |-> "a" ],

1 |-> [ x |-> 999, y |-> "b" ] ]

THEOREM sigma \sim_x tau

PROOF SKETCH:

BY Misc, DEF \sim_x

================================================

The above example also demonstrates that the TOPLAS paper defines the

operator `\sim_x' to be noncommutative, whereas the erratum defines

a commutative operator.

If the above reasoning is correct, then should the erratum be

considered a revision, or should we continue to use the TOPLAS definition?

The TOPLAS definition seems closer to physical intuition.

It does not allow "squeezing" `sigma' too much to obtain `tau'.

If there are steps in `sigma' that change the unhidden variable `x',

then those steps are preserved as nonstuttering ones in `Natural(sigma)',

and so should appear as nonstuttering steps in both `rho' and `tau'.

This ensures that the "refined" behavior `tau' has at least as many nonstuttering

steps as the "coarser" behavior `sigma'. Otherwise (using the erratum),

`tau' could omit steps that in `sigma' change the unhidden `x',

even though those steps could represent visible behavior of other components.

Of course, a shorter `tau' can always be elongated by stuttering,

so this may leave the definition of temporal quantification unaffected.

Two weeks ago, I observed the difference between the earlier erratum (from Oct 2005)

and TOPLAS, and was working on proving it. In case they may be useful to someone,

I have attached the relevant TLA+ file, and a Python script that

applies this earlier definition to the TOPLAS example.

Best regards,

Ioannis Filippidis--

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 .

<about_temporal_quantifiers.tla> <unstutter.py>

**References**:**operator `\sim_x' as defined in erratum differs from TOPLAS***From:*Ioannis Filippidis

**Re: [tlaplus] operator `\sim_x' as defined in erratum differs from TOPLAS***From:*Stephan Merz

- Prev by Date:
**Re: [tlaplus] operator `\sim_x' as defined in erratum differs from TOPLAS** - Next by Date:
**Temporal property** - Previous by thread:
**Re: [tlaplus] operator `\sim_x' as defined in erratum differs from TOPLAS** - Next by thread:
**Temporal property** - Index(es):