363 |
363 |
364 text {* |
364 text {* |
365 The key definition in the Myhill-Nerode theorem is the |
365 The key definition in the Myhill-Nerode theorem is the |
366 \emph{Myhill-Nerode relation}, which states that w.r.t.~a language two |
366 \emph{Myhill-Nerode relation}, which states that w.r.t.~a language two |
367 strings are related, provided there is no distinguishing extension in this |
367 strings are related, provided there is no distinguishing extension in this |
368 language. This can be defined as tertiary relation: |
368 language. This can be defined as tertiary relation. |
369 |
369 |
370 \begin{definition}[Myhill-Nerode Relation]\mbox{}\\ |
370 \begin{definition}[Myhill-Nerode Relation] Given a language @{text A}, two strings @{text x} and |
|
371 @{text y} are related provided |
|
372 \begin{center} |
371 @{thm str_eq_def[simplified str_eq_rel_def Pair_Collect]} |
373 @{thm str_eq_def[simplified str_eq_rel_def Pair_Collect]} |
|
374 \end{center} |
372 \end{definition} |
375 \end{definition} |
373 |
376 |
374 \noindent |
377 \noindent |
375 It is easy to see that @{term "\<approx>A"} is an equivalence relation, which |
378 It is easy to see that @{term "\<approx>A"} is an equivalence relation, which |
376 partitions the set of all strings, @{text "UNIV"}, into a set of disjoint |
379 partitions the set of all strings, @{text "UNIV"}, into a set of disjoint |
875 \noindent |
878 \noindent |
876 hold, which shows that @{term "UNIV // \<approx>(L r)"} must be finite.\qed |
879 hold, which shows that @{term "UNIV // \<approx>(L r)"} must be finite.\qed |
877 \end{proof} |
880 \end{proof} |
878 |
881 |
879 \noindent |
882 \noindent |
880 Much more interesting are the inductive cases, which seem hard to be solved |
883 Much more interesting, however, are the inductive cases. They seem hard to be solved |
881 directly. The reader is invited to try. Our method will rely on some |
884 directly. The reader is invited to try. |
|
885 |
|
886 Our method will rely on some |
882 \emph{tagging} functions of strings. Given the inductive hypothesis, it will |
887 \emph{tagging} functions of strings. Given the inductive hypothesis, it will |
883 be easy to prove that the range of these tagging functions is finite. |
888 be easy to prove that the range of these tagging functions is finite. |
|
889 With this we will be able to infer that the tagging functions, seen as a relation, |
|
890 give rise to finitely many equivalence classes of @{const UNIV}. Finally we |
|
891 will show that the tagging relation is more refined than @{term "\<approx>(L r)"}, which |
|
892 implies that @{term "UNIV // \<approx>(L r)"} must also be finite. For this we define the |
|
893 notion of a \emph{tag-relation} (which is often also called a kernel relation). |
|
894 |
|
895 \begin{definition}[Tag-Relation] Given a tag-function @{text tag}, then two strings @{text x} |
|
896 and @{text y} are tag-related provided |
|
897 \begin{center} |
|
898 @{text "x =tag= y \<equiv> tag x = tag y"} |
|
899 \end{center} |
|
900 \end{definition} |
|
901 |
|
902 \begin{lemma}\label{finone} |
|
903 @{thm[mode=IfThen] finite_eq_tag_rel} |
|
904 \end{lemma} |
|
905 |
|
906 \begin{proof} |
|
907 |
|
908 \end{proof} |
|
909 |
|
910 \noindent |
|
911 |
|
912 |
|
913 \begin{lemma}\label{fintwo} |
|
914 Given two equivalence relations @{text "R\<^isub>1"} and @{text "R\<^isub>2"}, then |
|
915 if @{thm (prem 1) refined_partition_finite[where A="UNIV" and ?R1.0="R\<^isub>1" and ?R2.0="R\<^isub>2"]} |
|
916 and @{thm (prem 2) refined_partition_finite[where A="UNIV" and ?R1.0="R\<^isub>1" and ?R2.0="R\<^isub>2"]} |
|
917 then @{thm (concl) refined_partition_finite[where A="UNIV" and ?R1.0="R\<^isub>1" and ?R2.0="R\<^isub>2"]}. |
|
918 \end{lemma} |
|
919 |
|
920 \begin{proof} |
|
921 |
|
922 \end{proof} |
|
923 |
|
924 \noindent |
|
925 Stringing Lem.~\ref{finone} and \ref{fintwo} together, means in order to show |
|
926 that @{term "UNIV // \<approx>(L r)"} is finite, we have to find a tagging function whose |
|
927 range is finite and whose tagging-relation refines @{term "\<approx>(L r)"}. |
|
928 |
884 |
929 |
885 @{thm tag_str_ALT_def[where ?L1.0="A" and ?L2.0="B"]} |
930 @{thm tag_str_ALT_def[where ?L1.0="A" and ?L2.0="B"]} |
886 |
931 |
887 @{thm tag_str_SEQ_def[where ?L1.0="A" and ?L2.0="B"]} |
932 @{thm tag_str_SEQ_def[where ?L1.0="A" and ?L2.0="B"]} |
888 |
933 |
889 @{thm tag_str_STAR_def[where ?L1.0="A"]} |
934 @{thm tag_str_STAR_def[where ?L1.0="A"]} |
890 *} |
935 *} |
|
936 |
891 |
937 |
892 |
938 |
893 section {* Conclusion and Related Work *} |
939 section {* Conclusion and Related Work *} |
894 |
940 |
895 text {* |
941 text {* |