277 Now we proceed to prove that $sdr \sim_{m\epsilon} dsr$. This can be reduced to proving $dr \sim_{m\epsilon} dsr$ as we know that $dr \sim_{m\epsilon} sdr$ by \autoref{lma2}.\\ |
285 Now we proceed to prove that $sdr \sim_{m\epsilon} dsr$. This can be reduced to proving $dr \sim_{m\epsilon} dsr$ as we know that $dr \sim_{m\epsilon} sdr$ by \autoref{lma2}.\\ |
278 |
286 |
279 we use an induction proof. Base cases are omitted. Here are the 3 inductive cases. |
287 we use an induction proof. Base cases are omitted. Here are the 3 inductive cases. |
280 \begin{itemize} |
288 \begin{itemize} |
281 |
289 |
282 \item{$r_1+r_2$} |
290 \item{$r_1+r_2$}\\ |
283 $r_1+r_2$\\ |
|
284 The most difficult case is when $sr1$ and $sr2$ are both ALTS, so that they will be opened up in the flats function and some terms in sr2 might be deleted. Or otherwise we can use the argument that $d(r_1+r_2) = dr_1 + dr_2 \sim_{m\epsilon} dsr_1 + dsr_2 \sim_{m\epsilon} ds(r_1+r_2)$, |
291 The most difficult case is when $sr1$ and $sr2$ are both ALTS, so that they will be opened up in the flats function and some terms in sr2 might be deleted. Or otherwise we can use the argument that $d(r_1+r_2) = dr_1 + dr_2 \sim_{m\epsilon} dsr_1 + dsr_2 \sim_{m\epsilon} ds(r_1+r_2)$, |
285 the last equivalence being established by \autoref{lma3}. |
292 the last equivalence being established by \autoref{lma3}. |
286 When $s(r_1), s(r_2)$ are both ALTS, we have to be more careful for the last equivalence step, namelly, $dsr_1 + dsr_2 \sim_{m\epsilon} ds(r_1+r_2)$. \\ |
293 When $s(r_1), s(r_2)$ are both ALTS, we have to be more careful for the last equivalence step, namelly, $dsr_1 + dsr_2 \sim_{m\epsilon} ds(r_1+r_2)$. \\ |
287 We have that $LHS = dsr_1 + dsr_2 = d(sr_1 +sr_2)$. Since $sr_1 = ALTS(bs1, rs1)$ and $sr_2 = ALTS(bs2, rs2)$ we have $ d(sr_1 +sr_2 ) \sim_{m\epsilon} d(ALTS(bs, bs1>>rs1 ++ bs2>>rs2))$ by \autoref{lma4}. |
294 We have that $LHS = dsr_1 + dsr_2 = d(sr_1 +sr_2)$. Since $sr_1 = ALTS(bs1, rs1)$ and $sr_2 = ALTS(bs2, rs2)$ we have $ d(sr_1 +sr_2 ) \sim_{m\epsilon} d(ALTS(bs, bs1>>rs1 ++ bs2>>rs2))$ by \autoref{lma4}. |
288 On the other hand, $RHS = ds(ALTS(bs, r1, r2)) = d Co(bs, dB(flats(s(r1), s(r2)) ) ) = d Co(bs, dB(bs1>>rs1 ++ bs2>>rs2))$ by definition of bsimp and flats.\\ |
295 On the other hand, $RHS = ds(ALTS(bs, r1, r2)) = d Co(bs, dB(flats(s(r1), s(r2)) ) ) = d Co(bs, dB(bs1>>rs1 ++ bs2>>rs2))$ by definition of bsimp and flats.\\ |
289 $d Co(bs, dB(bs1>>rs1 ++ bs2>>rs2)) = d Co(bs, (bs1>>rs1 ++ ((bs2>>rs2)--rs1))) $ by \autoref{lma5}.\\ $d Co(bs, (bs1>>rs1 ++ ((bs2>>rs2)--rs1) )) = d(ALTS(bs, bs1>>rs1 ++ (bs2>>rs2)--rs1))$ by \autoref{lma6}. \\ |
296 $d Co(bs, dB(bs1>>rs1 ++ bs2>>rs2)) = d Co(bs, (bs1>>rs1 ++ ((bs2>>rs2)--rs1))) $ by \autoref{lma5}.\\ $d Co(bs, (bs1>>rs1 ++ ((bs2>>rs2)--rs1) )) = d(ALTS(bs, bs1>>rs1 ++ (bs2>>rs2)--rs1))$ by \autoref{lma6}. \\ |
290 Using \autoref{lma8}, we have $d(ALTS(bs, bs1>>rs1 ++ (bs2>>rs2)--rs1)) \sim_{m\epsilon} d(ALTS(bs, bs1>>rs1 ++ bs2>>rs2)) \sim_{m\epsilon} RHS$.\\ |
297 Using \autoref{lma8}, we have $d(ALTS(bs, bs1>>rs1 ++ (bs2>>rs2)--rs1)) \sim_{m\epsilon} d(ALTS(bs, bs1>>rs1 ++ bs2>>rs2)) \sim_{m\epsilon} RHS$.\\ |
291 %only the last part we don't have an equality here. We use mkeps equivalence instead because these two regexes are indeed different syntactically. However, they have even more in common than just mkeps equal. We might later augment this proof so that this equivalence relation is changed to something like regular expression equivalence. |
298 %only the last part we don't have an equality here. We use mkeps equivalence instead because these two regexes are indeed different syntactically. However, they have even more in common than just mkeps equal. We might later augment this proof so that this equivalence relation is changed to something like regular expression equivalence. |
292 This completes the proof. |
299 This completes the proof. |
293 \item{$r*$}\\ |
300 \item{$r*$}\\ |
294 s(r*) = s(r). |
301 $s(r*) = r*$. Our goal is trivially achieved. |
295 \item{$r1.r2$}\\ |
302 \item{$r1 \cdot r2$}\\ |
296 using previous. |
303 When r1 is nullable, $ds r1r2 = dsr1 \cdot sr2 + dsr2 \sim_{m\epsilon} dr1 \cdot sr2 + dr2 = dr1 \cdot r2 + dr2 $. The last step uses \autoref{lma10}. |
|
304 When r1 is not nullable, $ds r1r2 = dsr1 \cdot sr2 \sim_{m\epsilon} dr1 \cdot sr2 \sim_{m\epsilon} dr1 \cdot r2 $ |
297 |
305 |
298 \end{itemize} |
306 \end{itemize} |
299 \item |
307 \item |
300 Proof of second part of the theorem: use a similar structure of argument as in the first part. |
308 Proof of second part of the theorem: use a similar structure of argument as in the first part. |
|
309 |
|
310 \item |
|
311 This proof has a major flaw: it assumes all dr is nullable along the path of deriving r by s. But it could be the case that $s\in L(r)$ but $ \exists s' \in Pref(s) \ s.t.\ ders(s', r)$ is not nullable (or equivalently, $s'\notin L(r)$). One remedy for this is to replace the mkepsBC equivalence relation into some other transitive relation that entails mkepsBC equivalence. |
301 \end{itemize} |
312 \end{itemize} |
302 \end{proof} |
313 \end{proof} |
|
314 |
|
315 \begin{theorem}{ |
|
316 This is a very strong claim that has yet to be more carefully examined and proved. However, experiments suggest a very good hope for this.}\\ |
|
317 Define pushbits as the following:\\ |
|
318 $pushbits(r) = if( r == ALTS(bs, rs) )\ then\ ALTS(Nil, rs.map(fuse(bs,\_))) \ else\ r$.\\ |
|
319 Then we have \mbox{\boldmath$pushbits(ders\_simp(ar, s) ) == simp(ders(ar,s)) \ or\ ders\_simp(ar, s) == simp(ders(ar, s))$}.\\ |
|
320 Unfortunately this does not hold. A counterexample is\\ |
|
321 \begin{verbatim} |
|
322 r = ASTAR(List(),ASEQ(List(),AALTS(List(),List(ACHAR(List(Z),c), ACHAR(List(S),b))),ASEQ(List(),ASTAR(List(),ACHAR(List(),a)),AALTS(List(),List(ACHAR(List(Z),a), ACHAR(List(S),a)))))) |
|
323 regex after ders simp |
|
324 |
|
325 SEQ |
|
326 └-ALT List(S, S, C(b)) |
|
327 | └-SEQ |
|
328 | | └-STA List(S, C(a), S, C(a)) |
|
329 | | | └-a |
|
330 | | └-a List(Z) |
|
331 | └-ONE List(S, C(a), Z, Z, C(a)) |
|
332 └-STA |
|
333 └-SEQ |
|
334 └-ALT |
|
335 | └-c List(Z) |
|
336 | └-b List(S) |
|
337 └-SEQ |
|
338 └-STA |
|
339 | └-a |
|
340 └-ALT |
|
341 └-a List(Z) |
|
342 └-a List(S) |
|
343 regex after ders and then a single simp |
|
344 SEQ |
|
345 └-ALT List(S) |
|
346 | └-SEQ List(S, C(b)) |
|
347 | | └-STA List(S, C(a), S, C(a)) |
|
348 | | | └-a |
|
349 | | └-a List(Z) |
|
350 | └-ONE List(S, C(b), S, C(a), Z, Z, C(a)) |
|
351 └-STA |
|
352 └-SEQ |
|
353 └-ALT |
|
354 | └-c List(Z) |
|
355 | └-b List(S) |
|
356 └-SEQ |
|
357 └-STA |
|
358 | └-a |
|
359 └-ALT |
|
360 └-a List(Z) |
|
361 └-a List(S) |
|
362 \end{verbatim} |
|
363 \end{theorem} |
303 |
364 |
304 \end{document} |
365 \end{document} |
305 |
366 |
306 %The second part might still need some more development. |
367 %The second part might still need some more development. |
307 %When s is not in the set L(ar), we have that s = s1@s2 s.t. s1 $\in$ L(ar), and any longer string that is a prefix of s does not belong to L(ar).\\ |
368 %When s is not in the set L(ar), we have that s = s1@s2 s.t. s1 $\in$ L(ar), and any longer string that is a prefix of s does not belong to L(ar).\\ |