New subject: syntactic stutter-invariance

10 May 2019

Hi Alexandre,

I've reconsidered first_match, apparently my suggestion to eliminate the exit arcs of
the accepting states in the NFA is wrong, e.g. for (a|a;a) the NFA has two accepting
states with no exit arcs and the transformation does not have any effect, whereas
first_match(a|a;a)=a. I guess the automaton has to be determinised before applying this
transformation (unless you have a better idea).

Regards,
Victor.

...
  -----Original Message-----
 From: Alexandre Duret-Lutz &lt;adl(a)lrde.epita.fr&gt;
 Sent: Tuesday, May 7, 2019 3:15 PM
 To: Victor Khomenko &lt;victor.khomenko(a)newcastle.ac.uk&gt;
 Cc: spot &lt;spot(a)lrde.epita.fr&gt;
 Subject: Re: [Spot] syntactic stutter-invariance

 On Tue, May 7, 2019 at 10:41 AM Victor Khomenko
 &lt;victor.khomenko(a)newcastle.ac.uk&gt; 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