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

*From*: Stephan Merz <stephan.merz@xxxxxxxxx>*Date*: Mon, 29 Apr 2024 16:58:17 +0200*References*: <4ba993d8-c1cc-4a65-9e9e-c2328bd9f138n@googlegroups.com>

It sounds like the macro- and microstates should also be parameters of the relevant operators (E and possibly epsilon). In formal mathematics, you cannot leave parameters implicit as it is sometimes done on a whiteboard or perhaps on paper: the machine is unforgiving and will not figure out what is implicit. This is not specific to TLA+ but also true of Coq, Isabelle or Lean. I am not sure about the quantifiers, however: do you really mean E(i,s,…) to be the same value for all parameters? Of course, a definition is never wrong: it may simply not represent what you have in mind, and the good thing about formal mathematics is that you can play with your definitions and find out if they say what you mean.
-- Stephan On 29 Apr 2024, at 15:58, marta zhango <martazhango@xxxxxxxxx> wrote:
You received this message because you are subscribed to the Google Groups "tlaplus" group. To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx. To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/87ED4423-3DAB-4206-BDEE-FEB89D21A6D2%40gmail.com. |

**Follow-Ups**:**Re: [tlaplus] Defining State_I as the state at energy level \epsilon(I)***From:*marta zhango

**References**:**Re: [tlaplus] Defining State_I as the state at energy level \epsilon(I)***From:*marta zhango

- Prev by Date:
**Re: [tlaplus] Defining State_I as the state at energy level \epsilon(I)** - Next by Date:
**Re: [tlaplus] Defining State_I as the state at energy level \epsilon(I)** - Previous by thread:
**Re: [tlaplus] Defining State_I as the state at energy level \epsilon(I)** - Next by thread:
**Re: [tlaplus] Defining State_I as the state at energy level \epsilon(I)** - Index(es):