312 \end{itemize} |
312 \end{itemize} |
313 \end{proof} |
313 \end{proof} |
314 |
314 |
315 \begin{theorem}{ |
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.}\\ |
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:\\ |
317 Define pushbits as the following:\\ |
318 $pushbits(r) = if( r == ALTS(bs, rs) )\ then\ ALTS(Nil, rs.map(fuse(bs,\_))) \ else\ r$.\\ |
318 \begin{verbatim} |
|
319 def pushbits(r: ARexp): ARexp = r match { |
|
320 case AALTS(bs, rs) => AALTS(Nil, rs.map(r=>fuse(bs, pushbits(r)))) |
|
321 case ASEQ(bs, r1, r2) => ASEQ(bs, pushbits(r1), pushbits(r2)) |
|
322 case r => r |
|
323 } |
|
324 \end{verbatim} |
319 Then we have \mbox{\boldmath$pushbits(ders\_simp(ar, s) ) == simp(ders(ar,s)) \ or\ ders\_simp(ar, s) == simp(ders(ar, s))$}.\\ |
325 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\\ |
326 Unfortunately this does not hold. A counterexample is\\ |
321 \begin{verbatim} |
327 \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)))))) |
328 baa |
|
329 original regex |
|
330 STA |
|
331 └-ALT |
|
332 └-STA List(Z) |
|
333 | └-a |
|
334 └-ALT List(S) |
|
335 └-b List(Z) |
|
336 └-a List(S) |
323 regex after ders simp |
337 regex after ders simp |
324 |
338 ALT List(S, S, Z, C(b)) |
325 SEQ |
339 └-SEQ |
326 └-ALT List(S, S, C(b)) |
340 | └-STA List(S, Z, S, C(a), S, C(a)) |
327 | └-SEQ |
341 | | └-a |
328 | | └-STA List(S, C(a), S, C(a)) |
342 | └-STA |
329 | | | └-a |
343 | └-ALT |
330 | | └-a List(Z) |
344 | └-STA List(Z) |
331 | └-ONE List(S, C(a), Z, Z, C(a)) |
345 | | └-a |
332 └-STA |
346 | └-ALT List(S) |
|
347 | └-b List(Z) |
|
348 | └-a List(S) |
|
349 └-SEQ List(S, Z, S, C(a), Z) |
|
350 └-ALT List(S) |
|
351 | └-STA List(Z, S, C(a)) |
|
352 | | └-a |
|
353 | └-ONE List(S, S, C(a)) |
|
354 └-STA |
|
355 └-ALT |
|
356 └-STA List(Z) |
|
357 | └-a |
|
358 └-ALT List(S) |
|
359 └-b List(Z) |
|
360 └-a List(S) |
|
361 regex after ders |
|
362 ALT |
|
363 └-SEQ |
|
364 | └-ALT List(S) |
|
365 | | └-SEQ List(Z) |
|
366 | | | └-ZERO |
|
367 | | | └-STA |
|
368 | | | └-a |
|
369 | | └-ALT List(S) |
|
370 | | └-ZERO |
|
371 | | └-ZERO |
|
372 | └-STA |
|
373 | └-ALT |
|
374 | └-STA List(Z) |
|
375 | | └-a |
|
376 | └-ALT List(S) |
|
377 | └-b List(Z) |
|
378 | └-a List(S) |
|
379 └-ALT List(S, S, Z, C(b)) |
333 └-SEQ |
380 └-SEQ |
|
381 | └-ALT List(S) |
|
382 | | └-ALT List(Z) |
|
383 | | | └-SEQ |
|
384 | | | | └-ZERO |
|
385 | | | | └-STA |
|
386 | | | | └-a |
|
387 | | | └-SEQ List(S, C(a)) |
|
388 | | | └-ONE List(S, C(a)) |
|
389 | | | └-STA |
|
390 | | | └-a |
|
391 | | └-ALT List(S) |
|
392 | | └-ZERO |
|
393 | | └-ZERO |
|
394 | └-STA |
|
395 | └-ALT |
|
396 | └-STA List(Z) |
|
397 | | └-a |
|
398 | └-ALT List(S) |
|
399 | └-b List(Z) |
|
400 | └-a List(S) |
|
401 └-SEQ List(S, Z, S, C(a), Z) |
|
402 └-ALT List(S) |
|
403 | └-SEQ List(Z) |
|
404 | | └-ONE List(S, C(a)) |
|
405 | | └-STA |
|
406 | | └-a |
|
407 | └-ALT List(S) |
|
408 | └-ZERO |
|
409 | └-ONE List(S, C(a)) |
|
410 └-STA |
|
411 └-ALT |
|
412 └-STA List(Z) |
|
413 | └-a |
|
414 └-ALT List(S) |
|
415 └-b List(Z) |
|
416 └-a List(S) |
|
417 regex after ders and then a single simp |
|
418 ALT |
|
419 └-SEQ List(S, S, Z, C(b)) |
|
420 | └-STA List(S, Z, S, C(a), S, C(a)) |
|
421 | | └-a |
|
422 | └-STA |
|
423 | └-ALT |
|
424 | └-STA List(Z) |
|
425 | | └-a |
|
426 | └-ALT List(S) |
|
427 | └-b List(Z) |
|
428 | └-a List(S) |
|
429 └-SEQ List(S, S, Z, C(b), S, Z, S, C(a), Z) |
|
430 └-ALT List(S) |
|
431 | └-STA List(Z, S, C(a)) |
|
432 | | └-a |
|
433 | └-ONE List(S, S, C(a)) |
|
434 └-STA |
334 └-ALT |
435 └-ALT |
335 | └-c List(Z) |
436 └-STA List(Z) |
336 | └-b List(S) |
|
337 └-SEQ |
|
338 └-STA |
|
339 | └-a |
437 | └-a |
340 └-ALT |
438 └-ALT List(S) |
341 └-a List(Z) |
439 └-b 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) |
440 └-a List(S) |
362 \end{verbatim} |
441 \end{verbatim} |
363 \end{theorem} |
442 \end{theorem} |
364 |
443 |
365 \end{document} |
444 \end{document} |