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

*From*: marta zhango <martazhango@xxxxxxxxx>*Date*: Mon, 29 Apr 2024 13:16:41 -0700 (PDT)*References*: <4ba993d8-c1cc-4a65-9e9e-c2328bd9f138n@googlegroups.com> <87ED4423-3DAB-4206-BDEE-FEB89D21A6D2@gmail.com> <dbc6f551-ffff-499f-8519-35bf2c69543bn@googlegroups.com> <81b3eeaf-2d56-482b-9e9e-ad73489db79an@googlegroups.com> <e465ac6a-5c1e-49e0-8d1b-fe06d6413accn@googlegroups.com>

Basically what I have is this

macrostates == {k \in 1..m} \* macrostate k,

microstates[k] == {j \in 1..p} \* Microstates for macrostate k

energy_levels == 1..n \* Set of energy levels

macrostate_energy[k] == i \in energy_levels \* Energy level of macrostate k

Finally I want to define the number of occurrences of microstate j having

macrostate_energy[k]. Nij

On Tuesday, April 30, 2024 at 4:33:51 AM UTC+12 marta zhango wrote:

N[i][g] ==LETnumerator == Sum(k, N[i][k] * W[i][k] * C[j])denominator == Sum(k, W[i][k] * C[j])INnumerator / denominatorOn Tuesday, April 30, 2024 at 4:25:16 AM UTC+12 marta zhango wrote:Specifically I compute the average number of particles at energy level i.Here, Sum(k, ...) represents the summation over all possible values of k.

N[i][k] represents the number of particles at energy level i in macrostate k.

W[i][k] represents a weight associated with macrostate k at energy level i.

C[j] represents an arbitrary microstate j within macrostate k.

N[i][g] == LET numerator == Sum(k, N[i][k] * W[i][k] * C[j]) denominator == Sum(k, W[i][k] * C[j]) IN numerator / denominatorOn Tuesday, April 30, 2024 at 4:10:48 AM UTC+12 marta zhango wrote:I want to define the number of particles N at energy level E_i for a given microstatep within macrostate k.On Tuesday, April 30, 2024 at 2:58:34 AM UTC+12 Stephan Merz wrote: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.Correct, energy level i of some particular state. E_i(s)Each state has n energy levels. There are also m macrostates at eachenergy level i, and each macrostate can have p possible microstates.How would I define them ?--On Monday, April 29, 2024 at 10:41:25 PM UTC+12 Stephan Merz wrote:I presume that should be E_i(s)? But then, I don’t understand the quantifiers, and the bound variables k and j appear nowhere in your definition?Would that translate to something like{ s \in S : \A i \in 1..n, k \in 1..m, j \in 1..p : E_i = \epsilon(i)} }to mean the state s in S such that the energy of s is \epsilon(i)for m macrostates and p microstates.--On Monday, April 29, 2024 at 5:41:46 PM UTC+12 Stephan Merz wrote:TLA+ has bounded set comprehension:{ x \in S : P(x) }Unbounded comprehension is disallowed: this helps making the definition of Russell’s “set” illegal.Stephan--Stephan MerzOn 29 Apr 2024, at 03:23, marta zhango <marta...@xxxxxxxxx> wrote:How can I define State_I as the state at energy level \epsilon(I)} ?

State_I \in {energy_level : energy_level = \epsilon(I)}--

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+u...@xxxxxxxxxxxxxxxx.

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/643c7e96-552f-4ae5-ba67-84a2f2c390d3n%40googlegroups.com.

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+u...@xxxxxxxxxxxxxxxx.To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/81197891-9342-4c88-867b-b47d47ad1068n%40googlegroups.com.

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+u...@xxxxxxxxxxxxxxxx.To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/4ba993d8-c1cc-4a65-9e9e-c2328bd9f138n%40googlegroups.com.

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/26d32283-7bd9-4253-bb9e-199e01f9ab28n%40googlegroups.com.

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

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

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

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

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

- Prev by Date:
**[tlaplus] Defining Energy Levels** - Next by Date:
**[tlaplus] General help with a simple spec** - Previous by thread:
**Re: [tlaplus] Defining State_I as the state at energy level \epsilon(I)** - Next by thread:
**[tlaplus] Defining Energy Levels** - Index(es):