(*<*)+
−
theory Paper+
−
imports "../Myhill" "LaTeXsugar"+
−
begin+
−
+
−
declare [[show_question_marks = false]]+
−
+
−
consts+
−
 REL :: "(string \<times> string) \<Rightarrow> bool"+
−
 UPLUS :: "'a set \<Rightarrow> 'a set \<Rightarrow> (nat \<times> 'a) set"+
−
+
−
+
−
notation (latex output)+
−
  str_eq_rel ("\<approx>\<^bsub>_\<^esub>") and+
−
  Seq (infixr "\<cdot>" 100) and+
−
  Star ("_\<^bsup>\<star>\<^esup>") and+
−
  pow ("_\<^bsup>_\<^esup>" [100, 100] 100) and+
−
  Suc ("_+1" [100] 100) and+
−
  quotient ("_ \<^raw:\ensuremath{\!\sslash\!}> _" [90, 90] 90) and+
−
  REL ("\<approx>") and+
−
  UPLUS ("_ \<^raw:\ensuremath{\uplus}> _" [90, 90] 90) and+
−
  L ("L '(_')" [0] 101)+
−
(*>*)+
−
+
−
section {* Introduction *}+
−
+
−
text {*+
−
  Regular languages are an important and well-understood subject in Computer+
−
  Science, with many beautiful theorems and many useful algorithms. There is a+
−
  wide range of textbooks on this subject, many of which are aimed at students+
−
  and contain very detailed ``pencil-and-paper'' proofs+
−
  (e.g.~\cite{Kozen97}). It seems natural to exercise theorem provers by+
−
  formalising these theorems and by verifying formally the algorithms.+
−
+
−
  There is however a problem: the typical approach to regular languages is to+
−
  introduce finite automata and then define everything in terms of them.  For+
−
  example, a regular language is normally defined as one whose strings are+
−
  recognised by a finite deterministic automaton. This approach has many+
−
  benefits. Among them is that it is easy to convince oneself from the fact that+
−
  regular languages are closed under complementation: one just has to exchange+
−
  the accepting and non-accepting states in the corresponding automaton to+
−
  obtain an automaton for the complement language.  The problem, however, lies with+
−
  formalising such reasoning in a HOL-based theorem prover, in our case+
−
  Isabelle/HOL. Automata consist of states and transitions. They need to be represented +
−
  as graphs or matrices, neither+
−
  of which can be defined as inductive datatype.\footnote{In some works+
−
  functions are used to represent state transitions, but also they are not+
−
  inductive datatypes.} This means we have to build our own reasoning+
−
  infrastructure for them, as neither Isabelle/HOL nor HOL4 nor HOLlight support+
−
  them with libraries.+
−
+
−
  Even worse, reasoning about graphs and matrices can be a real hassle in HOL-based+
−
  theorem provers.  Consider for example the operation of sequencing +
−
  two automata, say $A_1$ and $A_2$, by connecting the+
−
  accepting states of $A_1$ to the initial state of $A_2$:+
−
  +
−
  +
−
  \begin{center}+
−
  \begin{tabular}{ccc}+
−
  \begin{tikzpicture}[scale=0.8]+
−
  %\draw[step=2mm] (-1,-1) grid (1,1);+
−
  +
−
  \draw[rounded corners=1mm, very thick] (-1.0,-0.3) rectangle (-0.2,0.3);+
−
  \draw[rounded corners=1mm, very thick] ( 0.2,-0.3) rectangle ( 1.0,0.3);+
−
+
−
  \node (A) at (-1.0,0.0) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};+
−
  \node (B) at ( 0.2,0.0) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};+
−
  +
−
  \node (C) at (-0.2, 0.13) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};+
−
  \node (D) at (-0.2,-0.13) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};+
−
+
−
  \node (E) at (1.0, 0.2) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};+
−
  \node (F) at (1.0,-0.0) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};+
−
  \node (G) at (1.0,-0.2) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};+
−
+
−
  \draw (-0.6,0.0) node {\footnotesize$A_1$};+
