[Iris-Club] Several small questions on Iris

Ralf Jung jung at mpi-sws.org
Thu Feb 2 17:46:44 CET 2017


> - "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,

More information about the Iris-Club mailing list