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

*From*: Ron Pressler <r...@xxxxxxxxxxxxxxxxxxx>*Date*: Thu, 7 Jan 2016 11:14:14 -0800 (PST)*References*: <71319d03-6ab4-48a7-a6a2-53e7c9c48a51@googlegroups.com> <743b44d5-a917-4b27-b245-f7acc403e34f@googlegroups.com>

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

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

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

**Re: Tagged formulas***From:*Leslie Lamport

- 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):