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

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