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.--StephanOn 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?”
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 Q04 /\ m.bal = b}05 Q1bv == {m \in Q1b : m.mbal \geq 0}06 IN /\ \A a \in Q : \E m \in Q1b : m.acc = a07 /\ \/ Q1bv = {}08 \/ \E m \in Q1bv :09 /\ m.mval = v10 /\ \A mm \in Q1bv : m.mbal \geq mm.mbalOn 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 a topic in the Google Groups "tlaplus" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/tlaplus/NWaXjUZxW_c/unsubscribe.
To unsubscribe from this group and all its topics, 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.