# Re: Tagged formulas

On Thursday, January 7, 2016 at 8:28:17 PM UTC+2, Leslie Lamport wrote:

A TLA+ specification is a mathematical formula.  "Evaluation' is not a
meaningful concept in mathematics.

Naturally, but once you introduce the concept of _expression_ levels and the way the prime operator interacts differently with expressions of different levels, you can get something that feels like evaluation. 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

In almost all cases that arise in practice, it is easy to rewrite a
sensible action formula in a form that TLC can handle

Not entirely related, but a case where I generally find this a bit burdensome is when functions are concerned. 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]

but it is a hindrance to compositionality when, say, two function variables x and y (say, with the same domain) are involved. I'd like to have a simple formula:

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

and then use it as

\A t \in DOMAIN x (* = DOMAIN y *) : Foo(x[t], y[t])

As it stands, I either need to make a specialized Foo for this case, or have it return a tuple which I then destructure.

In any case, this is a separate issue from the one I am currently discussing, where:

VARIABLES x, y
Foo(a) == a + y

and then I'd want

Foo(Lower(x[5].f)) = Foo(c) \* If c is a constant and x[5].f = c in this state

Without Lower, I'm forced to define:

Foo(a) == a + y
Foo1(a) == a + y'

Now, this isn't too onerous by any means, but I was wondering if there was a way to lower _expression_ levels. I guess there isn't...

Ron