(*<*)

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

(*>*)