−
  \draw ( 0.6,0.0) node {\footnotesize$A_2$};+
−
  \end{tikzpicture}+
−
+
−
  & +
−
+
−
  \raisebox{1.1mm}{\bf\Large$\;\;\;\Rightarrow\,\;\;$}+
−
+
−
  &+
−
+
−
  \begin{tikzpicture}[scale=0.8]+
−
  %\draw[step=2mm] (-1,-1) grid (1,1);+
−
  +
−
  \draw[rounded corners=1mm, very thick] (-1.0,-0.3) rectangle (-0.2,0.3);+
−
  \draw[rounded corners=1mm, very thick] ( 0.2,-0.3) rectangle ( 1.0,0.3);+
−
+
−
  \node (A) at (-1.0,0.0) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};+
−
  \node (B) at ( 0.2,0.0) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};+
−
  +
−
  \node (C) at (-0.2, 0.13) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};+
−
  \node (D) at (-0.2,-0.13) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};+
−
+
−
  \node (E) at (1.0, 0.2) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};+
−
  \node (F) at (1.0,-0.0) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};+
−
  \node (G) at (1.0,-0.2) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};+
−
  +
−
  \draw (C) to [very thick, bend left=45] (B);+
−
  \draw (D) to [very thick, bend right=45] (B);+
−
+
−
  \draw (-0.6,0.0) node {\footnotesize$A_1$};+
−
  \draw ( 0.6,0.0) node {\footnotesize$A_2$};+
−
  \end{tikzpicture}+
−
+
−
  \end{tabular}+
−
  \end{center}+
−
+
−
  \noindent+
−
  On ``paper'' we can define the corresponding graph in terms of the disjoint +
−
  union of the state nodes. Unfortunately in HOL, the definition for disjoint +
−
  union, namely +
−
+
−
  \begin{center}+
−
  @{term "UPLUS A\<^isub>1 A\<^isub>2 \<equiv> {(1, x) | x. x \<in> A\<^isub>1} \<union> {(2, y) | y. y \<in> A\<^isub>2}"}+
−
  \end{center}+
−
+
−
  \noindent+
−
  changes the type---the disjoint union is not a set, but a set of pairs. +
−
  Using this definition for disjoint unions means we do not have a single type for automata+
−
  and hence will not be able to state properties about \emph{all}+
−
  automata, since there is no type quantification available in HOL. An+
−
  alternative, which provides us with a single type for automata, is to give every +
−
  state node an identity, for example a natural+
−
  number, and then be careful renaming these identities apart whenever+
−
  connecting two automata. This results in clunky proofs+
−
  establishing that properties are invariant under renaming. Similarly,+
−
  connecting two automata represented as matrices results in very adhoc+
−
  constructions, which are not pleasant to reason about.+
−
+
−
  Because of these problems to do with representing automata, there seems+
−
  to be no substantial formalisation of automata theory and regular languages +
−
  carried out in a HOL-based theorem prover. We are only aware of the +
−
  large formalisation of the automata theory in Nuprl \cite{Constable00} and +
−
  some smaller formalisations in Coq, for example \cite{Filliatre97}.+
−
  +
−
  In this paper, we will not attempt to formalise automata theory, but take a completely +
−
  different approach to regular languages. Instead of defining a regular language as one +
−
  where there exists an automaton that recognises all strings of the language, we define +
−
  a regular language as:+
−
+
−
  \begin{definition}[A Regular Language]+
−
  A language @{text A} is regular, provided there is a regular expression that matches all+
−
  strings of @{text "A"}.+
−
  \end{definition}+
−
  +
−
  \noindent+
−
  The reason is that regular expressions, unlike graphs and matrices, can+
−
  be easily defined as inductive datatype. Therefore a corresponding reasoning +
−
  infrastructure comes for free. This has recently been used for formalising regular +
−
  expression matching in HOL4 \cite{OwensSlind08}.  The purpose of this paper is to+
−
  show that a central result about regular languages, the Myhill-Nerode theorem,  +
