<div dir="ltr"><div>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".<br></div><div><br></div><div>Is my understanding correct that these "step-indexed relations" are the heterogenous generalization of OFEs or is there something more to them?</div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Wed, Aug 14, 2019 at 6:49 AM Ralf Jung <<a href="mailto:jung@mpi-sws.org">jung@mpi-sws.org</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">Hi Gregory,<br>
<br>
> This makes sense to me. Is there a pre-packaged way to express the views concept<br>
> in Iris?<br>
<br>
No, the closest we have is the general auth construction.<br>
<br>
> You were mentioning that it can be annoying to have fractional permissions and<br>
> such hanging out in the authoritative piece, so I was thinking that perhaps if<br>
> you had a way to generalize equality to a predicate, then you wouldn't need to<br>
> separate out the bijection.<br>
<br>
I don't follow.  The authoritative piece needs a fractional (or exclusive)<br>
permission, that is crucial for realizing its "authoritativeness".<br>
<br>
But indeed, my thinking is that we can generalize auth the way you suggested<br>
with a "models" relationship -- or rather, introduce a new "view" CMRA like<br>
that, and then define auth as an instance of it, and the "bijection-auth" would<br>
be another instance.<br>
<br>
The annoying part is generalizing this to step-indexing, where we will need a<br>
notion of "step-indexed relations". It is clear what that means (A -> B -> nat<br>
-> Prop, down-closed and non-expansive), but so far we managed to avoid<br>
realizing this notion in Coq. I have long advocated for adding it, though.<br>
<br>
; Ralf<br>
</blockquote></div><br clear="all"><br>-- <br><div dir="ltr" class="gmail_signature"><div dir="ltr"><div><div dir="ltr"><div>gregory malecha</div><div><a href="mailto:gregory@bedrocksystems.com" target="_blank">gregory@bedrocksystems.com</a></div><div><span>director of formal methods</span></div></div></div></div></div>