# [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

Right. In other words, InvNamesp is countable.
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