19   REL ("\<approx>")

    20   REL ("\<approx>") and

    20 

    21   UPLUS ("_ \<^raw:\ensuremath{\uplus}> _" [90, 90] 90)

    28   wide range of textbooks on this subject, many of which are aimed at

    29   wide range of textbooks on this subject, many of which are aimed at students

    29   students and contain very detailed ``pencil-and-paper'' proofs

    30   and contain very detailed ``pencil-and-paper'' proofs

    33   There is however a problem with this: the typical approach to regular

    34   There is however a problem: the typical approach to regular languages is to

    34   languages is to introduce finite automata and then define everything in terms of

    35   introduce finite automata and then define everything in terms of them.  For

    35   them.  For example, a regular language is normally defined as one where

    36   example, a regular language is normally defined as one whose strings are

    36   there is a finite deterministic automaton that recognises all the strings of

    37   recognised by a finite deterministic automaton. This approach has many

    37   the language. This approach has many benefits. One is that it is easy to convince

    38   benefits. Among them is that it is easy to convince oneself from the fact that

    38   oneself from the fact that regular languages are closed under

    39   regular languages are closed under complementation: one just has to exchange

    39   complementation: one just has to exchange the accepting and non-accepting

    40   the accepting and non-accepting states in the corresponding automaton to

    40   states in the corresponding automaton to obtain an automaton for the complement language.

    41   obtain an automaton for the complement language.  The problem, however, lies with

    41   The problem lies with formalising such reasoning in a theorem

    42   formalising such reasoning in a theorem prover, in our case

    42   prover, in our case Isabelle/HOL. Automata need to be represented as graphs 

    43   Isabelle/HOL. Automata need to be represented as graphs or matrices, neither

    43   or matrices, neither of which can be defined as inductive datatype.\footnote{In 

    44   of which can be defined as inductive datatype.\footnote{In some works

    44   some works functions are used to represent transitions, but they are also not 

    45   functions are used to represent state transitions, but also they are not

    45   inductive datatypes.} This means we have to build our own reasoning infrastructure

    46   inductive datatypes.} This means we have to build our own reasoning

    46   for them, as neither Isabelle nor HOL4 nor HOLlight support them with libraries.

    47   infrastructure for them, as neither Isabelle/HOL nor HOL4 nor HOLlight support

    47   

    48   them with libraries.

    48   Even worse, reasoning about graphs in typed languages can be a real hassle. 

    49 

    49   Consider for example the operation of combining 

    50   Even worse, reasoning about graphs and matrices can be a real hassle in HOL-based

    50   two automata into a new automaton by connecting their

    51   theorem provers.  Consider for example the operation of sequencing 

    51   initial states to a new initial state (similarly with the accepting states):

    52   two automata, say $A_1$ and $A_2$, by connecting the

    52   

    53   accepting states of one atomaton to the 

    53   \begin{center}

    54   initial state of the other:

    54   picture

    55   

    55   \end{center}

    56   

    56 

    57   \begin{center}

    57   \noindent

    58   \begin{tabular}{ccc}

    58   How should we implement this operation? On paper we can just

    59   \begin{tikzpicture}[scale=0.8]

    59   form the disjoint union of the state nodes and add two more nodes---one for the

    60   %\draw[step=2mm] (-1,-1) grid (1,1);

    60   new initial state, the other for the new accepting state. In a theorem

    61   

    61   prover based on set-theory, this operaton can be more or less

    62   \draw[rounded corners=1mm, very thick] (-1.0,-0.3) rectangle (-0.2,0.3);

    62   straightforwardly implemented. But in a HOL-based theorem prover the

    63   \draw[rounded corners=1mm, very thick] ( 0.2,-0.3) rectangle ( 1.0,0.3);

    63   standard definition of disjoint unions as pairs

    64 

    64 

    65   \node (A) at (-1.0,0.0) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};

    65   \begin{center}

    66   \node (B) at ( 0.2,0.0) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};

    66   definition

    67   

    67   \end{center}

    68   \node (C) at (-0.2, 0.13) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};

    68 

    69   \node (D) at (-0.2,-0.13) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};

    69   \noindent

    70 

    70   changes the type (from sets of nodes to sets of pairs). This means we

    71   \node (E) at (1.0, 0.2) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};

    71   cannot formulate in this represeantation any property about \emph{all} 

    72   \node (F) at (1.0,-0.0) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};

    72   automata---since there is no type quantification available in HOL-based

    73   \node (G) at (1.0,-0.2) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};

    73   theorem provers. A working alternative is to give every state node an 

    74 

    74   identity, for example a natural number, and then be careful to rename

    75   \draw (-0.6,0.0) node {\footnotesize$A_1$};

    75   these indentities appropriately when connecting two automata together. 

    76   \draw ( 0.6,0.0) node {\footnotesize$A_2$};

    76   This results in very clunky side-proofs establishing that properties

    77   \end{tikzpicture}

    77   are invariant under renaming. We are only aware of the formalisation 

    78 

    78   of automata theory in Nuprl that carries this approach trough and is

    79   & 

    79   quite substantial. 

    80 

    80   

    81   \raisebox{1.1mm}{\bf\Large$\;\;\;\Rightarrow\,\;\;$}

    81   We will take a completely different approach to formalising theorems

    82 

    82   about regular languages. Instead of defining a regular language as one 

    83   &

    83   where there exists an automaton that recognises all of its strings, we 

    84 

    84   define a regular language as

    85   \begin{tikzpicture}[scale=0.8]

    86   %\draw[step=2mm] (-1,-1) grid (1,1);

    87   

    88   \draw[rounded corners=1mm, very thick] (-1.0,-0.3) rectangle (-0.2,0.3);

    89   \draw[rounded corners=1mm, very thick] ( 0.2,-0.3) rectangle ( 1.0,0.3);

    90 

    91   \node (A) at (-1.0,0.0) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};

    92   \node (B) at ( 0.2,0.0) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};

    93   

    94   \node (C) at (-0.2, 0.13) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};

    95   \node (D) at (-0.2,-0.13) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};

    96 

    97   \node (E) at (1.0, 0.2) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};

    98   \node (F) at (1.0,-0.0) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};

    99   \node (G) at (1.0,-0.2) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};

   100   

   101   \draw (C) to [very thick, bend left=45] (B);

   102   \draw (D) to [very thick, bend right=45] (B);

   103 

   104   \draw (-0.6,0.0) node {\footnotesize$A_1$};

   105   \draw ( 0.6,0.0) node {\footnotesize$A_2$};

   106   \end{tikzpicture}

   107 

   108   \end{tabular}

   109   \end{center}

   110 

   111   \noindent

   112   On ``paper'' we can build the corresponding graph using the disjoint union of 

   113   the state nodes and add 

   114   two more nodes for the new initial state and the new accepting 

   115   state. Unfortunately in HOL, the definition for disjoint 

   116   union, namely 

   117 

   118   \begin{center}

   119   @{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}"}

   120   \end{center}

   121 

   122   \noindent

   123   changes the type---the disjoint union is not a set, but a set of pairs. 

   124   Using this definition for disjoint unions means we do not have a single type for automata

   125   and hence will not be able to state properties about \emph{all}

   126   automata, since there is no type quantification available in HOL. A working

   127   alternative is to give every state node an identity, for example a natural

   128   number, and then be careful renaming these identities apart whenever

   129   connecting two automata. This results in very clunky proofs

   130   establishing that properties are invariant under renaming. Similarly,

   131   combining two automata represented as matrices results in very adhoc

   132   constructions, which are not pleasant to reason about.

   133 

   134   Because of these problems to do with representing automata, there seems

   135   to be no substantial formalisation of automata theory and regular languages 

   136   carried out in a HOL-based theorem prover. We are only aware of the 

   137   large formalisation of the automata theory in Nuprl \cite{Constable00} and 

   138   some smaller in Coq \cite{Filliatre97}.

   139   

   140   In this paper, we will not attempt to formalise automata theory, but take a completely 

   141   different approach to regular languages. Instead of defining a regular language as one 

   142   where there exists an automaton that recognises all strings of the language, we define 

   143   a regular language as

    87   A language @{text A} is regular, if there is a regular expression that matches all

   146   A language @{text A} is regular, provided there is a regular expression that matches all

    92   The reason is that regular expressinons, unlike graphs and metrices, can

   151   The reason is that regular expressions, unlike graphs and matrices, can

    93   be eaily defined as inductive datatype and this means a reasoning infrastructre

   152   be easily defined as inductive datatype. Therefore a corresponding reasoning 

    94   comes for them in Isabelle for free. The purpose of this paper is to

   153   infrastructure comes in Isabelle for free. The purpose of this paper is to

    95   show that a central and highly non-trivisl result about regular languages, 

   154   show that a central result about regular languages, the Myhill-Nerode theorem,  

    96   namely the Myhill-Nerode theorem,  can be recreated only using regular 

   155   can be recreated by only using regular expressions. A corollary of this

    97   expressions. In our approach we do not need to formalise graps or

   156   theorem will be the usual closure properties, including complementation,

    98   metrices.

   157   of regular languages.