Re: [tlaplus] Tagged formulas

[Stephan Merz <stepha...@xxxxxxxxx>]

My sincere apologies for these messages: I don't know what I was thinking. Of course the level of

  CHOOSE x : x = e

is determined by the level of e, and CAPTURE cannot be defined in TLA+.

Stephan

> On 14 Jan 2016, at 14:42, Stephan Merz <Stepha...@xxxxxxxxx> wrote:
>>> 
>>> Sorry for being late to this discussion. I think that basically what you want is
>>> 
>>> Capture(e) == CHOOSE x : x = e
>>> 
>>> with the additional effect that the expression Capture(e) is considered as a level-0 expression by SANY. (If you try writing Capture(x')' for the above definition where x is a state variable, SANY will complain about level-incorrectness.)
>>> 
>>> It seems to me that this wouldn't cause problems semantically. In fact, the more general solution would be to consider any expression
>>> 
>>>   CHOOSE x : P
>>> 
>>> to be of level 0, whatever the level of P (currently, P must be of level <= 2, but even an extension to CHOOSE expressions for temporal formulas should be acceptable).
>>> 
> 
>> That was my original intuition. I don't know what TLA+'s policy on backwards compatibility is, but changing the action semantics of CHOOSE now may break existing specs in possibly subtle ways. 
> 
> No, it shouldn't. A CHOOSE expression returns a value, i.e., a constant. So the proposed change doesn't break the semantics but only the level-checking algorithm, which we know to be an approximation.
> 
> Stephan
>