[Iris-Club] Typos (, I think,) in the Iris 2.0 documentation
Ralf Jung
jung at mpi-sws.org
Wed Aug 17 11:34:23 CEST 2016
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
More information about the Iris-Club
mailing list