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

[tlaplus] Re: [Newbie Question] Engineer trying to get maths meaning

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:

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.



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.