[Iris-Club] Fractional Monoid

Derek Dreyer dreyer at mpi-sws.org
Mon Nov 9 20:29:24 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)?

Derek

On Mon, Nov 9, 2015 at 8:22 PM, Ralf Jung <jung at mpi-sws.org> wrote:
> Hi all,
>
> I think the way the fractional monoid is defined in the appendix right
> now is not perfect, and I'd like to extend that definition to cover more
> use-cases that come up in my Rust stuff.
>
> # Current definition
>
> Right now, the members of the fractional monoid Frac(A) are pairs (q, a)
> of a fraction q > 0 and a data element a \in A. A can be any set.
> Composition is defined as
>
>   (q, a) * (q', a') = (q+q', a)   if a=a'
>
> The only frame-preserving update is
>
>   (1, a) --> (1, b)
>
> # The problem
>
> For my Rust work, I'd like to have a construction that provides
> fractions, while also maintaining some separation on the data elements.
> Concretely, I need fractional ownership of pairs consisting of a
> lockstate (unlocked, writing, reading N) and a value, and there is
> interesting separation going on in the lockstate, e.g.
>
>   reading N * reading M = reading N+M
>
> The Frac construction above ignores any separation on A, treats it as a set.
>
> # The solution
>
> What I'd like to do is to let Frac(M) inherit the separation of M. The
> idea is that Frac(M) is a lot like M, but we also track the fraction so
> that we know when we have full ownership, and we can do any
> frame-preserving update.
> So, we'd have Frac(M) with the same elements as above, but
>
>   (q, a) * (q', a') = (q+q', a*a')
>
> We can then have the above frame-preserving update, plus:
>
>         a --> b
>   -------------------
>    (q, a) --> (q, b)
>
> The old Frac(A) now becomes Frac(Ag(A)). The equality constraint that
> was baked into Frac, now arises from the use of agreement. I think this
> significantly improves the overall story for fractions, and makes them
> much more modular.
>
> # The questions
>
> In your work with Iris, did you ever encounter the need for fractions
> the way I need them for Rust, something that provides the second
> frame-preserving update? Would the proposed Frac(M) give you the right
> separation? Did you ever encounter the need for fractions that cannot be
> covered by Frac(M)?
>
> Also, note that Ag(A) of course *could* be my really complicated
> agreement construction that I presented for HOPE. But that's not
> necessary here. In all cases I encountered so far, A has decidable
> equality and a discrete metric, in which case Ag(A) can be constructed
> in avery straight-froward way (that is actually already formalized in
> the current Coq development). I call this simplified version AgDec, and
> I'd like to put it into the appendix. Did you encounter the need for
> agreement on types which don't have decidable equality?
>
> 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




More information about the Iris-Club mailing list