Journal/Paper.thy
changeset 249 061b32d78471
parent 248 47446f111550
child 250 b1946e131ce8
equal deleted inserted replaced
248:47446f111550 249:061b32d78471
   425   main purpose of this paper is to show that a central result about regular
   425   main purpose of this paper is to show that a central result about regular
   426   languages---the Myhill-Nerode Theorem---can be recreated by only using
   426   languages---the Myhill-Nerode Theorem---can be recreated by only using
   427   regular expressions. This theorem gives necessary and sufficient conditions
   427   regular expressions. This theorem gives necessary and sufficient conditions
   428   for when a language is regular. As a corollary of this theorem we can easily
   428   for when a language is regular. As a corollary of this theorem we can easily
   429   establish the usual closure properties, including complementation, for
   429   establish the usual closure properties, including complementation, for
   430   regular languages. We use the continuation lemma \cite{Rosenberg06}, 
   430   regular languages. We use the Continuation Lemma \cite{Rosenberg06}, 
   431   which is also a corollary of the Myhill-Nerode Theorem, for establishing 
   431   which is also a corollary of the Myhill-Nerode Theorem, for establishing 
   432   the non-regularity of the language @{text "a\<^isup>nb\<^isup>n"}.\medskip
   432   the non-regularity of the language @{text "a\<^isup>nb\<^isup>n"}.\medskip
   433   
   433   
   434   \noindent 
   434   \noindent 
   435   {\bf Contributions:} There is an extensive literature on regular languages.
   435   {\bf Contributions:} There is an extensive literature on regular languages.
  2396   characterised as the strings starting from that state leading to the
  2396   characterised as the strings starting from that state leading to the
  2397   terminal states.  The first choice has consequences about how the initial
  2397   terminal states.  The first choice has consequences about how the initial
  2398   equational system is set up. We have the $\lambda$-term on our `initial
  2398   equational system is set up. We have the $\lambda$-term on our `initial
  2399   state', while Brzozowski has it on the terminal states. This means we also
  2399   state', while Brzozowski has it on the terminal states. This means we also
  2400   need to reverse the direction of Arden's Lemma. We have not found anything
  2400   need to reverse the direction of Arden's Lemma. We have not found anything
  2401   in the literature about our way of proving the first direction of the
  2401   in the `pencil-and-paper-reasoning' literature about our way of proving the 
  2402   Myhill-Nerode Theorem, but it appears to be folklore.
  2402   first direction of the Myhill-Nerode Theorem, but it appears to be folklore.
  2403 
  2403 
  2404   We presented two proofs for the second direction of the Myhill-Nerode
  2404   We presented two proofs for the second direction of the Myhill-Nerode
  2405   Theorem. One direct proof using tagging-functions and another using partial
  2405   Theorem. One direct proof using tagging-functions and another using partial
  2406   derivatives. This part of our work is where our method using regular
  2406   derivatives. This part of our work is where our method using regular
  2407   expressions shines, because we can completely side-step the standard
  2407   expressions shines, because we can completely side-step the standard