24 |
24 |
25 text {* |
25 text {* |
26 Regular languages are an important and well-understood subject in Computer |
26 Regular languages are an important and well-understood subject in Computer |
27 Science, with many beautiful theorems and many useful algorithms. There is a |
27 Science, with many beautiful theorems and many useful algorithms. There is a |
28 wide range of textbooks on this subject, many of which are aimed at |
28 wide range of textbooks on this subject, many of which are aimed at |
29 students containing very detailed ``pencil-and-paper'' proofs |
29 students and contain very detailed ``pencil-and-paper'' proofs |
30 (e.g.~\cite{Kozen97}). It seems natural to exercise theorem provers by |
30 (e.g.~\cite{Kozen97}). It seems natural to exercise theorem provers by |
31 formalising these theorems and by verifying formally the algorithms. |
31 formalising these theorems and by verifying formally the algorithms. |
32 |
32 |
33 There is however a problem with this: the typical approach to regular |
33 There is however a problem with this: the typical approach to regular |
34 languages is to introduce automata and then define everything in terms of |
34 languages is to introduce finite automata and then define everything in terms of |
35 them. For example, a regular language is normally defined as one where |
35 them. For example, a regular language is normally defined as one where |
36 there is a finite deterministic automaton that recognises all the strings of |
36 there is a finite deterministic automaton that recognises all the strings of |
37 the language. One benefit of this approach is that it is easy to convince |
37 the language. This approach has many benefits. One is that it is easy to convince |
38 oneself from the fact that regular languages are closed under |
38 oneself from the fact that regular languages are closed under |
39 complementation: one just has to exchange the accepting and non-accepting |
39 complementation: one just has to exchange the accepting and non-accepting |
40 states in the automaton to obtain an automaton for the complement language. |
40 states in the corresponding automaton to obtain an automaton for the complement language. |
41 |
|
42 The problem lies with formalising such reasoning in a theorem |
41 The problem lies with formalising such reasoning in a theorem |
43 prover, in our case Isabelle/HOL. Automata need to be represented as graphs |
42 prover, in our case Isabelle/HOL. Automata need to be represented as graphs |
44 or matrices, neither of which can be defined as inductive datatype.\footnote{In |
43 or matrices, neither of which can be defined as inductive datatype.\footnote{In |
45 some works functions are used to represent transitions, but they are also not |
44 some works functions are used to represent transitions, but they are also not |
46 inductive datatypes.} This means we have to build our own reasoning infrastructure |
45 inductive datatypes.} This means we have to build our own reasoning infrastructure |
47 for them, as neither Isabelle nor HOL4 support them with libraries. |
46 for them, as neither Isabelle nor HOL4 nor HOLlight support them with libraries. |
48 Even worse, reasoning about graphs in typed languages can be a real hassle |
47 |
49 making proofs quite clunky. Consider for example the operation of combining |
48 Even worse, reasoning about graphs in typed languages can be a real hassle. |
|
49 Consider for example the operation of combining |
50 two automata into a new automaton by connecting their |
50 two automata into a new automaton by connecting their |
51 initial states to a new initial state (similarly with the accepting states):a |
51 initial states to a new initial state (similarly with the accepting states): |
52 |
52 |
53 \begin{center} |
53 \begin{center} |
54 picture |
54 picture |
55 \end{center} |
55 \end{center} |
56 |
56 |
57 \noindent |
57 \noindent |
58 How should we implement this operation? On paper we can just |
58 How should we implement this operation? On paper we can just |
59 form the disjoint union of the state nodes and add two more nodes---one for the |
59 form the disjoint union of the state nodes and add two more nodes---one for the |
60 new initial state, the other for the new accepting state. |
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 |
62 straightforwardly implemented. But in a HOL-based theorem prover the |
63 |
63 standard definition of disjoint unions as pairs |
64 |
64 |
65 |
65 \begin{center} |
66 |
66 definition |
67 |
67 \end{center} |
68 |
68 |
69 |
69 \noindent |
70 Therefore instead of defining a regular language as being one where there exists an |
70 changes the type (from sets of nodes to sets of pairs). This means we |
71 automata that recognises all of its strings, we define |
71 cannot formulate in this represeantation any property about \emph{all} |
|
72 automata---since there is no type quantification available in HOL-based |
|
73 theorem provers. A working alternative is to give every state node an |
|
74 identity, for example a natural number, and then be careful to rename |
|
75 these indentities appropriately when connecting two automata together. |
|
76 This results in very clunky side-proofs establishing that properties |
|
77 are invariant under renaming. We are only aware of the formalisation |
|
78 of automata theory in Nuprl that carries this approach trough and is |
|
79 quite substantial. |
|
80 |
|
81 We will take a completely different approach to formalising theorems |
|
82 about regular languages. Instead of defining a regular language as one |
|
83 where there exists an automaton that recognises all of its strings, we |
|
84 define a regular language as |
72 |
85 |
73 \begin{definition}[A Regular Language] |
86 \begin{definition}[A Regular Language] |
74 A language @{text A} is regular, if there is a regular expression that matches all |
87 A language @{text A} is regular, if there is a regular expression that matches all |
75 strings of @{text "A"}. |
88 strings of @{text "A"}. |
76 \end{definition} |
89 \end{definition} |
77 |
90 |
|
91 \noindent |
|
92 The reason is that regular expressinons, unlike graphs and metrices, can |
|
93 be eaily defined as inductive datatype and this means a reasoning infrastructre |
|
94 comes for them in Isabelle for free. The purpose of this paper is to |
|
95 show that a central and highly non-trivisl result about regular languages, |
|
96 namely the Myhill-Nerode theorem, can be recreated only using regular |
|
97 expressions. In our approach we do not need to formalise graps or |
|
98 metrices. |
|
99 |
|
100 |
78 \noindent |
101 \noindent |
79 {\bf Contributions:} A proof of the Myhill-Nerode Theorem based on regular expressions. The |
102 {\bf Contributions:} A proof of the Myhill-Nerode Theorem based on regular expressions. The |
80 finiteness part of this theorem is proved using tagging-functions (which to our knowledge |
103 finiteness part of this theorem is proved using tagging-functions (which to our knowledge |
81 are novel in this context). |
104 are novel in this context). |
82 |
105 |