regexp: Journal/document/root.tex@8ce9a432680b (annotated)

350 8ce9a432680b made changes for another journal submission of the MN-paper urbanc parents: 348 diff changeset	1	\documentclass[acmtocl,final]{acmtrans2m}
24 f72c82bf59e5 added paper urbanc parents: diff changeset	2	\usepackage{isabelle}
f72c82bf59e5 added paper urbanc parents: diff changeset	3	\usepackage{isabellesym}
f72c82bf59e5 added paper urbanc parents: diff changeset	4	\usepackage{amsmath}
f72c82bf59e5 added paper urbanc parents: diff changeset	5	\usepackage{amssymb}
f72c82bf59e5 added paper urbanc parents: diff changeset	6	\usepackage{tikz}
f72c82bf59e5 added paper urbanc parents: diff changeset	7	\usepackage{pgf}
125 62925473bf6b added pictures for seq-case urbanc parents: 123 diff changeset	8	\usetikzlibrary{arrows,automata,decorations,fit,calc}
62925473bf6b added pictures for seq-case urbanc parents: 123 diff changeset	9	\usetikzlibrary{shapes,shapes.arrows,snakes,positioning}
62925473bf6b added pictures for seq-case urbanc parents: 123 diff changeset	10	\usepgflibrary{shapes.misc} % LATEX and plain TEX and pure pgf
62925473bf6b added pictures for seq-case urbanc parents: 123 diff changeset	11	\usetikzlibrary{matrix}
350 8ce9a432680b made changes for another journal submission of the MN-paper urbanc parents: 348 diff changeset	12	%%%\usepackage{pdfsetup}
24 f72c82bf59e5 added paper urbanc parents: diff changeset	13	\usepackage{ot1patch}
f72c82bf59e5 added paper urbanc parents: diff changeset	14	\usepackage{times}
52 4a517c6ac07d tuning of the syntax; needs the stmaryrd latex package urbanc parents: 24 diff changeset	15	\usepackage{stmaryrd}
233 e2dc11e12e0b added section about SUBSEQ and SUPSEQ urbanc parents: 200 diff changeset	16	\usepackage{mathpartir}
348 bea94f1e6771 made changes for another journal submission of the MH-paper urbanc parents: 334 diff changeset	17	\usepackage{longtable}
123 23c0e6f2929d polished everywhere...two cases still missing urbanc parents: 116 diff changeset	18
24 f72c82bf59e5 added paper urbanc parents: diff changeset	19	\urlstyle{rm}
f72c82bf59e5 added paper urbanc parents: diff changeset	20	\isabellestyle{it}
f72c82bf59e5 added paper urbanc parents: diff changeset	21	\renewcommand{\isastyleminor}{\it}%
f72c82bf59e5 added paper urbanc parents: diff changeset	22	\renewcommand{\isastyle}{\normalsize\it}%
f72c82bf59e5 added paper urbanc parents: diff changeset	23
174 2b414a8a7132 more on the section about derivatives urbanc parents: 172 diff changeset	24	\newcommand*{\threesim}{%
2b414a8a7132 more on the section about derivatives urbanc parents: 172 diff changeset	25	\mathrel{\vcenter{\offinterlineskip
2b414a8a7132 more on the section about derivatives urbanc parents: 172 diff changeset	26	\hbox{$\sim$}\vskip-.35ex\hbox{$\sim$}\vskip-.35ex\hbox{$\sim$}}}}
24 f72c82bf59e5 added paper urbanc parents: diff changeset	27
f72c82bf59e5 added paper urbanc parents: diff changeset	28	\def\dn{\,\stackrel{\mbox{\scriptsize def}}{=}\,}
f72c82bf59e5 added paper urbanc parents: diff changeset	29	\renewcommand{\isasymequiv}{$\dn$}
f72c82bf59e5 added paper urbanc parents: diff changeset	30	\renewcommand{\isasymemptyset}{$\varnothing$}
f72c82bf59e5 added paper urbanc parents: diff changeset	31	\renewcommand{\isacharunderscore}{\mbox{$\_\!\_$}}
f72c82bf59e5 added paper urbanc parents: diff changeset	32
83 f438f4dbaada a bit more on the paper urbanc parents: 82 diff changeset	33	\newcommand{\isasymcalL}{\ensuremath{\cal{L}}}
90 97b783438316 added an example urbanc parents: 88 diff changeset	34	\newcommand{\isasymbigplus}{\ensuremath{\bigplus}}
97b783438316 added an example urbanc parents: 88 diff changeset	35
94 5b12cd0a3b3c latest on the paper urbanc parents: 92 diff changeset	36	\newcommand{\bigplus}{\mbox{\Large\bf$+$}}
348 bea94f1e6771 made changes for another journal submission of the MH-paper urbanc parents: 334 diff changeset	37
bea94f1e6771 made changes for another journal submission of the MH-paper urbanc parents: 334 diff changeset	38	\newtheorem{thrm}{Theorem}[section]
bea94f1e6771 made changes for another journal submission of the MH-paper urbanc parents: 334 diff changeset	39	\newtheorem{lmm}{Lemma}[section]
bea94f1e6771 made changes for another journal submission of the MH-paper urbanc parents: 334 diff changeset	40	\newtheorem{dfntn}{Definition}[section]
bea94f1e6771 made changes for another journal submission of the MH-paper urbanc parents: 334 diff changeset	41	\newtheorem{prpstn}{Proposition}[section]
bea94f1e6771 made changes for another journal submission of the MH-paper urbanc parents: 334 diff changeset	42
24 f72c82bf59e5 added paper urbanc parents: diff changeset	43
172 21ee3a852a02 more on the journal paper urbanc parents: 167 diff changeset	44	\title{A Formalisation of the Myhill-Nerode Theorem\\ based on Regular
348 bea94f1e6771 made changes for another journal submission of the MH-paper urbanc parents: 334 diff changeset	45	Expressions$^\star$}
bea94f1e6771 made changes for another journal submission of the MH-paper urbanc parents: 334 diff changeset	46	%%\thanks{This is a revised and expanded version of \cite{WuZhangUrban11}.}
bea94f1e6771 made changes for another journal submission of the MH-paper urbanc parents: 334 diff changeset	47	\author{Chunhan Wu\\PLA University of Science and Technology Nanjing, China \and
bea94f1e6771 made changes for another journal submission of the MH-paper urbanc parents: 334 diff changeset	48	Xingyuan Zhang\\PLA University of Science and Technology Nanjing, China \and
bea94f1e6771 made changes for another journal submission of the MH-paper urbanc parents: 334 diff changeset	49	Christian Urban\\ King's College London, United Kingdom}
24 f72c82bf59e5 added paper urbanc parents: diff changeset	50
350 8ce9a432680b made changes for another journal submission of the MN-paper urbanc parents: 348 diff changeset	51	\markboth{C.~Wu et al.}{A Formalisation of the Myhill-Nerode Theorem based on Regular
8ce9a432680b made changes for another journal submission of the MN-paper urbanc parents: 348 diff changeset	52	Expressions}
8ce9a432680b made changes for another journal submission of the MN-paper urbanc parents: 348 diff changeset	53
24 f72c82bf59e5 added paper urbanc parents: diff changeset	54	\begin{abstract}
350 8ce9a432680b made changes for another journal submission of the MN-paper urbanc parents: 348 diff changeset	55	There are numerous textbooks on regular languages. Many of them focus
8ce9a432680b made changes for another journal submission of the MN-paper urbanc parents: 348 diff changeset	56	on finite automata for proving properties. Unfortunately, automata
8ce9a432680b made changes for another journal submission of the MN-paper urbanc parents: 348 diff changeset	57	are not so straightforward to formalise in theorem provers. The reason
8ce9a432680b made changes for another journal submission of the MN-paper urbanc parents: 348 diff changeset	58	is that natural representations for automata are graphs, matrices or
8ce9a432680b made changes for another journal submission of the MN-paper urbanc parents: 348 diff changeset	59	functions, none of which are inductive datatypes. Regular
8ce9a432680b made changes for another journal submission of the MN-paper urbanc parents: 348 diff changeset	60	expressions can be defined straightforwardly as a datatype and a
8ce9a432680b made changes for another journal submission of the MN-paper urbanc parents: 348 diff changeset	61	corresponding reasoning infrastructure comes for free in theorem
8ce9a432680b made changes for another journal submission of the MN-paper urbanc parents: 348 diff changeset	62	provers. We show in this paper that a central result from formal
8ce9a432680b made changes for another journal submission of the MN-paper urbanc parents: 348 diff changeset	63	language theory---the Myhill-Nerode Theorem---can be recreated using
8ce9a432680b made changes for another journal submission of the MN-paper urbanc parents: 348 diff changeset	64	only regular expressions. From this theorem many closure properties of
8ce9a432680b made changes for another journal submission of the MN-paper urbanc parents: 348 diff changeset	65	regular languages follow.
24 f72c82bf59e5 added paper urbanc parents: diff changeset	66	\end{abstract}
348 bea94f1e6771 made changes for another journal submission of the MH-paper urbanc parents: 334 diff changeset	67	\category{F.4.1}{Mathematical Logic and Formal Languages}{Mechanical Theorem Proving}
bea94f1e6771 made changes for another journal submission of the MH-paper urbanc parents: 334 diff changeset	68	\category{F.4.3}{Mathematical Logic and Formal Languages}{Formal Languages}
bea94f1e6771 made changes for another journal submission of the MH-paper urbanc parents: 334 diff changeset	69	\terms{Interactive theorem proving, regular languages}
bea94f1e6771 made changes for another journal submission of the MH-paper urbanc parents: 334 diff changeset	70	\keywords{Myhill-Nerode theorem, regular expressions, Isabelle theorem prover}
bea94f1e6771 made changes for another journal submission of the MH-paper urbanc parents: 334 diff changeset	71	\begin{document}
bea94f1e6771 made changes for another journal submission of the MH-paper urbanc parents: 334 diff changeset	72	\begin{bottomstuff}
bea94f1e6771 made changes for another journal submission of the MH-paper urbanc parents: 334 diff changeset	73	Corresponding Author: Christian Urban, Department of Informatics, King's College London,
bea94f1e6771 made changes for another journal submission of the MH-paper urbanc parents: 334 diff changeset	74	Strand, London WC2R 2LS, UK. Email: christian.urban@kcl.ac.uk.\\
bea94f1e6771 made changes for another journal submission of the MH-paper urbanc parents: 334 diff changeset	75	$^\star$This is a revised and expanded version of \cite{WuZhangUrban11}.
bea94f1e6771 made changes for another journal submission of the MH-paper urbanc parents: 334 diff changeset	76	\end{bottomstuff}
167 61d0a412a3ae added a journal version urbanc parents: 162 diff changeset	77	\maketitle
75 d63baacbdb16 parts of the 3 section urbanc parents: 61 diff changeset	78
348 bea94f1e6771 made changes for another journal submission of the MH-paper urbanc parents: 334 diff changeset	79
24 f72c82bf59e5 added paper urbanc parents: diff changeset	80	\input{session}
f72c82bf59e5 added paper urbanc parents: diff changeset	81
f72c82bf59e5 added paper urbanc parents: diff changeset	82	\end{document}
f72c82bf59e5 added paper urbanc parents: diff changeset	83
f72c82bf59e5 added paper urbanc parents: diff changeset	84	%%% Local Variables:
f72c82bf59e5 added paper urbanc parents: diff changeset	85	%%% mode: latex
f72c82bf59e5 added paper urbanc parents: diff changeset	86	%%% TeX-master: t
f72c82bf59e5 added paper urbanc parents: diff changeset	87	%%% End:

author	urbanc
	Mon, 23 Apr 2012 08:01:37 +0000
changeset 350	8ce9a432680b
parent 348	bea94f1e6771
child 375	44c4450152e3
permissions	-rw-r--r--