[Iris-Club] Fractional Monoid

Ralf Jung jung at mpi-sws.org
Mon Nov 9 21:20:38 CET 2015


> I'm confused.  How is your proposed new Frac(M) different from just a
> product of two separate monoids -- Frac and M -- where Frac is defined
> as fractions with composition as addition (only defined if the sum is
> <= 1)?

I had exactly the same thought, and actually wrote the mail first with
that monoid. However, what that does *not* give us is the first
frame-preserving update:

   (1, a) --> (1, b)

for any a, b. The reason is that just because you own (1, a), does not
mean someone else could not own (unit, b). However, with the proposed
definition, the latter element does not exist.

Kind regards,

More information about the Iris-Club mailing list