[Iris-Club] Two Monoid Questions

[Ralf Jung]

Ah sorry, somehow I thought now you were referring to the fraction "outside" the
authoritative component that we also have (to support splitting said component).

Generalizing equality to a relation works fine.  Generalizing it to a predicate
is much more subtle because that predicate would have to *change*, just like
currently the authoritative element can change.  But if at the same time the
fragments can exploit what the predicate is, you can't change it any more.
That's why I think a relation should work better.

; Ralf

On 14.08.19 18:08, Gregory Malecha wrote:
> 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
> <mailto: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 <mailto:gregory at bedrocksystems.com>
> director of formal methods

-- 
Website: https://people.mpi-sws.org/~jung/