<div dir="ltr">Among Jeehoon's most important observations:<div><br></div><div>- It's indeed "composability", not "composeability".</div><div><br></div><div>Frankly, to completely misquote George Orwell, neither of them is a word, but the latter is even less of a word than the former.</div><div><br></div><div>Derek</div></div><div class="gmail_extra"><br><div class="gmail_quote">On Thu, Feb 2, 2017 at 5:46 PM, Ralf Jung <span dir="ltr"><<a href="mailto:jung@mpi-sws.org" target="_blank">jung@mpi-sws.org</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hi,<br>
<span class=""><br>
> - "we can use the maps ξ and ξ^{−1} in the logic to convert" [2, S8.1,<br>
> p26]: I think by using ξ and ξ^{−1} in the Iris logic you actually<br>
> extends the base logic, and we no longer cannot say that Iris is an<br>
> instantiation of the base logic.  I know it is a somewhat pedantic<br>
> comment; I just want to know the motivation of the explanation in [2, S8.1].<br>
<br>
</span>Ah, good question :)<br>
I am actually not 100% sure myself, but I *think* we can say that these<br>
two maps are added to the signature of function symbols, having types<br>
(in the logic!)<br>
<br>
  ξ : UPred(F(Prop, Prop)) -> Prop<br>
  ξ^-1 : Prop -> UPred(F(Prop, Prop))<br>
<br>
Then, when it comes to giving interpretations for the signature, we pick<br>
the isomorphism obtained from solving the domain equation.<br>
<br>
Or maybe that could be considered cheating, because we are supposed to<br>
construct the interpretation of the signature before passing it to the<br>
"opaque block" described by §5, which constructs a model for the logic.<br>
In that case, yes, strictly speaking, we would not be working in an<br>
instance of the logic described previously, but instead in an instance<br>
of the logic described previously but parameterized over a *functor* F<br>
(instead of a CMRA M) and with appropriate rules.  I honestly don't know<br>
how to properly do this in the syntactic deep embedding.  I wanted to<br>
keep the initial presentation of the logic syntactic because that seems<br>
to be the usual things to do, but ultimately all of these problems<br>
mentioned above entirely disappear when doing a shallow embedding, and I<br>
didn't want to spend unreasonable amounts of time on trying to figure<br>
out these details without there being a good reason.<br>
<span class=""><br>
> - typo? "composeability" [2, S8.1, p25] for "composability"<br>
<br>
</span>Any native speaker on this list that could tell us the right spelling?<br>
I don't know, and neither does my spellchecker. ;)<br>
<span class=""><br>
> - On composability [2, S8.1, p25]: why don't you just product over all<br>
> possible bifunctor \Sigma?  In that way you can just assume "the" family<br>
> of functors, and composability is no longer an issue.  (I currently am<br>
> guessing it is related to universe size or impredicativity problem in Coq..)<br>
<br>
</span>Indeed, if you do that in Coq, you get a universe conflict.  And I think<br>
that's not just superficial; if you do the same in set theory, you would<br>
get the same problem -- the "CMRA of all CMRAs" can't contain itself, or<br>
else Russel comes and hits you with his paradox.<br>
<span class=""><br>
> - "STATE" [2, S8.2, p27] is used without definition: "Finally, STATE is<br>
> used to provide ..."<br>
<br>
</span>That sentence should be gone, thanks for catching it.<br>
<span class=""><br>
> - The view shifts for normal update modality is used in the (VS-UPDATE)<br>
> and (VS-TIMELESS) rules without definition [2, S8.2, p28].  (There is<br>
> only one possible interpretation of it, though..)<br>
<br>
</span>Those are actually fancy update modalities with any (or, equivalently,<br>
the empty) mask.  Will fix, thanks.<br>
<span class=""><br>
> - For the physical state interpretation function, [1] uses "I" and [2]<br>
> uses "S" as the ranging meta-variable.  I think it would be nice for the<br>
> two documents to use the same symbol here.<br>
<br>
</span>Ouch.  Robbert and me did not coordinate here, it seems... and<br>
unfortunately Robbert was the one writing the harder-to-change document<br>
[1], so if we want to be consistent, we have to use his choice.  Well<br>
played, Robbert. ;)<br>
<span class=""><br>
> - In the definition of "legal return value" [2, p29], T'' is not<br>
> constrained at all.<br>
<br>
</span>Indeed a prime' was missing.<br>
<span class=""><br>
> - In [2, S8.5, p32], I couldn't understand the following sentence:<br>
> "Using (vs-trans) and (Ht-atomic) (or the corresponding proof rules for<br>
> fancy updates and weakest preconditions), we can show that it is<br>
> possible to open an accessor around any view shift and any atomic<br>
> expression."  May I ask what did you mean by this sentence?<br>
<br>
</span>I uploaded a new version that prints the proof rules that can be derived<br>
this way.  Does this help?<br>
<br>
Let me know if this answers your questions :)<br>
<div class="HOEnZb"><div class="h5"><br>
Kind regards,<br>
Ralf<br>
<br>
--<br>
<a href="mailto:iris-club@lists.mpi-sws.org">iris-club@lists.mpi-sws.org</a> - Mailing List for the Iris Logic<br>
Management: <a href="https://lists.mpi-sws.org/listinfo/iris-club" rel="noreferrer" target="_blank">https://lists.mpi-sws.org/<wbr>listinfo/iris-club</a><br>
Unsubscribe: <a href="mailto:iris-club-unsubscribe@lists.mpi-sws.org">iris-club-unsubscribe@lists.<wbr>mpi-sws.org</a><br>
</div></div></blockquote></div><br></div>