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

*From*: Igor Konnov <igor.konnov@xxxxxxxxx>*Date*: Sat, 3 Oct 2020 10:58:50 +0200*Cc*: Igor Konnov <igor.konnov@xxxxxxxxx>*References*: <3db0a094-02e8-484b-9aae-eb2930f4e269n@googlegroups.com> <f51dc912-3169-48d3-a108-7b86fcc2f3b1n@googlegroups.com> <A72E8EDE-0DC2-408F-BB25-21087815B1E4@gmail.com>

Hi Frank, Would you have trouble understanding the following piece of code in a functional language (Scala)? Set(Set(1, 2), Set(1, 3), Set(2, 3)).exists(Q => Q.contains(2) ) /// Since the TLA+ code in lines 2-10 does not mention primed variables, you can think of it as a collection of set iterators (exists and forall) and set comprehensions (filter, map). The important differences are: 1. The order of set traversal is not fixed. You would not not expect a fixed order within hash sets in many languages either. Golang goes even further by randomizing iteration over maps. 2. The evaluation order of /\ and \/ is also arbitrary. Though TLC explores these expressions in a fixed top-down and left-to-right order. 3. As Rodrick mentioned, the rest is just mathematical syntax :-) — Igor > On 03.10.2020, at 08:24, Stephan Merz <stephan.merz@xxxxxxxxx> wrote: > > To follow up on this, Q is not really "defined" by this formula because a definition would have to be unambiguous. The formula checks for the existence of a quorum satisfying certain properties. The quantifier introduces (or "declares") a name Q for naming the value whose properties are being described in lines 2-10 and requires Q to belong to the set Quorum. The formula is true if some such value exists and false otherwise. Also, the scope of Q is restricted to the body of the formula, and Q has no meaning after the formula has been evaluated, in contrast to a definition that introduces a name that can be used later. > > Stephan > >> On 3 Oct 2020, at 01:42, Rodrick Chapman <rodrick@xxxxxxxxxxxx> wrote: >> >> It's just syntax. It happens to be syntax that's based on century-old mathematical notation, but at the end of the day, it's still just syntax. >> >> The trouble you’re having is caused by your assumption that Q is defined on the left side of the colon ("\E Q \in Quorum"), and then used on the right side. >> >> But, in fact, Q is actually defined on the right side of the colon and then used on the left. In other words, we define Q and then ask “is there any element in the set Quorum that meets the definition of Q?” >> >> >> >> On Friday, October 2, 2020 at 12:44:13 PM UTC-5 franke...@xxxxxxxxx wrote: >> Hi, >> >> I'm trying to understand this part of the paxos specification. I'm not trying to understand how paxos works, I get that, I'm just trying to understand how to read and understand this part of the specification. >> >> 01 /\ \E Q \in Quorum : >> 02 LET Q1b == {m \in msgs : /\ m.type = "1b" >> 03 /\ m.acc \in Q >> 04 /\ m.bal = b} >> 05 Q1bv == {m \in Q1b : m.mbal \geq 0} >> 06 IN /\ \A a \in Q : \E m \in Q1b : m.acc = a >> 07 /\ \/ Q1bv = {} >> 08 \/ \E m \in Q1bv : >> 09 /\ m.mval = v >> 10 /\ \A mm \in Q1bv : m.mbal \geq mm.mbal >> >> On line 01 you define that Q is in set of Quorum and then lines 02-10 define what Q will be. My confusion is on Line 03 Q is referenced. How can you reference something that hasn't been assigned a value yet. >> >> I may very well be suffering from "... brain washing done by years of C programming". >> >> Any help that I could get in understanding this would be greatly appreciated. Also, is there a place on the web were I can better familiarize my self with such concepts. >> >> Thanks, >> >> -Frank >> >> -- >> 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/f51dc912-3169-48d3-a108-7b86fcc2f3b1n%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/A72E8EDE-0DC2-408F-BB25-21087815B1E4%40gmail.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/77C638C2-2D31-4319-991E-47EA98524C56%40gmail.com.

**References**:**[tlaplus] [Newbie Question] Engineer trying to get maths meaning***From:*Frank Eaves

**[tlaplus] Re: [Newbie Question] Engineer trying to get maths meaning***From:*Rodrick Chapman

**Re: [tlaplus] Re: [Newbie Question] Engineer trying to get maths meaning***From:*Stephan Merz

- Prev by Date:
**Re: [tlaplus] Re: [Newbie Question] Engineer trying to get maths meaning** - Next by Date:
**Re: [tlaplus] Re: [Newbie Question] Engineer trying to get maths meaning** - Previous by thread:
**Re: [tlaplus] Re: [Newbie Question] Engineer trying to get maths meaning** - Next by thread:
**Re: [tlaplus] Re: [Newbie Question] Engineer trying to get maths meaning** - Index(es):