[Iris-Club] Two Monoid Questions

[Gregory Malecha]

I think I just used the wrong phrasing here. Originally (much earlier in
this thread) you said that it was sometimes annoying to have fractions
inside of the authoritative component just because they are in the view
component since the authoritative component had all of these fractions at
1. By relaxing the equivalence to a relation, this fact could be
established in the relation keeping the authoritative element "clean".

Is my understanding correct that these "step-indexed relations" are the
heterogenous generalization of OFEs or is there something more to them?

On Wed, Aug 14, 2019 at 6:49 AM Ralf Jung <jung at mpi-sws.org> wrote:

> Hi Gregory,
>
> > This makes sense to me. Is there a pre-packaged way to express the views
> concept
> > in Iris?
>
> No, the closest we have is the general auth construction.
>
> > You were mentioning that it can be annoying to have fractional
> permissions and
> > such hanging out in the authoritative piece, so I was thinking that
> perhaps if
> > you had a way to generalize equality to a predicate, then you wouldn't
> need to
> > separate out the bijection.
>
> I don't follow.  The authoritative piece needs a fractional (or exclusive)
> permission, that is crucial for realizing its "authoritativeness".
>
> But indeed, my thinking is that we can generalize auth the way you
> suggested
> with a "models" relationship -- or rather, introduce a new "view" CMRA like
> that, and then define auth as an instance of it, and the "bijection-auth"
> would
> be another instance.
>
> The annoying part is generalizing this to step-indexing, where we will
> need a
> notion of "step-indexed relations". It is clear what that means (A -> B ->
> nat
> -> Prop, down-closed and non-expansive), but so far we managed to avoid
> realizing this notion in Coq. I have long advocated for adding it, though.
>
> ; Ralf
>


-- 
gregory malecha
gregory at bedrocksystems.com
director of formal methods
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.mpi-sws.org/pipermail/iris-club/attachments/20190814/fea6cc05/attachment.html>