[Iris-Club] Several small questions on Iris

[Derek Dreyer]

Among Jeehoon's most important observations:

- It's indeed "composability", not "composeability".

Frankly, to completely misquote George Orwell, neither of them is a word,
but the latter is even less of a word than the former.

Derek

On Thu, Feb 2, 2017 at 5:46 PM, Ralf Jung <jung at mpi-sws.org> wrote:

> Hi,
>
> > - "we can use the maps ξ and ξ^{−1} in the logic to convert" [2, S8.1,
> > p26]: I think by using ξ and ξ^{−1} in the Iris logic you actually
> > extends the base logic, and we no longer cannot say that Iris is an
> > instantiation of the base logic.  I know it is a somewhat pedantic
> > comment; I just want to know the motivation of the explanation in [2,
> S8.1].
>
> Ah, good question :)
> I am actually not 100% sure myself, but I *think* we can say that these
> two maps are added to the signature of function symbols, having types
> (in the logic!)
>
>   ξ : UPred(F(Prop, Prop)) -> Prop
>   ξ^-1 : Prop -> UPred(F(Prop, Prop))
>
> Then, when it comes to giving interpretations for the signature, we pick
> the isomorphism obtained from solving the domain equation.
>
> Or maybe that could be considered cheating, because we are supposed to
> construct the interpretation of the signature before passing it to the
> "opaque block" described by §5, which constructs a model for the logic.
> In that case, yes, strictly speaking, we would not be working in an
> instance of the logic described previously, but instead in an instance
> of the logic described previously but parameterized over a *functor* F
> (instead of a CMRA M) and with appropriate rules.  I honestly don't know
> how to properly do this in the syntactic deep embedding.  I wanted to
> keep the initial presentation of the logic syntactic because that seems
> to be the usual things to do, but ultimately all of these problems
> mentioned above entirely disappear when doing a shallow embedding, and I
> didn't want to spend unreasonable amounts of time on trying to figure
> out these details without there being a good reason.
>
> > - typo? "composeability" [2, S8.1, p25] for "composability"
>
> Any native speaker on this list that could tell us the right spelling?
> I don't know, and neither does my spellchecker. ;)
>
> > - On composability [2, S8.1, p25]: why don't you just product over all
> > possible bifunctor \Sigma?  In that way you can just assume "the" family
> > of functors, and composability is no longer an issue.  (I currently am
> > guessing it is related to universe size or impredicativity problem in
> Coq..)
>
> Indeed, if you do that in Coq, you get a universe conflict.  And I think
> that's not just superficial; if you do the same in set theory, you would
> get the same problem -- the "CMRA of all CMRAs" can't contain itself, or
> else Russel comes and hits you with his paradox.
>
> > - "STATE" [2, S8.2, p27] is used without definition: "Finally, STATE is
> > used to provide ..."
>
> That sentence should be gone, thanks for catching it.
>
> > - The view shifts for normal update modality is used in the (VS-UPDATE)
> > and (VS-TIMELESS) rules without definition [2, S8.2, p28].  (There is
> > only one possible interpretation of it, though..)
>
> Those are actually fancy update modalities with any (or, equivalently,
> the empty) mask.  Will fix, thanks.
>
> > - For the physical state interpretation function, [1] uses "I" and [2]
> > uses "S" as the ranging meta-variable.  I think it would be nice for the
> > two documents to use the same symbol here.
>
> Ouch.  Robbert and me did not coordinate here, it seems... and
> unfortunately Robbert was the one writing the harder-to-change document
> [1], so if we want to be consistent, we have to use his choice.  Well
> played, Robbert. ;)
>
> > - In the definition of "legal return value" [2, p29], T'' is not
> > constrained at all.
>
> Indeed a prime' was missing.
>
> > - In [2, S8.5, p32], I couldn't understand the following sentence:
> > "Using (vs-trans) and (Ht-atomic) (or the corresponding proof rules for
> > fancy updates and weakest preconditions), we can show that it is
> > possible to open an accessor around any view shift and any atomic
> > expression."  May I ask what did you mean by this sentence?
>
> I uploaded a new version that prints the proof rules that can be derived
> this way.  Does this help?
>
> Let me know if this answers your questions :)
>
> 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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.mpi-sws.org/pipermail/iris-club/attachments/20170203/014d7d90/attachment.html>