Re:Modeling CRDTs in Alloy – the importance of idempotence
by Twisol on Monday October 09, 2023 @10:45AM
(#37820970)
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.
[ Parent
| on HN ]
Re:Modeling CRDTs in Alloy – the importance of idempotence
by nyssos on Monday October 09, 2023 @11:12AM
(#37821277)
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.
Re:Modeling CRDTs in Alloy – the importance of idempotence
by Twisol on Monday October 09, 2023 @03:58PM
(#37824738)
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 ^_^)