1 \documentclass[acmtocl]{acmtrans2m} |
1 \documentclass[acmtocl,final]{acmtrans2m} |
2 \usepackage{isabelle} |
2 \usepackage{isabelle} |
3 \usepackage{isabellesym} |
3 \usepackage{isabellesym} |
4 \usepackage{amsmath} |
4 \usepackage{amsmath} |
5 \usepackage{amssymb} |
5 \usepackage{amssymb} |
6 \usepackage{tikz} |
6 \usepackage{tikz} |
7 \usepackage{pgf} |
7 \usepackage{pgf} |
8 \usetikzlibrary{arrows,automata,decorations,fit,calc} |
8 \usetikzlibrary{arrows,automata,decorations,fit,calc} |
9 \usetikzlibrary{shapes,shapes.arrows,snakes,positioning} |
9 \usetikzlibrary{shapes,shapes.arrows,snakes,positioning} |
10 \usepgflibrary{shapes.misc} % LATEX and plain TEX and pure pgf |
10 \usepgflibrary{shapes.misc} % LATEX and plain TEX and pure pgf |
11 \usetikzlibrary{matrix} |
11 \usetikzlibrary{matrix} |
12 %%\usepackage{pdfsetup} |
12 %%%\usepackage{pdfsetup} |
13 \usepackage{ot1patch} |
13 \usepackage{ot1patch} |
14 \usepackage{times} |
14 \usepackage{times} |
15 \usepackage{stmaryrd} |
15 \usepackage{stmaryrd} |
16 \usepackage{mathpartir} |
16 \usepackage{mathpartir} |
17 \usepackage{longtable} |
17 \usepackage{longtable} |
46 %%\thanks{This is a revised and expanded version of \cite{WuZhangUrban11}.} |
46 %%\thanks{This is a revised and expanded version of \cite{WuZhangUrban11}.} |
47 \author{Chunhan Wu\\PLA University of Science and Technology Nanjing, China \and |
47 \author{Chunhan Wu\\PLA University of Science and Technology Nanjing, China \and |
48 Xingyuan Zhang\\PLA University of Science and Technology Nanjing, China \and |
48 Xingyuan Zhang\\PLA University of Science and Technology Nanjing, China \and |
49 Christian Urban\\ King's College London, United Kingdom} |
49 Christian Urban\\ King's College London, United Kingdom} |
50 |
50 |
|
51 \markboth{C.~Wu et al.}{A Formalisation of the Myhill-Nerode Theorem based on Regular |
|
52 Expressions} |
|
53 |
51 \begin{abstract} |
54 \begin{abstract} |
52 There are numerous textbooks on regular languages. Nearly all of them |
55 There are numerous textbooks on regular languages. Many of them focus |
53 introduce the subject by describing finite automata and only |
56 on finite automata for proving properties. Unfortunately, automata |
54 mentioning on the side a connection with regular |
57 are not so straightforward to formalise in theorem provers. The reason |
55 expressions. Unfortunately, automata are not so straightforward to |
58 is that natural representations for automata are graphs, matrices or |
56 formalise in theorem provers. The reason is that a natural |
59 functions, none of which are inductive datatypes. Regular |
57 representation for automata are graphs, matrices or functions, none of |
60 expressions can be defined straightforwardly as a datatype and a |
58 which are inductive datatypes. Also convenient operations for disjoint |
61 corresponding reasoning infrastructure comes for free in theorem |
59 unions of graphs, matrices and functions are not easily formalisiable |
62 provers. We show in this paper that a central result from formal |
60 in Isabelle/HOL, the theorem prover we are using. In contrast, regular |
63 language theory---the Myhill-Nerode Theorem---can be recreated using |
61 expressions can be defined conveniently as a datatype and a |
64 only regular expressions. From this theorem many closure properties of |
62 corresponding reasoning infrastructure comes for free. We show in this |
65 regular languages follow. |
63 paper that a central result from formal language theory---the |
|
64 Myhill-Nerode Theorem---can be recreated using only regular |
|
65 expressions. From this theorem many closure properties of regular |
|
66 languages follow. |
|
67 \end{abstract} |
66 \end{abstract} |
68 \category{F.4.1}{Mathematical Logic and Formal Languages}{Mechanical Theorem Proving} |
67 \category{F.4.1}{Mathematical Logic and Formal Languages}{Mechanical Theorem Proving} |
69 \category{F.4.3}{Mathematical Logic and Formal Languages}{Formal Languages} |
68 \category{F.4.3}{Mathematical Logic and Formal Languages}{Formal Languages} |
70 \terms{Interactive theorem proving, regular languages} |
69 \terms{Interactive theorem proving, regular languages} |
71 \keywords{Myhill-Nerode theorem, regular expressions, Isabelle theorem prover} |
70 \keywords{Myhill-Nerode theorem, regular expressions, Isabelle theorem prover} |