# [Iris-Club] Typos (, I think,) in the Iris 2.0 documentation

Ralf Jung jung at mpi-sws.org
Thu Aug 11 13:03:28 CEST 2016

Hi Jeehoon,

> Dear Iris Club,
>
> I think the following is typos
> for http://plv.mpi-sws.org/iris/appendix-2.0.pdf .  Would anyone please
> confirm or deny?
>
> Many of them are really minor; but as a novice I was not confident with
> my understanding, and not sure that those are really typos.  On the
> other hand, some of them are rather a question or call for clarification
> than just typos..  For both cases any kind of resolutions by the authors
> will really help me to read the document.

Sure :)

> - Page 2: "Note that \mathcal{COFE} is cartesian closed:": I think the
> following definition (Definition 6) saying something different from
> cartesian closedness..

True... having the arrows of the category reflected inside the objects
is an important ingredient to cartesian closedness, but it is not
sufficient.  However, the other ingredient (products) is so trivial that
I considered it not worth mentioning. ;)

> - Page 2: "if its action F1 on arrows": I think "F1" here is a little
> bit confusing.  What exactly does it mean?

As far as I know, this is standard terminology/notation in category
theory. Given a functor F : C1 -> C2, it is really two functions: F_0,
the action on objects (mapping objects of C0 to objects of C1), and F_1,
the action on arrows (mapping arrows of C0 to arrows of C1, and suitably
compatible with F_0).
So, in this case, we are saying that the function "\lambda f. F(f)",
i.e. calling the functor F on arrows f of the category COFE, must be
non-expansive.

The idea behind these category-theoretic remarks is that if you know
category theory, they should be helfpul; if not, just ignore them. :)
Understanding them is certainly not required to just use Iris as a logic.

> - Page 7: the (FPFN-ALLOC) rule does not require K to be infinite, but I
> think it should be.  I guess "Given some countable K" is a typo for
> "Given some infinitely countable K".  May I ask it is indeed the case?

You are right. Fixed.

> - Page 8: "Given a cofe T" -> "Given a COFE T"

Fixed.

> - Page 9: "we construct a monoid modeling": in fact you are modeling an
> RA, which is evident from the fact the "the core is no a homomorphism."

Yeah, this is some really old text^^. Fixed.

> - Page 9: in what sense "↑(S, T)" is the closure?  I mean, is it minimal
> w.r.t. the closedness?  If so, is it obvious?

It is adding exactly those elements that successors of elements in S.
So I would say it is pretty obvious that this makes it the smallest set
containing S that is closed under successors.

> - Page 10: "when e1 reduces to e" -> "when e1 reduces to e2"

Fixed.

> - Page 10: "Exp^n" -> "Expr^n"

Fixed.

> - Page 10: in the machine reduction rules, σ's subscripts ae wrong in
> the conclusion: σ should be σ_1 and σ' should be σ_2.

Fixed.

> - Page 15: it is not a typo; but I think it is a little bit hard to
> parse the conclusion of (WP-LIFT-STEP); may I ask if you could insert
> some redundant parentheses?

Yeah, that rule is a monster. And it's already been simplified. ;)
I tried to give it more visual structure.

> - Page 16: in the interpretation of logical implication, I think
> [[...]]_r(a) should be [[...]]_r(b).

You right, fixed.

> - Page 17: "if F is locally contractive, then so is ResF." What is F?

*oops* should be \Sigma.

> - Page 19: in the interpretation of entailment, [[Gamma | Theta | Q]]
> should be [[Gamma | Theta | P]], I think.

Right... Fixed.

> - Page 19: what is the meaning if ": 2" in the box?

This is the "type" of the entailment, concretely, "2" is the 2-element
set, i.e., truth values.  However, we wrote "Prop" elsewhere for
meta-level assertions, so we should to the same here.

> - Page 20: "corresponding type.." two dots.

Fixed.

Thanks a lot for this helpful feedback!

Kind regards,
Ralf