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

[Ralf Jung]

Hi,

>     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. ;)
> 
> 
> Ah I see!  I interpreted the definition in a wrong way, by inserting
> parenthesis in wrong places:
> "closed(S, T) , ∀s ∈ S. ((L(s) # T ∧ ∀s 0 . s T −→ s 0) ⇒ s 0 ∈ S) "

D'oh, I see ;)

> In essence, I was confused about the precedence between /\ and =>.  I
> know it is an established convention, and yet I think it would be
> helpful to insert some redundant parenthesis for readers ;-)

The precedence here is determined by the \forall, which generally ranges
"as far as possible". For this reason, the => has to be "below" the \forall.
If it were not for the forall, you would be right; => generally binds
weaker than /\ and \/.

There's always this problem with adding redundant parentheses in some
places only that people may take the *absence* of redundant parentheses
elsewhere to mean something. For example, should I be adding more
parentheses to clarify that the outermost \forall ranges over both sides
of the conjunction? (I'd say no, because otherwise the formula is not
even well-formed -- s is being used on the right -- but the same applies
to your interpretation; the rightmost s0 above is not bound.)
Also, if I do this, we end up with 4 more parentheses on this line alone
-- I am not convinced having every line end in a stack of half a dozen
parentheses increases readability.

Unfortunately, I haven't found a good balance yet.

Kind regards,
Ralf