Re: Tagged formulas

[Ron Pressler <r...@xxxxxxxxxxxxxxxxxxx>]

On Thursday, January 7, 2016 at 10:08:16 PM UTC+2, Leslie Lamport wrote:

 it may help

to observe that if Foo is defined by

   Foo(a, b) == a' = e1 /\ b' = e2

Then  \E t : (t=x) /\ Foo(t,y)'  is equivalent to Foo(x, y').

Oh, I see. It only helps with boolean expressions, though.

 

Those

two formulas are not equivalent.  The second determines the value of
x'.  The first tells you very little about the value of x'.  All it tells
you are the values of x'[t] for t \in DOMAIN x.  It tells you nothing
about the domain of x'.  It doesn't even tell you if x' is a function.
Hence, it's not a sensible formula--at least, not by itself.  The following
formula is equivalent to the second one:

   /\ x' = [t \in DOMAIN x |-> x'[t]]
   /\ \A t \in DOMAIN x : x'[t] = e

but it's hardly simper than the second one.

Hmmm, right. Although you could define the first conjunct as a formula

    F(x) == [t \in DOMAIN x |-> x'[t]]

and then my example could be written as:

 

    F(x) /\ F(y) /\ \A t \in DOMAIN x : Foo(x[t], y[t])

which may be simpler than any of the alternatives (but won't work in TLC), especially if you collect all of these into a single formula, 

     Types == F(x) /\ F(y) /\ ....

and conjunct it at a top level with the next-state formula.

So, as I wrote before, when TLC doesn't allow you to write something
you think it should, then it's often the case that what you wrote
isn't what you meant to write.  You should learn to read what a
formula says rather than what you want it to say.  This requires that
you stop thinking of TLA+ formula as a program and start thinking of
it as a mathematical assertion. 

Just when I think I totally get it I'm surprised again, but it all makes sense in the end (and to be fair, theses "problems" usually pop up only when I try to be clever...)

 

Occasionally, this is difficult.  For
example, if you write

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

it's not easy to realize that if x is a variable, then f[2] is not
equal to the illegal _expression_ (x')'.

Because f would then be the fixpoint f[n] = x ??

Thanks!

Ron