--- a/Paper/Paper.thy Fri Feb 18 14:26:23 2011 +0000
+++ b/Paper/Paper.thy Fri Feb 18 15:06:06 2011 +0000
@@ -45,7 +45,7 @@
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
+ and contain very detailed `pencil-and-paper' proofs
(e.g.~\cite{Kozen97}). It seems natural to exercise theorem provers by
formalising the theorems and by verifying formally the algorithms.
@@ -58,7 +58,7 @@
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 are build up from states and transitions that
+ Isabelle/HOL. Automata are built up from states and transitions that
need to be represented as graphs, matrices or functions, none
of which can be defined as inductive datatype.
@@ -124,7 +124,7 @@
\end{center}
\noindent
- On ``paper'' we can define the corresponding graph in terms of the disjoint
+ On `paper' we can define the corresponding graph in terms of the disjoint
union of the state nodes. Unfortunately in HOL, the standard definition for disjoint
union, namely
%
@@ -181,13 +181,13 @@
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 HOL-based theorem provers. Nipkow establishes in
- \cite{Nipkow98} the link between regular expressions and automata in
- the context of lexing. Berghofer and Reiter formalise automata working over
- bit strings in the context of Presburger arithmetic \cite{BerghoferReiter09}.
+ carried out in HOL-based theorem provers. Nipkow \cite{Nipkow98} establishes
+ the link between regular expressions and automata in
+ the context of lexing. Berghofer and Reiter \cite{BerghoferReiter09}
+ formalise automata working over
+ bit strings in the context of Presburger arithmetic.
The only larger formalisations of automata theory
- are carried out in Nuprl \cite{Constable00} and in Coq (for example
- \cite{Filliatre97}).
+ are carried out in Nuprl \cite{Constable00} and in Coq \cite{Filliatre97}.
In this paper, we will not attempt to formalise automata theory in
Isabelle/HOL, but take a completely different approach to regular
@@ -268,14 +268,14 @@
Central to our proof will be the solution of equational systems
- involving equivalence classes of languages. For this we will use Arden's lemma \cite{Brzozowski64}
+ involving equivalence classes of languages. For this we will use Arden's lemma \cite{Brzozowski64},
which solves equations of the form @{term "X = A ;; X \<union> B"} provided
- @{term "[] \<notin> A"}. However we will need the following ``reverse''
+ @{term "[] \<notin> A"}. However we will need the following `reverse'
version of Arden's lemma.
\begin{lemma}[Reverse Arden's Lemma]\label{arden}\mbox{}\\
If @{thm (prem 1) arden} then
- @{thm (lhs) arden} has the unique solution
+ @{thm (lhs) arden} if and only if
@{thm (rhs) arden}.
\end{lemma}
@@ -365,7 +365,7 @@
The key definition in the Myhill-Nerode theorem is the
\emph{Myhill-Nerode relation}, which states that w.r.t.~a language two
strings are related, provided there is no distinguishing extension in this
- language. This can be defined as:
+ language. This can be defined as tertiary relation:
\begin{definition}[Myhill-Nerode Relation]\mbox{}\\
@{thm str_eq_def[simplified str_eq_rel_def Pair_Collect]}
@@ -453,11 +453,11 @@
equivalence classes and only finitely many characters. The term @{text
"\<lambda>(EMPTY)"} in the first equation acts as a marker for the equivalence class
containing @{text "[]"}.\footnote{Note that we mark, roughly speaking, the
- single ``initial'' state in the equational system, which is different from
+ single `initial' state in the equational system, which is different from
the method by Brzozowski \cite{Brzozowski64}, where he marks the
- ``terminal'' states. We are forced to set up the equational system in our
- way, because the Myhill-Nerode relation determines the ``direction'' of the
- transitions. The successor ``state'' of an equivalence class @{text Y} can
+ `terminal' states. We are forced to set up the equational system in our
+ way, because the Myhill-Nerode relation determines the `direction' of the
+ transitions. The successor `state' of an equivalence class @{text Y} can
be reached by adding characters to the end of @{text Y}. This is also the
reason why we have to use our reverse version of Arden's lemma.}
Overloading the function @{text \<calL>} for the two kinds of terms in the
@@ -569,7 +569,7 @@
\begin{lemma}\label{ardenable}
Given an equation @{text "X = rhs"}.
If @{text "X = \<Union>\<calL> ` rhs"},
- @{thm (prem 2) Arden_keeps_eq} and
+ @{thm (prem 2) Arden_keeps_eq}, and
@{thm (prem 3) Arden_keeps_eq}, then
@{text "X = \<Union>\<calL> ` (Arden X rhs)"}
\end{lemma}
@@ -640,11 +640,11 @@
\noindent
We are not concerned here with the definition of this operator
- (see \cite{BerghoferNipkow00}), but note that we eliminate
+ (see Berghofer and Nipkow \cite{BerghoferNipkow00}), but note that we eliminate
in each @{const Iter}-step a single equation, and therefore
have a well-founded termination order by taking the cardinality
of the equational system @{text ES}. This enables us to prove
- properties about our definition of @{const Solve} when we ``call'' it with
+ properties about our definition of @{const Solve} when we `call' it with
the equivalence class @{text X} and the initial equational system
@{term "Init (UNIV // \<approx>A)"} from
\eqref{initcs} using the principle:
@@ -690,7 +690,7 @@
\noindent
The first two ensure that the equational system is always finite (number of equations
- and number of terms in each equation); the second makes sure the ``meaning'' of the
+ and number of terms in each equation); the second makes sure the `meaning' of the
equations is preserved under our transformations. The other properties are a bit more
technical, but are needed to get our proof through. Distinctness states that every
equation in the system is distinct. Ardenable ensures that we can always
@@ -880,8 +880,8 @@
text {*
In this paper we took the view that a regular language is one where there
- exists a regular expression that matches all its strings. Regular
- expressions can be conveniently defined as a datatype in a HOL-based theorem
+ exists a regular expression that matches all of its strings. Regular
+ expressions can conveniently be defined as a datatype in a HOL-based theorem
prover. For us it was therefore interesting to find out how far we can push
this point of view.
@@ -940,7 +940,7 @@
state leading up to that state. Usually, however, the states are characterised as the
ones starting from that state leading to the terminal states. The first
choice has consequences how the initial equational system is set up. We have
- the $\lambda$-term on our ``initial state'', while Brzozowski has it on the
+ the $\lambda$-term on our `initial state', while Brzozowski has it on the
terminal states. This means we also need to reverse the direction of Arden's
lemma.
@@ -964,7 +964,7 @@
limitations. One is that there seems to be no notion of a minimal regular
expression, like there is for automata. For an implementation of a simple
regular expression matcher, whose correctness has been formally
- established, we refer the reader to \cite{OwensSlind08}.
+ established, we refer the reader to Owens and Slind \cite{OwensSlind08}.
*}