[Iris-Club] A question on invariant identifier namespaces
Ralf Jung
jung at mpi-sws.org
Tue Aug 16 10:43:51 CEST 2016
Hi,
> 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.
*oops*
> 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?
Right. In other words, InvNamesp is countable.
What did you find unclear about this sentence? I can't find any other
interpretation, so I guess I need your help to improve it. ;)
> 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?
`#` ("disjoint") is defined on all sorts of things. In this section, we
first define what it means for namespaces to be disjoint; later, we use
"#" to refer to disjointness of sets. In other places of the document,
we also use "#" for disjointness of (CM)RA elements.
> 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.
N and N↑ don't even have the same type (one is a namespace and one is a
set of invariant names), so I am not sure what relation you are looking
for here.
Notice that we overloaded the invariant notation depending on whether
there is an \iota or an N in the superscript. Furthermore, the N
subscript at the viewshift is implicitly closed. So, after unfolding the
newly defined box (and using just the "primitive" invariant notation,
the rule says:
▷ P |- |=>_{N↑} \Exists \iota \in N↑. Inv(\iota, P)
This is just a straight-forward instance of the normal rule for
allocating invariants, using the fact that N↑ is always infinite.
Does this help?
Kind regards,
Ralf
More information about the Iris-Club
mailing list