<div dir="auto">Hello --<div dir="auto"><br></div><div dir="auto">I thought that I had an intuition about the authoritative monoid construction and someone recently pointed out that I am using a slightly different definition and I'm wondering if they are roughly equivalent.</div><div dir="auto"><br></div><div dir="auto">My fuzzy intuition was that I the type of the authoritative state could be different than the type of the RA in the view and the compatibility relation (which is equality in the paper) could be a generic "models" relation <a href="http://a.la">a.la</a>. the usual separation logic soundness definition. Semi-formally:</div><div dir="auto"><br></div><div dir="auto">Auth(A, R, |=) :=</div><div dir="auto">  { v : option A * R | match fst v with</div><div dir="auto">                                   | Some a => exists f, a |= snd v * f (* using * to mean join *)</div><div dir="auto">                                   | None => True</div><div dir="auto">                                  end }.</div><div dir="auto"><br></div><div dir="auto">This seems like it could be encoded via an extra invariant tying my A to an R and placing the |= relation inside that invariant.</div><div dir="auto"><br></div><div dir="auto">A second, slightly related, question. What is best to read to understand why join (in CMRA) is a function and not a deterministic relation? Is it necessary to the construction? Or is it for convenience?</div><div dir="auto"><br></div><div dir="auto">Thanks so much.</div><div dir="auto"><br></div></div>