[Iris-Club] Two Monoid Questions

[Gregory Malecha]

Hello --

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.

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.la. the usual separation logic soundness definition.
Semi-formally:

Auth(A, R, |=) :=
  { v : option A * R | match fst v with
                                   | Some a => exists f, a |= snd v * f (*
using * to mean join *)
                                   | None => True
                                  end }.

This seems like it could be encoded via an extra invariant tying my A to an
R and placing the |= relation inside that invariant.

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?

Thanks so much.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.mpi-sws.org/pipermail/iris-club/attachments/20190723/f7c1e3ba/attachment.html>