7 May
2019
7 May
'19
8:48 a.m.
Hi Victor,
On Tue, Apr 30, 2019 at 12:03 PM Victor Khomenko <
victor.khomenko(a)newcastle.ac.uk> wrote:
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/
> 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).