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

Re: Nondeterminism and equivalence

Hi Ron,


I have two comments.


First, the main reason that specifications that aren't machine closed

are usually bad has nothing to do with provability.  It's because they

are usually hard to understand.  Moreover, if they are supposed to

describe an algorithm, they are almost certainly wrong.  There are

rare cases in which a non-machine closed spec is the best way to

describe what a system is supposed to do (rather than how it does it).

The simplest spec I know of sequential consistency is not machine



Second, you seem to forget that a TLA+ specification is a mathematical

formula.  Mathematics cannot express anything about the syntax in

which a mathematical formula is written.  You can model a language

like TLA+ in TLA+ and make all sorts of statements about the TLA+

formulas--for example that the meaning of a certain sequence seq of

characters is the formula F, and that seq is the shortest sequence of

characters whose meeaning is F.  However, that's a statement about a

sequences of characters, not about a mathematical formula.


Thus, if Wiles's proof is correct, then the following two formulas A

and B are completely equivalent


   A  ==  q = 42


   B  ==

     (\A x, y, z, n \in Nat \ {0} : (n>2) => (x^n + y^n # z^n))

        => (q = 42)


Thus, P(A) = P(B) for any mathematical (or TLA+) operator P. A tool

like TLC may be able to evaluate one and not the other, but that's because

tools operate on strings of characters representing formulas, not on

formulas.  The correctness condition that TLC is supposed to satisfy

is that if it can evaluate both P(A) and P(B), then it gets the same

value for both .  Mathematics gives no meaning to the concept of evaluation

of a formula.


If you want to distinguish between two TLA+ formulas that are

mathematically equivalent (which I believe is what you mean by

equivalent with respect to behaviors), then you're looking for a tool

not for a logic.  We already have one such tool: the TLATeX

pretty-printer.  Also, a lot of the output that TLC produces depends

on the particular way a specification is written--even if TLC

produces the same yes or no answer of whether the spec satisfies the

properties that TLC is checking.  Perhaps there are others tools that

can tell us something useful about a specification that depends on how

it's written.