Hi Alexandre,
Can we detect prefix- or suffix-closure
syntactically?
Not sure about omega-languages, but for the "usual" ones the prefix- and
suffix-closed languages are closed wrt. | && ; + * at least (and so the derived
operations). Not sure about ":", but hope so. Definitely not closed wrt.
complement (prefix- and suffix-closed languages always contain the empty word, which is
not in the complement). I hope these can be generalized to suffix-closed omega
languages.
I have machine proofs for most of these, including the proof that K;L is si if both K and
L are si and either K is prefix-closed or L is suffix-closed.
Meanwhile, I have implemented SVA's first_match
and ##[i:j].
Excellent news!
a ##[i:j] b = a:([*i:j];b)
Do you know whether A:(B;C)=(A:B);C ? I'd guess yes, but have no proof yet. Generally,
what properties does ":" have?
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)
I'd add:
first_match(L+)= first_match(L) [* is already handled by your rules]
first_match(K;L)= first_match(K) if the empty word is in L
first_match(K;L)= K;first_match(L) [correct?? It would then imply the above rule]
Regards,
Victor.