equal
deleted
inserted
replaced
371 One direction of the Myhill-Nerode theorem establishes |
371 One direction of the Myhill-Nerode theorem establishes |
372 that if there are finitely many equivalence classes, like in the example above, then |
372 that if there are finitely many equivalence classes, like in the example above, then |
373 the language is regular. In our setting we therefore have to show: |
373 the language is regular. In our setting we therefore have to show: |
374 |
374 |
375 \begin{theorem}\label{myhillnerodeone} |
375 \begin{theorem}\label{myhillnerodeone} |
376 @{thm[mode=IfThen] hard_direction} |
376 @{thm[mode=IfThen] Myhill_Nerode1} |
377 \end{theorem} |
377 \end{theorem} |
378 |
378 |
379 \noindent |
379 \noindent |
380 To prove this theorem, we first define the set @{term "finals A"} as those equivalence |
380 To prove this theorem, we first define the set @{term "finals A"} as those equivalence |
381 classes that contain strings of @{text A}, namely |
381 classes that contain strings of @{text A}, namely |
532 We again delete first all occurence of @{text "(X, r)"} in @{text rhs}; we then calculate |
532 We again delete first all occurence of @{text "(X, r)"} in @{text rhs}; we then calculate |
533 the regular expression corresponding to the deleted terms; finally we append this |
533 the regular expression corresponding to the deleted terms; finally we append this |
534 regular expression to @{text "xrhs"} and union it up with @{text rhs'}. When we use |
534 regular expression to @{text "xrhs"} and union it up with @{text rhs'}. When we use |
535 the substitution operation we will arrange it so that @{text "xrhs"} does not contain |
535 the substitution operation we will arrange it so that @{text "xrhs"} does not contain |
536 any occurence of @{text X}. |
536 any occurence of @{text X}. |
|
537 |
|
538 We lift these two operation to work over equational systems @{text ES}: @{const Subst_all} |
|
539 substitutes an equation @{text "X = xrhs"} throughout an equational system @{text ES}; |
|
540 @{const Remove} completely removes such an equaution from @{text ES} by substituting |
|
541 it to the rest of the equational system, but first removing all recursive occurences |
|
542 of @{text X} by applying @{const Arden} to @{text "xrhs"}. |
|
543 |
|
544 \begin{center} |
|
545 \begin{tabular}{rcl} |
|
546 @{thm (lhs) Subst_all_def} & @{text "\<equiv>"} & @{thm (rhs) Subst_all_def}\\ |
|
547 @{thm (lhs) Remove_def} & @{text "\<equiv>"} & @{thm (rhs) Remove_def} |
|
548 \end{tabular} |
|
549 \end{center} |
537 *} |
550 *} |
538 |
551 |
539 section {* Regular Expressions Generate Finitely Many Partitions *} |
552 section {* Regular Expressions Generate Finitely Many Partitions *} |
540 |
553 |
541 text {* |
554 text {* |