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

*From*: Leslie Lamport <tlapl...@xxxxxxxxx>*Date*: Thu, 7 Jan 2016 12:08:15 -0800 (PST)*References*: <71319d03-6ab4-48a7-a6a2-53e7c9c48a51@googlegroups.com>

Basically I'm looking for a "lowering" operator where:

Lower(x) == the level-0 _expression_ (constant value) which

is equal to x in this state

I can't think of any way to define such an operator, but 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').

TLC's requirement that x' be determined in a single _expression_ means

that I can't write:

\A t \in DOMAIN x : x'[t] = e \* e is some _expression_

This is not a problem when only one variable is involved, as you can

do:

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

This is exactly the kind of situation that I was talking about. 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.

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. 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')'.

Leslie

**Follow-Ups**:**Re: Tagged formulas***From:*Ron Pressler

**References**:**Tagged formulas***From:*Ron Pressler

- Prev by Date:
**Re: Tagged formulas** - Next by Date:
**Re: Tagged formulas** - Previous by thread:
**Re: Tagged formulas** - Next by thread:
**Re: Tagged formulas** - Index(es):