[Iris-Club] A question on invariant identifier namespaces
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.
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...
More information about the Iris-Club