[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