−
  can be recreated by only using regular expressions. This theorem give a necessary+
−
  and sufficient condition for when a language is regular. As a corollary of this+
−
  theorem we can easily establish the usual closure properties, including +
−
  complementation, for regular languages.\smallskip+
−
  +
−
  \noindent+
−
  {\bf Contributions:} To our knowledge, our proof of the Myhill-Nerode theorem is the+
−
  first that is based on regular expressions, only. We prove the part of this theorem +
−
  stating that a regular expression has only finitely many partitions using certain +
−
  tagging-functions. Again to our best knowledge, these tagging functions have+
−
  not been used before to establish the Myhill-Nerode theorem.+
−
*}+
−
+
−
section {* Preliminaries *}+
−
+
−
text {*+
−
  Strings in Isabelle/HOL are lists of characters with the \emph{empty string}+
−
  being represented by the empty list, written @{term "[]"}. \emph{Languages}+
−
  are sets of strings. The language containing all strings is written in+
−
  Isabelle/HOL as @{term "UNIV::string set"}.  The notation for the quotient+
−
  of a language @{text A} according to a relation @{term REL} is @{term "A //+
−
  REL"}. The concatenation of two languages is written @{term "A ;; B"}; a+
−
  language raised to the power $n$ is written @{term "A \<up> n"}. Both concepts+
−
  are defined as+
−
+
−
  \begin{center}+
−
  @{thm Seq_def[THEN eq_reflection, where A1="A" and B1="B"]}+
−
  \hspace{7mm}+
−
  @{thm pow.simps(1)[THEN eq_reflection, where A1="A"]}+
−
  \hspace{7mm}+
−
  @{thm pow.simps(2)[THEN eq_reflection, where A1="A" and n1="n"]}+
−
  \end{center}+
−
+
−
  \noindent+
−
  where @{text "@"} is the usual list-append operation. The Kleene-star of a language @{text A}+
−
  is defined as the union over all powers, namely @{thm Star_def}.+
−
  +
−
  Central to our proof will be the solution of equational systems+
−
  involving regular expressions. For this we will use the following ``reverse'' +
−
  version of Arden's lemma.+
−
+
−
  \begin{lemma}[Reverse Arden's Lemma]\mbox{}\\+
−
  If @{thm (prem 1) ardens_revised} then+
−
  @{thm (lhs) ardens_revised} has the unique solution+
−
  @{thm (rhs) ardens_revised}.+
−
  \end{lemma}+
−
+
−
  \begin{proof}+
−
  For the right-to-left direction we assume @{thm (rhs) ardens_revised} and show+
−
  that @{thm (lhs) ardens_revised} holds. From Lemma ??? we have @{term "A\<star> = {[]} \<union> A ;; A\<star>"},+
−
  which is equal to @{term "A\<star> = {[]} \<union> A\<star> ;; A"}. Adding @{text B} to both +
−
  sides gives @{term "B ;; A\<star> = B ;; ({[]} \<union> A\<star> ;; A)"}, whose right-hand side+
−
  is equal to @{term "(B ;; A\<star>) ;; A \<union> B"}. This completes this direction. +
−
+
−
  For the other direction we assume @{thm (lhs) ardens_revised}. By a simple induction+
−
  on @{text n}, we can establish the property+
−
+
−
  \begin{center}+
−
  @{text "(*)"}\hspace{5mm} @{thm (concl) ardens_helper}+
−
  \end{center}+
−
  +
−
  \noindent+
−
  Using this property we can show that @{term "B ;; (A \<up> n) \<subseteq> X"} holds for+
−
  all @{text n}. From this we can infer @{term "B ;; A\<star> \<subseteq> X"} using Lemma ???.+
−
  For the inclusion in the other direction we assume a string @{text s}+
−
  with length @{text k} is element in @{text X}. Since @{thm (prem 1) ardens_revised}+
−
  we know that @{term "s \<notin> X ;; (A \<up> Suc k)"} since its length is only @{text k}+
−
  (the strings in @{term "X ;; (A \<up> Suc k)"} are all longer). +
−
  From @{text "(*)"} it follows then that+
−
  @{term s} must be element in @{term "(\<Union>m\<in>{0..k}. B ;; (A \<up> m))"}. This in turn+
−
  implies that @{term s} is in @{term "(\<Union>n. B ;; (A \<up> n))"}. Using Lemma ??? this+
−
  is equal to @{term "B ;; A\<star>"}, as we needed to show.\qed+
−
  \end{proof}+
−
+
−
  \noindent+
−
  Regular expressions are defined as the following inductive datatype+
−
+
−
  \begin{center}+
−
  @{text r} @{text "::="}+
−
  @{term NULL}\hspace{1.5mm}@{text"|"}\hspace{1.5mm} +
−
  @{term EMPTY}\hspace{1.5mm}@{text"|"}\hspace{1.5mm} +
−
  @{term "CHAR c"}\hspace{1.5mm}@{text"|"}\hspace{1.5mm} +
−
  @{term "SEQ r r"}\hspace{1.5mm}@{text"|"}\hspace{1.5mm} +
−
  @{term "ALT r r"}\hspace{1.5mm}@{text"|"}\hspace{1.5mm} +
−
  @{term "STAR r"}+
−
  \end{center}+
−
+
−
  \noindent+
−
  The language matched by a regular expression is defined as usual:+
−
+
−
  \begin{center}+
−
  \begin{tabular}{c@ {\hspace{10mm}}c}+
−
  \begin{tabular}{rcl}+
−
  @{thm (lhs) L_rexp.simps(1)} & @{text "\<equiv>"} & @{thm (rhs) L_rexp.simps(1)}\\+
−
  @{thm (lhs) L_rexp.simps(2)} & @{text "\<equiv>"} & @{thm (rhs) L_rexp.simps(2)}\\+
−
  @{thm (lhs) L_rexp.simps(3)[where c="c"]} & @{text "\<equiv>"} & @{thm (rhs) L_rexp.simps(3)[where c="c"]}\\+
−
  \end{tabular}+
−
  &+
−
  \begin{tabular}{rcl}+
−
  @{thm (lhs) L_rexp.simps(4)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]} & @{text "\<equiv>"} &+
−
       @{thm (rhs) L_rexp.simps(4)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}\\+
−
  @{thm (lhs) L_rexp.simps(5)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]} & @{text "\<equiv>"} &+
−
       @{thm (rhs) L_rexp.simps(5)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}\\+
−
  @{thm (lhs) L_rexp.simps(6)[where r="r"]} & @{text "\<equiv>"} &+
−
      @{thm (rhs) L_rexp.simps(6)[where r="r"]}\\+
−
  \end{tabular}+
−
  \end{tabular}+
−
  \end{center}+
−
*}+
−
+
−
section {* Finite Partitions Imply Regularity of a Language *}+
−
+
−
text {*+
−
  \begin{theorem}+
−
  Given a language @{text A}.+
−
  @{thm[mode=IfThen] hard_direction[where Lang="A"]}+
−
  \end{theorem}+
−
*}+
−
+
−
section {* Regular Expressions Generate Finitely Many Partitions *}+
−
+
−
text {*+
−
+
−
  \begin{theorem}+
−
  Given @{text "r"} is a regular expressions, then @{thm rexp_imp_finite}.+
−
  \end{theorem}  +
−
+
−
  \begin{proof}+
−
  By induction on the structure of @{text r}. The cases for @{const NULL}, @{const EMPTY}+
−
  and @{const CHAR} are straightforward, because we can easily establish+
−
+
−
  \begin{center}+
−
  \begin{tabular}{l}+
−
  @{thm quot_null_eq}\\+
−
  @{thm quot_empty_subset}\\+
−
  @{thm quot_char_subset}+
−
  \end{tabular}+
−
  \end{center}+
−
+
−
  \end{proof}+
−
*}+
−
+
−
+
−
section {* Conclusion and Related Work *}+
−
+
−
(*<*)+
−
end+
−
(*>*)+
−