1 \documentclass{ita} |
1 \documentclass[acmtocl]{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{proof} |
|
16 %%\usepackage{mathabx} |
|
17 \usepackage{stmaryrd} |
15 \usepackage{stmaryrd} |
18 \usepackage{mathpartir} |
16 \usepackage{mathpartir} |
|
17 \usepackage{longtable} |
19 |
18 |
20 \urlstyle{rm} |
19 \urlstyle{rm} |
21 \isabellestyle{it} |
20 \isabellestyle{it} |
22 \renewcommand{\isastyleminor}{\it}% |
21 \renewcommand{\isastyleminor}{\it}% |
23 \renewcommand{\isastyle}{\normalsize\it}% |
22 \renewcommand{\isastyle}{\normalsize\it}% |
33 |
32 |
34 \newcommand{\isasymcalL}{\ensuremath{\cal{L}}} |
33 \newcommand{\isasymcalL}{\ensuremath{\cal{L}}} |
35 \newcommand{\isasymbigplus}{\ensuremath{\bigplus}} |
34 \newcommand{\isasymbigplus}{\ensuremath{\bigplus}} |
36 |
35 |
37 \newcommand{\bigplus}{\mbox{\Large\bf$+$}} |
36 \newcommand{\bigplus}{\mbox{\Large\bf$+$}} |
38 \begin{document} |
37 |
|
38 \newtheorem{thrm}{Theorem}[section] |
|
39 \newtheorem{lmm}{Lemma}[section] |
|
40 \newtheorem{dfntn}{Definition}[section] |
|
41 \newtheorem{prpstn}{Proposition}[section] |
|
42 |
39 |
43 |
40 \title{A Formalisation of the Myhill-Nerode Theorem\\ based on Regular |
44 \title{A Formalisation of the Myhill-Nerode Theorem\\ based on Regular |
41 Expressions} |
45 Expressions$^\star$} |
42 \thanks{This is a revised and expanded version of \cite{WuZhangUrban11}.} |
46 %%\thanks{This is a revised and expanded version of \cite{WuZhangUrban11}.} |
43 \author{Chunhan Wu}\address{PLA University of Science and Technology, China} |
47 \author{Chunhan Wu\\PLA University of Science and Technology Nanjing, China \and |
44 \author{Xingyuan Zhang}\sameaddress{1} |
48 Xingyuan Zhang\\PLA University of Science and Technology Nanjing, China \and |
45 \author{Christian Urban}\address{King's College London, United Kingdom}\secondaddress{corresponding author} |
49 Christian Urban\\ King's College London, United Kingdom} |
46 \subjclass{68Q45} |
|
47 \keywords{Myhill-Nerode theorem, regular expressions, Isabelle theorem prover} |
|
48 |
50 |
49 \begin{abstract} |
51 \begin{abstract} |
50 There are numerous textbooks on regular languages. Nearly all of them |
52 There are numerous textbooks on regular languages. Nearly all of them |
51 introduce the subject by describing finite automata and only mentioning on the |
53 introduce the subject by describing finite automata and only |
52 side a connection with regular expressions. Unfortunately, automata are difficult |
54 mentioning on the side a connection with regular |
53 to formalise in HOL-based theorem provers. The reason is that |
55 expressions. Unfortunately, automata are not so straightforward to |
54 they need to be represented as graphs, matrices or functions, none of which |
56 formalise in theorem provers. The reason is that a natural |
55 are inductive datatypes. Also convenient operations for disjoint unions of |
57 representation for automata are graphs, matrices or functions, none of |
56 graphs, matrices and functions are not easily formalisiable in HOL. In contrast, regular |
58 which are inductive datatypes. Also convenient operations for disjoint |
57 expressions can be defined conveniently as a datatype and a corresponding |
59 unions of graphs, matrices and functions are not easily formalisiable |
58 reasoning infrastructure comes for free. We show in this paper that a central |
60 in Isabelle/HOL, the theorem prover we are using. In contrast, regular |
59 result from formal language theory---the Myhill-Nerode Theorem---can be |
61 expressions can be defined conveniently as a datatype and a |
60 recreated using only regular expressions. From this theorem many closure |
62 corresponding reasoning infrastructure comes for free. We show in this |
61 properties of 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. |
62 \end{abstract} |
67 \end{abstract} |
|
68 \category{F.4.1}{Mathematical Logic and Formal Languages}{Mechanical Theorem Proving} |
|
69 \category{F.4.3}{Mathematical Logic and Formal Languages}{Formal Languages} |
|
70 \terms{Interactive theorem proving, regular languages} |
|
71 \keywords{Myhill-Nerode theorem, regular expressions, Isabelle theorem prover} |
|
72 \begin{document} |
|
73 \begin{bottomstuff} |
|
74 Corresponding Author: Christian Urban, Department of Informatics, King's College London, |
|
75 Strand, London WC2R 2LS, UK. Email: christian.urban@kcl.ac.uk.\\ |
|
76 $^\star$This is a revised and expanded version of \cite{WuZhangUrban11}. |
|
77 \end{bottomstuff} |
63 \maketitle |
78 \maketitle |
64 |
79 |
|
80 |
65 \input{session} |
81 \input{session} |
66 |
|
67 %%\mbox{}\\[-10mm] |
|
68 \bibliographystyle{plain} |
|
69 \bibliography{root} |
|
70 |
82 |
71 \end{document} |
83 \end{document} |
72 |
84 |
73 %%% Local Variables: |
85 %%% Local Variables: |
74 %%% mode: latex |
86 %%% mode: latex |