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

[Ralf Jung]

Hi,

> 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

How that? We have L(s1) = {T}, so the tokens overlap, so no state set
containing s1 can be closed if T is in the token set.
What happens here is that closure({s1},{T}) is not actually closed,
which is caused by the input being "ill-formed".  So, in that sense the
closure fails to be complete (it's not always producing something
closed).  However, the combination of the state set {s1} and the token
set {T} doesn't make any sense to start with (since T \in L(s1)), so
"garbage in, garbage out" applies. ;)

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

I never gave much thought to this term.
It's an operation which makes the state set larger until it is "closed
under taking a step", so we dubbed it "closure".  Nothing deep going on
here, as far as I can tell.

Kind regards,
Ralf