Hi Victor,

On Tue, Apr 30, 2019 at 12:03 PM Victor Khomenko <victor.khomenko@newcastle.ac.uk> wrote:
> > However now that you have written this down, I think your interpretation  r
> > SSI =>  r[+] SSI and r[*] SSI  is also sound, but I have no proof for this.
>
> I tried to prove this, but failed, and then found a counterexample: e.g. if L = a[+];(!a)[+];a[+], then L is si but both L[+] and L[*] are not si. I believe if one in addition requires that L is prefix-closed or suffix-closed, then the result would hold (I have an idea how to prove this).
>

Thank you for the counterexamples.
Can we detect prefix- or suffix-closure syntactically?


Meanwhile, I have implemented SVA's first_match and ##[i:j].

The latter is just syntactic sugar: 
a ##[i:j] b = a:([*i:j];b)
##[i:j] b = [*i:j];b
##i = ##[i:i]

The former is a new operator, with three automatic simplifications:
 first_match(b) = b if b is Boolean,
 first_match(first_match(r)) = first_match(r),
 first_match(r) = [*0] if r accepts the empty word.
(this last rule makes the translation to automata works almost automatically)

This can be tested on the version of the app that uses the development version:
https://spot-dev.lrde.epita.fr/app/