[Iris-Club] Several small questions on Iris

[Jeehoon Kang]

I have more questions...


- "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].

- typo? "composeability" [2, S8.1, p25] for "composability"

- 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..)

- "STATE" [2, S8.2, p27] is used without definition: "Finally, STATE is
used to provide ..."

- 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..)

- 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.

- In the definition of "legal return value" [2, p29], T'' is not
constrained at all.

- 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?


Thank you,
Jeehoon



2017-01-31 21:02 GMT+01:00 Jeehoon Kang <jeehoon.kang at sf.snu.ac.kr>:

> Dear Iris Club,
>
>
> As usual, I have several small questions on Iris :)
>
>
> First things first, here are references:
> - [1] Iris 3.0 paper
> - [2] Iris 3.0 appendix
>
>
> Now questions:
>
> - I don't understand why it is okay *not* to have "Own(\iota,
> \gamma_{EN})" at the conclusion of the rules (WSAT-ALLOC) and (INV-ALLOC)
> [1].  More specifically, why is it okay to "forget" the fact that the
> "\iota" invariant is enabled when it is created?
>
> - Why "K" should be countably infinite for the CMRA construction of finite
> partial function [2, S3.4, p11]?  More precisely, why not (possibly)
> uncountably infinite K?
>
> - What is "c" in the definition of AG(T) [2, S3.5, p11]?
>
> - I don't quite understand what "Variable conventions." means [2, S4.1]:
> "We assume that, if a term occurs multiple times in a rule, its free
> variables are exactly those binders which are available at every
> occurrence."
>
> - I think "Res" in the definition of the interpretation of entailment in
> [2, p20], should be "M".
>
> - It seems the semantics of "\Gamma | P => Q" and "\Gamma | P |- Q" are
> much related [2].  I wonder if the notion of logical entailment can be
> encoded with the semantics of implications.  (Yes, I know it is a program
> logic newbie question :-)  I just want to know the motivation behind the
> concept of logical entailment.)
>
> - typo: "ruels" in [2, p22]
>
> - typo: "Stateof" in [2, p24] (rather than "State of")
>
>
> Best regards,
> Jeehoon
>
> --
> Jeehoon Kang (Ph.D. student) <http://sf.snu.ac.kr/jeehoon.kang>
> Software Foundations Laboratory <http://sf.snu.ac.kr>
> Seoul National University <http://www.snu.ac.kr>
>



-- 
Jeehoon Kang (Ph.D. student) <http://sf.snu.ac.kr/jeehoon.kang>
Software Foundations Laboratory <http://sf.snu.ac.kr>
Seoul National University <http://www.snu.ac.kr>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.mpi-sws.org/pipermail/iris-club/attachments/20170201/832df999/attachment.html>