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

[Jeehoon Kang]

>
> > 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.
>
> Oh, right, we also added this well-formedness condition here because we
> are lazy. However, considering T to be fixed, this condition is
> monotone, i.e., if it rules out a set then it also rules out all larger
> sets. How should this violate minimality?


Consider an STS consisting of two nodes s1, s2 and an edge s1 -> s2, with
L(s1)={T} and L(s2)={}.  Then closure({s1},{T}) = {s1,s2}.  But ({s1},{T}),
which is less than (closure({s1},{T}),{T}), is also closed.  Which implies
that a closure may not be minimal w.r.t. the closedness.

I started to understand why you called it "closure", and yet I want to know
the exact meaning of the word in this context.  This is partly because when
reading the POPL 2015 paper I couldn't understand the STS construction..

-- 
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/20160817/266f81ba/attachment.html>