operator `\sim_x' as defined in erratum differs from TOPLAS

[Ioannis Filippidis <jfili...@xxxxxxxxx>]

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

Attachment: about_temporal_quantifiers.tla
Description: Binary data

#!/usr/bin/env python
"""Compute the unstuttering map as in: Lamport, "Specifying systems"."""


def unstutter(s):
    """Remove repetitions of states from behavior `s`."""
    m = len(s)
    dom = {f(n, s): n for n in range(m)}
    k = len(dom)
    assert set(dom) == set(range(k)), dom
    r = [s[dom[n]] for n in range(k)]
    return r


def f(n, s):
    """Map index `n` to index of stutter-free behavior."""
    if n == 0:
        return 0
    assert n > 0, n
    r = f(n - 1, s)
    if s[n] != s[n - 1]:
        r += 1
    return r


def sim_up_to_var(sigma, tau, var):
    """Return `True` if behaviors `sigma, tau` similar modulo `var`."""
    t = unstutter(tau)
    s = unstutter(sigma)
    r = list()
    for n, state in enumerate(t):
        d = dict(state)
        d[var] = s[n][var]
        r.append(d)
    print('[n \in DOMAIN t |-> t[n] EXCEPT ![var] = s[n][var]] =')
    pprint_behavior(r)
    return s == r


def main():
    """Example from 1994 Lamport TOPLAS."""
    tau = [
        dict(x=1, y='a'),
        dict(x=2, y='a'),
        dict(x=2, y='b')]
    sigma = [
        dict(x=999, y='a'),
        dict(x=999, y='a'),
        dict(x=999, y='b')]
    # makes domains equal, but still not (sigma ~_x tau)
    # sigma.append(dict(x=3, y='b'))
    t = unstutter(tau)
    s = unstutter(sigma)
    print('Natural(tau) =')
    pprint_behavior(t)
    print('Natural(sigma) =')
    pprint_behavior(s)
    var = 'x'
    sim = sim_up_to_var(sigma, tau, var)
    if sim:
        print('sigma ~_x tau')
    else:
        print('not (sigma ~_x tau)')


def pprint_behavior(t):
    """Pretty print behavior `t`."""
    for state in t:
        print(state)
    print('\n')


if __name__ == '__main__':
    main()