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/