diff -r c1d9a4ac9f8e -r 828ea293b61f Paper/Paper.thy --- 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 \ string) \ bool" + UPLUS :: "'a set \ 'a set \ (nat \ '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 ("\") - + REL ("\") 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 \ {(1, x) | x. x \ A\<^isub>1} \ {(2, y) | y. y \ 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