equal
deleted
inserted
replaced
152 |
152 |
153 \begin{quote} |
153 \begin{quote} |
154 \it% |
154 \it% |
155 \begin{tabular}{@ {}l@ {}p{0.88\textwidth}@ {}} |
155 \begin{tabular}{@ {}l@ {}p{0.88\textwidth}@ {}} |
156 `` & If the reader finds the above treatment in terms of bit lists revoltingly |
156 `` & If the reader finds the above treatment in terms of bit lists revoltingly |
157 concrete, I cannot disagree.''\\ |
157 concrete, I cannot disagree. A more abstract approach is clearly desirable.''\\ |
158 `` & All lemmas appear obvious given a picture of the composition of automata\ldots |
158 `` & All lemmas appear obvious given a picture of the composition of automata\ldots |
159 Yet their proofs require a painful amount of detail.'' |
159 Yet their proofs require a painful amount of detail.'' |
160 \end{tabular} |
160 \end{tabular} |
161 \end{quote} |
161 \end{quote} |
162 |
162 |
389 It is straightforward to show that in general @{thm lang_is_union_of_finals} and |
389 It is straightforward to show that in general @{thm lang_is_union_of_finals} and |
390 @{thm finals_in_partitions} hold. |
390 @{thm finals_in_partitions} hold. |
391 Therefore if we know that there exists a regular expression for every |
391 Therefore if we know that there exists a regular expression for every |
392 equivalence class in @{term "finals A"} (which by assumption must be |
392 equivalence class in @{term "finals A"} (which by assumption must be |
393 a finite set), then we can use @{text "\<bigplus>"} to obtain a regular expression |
393 a finite set), then we can use @{text "\<bigplus>"} to obtain a regular expression |
394 using that matches every string in @{text A}. |
394 that matches every string in @{text A}. |
395 |
395 |
396 |
396 |
397 Our proof of Thm.~\ref{myhillnerodeone} relies on a method that can calculate a |
397 Our proof of Thm.~\ref{myhillnerodeone} relies on a method that can calculate a |
398 regular expression for \emph{every} equivalence class, not just the ones |
398 regular expression for \emph{every} equivalence class, not just the ones |
399 in @{term "finals A"}. We |
399 in @{term "finals A"}. We |
406 |
406 |
407 \noindent |
407 \noindent |
408 which means that if we concatenate the character @{text c} to the end of all |
408 which means that if we concatenate the character @{text c} to the end of all |
409 strings in the equivalence class @{text Y}, we obtain a subset of |
409 strings in the equivalence class @{text Y}, we obtain a subset of |
410 @{text X}. Note that we do not define an automaton here, we merely relate two sets |
410 @{text X}. Note that we do not define an automaton here, we merely relate two sets |
411 (with the help of a regular expression). In our concrete example we have |
411 (with respect to a character). In our concrete example we have |
412 @{term "X\<^isub>1 \<Turnstile>c\<Rightarrow> X\<^isub>2"}, @{term "X\<^isub>1 \<Turnstile>d\<Rightarrow> X\<^isub>3"} with @{text d} being any |
412 @{term "X\<^isub>1 \<Turnstile>c\<Rightarrow> X\<^isub>2"}, @{term "X\<^isub>1 \<Turnstile>d\<Rightarrow> X\<^isub>3"} with @{text d} being any |
413 other character than @{text c}, and @{term "X\<^isub>3 \<Turnstile>d\<Rightarrow> X\<^isub>3"} for any @{text d}. |
413 other character than @{text c}, and @{term "X\<^isub>3 \<Turnstile>d\<Rightarrow> X\<^isub>3"} for any @{text d}. |
414 |
414 |
415 Next we build an equational system that |
415 Next we build an equational system that |
416 contains an equation for each equivalence class. Suppose we have |
416 contains an equation for each equivalence class. Suppose we have |
426 @{text "X\<^isub>n"} & @{text "="} & @{text "(Y\<^isub>n\<^isub>1, CHAR c\<^isub>n\<^isub>1) + \<dots> + (Y\<^isub>n\<^isub>q, CHAR c\<^isub>n\<^isub>q)"}\\ |
426 @{text "X\<^isub>n"} & @{text "="} & @{text "(Y\<^isub>n\<^isub>1, CHAR c\<^isub>n\<^isub>1) + \<dots> + (Y\<^isub>n\<^isub>q, CHAR c\<^isub>n\<^isub>q)"}\\ |
427 \end{tabular} |
427 \end{tabular} |
428 \end{center} |
428 \end{center} |
429 |
429 |
430 \noindent |
430 \noindent |
431 where the pairs @{text "(Y\<^isub>i\<^isub>j, CHAR c\<^isub>i\<^isub>j)"} stand for all transitions |
431 where the terms @{text "(Y\<^isub>i\<^isub>j, CHAR c\<^isub>i\<^isub>j)"} stand for all transitions |
432 @{term "Y\<^isub>i\<^isub>j \<Turnstile>c\<^isub>i\<^isub>j\<Rightarrow> X\<^isub>i"}. Our internal represeantation for the right-hand |
432 @{term "Y\<^isub>i\<^isub>j \<Turnstile>c\<^isub>i\<^isub>j\<Rightarrow> X\<^isub>i"}. Our internal represeantation for the right-hand |
433 sides are sets of terms. |
433 sides are sets of terms. |
434 There can only be finitely many such |
434 There can only be finitely many such |
435 terms since there are only finitely many equivalence classes |
435 terms since there are only finitely many equivalence classes |
436 and only finitely many characters. |
436 and only finitely many characters. |