[Iris-Club] Fractional Monoid

[Derek Dreyer]

Good, thanks.

Derek


On Mon, Nov 9, 2015 at 9:20 PM, Ralf Jung <jung at mpi-sws.org> wrote:
> Hi,
>
>> 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,
> Ralf
>
> --
> iris-club at lists.mpi-sws.org - Mailing List for the Iris Logic
> Management: https://lists.mpi-sws.org/listinfo/iris-club
> Unsubscribe: iris-club-unsubscribe at lists.mpi-sws.org