--- a/Paper/Paper.thy Fri Feb 04 13:33:18 2011 +0000
+++ b/Paper/Paper.thy Fri Feb 04 22:54:29 2011 +0000
@@ -7,6 +7,7 @@
consts
REL :: "(string \<times> string) \<Rightarrow> bool"
+ UPLUS :: "'a set \<Rightarrow> 'a set \<Rightarrow> (nat \<times> 'a) set"
notation (latex output)
@@ -16,8 +17,8 @@
pow ("_\<^bsup>_\<^esup>" [100, 100] 100) and
Suc ("_+1" [100] 100) and
quotient ("_ \<^raw:\ensuremath{\!\sslash\!}> _" [90, 90] 90) and
- REL ("\<approx>")
-
+ REL ("\<approx>") and
+ UPLUS ("_ \<^raw:\ensuremath{\uplus}> _" [90, 90] 90)
(*>*)
section {* Introduction *}
@@ -25,77 +26,135 @@
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
+ 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 with this: 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 where
- there is a finite deterministic automaton that recognises all the strings of
- the language. This approach has many benefits. One 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 lies with formalising such reasoning in a theorem
- prover, in our case Isabelle/HOL. Automata 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 transitions, but they are also not
- inductive datatypes.} This means we have to build our own reasoning infrastructure
- for them, as neither Isabelle nor HOL4 nor HOLlight support them with libraries.
+ 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 theorem prover, in our case
+ Isabelle/HOL. Automata 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 one atomaton to the
+ initial state of the other:
- Even worse, reasoning about graphs in typed languages can be a real hassle.
- Consider for example the operation of combining
- two automata into a new automaton by connecting their
- initial states to a new initial state (similarly with the accepting states):
\begin{center}
- picture
+ \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
- How should we implement this operation? On paper we can just
- form the disjoint union of the state nodes and add two more nodes---one for the
- new initial state, the other for the new accepting state. In a theorem
- prover based on set-theory, this operaton can be more or less
- straightforwardly implemented. But in a HOL-based theorem prover the
- standard definition of disjoint unions as pairs
+ On ``paper'' we can build the corresponding graph using the disjoint union of
+ the state nodes and add
+ two more nodes for the new initial state and the new accepting
+ state. Unfortunately in HOL, the definition for disjoint
+ union, namely
\begin{center}
- definition
+ @{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 (from sets of nodes to sets of pairs). This means we
- cannot formulate in this represeantation any property about \emph{all}
- automata---since there is no type quantification available in HOL-based
- theorem provers. A working alternative is to give every state node an
- identity, for example a natural number, and then be careful to rename
- these indentities appropriately when connecting two automata together.
- This results in very clunky side-proofs establishing that properties
- are invariant under renaming. We are only aware of the formalisation
- of automata theory in Nuprl that carries this approach trough and is
- quite substantial.
+ 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. A working
+ alternative 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 very clunky proofs
+ establishing that properties are invariant under renaming. Similarly,
+ combining 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 in Coq \cite{Filliatre97}.
- We will take a completely different approach to formalising theorems
- about regular languages. Instead of defining a regular language as one
- where there exists an automaton that recognises all of its strings, we
- define a regular language as
+ 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, if there is a regular expression that matches all
+ 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 expressinons, unlike graphs and metrices, can
- be eaily defined as inductive datatype and this means a reasoning infrastructre
- comes for them in Isabelle for free. The purpose of this paper is to
- show that a central and highly non-trivisl result about regular languages,
- namely the Myhill-Nerode theorem, can be recreated only using regular
- expressions. In our approach we do not need to formalise graps or
- metrices.
+ The reason is that regular expressions, unlike graphs and matrices, can
+ be easily defined as inductive datatype. Therefore a corresponding reasoning
+ infrastructure comes in Isabelle for free. 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. A corollary of this
+ theorem will be the usual closure properties, including complementation,
+ of regular languages.
\noindent