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

[Jeehoon Kang]

Hello Ralf,

Thank you for all the answers!  It really helped me.  Now I understand more
of the documentation, and yet I still have some remaining questions:


> > - 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.
>

Ah I see :-)  May I ask which reference/textbook you are consulting to?
Because it is different from the convention in the textbook I learned from
(Mac Lane. Categories for the Working Mathematician. Springer GTM 5)..


> - 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.


I am concerned with the condition of the closedness that \mathcal{L}(s) #
T..  Due to this restriction I believe the closure is in general not
minimal w.r.t. the closedness.

Another remark on the closedness is: the definition of s
\stackrel{T}{\rightarrow} s' involves the existential quantification of T1
and T2, and I think there exists an alternative definition that does not
involve that quantification:
    [(\mathcal{L}(s') # T) /\ s \rightarrow s' .]
This is obtained by letting T1 and T2 be (\mathcal{L}(s') \setminus
\mathcal{L}(s)) and (\mathcal{L}(s) \setminus \mathcal{L}(s')).  I guess
the definition in the documentation is more amenable to the proof, and for
this reason you choose to define in that way.  May I ask what is the reason?


Thank you,
Jeehoon

-- 
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...
URL: <http://lists.mpi-sws.org/pipermail/iris-club/attachments/20160812/479ae60e/attachment.html>