# HG changeset patch # User urbanc # Date 1297949129 0 # Node ID d65d071798ff09ec8a8ce54194b8f8d8a49d2123 # Parent e500cab16be4497e133b2af95ab47bb70e6ebc93 first ideas about conclusion diff -r e500cab16be4 -r d65d071798ff Paper/Paper.thy --- a/Paper/Paper.thy Thu Feb 17 11:42:16 2011 +0000 +++ b/Paper/Paper.thy Thu Feb 17 13:25:29 2011 +0000 @@ -865,12 +865,45 @@ text {* In this paper we took the view that a regular language is one where there exists - a regular expression that matches all its strings. For us it was important to find + a regular expression that matches all its strings. For us it was ineteresting to find out how far we can push this point of view. Having formalised the Myhill-Nerode theorem means pushed quite far. Having the Myhill-Nerode theorem means we can formalise much of the textbook results in this subject. + Our proof of the first direction is very much inspired by \emph{Brz + algebraic mehod} used to convert a finite atomaton to a regular + expression. The close connection can be seen by considering the equivalence + classes as the states of the minimal automaton for the regular language. + However there are some subtle differences. If we identify equivalence + classes with the states of the automaton, then the most natural choice is to + characterise each state with the set of strings starting from the initial + state leading up to that state. Usually the states are characterised as the + ones starting from that state leading to the terminal states. The first + choice has consequences how the initial equational system is set up. We have + the $\lambda$-term on our ``initial state'', while Brz has it on the + terminal states. This means we also need to reverse the direction of Arden's + lemma. + We briefly considered using the method Brz presented in the Appendix of ??? + in order to prove the second direction of the Myhill-Nerode thereom. There + he calculates the derivatives for regular expressions and shows that there + can be only finitely many of them. We could use as the tag of a string + @{text s} the derivative of a regular expression generated with respect to + @{text s}. Using the fact that two strings are Myhill-Nerode related + whenever their derivative is the same together with the fact that there are + only finitely many derivatives for a regular expression would give us the + same argument. However it seems not so easy to calculate the derivatives + and then to count them. Therefore we preferred our direct method of + using tagging-functions involving equivalence classes. This is also where + our method shines, because we can completely side-step the standard + argument \cite{Kozen97} where automata need to be composed, which is not so + convenient to formalise in a HOL-based theorem prover. + + + Lines of code / nuprl + + closure properties + *} diff -r e500cab16be4 -r d65d071798ff tphols-2011/myhill.pdf Binary file tphols-2011/myhill.pdf has changed