[Iris-Club] A question on invariant identifier namespaces

Jeehoon Kang jeehoon.kang at sf.snu.ac.kr
Sun Aug 14 08:57:58 CEST 2016

Dear Iris Club,

I have several questions on the invariant identifier namespaces (Iris 2.0
documentation Section 7.4)..

1. I think the first line ("Let N ∋ InvNamesp list(InvName) be ...") has a
typo: the inclusion order seems reversed.

2. "Notice that there is an injection namesp_inj : InvNamesp → InvName": I
read this sentence as, there exists an injection `namesp_inj`, as both the
domain and the codomain have the same cardinality as the set of the natural
numbers.  May I ask if I read correctly?

3. the `#` operator is defined as `InvNamesp -> InvNamesp -> Prop`, while
it is also used as `set(InvName) -> set(InvName) -> Prop`, as in `N2↑ #
N1↑`.  May I ask if what am I missing?

4. I am not sure why the following rule holds: "◃P⊢⤊_N [P]^N" (I am sorry
in that I couldn't properly type it in unicode..  It is the third rule in
page 23.)  If my understanding of `namesp_inj` in 2. is correct, N and N↑
in general need not be related.. a lot.  In particular it may be the case
that N and N↑ have no intersection.  So I am not sure why the rule holds.

Thank you,

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/20160814/97b42631/attachment.html>

More information about the Iris-Club mailing list