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.
On Tue, May 7, 2019 at 10:41 AM Victor Khomenko <victor.khomenko@newcastle.ac.uk> wrote:
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.
Interesting.
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.
That would not work when B=[*0], because A:[*0] = false. However if you assume that B has at least one letter, I believe that works. In the case of "a ##[i:j] b" if i>0 Spot actually rewrite this as "a;[*i-1:j-1];b" without using ":".
I'd add: first_match(L+)= first_match(L) [* is already handled by your rules]
So the general case is first_match(L[*i:j]) = first_match(L[*i]). And if L is boolean, this becomes just L[*i].
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]
That last rule doesn't look right to me. first_match(a[*];b[*]) = [*0] a[*];first_match(b[*]) = a[*] Maybe that rule works if all words accepted by K have the same length. (So for an easier rule, if K is Boolean). So to summarize, assuming b is Boolean, e accepts empty words, and f, and g are anything else: first_match(b[*i..j]) = b[*i] first_match(f[*i..j]) = first_match(f[*i]) first_match(b;f) = b;first_match(f) first_match(f;g[*i..j]) = first_match(f;g[*i]) first_match(f;e) = first_match(f) It's not clear that any of those is going to improve the output -- Alexandre Duret-Lutz
participants (2)
-
Alexandre Duret-Lutz -
Victor Khomenko