Journal/document/root.tex
changeset 348 bea94f1e6771
parent 334 d47c2143ab8a
child 350 8ce9a432680b
equal deleted inserted replaced
347:73127f5db18f 348:bea94f1e6771
     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