[HN Gopher] Modeling CRDTs in Alloy - the importance of idempotence
       ___________________________________________________________________
        
       Modeling CRDTs in Alloy - the importance of idempotence
        
       Author : brianhicks
       Score  : 95 points
       Date   : 2023-10-09 12:23 UTC (10 hours ago)
        
 (HTM) web link (bytes.zone)
 (TXT) w3m dump (bytes.zone)
        
       | matlin wrote:
       | For those like me who didn't know what Alloy is, it looks like
       | it's a general purpose constraint solver for testing correctness
       | in range of different algorithms.
       | 
       | https://alloytools.org/
        
       | Twisol wrote:
       | Nice article! The statement of idempotence is a little
       | nonstandard, I think -- I'm used to it being stated as `merge(a,
       | a) = a`. The form in the article makes more sense if you have set
       | of operations _acting on_ a state, so that `apply(apply(st, a),
       | a) = apply(st, a)` -- but this follows from the more usual merge
       | law above, since `apply(apply(st, a), a) = apply(st, merge(a, a)`
       | by the laws of monoid actions, then `apply(st, merge(a, a)) =
       | apply(st, a)` by (standard) idempotence.
        
         | nyssos wrote:
         | They're talking about idempotence of `merge(a, _ )` (under
         | function composition), whereas you're talking about idempotence
         | of `a` (with composition given by `merge`). Same property,
         | different object.
        
           | Twisol wrote:
           | Right, but then for commutativity I would expect them to use
           | `merge(merge(a, b), c) = merge(merge(a, c), b)`, whereas what
           | they actually have is the usual `merge(a, b) = merge(b, a)`.
           | They're sort of mixing and matching from the axioms of
           | monoids[^] and the axioms of actions (what you're referring
           | to as "function composition").
           | 
           | [^] (well, properly, _semilattices_ , because that's what
           | state-based CRDTs are based on. But semilattices are "just"
           | commutative idempontent monoids ^_^)
        
       ___________________________________________________________________
       (page generated 2023-10-09 23:01 UTC)