ninems/ninems.tex
author Chengsong
Tue, 02 Jul 2019 00:14:42 +0100
changeset 36 97c9ac95194d
parent 35 f70e9ab4e680
child 37 17d8e7599a01
permissions -rw-r--r--
chages
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
34
96bba9b493e9 hope works
Chengsong
parents: 30
diff changeset
     1
 \documentclass[a4paper,UKenglish]{lipics}
30
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
     2
\usepackage{graphic}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
     3
\usepackage{data}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
     4
\usepackage{tikz-cd}
35
f70e9ab4e680 psuedocode added
Chengsong
parents: 34
diff changeset
     5
\usepackage{algorithm}
f70e9ab4e680 psuedocode added
Chengsong
parents: 34
diff changeset
     6
\usepackage{amsmath}
f70e9ab4e680 psuedocode added
Chengsong
parents: 34
diff changeset
     7
\usepackage[noend]{algpseudocode}
30
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
     8
% \documentclass{article}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
     9
%\usepackage[utf8]{inputenc}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    10
%\usepackage[english]{babel}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    11
%\usepackage{listings}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    12
% \usepackage{amsthm}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    13
% \usepackage{hyperref}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    14
% \usepackage[margin=0.5in]{geometry}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    15
%\usepackage{pmboxdraw}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    16
 
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    17
\title{POSIX Regular Expression Matching and Lexing}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    18
\author{Chengsong Tan}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    19
\affil{King's College London\\
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    20
London, UK\\
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    21
\texttt{chengsong.tan@kcl.ac.uk}}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    22
\authorrunning{Chengsong Tan}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    23
\Copyright{Chengsong Tan}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    24
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    25
\newcommand{\dn}{\stackrel{\mbox{\scriptsize def}}{=}}%
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    26
\newcommand{\ZERO}{\mbox{\bf 0}}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    27
\newcommand{\ONE}{\mbox{\bf 1}}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    28
\def\lexer{\mathit{lexer}}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    29
\def\mkeps{\mathit{mkeps}}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    30
\def\inj{\mathit{inj}}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    31
\def\Empty{\mathit{Empty}}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    32
\def\Left{\mathit{Left}}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    33
\def\Right{\mathit{Right}}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    34
\def\Stars{\mathit{Stars}}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    35
\def\Char{\mathit{Char}}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    36
\def\Seq{\mathit{Seq}}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    37
\def\Der{\mathit{Der}}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    38
\def\nullable{\mathit{nullable}}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    39
\def\Z{\mathit{Z}}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    40
\def\S{\mathit{S}}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    41
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    42
%\theoremstyle{theorem}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    43
%\newtheorem{theorem}{Theorem}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    44
%\theoremstyle{lemma}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    45
%\newtheorem{lemma}{Lemma}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    46
%\newcommand{\lemmaautorefname}{Lemma}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    47
%\theoremstyle{definition}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    48
%\newtheorem{definition}{Definition}
35
f70e9ab4e680 psuedocode added
Chengsong
parents: 34
diff changeset
    49
\algnewcommand\algorithmicswitch{\textbf{switch}}
f70e9ab4e680 psuedocode added
Chengsong
parents: 34
diff changeset
    50
\algnewcommand\algorithmiccase{\textbf{case}}
f70e9ab4e680 psuedocode added
Chengsong
parents: 34
diff changeset
    51
\algnewcommand\algorithmicassert{\texttt{assert}}
f70e9ab4e680 psuedocode added
Chengsong
parents: 34
diff changeset
    52
\algnewcommand\Assert[1]{\State \algorithmicassert(#1)}%
f70e9ab4e680 psuedocode added
Chengsong
parents: 34
diff changeset
    53
% New "environments"
f70e9ab4e680 psuedocode added
Chengsong
parents: 34
diff changeset
    54
\algdef{SE}[SWITCH]{Switch}{EndSwitch}[1]{\algorithmicswitch\ #1\ \algorithmicdo}{\algorithmicend\ \algorithmicswitch}%
f70e9ab4e680 psuedocode added
Chengsong
parents: 34
diff changeset
    55
\algdef{SE}[CASE]{Case}{EndCase}[1]{\algorithmiccase\ #1}{\algorithmicend\ \algorithmiccase}%
f70e9ab4e680 psuedocode added
Chengsong
parents: 34
diff changeset
    56
\algtext*{EndSwitch}%
f70e9ab4e680 psuedocode added
Chengsong
parents: 34
diff changeset
    57
\algtext*{EndCase}%
30
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    58
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    59
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    60
\begin{document}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    61
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    62
\maketitle
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    63
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    64
\begin{abstract}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    65
  Brzozowski introduced in 1964 a beautifully simple algorithm for
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    66
  regular expression matching based on the notion of derivatives of
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    67
  regular expressions. In 2014, Sulzmann and Lu extended this
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    68
  algorithm to not just give a YES/NO answer for whether or not a regular
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    69
  expression matches a string, but in case it matches also \emph{how}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    70
  it matches the string.  This is important for applications such as
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    71
  lexing (tokenising a string). The problem is to make the algorithm
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    72
  by Sulzmann and Lu fast on all inputs without breaking its
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    73
  correctness.
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    74
\end{abstract}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    75
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    76
\section{Introduction}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    77
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    78
This PhD-project is about regular expression matching and
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    79
lexing. Given the maturity of this topic, the reader might wonder:
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    80
Surely, regular expressions must have already been studied to death?
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    81
What could possibly be \emph{not} known in this area? And surely all
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    82
implemented algorithms for regular expression matching are blindingly
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    83
fast?
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    84
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    85
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    86
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    87
Unfortunately these preconceptions are not supported by evidence: Take
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    88
for example the regular expression $(a^*)^*\,b$ and ask whether
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    89
strings of the form $aa..a$ match this regular
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    90
expression. Obviously they do not match---the expected $b$ in the last
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    91
position is missing. One would expect that modern regular expression
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    92
matching engines can find this out very quickly. Alas, if one tries
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    93
this example in JavaScript, Python or Java 8 with strings like 28
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    94
$a$'s, one discovers that this decision takes around 30 seconds and
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    95
takes considerably longer when adding a few more $a$'s, as the graphs
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    96
below show:
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    97
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    98
\begin{center}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    99
\begin{tabular}{@{}c@{\hspace{0mm}}c@{\hspace{0mm}}c@{}}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   100
\begin{tikzpicture}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   101
\begin{axis}[
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   102
    xlabel={$n$},
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   103
    x label style={at={(1.05,-0.05)}},
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   104
    ylabel={time in secs},
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   105
    enlargelimits=false,
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   106
    xtick={0,5,...,30},
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   107
    xmax=33,
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   108
    ymax=35,
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   109
    ytick={0,5,...,30},
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   110
    scaled ticks=false,
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   111
    axis lines=left,
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   112
    width=5cm,
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   113
    height=4cm, 
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   114
    legend entries={JavaScript},  
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   115
    legend pos=north west,
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   116
    legend cell align=left]
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   117
\addplot[red,mark=*, mark options={fill=white}] table {re-js.data};
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   118
\end{axis}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   119
\end{tikzpicture}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   120
  &
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   121
\begin{tikzpicture}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   122
\begin{axis}[
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   123
    xlabel={$n$},
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   124
    x label style={at={(1.05,-0.05)}},
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   125
    %ylabel={time in secs},
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   126
    enlargelimits=false,
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   127
    xtick={0,5,...,30},
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   128
    xmax=33,
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   129
    ymax=35,
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   130
    ytick={0,5,...,30},
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   131
    scaled ticks=false,
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   132
    axis lines=left,
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   133
    width=5cm,
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   134
    height=4cm, 
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   135
    legend entries={Python},  
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   136
    legend pos=north west,
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   137
    legend cell align=left]
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   138
\addplot[blue,mark=*, mark options={fill=white}] table {re-python2.data};
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   139
\end{axis}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   140
\end{tikzpicture}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   141
  &
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   142
\begin{tikzpicture}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   143
\begin{axis}[
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   144
    xlabel={$n$},
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   145
    x label style={at={(1.05,-0.05)}},
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   146
    %ylabel={time in secs},
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   147
    enlargelimits=false,
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   148
    xtick={0,5,...,30},
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   149
    xmax=33,
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   150
    ymax=35,
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   151
    ytick={0,5,...,30},
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   152
    scaled ticks=false,
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   153
    axis lines=left,
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   154
    width=5cm,
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   155
    height=4cm, 
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   156
    legend entries={Java 8},  
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   157
    legend pos=north west,
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   158
    legend cell align=left]
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   159
\addplot[cyan,mark=*, mark options={fill=white}] table {re-java.data};
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   160
\end{axis}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   161
\end{tikzpicture}\\
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   162
\multicolumn{3}{c}{Graphs: Runtime for matching $(a^*)^*\,b$ with strings 
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   163
           of the form $\underbrace{aa..a}_{n}$.}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   164
\end{tabular}    
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   165
\end{center}  
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   166
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   167
\noindent These are clearly abysmal and possibly surprising results.
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   168
One would expect these systems doing much better than that---after
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   169
all, given a DFA and a string, whether a string is matched by this DFA
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   170
should be linear.
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   171
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   172
Admittedly, the regular expression $(a^*)^*\,b$ is carefully chosen to
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   173
exhibit this ``exponential behaviour''.  Unfortunately, such regular
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   174
expressions are not just a few ``outliers'', but actually they are
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   175
frequent enough that a separate name has been created for
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   176
them---\emph{evil regular expressions}. In empiric work, Davis et al
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   177
report that they have found thousands of such evil regular expressions
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   178
in the JavaScript and Python ecosystems \cite{Davis18}.
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   179
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   180
This exponential blowup sometimes causes real pain in real life:
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   181
for example on 20 July 2016 one evil regular expression brought the
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   182
webpage \href{http://stackexchange.com}{Stack Exchange} to its knees \footnote{https://stackstatus.net/post/147710624694/outage-postmortem-july-20-2016}.
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   183
In this instance, a regular expression intended to just trim white
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   184
spaces from the beginning and the end of a line actually consumed
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   185
massive amounts of CPU-resources and because of this the web servers
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   186
ground to a halt. This happened when a post with 20,000 white spaces
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   187
was submitted, but importantly the white spaces were neither at the
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   188
beginning nor at the end. As a result, the regular expression matching
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   189
engine needed to backtrack over many choices.
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   190
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   191
The underlying problem is that many ``real life'' regular expression
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   192
matching engines do not use DFAs for matching. This is because they
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   193
support regular expressions that are not covered by the classical
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   194
automata theory, and in this more general setting there are quite a
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   195
few research questions still unanswered and fast algorithms still need
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   196
to be developed.
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   197
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   198
There is also another under-researched problem to do with regular
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   199
expressions and lexing, i.e.~the process of breaking up strings into
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   200
sequences of tokens according to some regular expressions. In this
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   201
setting one is not just interested in whether or not a regular
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   202
expression matches a string, but if it matches also in \emph{how} it
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   203
matches the string.  Consider for example a regular expression
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   204
$r_{key}$ for recognising keywords such as \textit{if}, \textit{then}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   205
and so on; and a regular expression $r_{id}$ for recognising
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   206
identifiers (say, a single character followed by characters or
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   207
numbers). One can then form the compound regular expression
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   208
$(r_{key} + r_{id})^*$ and use it to tokenise strings.  But then how
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   209
should the string \textit{iffoo} be tokenised?  It could be tokenised
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   210
as a keyword followed by an identifier, or the entire string as a
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   211
single identifier.  Similarly, how should the string \textit{if} be
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   212
tokenised? Both regular expressions, $r_{key}$ and $r_{id}$, would
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   213
``fire''---so is it an identifier or a keyword?  While in applications
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   214
there is a well-known strategy to decide these questions, called POSIX
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   215
matching, only relatively recently precise definitions of what POSIX
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   216
matching actually means have been formalised
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   217
\cite{AusafDyckhoffUrban2016,OkuiSuzuki2010,Vansummeren2006}. Roughly,
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   218
POSIX matching means matching the longest initial substring and
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   219
in the case of a tie, the initial submatch is chosen according to some priorities attached to the
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   220
regular expressions (e.g.~keywords have a higher priority than
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   221
identifiers). This sounds rather simple, but according to Grathwohl et
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   222
al \cite[Page 36]{CrashCourse2014} this is not the case. They wrote:
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   223
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   224
\begin{quote}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   225
\it{}``The POSIX strategy is more complicated than the greedy because of 
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   226
the dependence on information about the length of matched strings in the 
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   227
various subexpressions.''
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   228
\end{quote}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   229
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   230
\noindent
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   231
This is also supported by evidence collected by Kuklewicz
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   232
\cite{Kuklewicz} who noticed that a number of POSIX regular expression
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   233
matchers calculate incorrect results.
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   234
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   235
Our focus is on an algorithm introduced by Sulzmann and Lu in 2014 for
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   236
regular expression matching according to the POSIX strategy
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   237
\cite{Sulzmann2014}. Their algorithm is based on an older algorithm by
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   238
Brzozowski from 1964 where he introduced the notion of derivatives of
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   239
regular expressions \cite{Brzozowski1964}. We shall briefly explain
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   240
the algorithms next.
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   241
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   242
\section{The Algorithms by  Brzozowski, and Sulzmann and Lu}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   243
36
Chengsong
parents: 35
diff changeset
   244
Suppose regular expressions are given by the following grammar:\\
Chengsong
parents: 35
diff changeset
   245
			$r$  $::=$   $\ZERO$ $\mid$  $\ONE$   
Chengsong
parents: 35
diff changeset
   246
			 $\mid$  $c$          
Chengsong
parents: 35
diff changeset
   247
			 $\mid$  $r_1 \cdot r_2$
Chengsong
parents: 35
diff changeset
   248
			 $\mid$  $r_1 + r_2$   
Chengsong
parents: 35
diff changeset
   249
			 $\mid$  $r^*$         
30
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   250
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   251
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   252
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   253
\noindent
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   254
The intended meaning of the regular expressions is as usual: $\ZERO$
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   255
cannot match any string, $\ONE$ can match the empty string, the
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   256
character regular expression $c$ can match the character $c$, and so
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   257
on. The brilliant contribution by Brzozowski is the notion of
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   258
\emph{derivatives} of regular expressions.  The idea behind this
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   259
notion is as follows: suppose a regular expression $r$ can match a
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   260
string of the form $c\!::\! s$ (that is a list of characters starting
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   261
with $c$), what does the regular expression look like that can match
36
Chengsong
parents: 35
diff changeset
   262
just $s$? Brzozowski gave a neat answer to this question. He started with the definition of $nullable$:
Chengsong
parents: 35
diff changeset
   263
\begin{center}
Chengsong
parents: 35
diff changeset
   264
		\begin{tabular}{lcl}
Chengsong
parents: 35
diff changeset
   265
			$\nullable(\ZERO)$     & $\dn$ & $\mathit{false}$ \\  
Chengsong
parents: 35
diff changeset
   266
			$\nullable(\ONE)$      & $\dn$ & $\mathit{true}$ \\
Chengsong
parents: 35
diff changeset
   267
			$\nullable(c)$ 	       & $\dn$ & $\mathit{false}$ \\
Chengsong
parents: 35
diff changeset
   268
			$\nullable(r_1 + r_2)$ & $\dn$ & $\nullable(r_1) \vee \nullable(r_2)$ \\
Chengsong
parents: 35
diff changeset
   269
			$\nullable(r_1\cdot r_2)$  & $\dn$ & $\nullable(r_1) \wedge \nullable(r_2)$ \\
Chengsong
parents: 35
diff changeset
   270
			$\nullable(r^*)$       & $\dn$ & $\mathit{true}$ \\
Chengsong
parents: 35
diff changeset
   271
		\end{tabular}
Chengsong
parents: 35
diff changeset
   272
	\end{center}
Chengsong
parents: 35
diff changeset
   273
The function tests whether the empty string is in $L(r)$.
Chengsong
parents: 35
diff changeset
   274
He then defined
30
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   275
the following operation on regular expressions, written
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   276
$r\backslash c$ (the derivative of $r$ w.r.t.~the character $c$):
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   277
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   278
\begin{center}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   279
\begin{tabular}{lcl}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   280
		$\ZERO \backslash c$ & $\dn$ & $\ZERO$\\  
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   281
		$\ONE \backslash c$  & $\dn$ & $\ZERO$\\
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   282
		$d \backslash c$     & $\dn$ & 
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   283
		$\mathit{if} \;c = d\;\mathit{then}\;\ONE\;\mathit{else}\;\ZERO$\\
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   284
$(r_1 + r_2)\backslash c$     & $\dn$ & $r_1 \backslash c \,+\, r_2 \backslash c$\\
36
Chengsong
parents: 35
diff changeset
   285
$(r_1 \cdot r_2)\backslash c$ & $\dn$ & $\mathit{if} \, nullable(r_1)$\\
30
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   286
	&   & $\mathit{then}\;(r_1\backslash c) \cdot r_2 \,+\, r_2\backslash c$\\
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   287
	&   & $\mathit{else}\;(r_1\backslash c) \cdot r_2$\\
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   288
	$(r^*)\backslash c$           & $\dn$ & $(r\backslash c) \cdot r^*$\\
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   289
\end{tabular}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   290
\end{center}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   291
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   292
\noindent
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   293
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   294
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   295
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   296
 %Assuming the classic notion of a
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   297
%\emph{language} of a regular expression, written $L(\_)$, t
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   298
The main
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   299
property of the derivative operation is that
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   300
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   301
\begin{center}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   302
$c\!::\!s \in L(r)$ holds
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   303
if and only if $s \in L(r\backslash c)$.
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   304
\end{center}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   305
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   306
\noindent
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   307
So if we want to find out whether a string $s$
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   308
matches with a regular expression $r$, build the derivatives of $r$
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   309
w.r.t.\ (in succession) all the characters of the string $s$. Finally,
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   310
test whether the resulting regular expression can match the empty
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   311
string.  If yes, then $r$ matches $s$, and no in the negative
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   312
case.\\
36
Chengsong
parents: 35
diff changeset
   313
We can generalise the derivative operation for strings like this:
30
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   314
\begin{center}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   315
\begin{tabular}{lcl}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   316
$r \backslash (c\!::\!s) $ & $\dn$ & $(r \backslash c) \backslash s$ \\
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   317
$r \backslash \epsilon $ & $\dn$ & $r$
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   318
\end{tabular}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   319
\end{center}
35
f70e9ab4e680 psuedocode added
Chengsong
parents: 34
diff changeset
   320
 For us the main advantage is that derivatives can be
f70e9ab4e680 psuedocode added
Chengsong
parents: 34
diff changeset
   321
straightforwardly implemented in any functional programming language,
f70e9ab4e680 psuedocode added
Chengsong
parents: 34
diff changeset
   322
and are easily definable and reasoned about in theorem provers---the
f70e9ab4e680 psuedocode added
Chengsong
parents: 34
diff changeset
   323
definitions just consist of inductive datatypes and simple recursive
f70e9ab4e680 psuedocode added
Chengsong
parents: 34
diff changeset
   324
functions. Moreover, the notion of derivatives can be easily
f70e9ab4e680 psuedocode added
Chengsong
parents: 34
diff changeset
   325
generalised to cover extended regular expression constructors such as
f70e9ab4e680 psuedocode added
Chengsong
parents: 34
diff changeset
   326
the not-regular expression, written $\neg\,r$, or bounded repetitions
f70e9ab4e680 psuedocode added
Chengsong
parents: 34
diff changeset
   327
(for example $r^{\{n\}}$ and $r^{\{n..m\}}$), which cannot be so
f70e9ab4e680 psuedocode added
Chengsong
parents: 34
diff changeset
   328
straightforwardly realised within the classic automata approach.
f70e9ab4e680 psuedocode added
Chengsong
parents: 34
diff changeset
   329
30
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   330
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   331
We obtain a simple and elegant regular
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   332
expression matching algorithm: 
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   333
\begin{definition}{matcher}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   334
\[
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   335
match\;s\;r \;\dn\; nullable(r\backslash s)
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   336
\]
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   337
\end{definition}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   338
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   339
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   340
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   341
One limitation, however, of Brzozowski's algorithm is that it only
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   342
produces a YES/NO answer for whether a string is being matched by a
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   343
regular expression.  Sulzmann and Lu~\cite{Sulzmann2014} extended this
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   344
algorithm to allow generation of an actual matching, called a
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   345
\emph{value}.  
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   346
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   347
\begin{center}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   348
	\begin{tabular}{c@{\hspace{20mm}}c}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   349
		\begin{tabular}{@{}rrl@{}}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   350
			\multicolumn{3}{@{}l}{\textbf{Regular Expressions}}\medskip\\
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   351
			$r$ & $::=$  & $\ZERO$\\
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   352
			& $\mid$ & $\ONE$   \\
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   353
			& $\mid$ & $c$          \\
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   354
			& $\mid$ & $r_1 \cdot r_2$\\
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   355
			& $\mid$ & $r_1 + r_2$   \\
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   356
			\\
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   357
			& $\mid$ & $r^*$         \\
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   358
		\end{tabular}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   359
		&
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   360
		\begin{tabular}{@{\hspace{0mm}}rrl@{}}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   361
			\multicolumn{3}{@{}l}{\textbf{Values}}\medskip\\
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   362
			$v$ & $::=$  & \\
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   363
			&        & $\Empty$   \\
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   364
			& $\mid$ & $\Char(c)$          \\
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   365
			& $\mid$ & $\Seq\,v_1\, v_2$\\
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   366
			& $\mid$ & $\Left(v)$   \\
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   367
			& $\mid$ & $\Right(v)$  \\
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   368
			& $\mid$ & $\Stars\,[v_1,\ldots\,v_n]$ \\
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   369
		\end{tabular}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   370
	\end{tabular}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   371
\end{center}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   372
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   373
\noindent
35
f70e9ab4e680 psuedocode added
Chengsong
parents: 34
diff changeset
   374
 Here we put the regular expression and values of the same shape on the same level to illustrate the corresponding relation between them. 
36
Chengsong
parents: 35
diff changeset
   375
 The flatten notation $| v |$ means extracting the characters in the value $v$ to form a string. For example, $|\mathit{Seq} \, \mathit{Char(c)} \, \mathit{Char(d)}|$ = $cd$. We omit this straightforward definition.
Chengsong
parents: 35
diff changeset
   376
 Values are a way of expressing parse trees(the tree structure that tells how a sub-regex matches a substring). For example, $\Seq\,v_1\, v_2$ tells us how the string $|v_1| \cdot |v_2|$ matches the regex $r_1 \cdot r_2$: $r_1$ matches $|v_1|$ and $r_2$ matches $|v_2|$. Exactly how these two are matched are contained in the sub-structure of $v_1$ and $v_2$. 
30
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   377
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   378
 To give a concrete example of how value works, consider the string $xy$ and the
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   379
regular expression $(x + (y + xy))^*$. We can view this regular
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   380
expression as a tree and if the string $xy$ is matched by two Star
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   381
``iterations'', then the $x$ is matched by the left-most alternative
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   382
in this tree and the $y$ by the right-left alternative. This suggests
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   383
to record this matching as
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   384
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   385
\begin{center}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   386
$\Stars\,[\Left\,(\Char\,x), \Right(\Left(\Char\,y))]$
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   387
\end{center}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   388
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   389
\noindent
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   390
where $\Stars$ records how many
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   391
iterations were used; and $\Left$, respectively $\Right$, which
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   392
alternative is used. The value for
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   393
matching $xy$ in a single ``iteration'', i.e.~the POSIX value,
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   394
would look as follows
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   395
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   396
\begin{center}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   397
$\Stars\,[\Seq\,(\Char\,x)\,(\Char\,y)]$
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   398
\end{center}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   399
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   400
\noindent
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   401
where $\Stars$ has only a single-element list for the single iteration
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   402
and $\Seq$ indicates that $xy$ is matched by a sequence regular
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   403
expression.
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   404
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   405
The contribution of Sulzmann and Lu is an extension of Brzozowski's
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   406
algorithm by a second phase (the first phase being building successive
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   407
derivatives). In this second phase, for every successful match the
35
f70e9ab4e680 psuedocode added
Chengsong
parents: 34
diff changeset
   408
corresponding POSIX value is computed. The whole process looks like the following diagram(the working flow of the simple matching algorithm that just gives a $YES/NO$ answer is provided on the right for the purpose of comparison):\\
30
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   409
\begin{tikzcd}
36
Chengsong
parents: 35
diff changeset
   410
r_0 \arrow[r, "\backslash c_0"]  \arrow[d] & r_1 \arrow[r, "\backslash c_1"] \arrow[d] & r_2 \arrow[r, dashed] \arrow[d] & r_n \arrow[d, "mkeps" description] \\
30
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   411
v_0           & v_1 \arrow[l,"inj_{r_0} c_0"]                & v_2 \arrow[l, "inj_{r_1} c_1"]              & v_n \arrow[l, dashed]         
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   412
\end{tikzcd}
36
Chengsong
parents: 35
diff changeset
   413
\begin{tikzcd}
Chengsong
parents: 35
diff changeset
   414
r_0 \arrow[r, "\backslash c_0"]  & r_1 \arrow[r, "\backslash c_1"] & r_2 \arrow[r, dashed]  & r_n   
Chengsong
parents: 35
diff changeset
   415
\end{tikzcd}
35
f70e9ab4e680 psuedocode added
Chengsong
parents: 34
diff changeset
   416
30
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   417
We shall briefly explain this interesting process.\\ For the convenience of explanation, we have the following notations: the regular expression $r$ used for matching is also called $r_0$ and the string $s$ is composed of $n$ characters $c_0 c_1 ... c_{n-1}$.
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   418
First, we do the derivative operation on $r_0$, $r_1$, ..., using characters $c_0$, $c_1$, ...  until we get the final derivative $r_n$.We test whether it is $nullable$ or not. If no we know immediately the string does not match the regex. If yes, we start building the parse tree incrementally. We first call $mkeps$(which stands for make epsilon--make the parse tree for the empty word epsilon) to construct the parse tree $v_n$ for how the final derivative $r_n$ matches the empty string:
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   419
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   420
 After this, we inject back the characters one by one, in reverse order as they were chopped off, to build the parse tree $v_i$ for how the regex $r_i$ matches the string $s_i$($s_i$ means the string s with the first $i$ characters being chopped off) from the previous parse tree. After $n$ transformations, we get the parse tree for how $r_0$ matches $s$, exactly as we wanted.
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   421
An inductive proof can be routinely established.
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   422
We omit the details of injection function, which is provided by Sulzmann and Lu's paper \cite{Sulzmann2014}. Rather, we shall focus next on the
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   423
process of simplification of regular expressions, which is needed in
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   424
order to obtain \emph{fast} versions of the Brzozowski's, and Sulzmann
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   425
and Lu's algorithms.  This is where the PhD-project hopes to advance
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   426
the state-of-the-art.
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   427
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   428
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   429
\section{Simplification of Regular Expressions}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   430
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   431
The main drawback of building successive derivatives according to
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   432
Brzozowski's definition is that they can grow very quickly in size.
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   433
This is mainly due to the fact that the derivative operation generates
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   434
often ``useless'' $\ZERO$s and $\ONE$s in derivatives.  As a result,
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   435
if implemented naively both algorithms by Brzozowski and by Sulzmann
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   436
and Lu are excruciatingly slow. For example when starting with the
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   437
regular expression $(a + aa)^*$ and building 12 successive derivatives
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   438
w.r.t.~the character $a$, one obtains a derivative regular expression
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   439
with more than 8000 nodes (when viewed as a tree). Operations like
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   440
derivative and $\nullable$ need to traverse such trees and
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   441
consequently the bigger the size of the derivative the slower the
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   442
algorithm. Fortunately, one can simplify regular expressions after
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   443
each derivative step. Various simplifications of regular expressions
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   444
are possible, such as the simplifications of $\ZERO + r$,
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   445
$r + \ZERO$, $\ONE\cdot r$, $r \cdot \ONE$, and $r + r$ to just
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   446
$r$. These simplifications do not affect the answer for whether a
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   447
regular expression matches a string or not, but fortunately also do
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   448
not affect the POSIX strategy of how regular expressions match
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   449
strings---although the latter is much harder to establish. Some
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   450
initial results in this regard have been obtained in
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   451
\cite{AusafDyckhoffUrban2016}. However, what has not been achieved yet
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   452
is a very tight bound for the size. Such a tight bound is suggested by
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   453
work of Antimirov who proved that (partial) derivatives can be bound
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   454
by the number of characters contained in the initial regular
35
f70e9ab4e680 psuedocode added
Chengsong
parents: 34
diff changeset
   455
expression \cite{Antimirov95}.
f70e9ab4e680 psuedocode added
Chengsong
parents: 34
diff changeset
   456
f70e9ab4e680 psuedocode added
Chengsong
parents: 34
diff changeset
   457
Antimirov defined the "partial derivatives" of regular expressions to be this:
f70e9ab4e680 psuedocode added
Chengsong
parents: 34
diff changeset
   458
%TODO definition of partial derivatives
f70e9ab4e680 psuedocode added
Chengsong
parents: 34
diff changeset
   459
f70e9ab4e680 psuedocode added
Chengsong
parents: 34
diff changeset
   460
it is essentially a set of regular expressions that come from the sub-structure of the original regular expression. 
f70e9ab4e680 psuedocode added
Chengsong
parents: 34
diff changeset
   461
Antimirov has proved a nice size bound of the size of partial derivatives. Roughly speaking the size will not exceed the fourth power of the number of nodes in that regular expression.  Interestingly, we observed from experiment that after the simplification step, our regular expression has the same size or is smaller than the partial derivatives. This allows us to prove a tight bound on the size of regular expression during the running time of the algorithm if we can establish the connection between our simplification rules and partial derivatives.
f70e9ab4e680 psuedocode added
Chengsong
parents: 34
diff changeset
   462
f70e9ab4e680 psuedocode added
Chengsong
parents: 34
diff changeset
   463
 %We believe, and have generated test
f70e9ab4e680 psuedocode added
Chengsong
parents: 34
diff changeset
   464
%data, that a similar bound can be obtained for the derivatives in
f70e9ab4e680 psuedocode added
Chengsong
parents: 34
diff changeset
   465
%Sulzmann and Lu's algorithm. Let us give some details about this next.
30
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   466
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   467
We first followed Sulzmann and Lu's idea of introducing
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   468
\emph{annotated regular expressions}~\cite{Sulzmann2014}. They are
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   469
defined by the following grammar:
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   470
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   471
\begin{center}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   472
\begin{tabular}{lcl}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   473
  $\textit{a}$ & $::=$  & $\textit{ZERO}$\\
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   474
                  & $\mid$ & $\textit{ONE}\;\;bs$\\
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   475
                  & $\mid$ & $\textit{CHAR}\;\;bs\,c$\\
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   476
                  & $\mid$ & $\textit{ALTS}\;\;bs\,as$\\
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   477
                  & $\mid$ & $\textit{SEQ}\;\;bs\,a_1\,a_2$\\
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   478
                  & $\mid$ & $\textit{STAR}\;\;bs\,a$
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   479
\end{tabular}    
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   480
\end{center}  
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   481
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   482
\noindent
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   483
where $bs$ stands for bitsequences, and $as$ (in \textit{ALTS}) for a
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   484
list of annotated regular expressions. These bitsequences encode
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   485
information about the (POSIX) value that should be generated by the
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   486
Sulzmann and Lu algorithm. Bitcodes are essentially incomplete values.
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   487
This can be straightforwardly seen in the following transformation: 
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   488
\begin{center}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   489
\begin{tabular}{lcl}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   490
  $\textit{code}(\Empty)$ & $\dn$ & $[]$\\
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   491
  $\textit{code}(\Char\,c)$ & $\dn$ & $[]$\\
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   492
  $\textit{code}(\Left\,v)$ & $\dn$ & $\Z :: code(v)$\\
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   493
  $\textit{code}(\Right\,v)$ & $\dn$ & $\S :: code(v)$\\
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   494
  $\textit{code}(\Seq\,v_1\,v_2)$ & $\dn$ & $code(v_1) \,@\, code(v_2)$\\
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   495
  $\textit{code}(\Stars\,[])$ & $\dn$ & $[\S]$\\
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   496
  $\textit{code}(\Stars\,(v\!::\!vs))$ & $\dn$ & $\Z :: code(v) \;@\;
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   497
                                                 code(\Stars\,vs)$
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   498
\end{tabular}    
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   499
\end{center} 
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   500
where $\Z$ and $\S$ are arbitrary names for the bits in the
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   501
bitsequences. 
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   502
Here code encodes a value into a bitsequence by converting Left into $\Z$, Right into $\S$, the start point of a non-empty star iteration into $\S$, and the border where a local star terminates into $\Z$. This conversion is apparently lossy, as it throws away the character information, and does not decode the boundary between the two operands of the sequence constructor. Moreover, with only the bitcode we cannot even tell whether the $\S$s and $\Z$s are for $Left/Right$ or $Stars$. The reason for choosing this compact way of storing information is that the relatively small size of bits can be easily moved around during the lexing process. In order to recover the bitcode back into values, we will need the regular expression as the extra information and decode them back into value:\\
36
Chengsong
parents: 35
diff changeset
   503
\begin{definition}[Bitdecoding of Values]\mbox{}
Chengsong
parents: 35
diff changeset
   504
\begin{center}
Chengsong
parents: 35
diff changeset
   505
\begin{tabular}{@{}l@{\hspace{1mm}}c@{\hspace{1mm}}l@{}}
Chengsong
parents: 35
diff changeset
   506
  $\textit{decode}'\,bs\,(\ONE)$ & $\dn$ & $(\Empty, bs)$\\
Chengsong
parents: 35
diff changeset
   507
  $\textit{decode}'\,bs\,(c)$ & $\dn$ & $(\Char\,c, bs)$\\
Chengsong
parents: 35
diff changeset
   508
  $\textit{decode}'\,(\Z\!::\!bs)\;(r_1 + r_2)$ & $\dn$ &
Chengsong
parents: 35
diff changeset
   509
     $\textit{let}\,(v, bs_1) = \textit{decode}'\,bs\,r_1\;\textit{in}\;
Chengsong
parents: 35
diff changeset
   510
       (\Left\,v, bs_1)$\\
Chengsong
parents: 35
diff changeset
   511
  $\textit{decode}'\,(\S\!::\!bs)\;(r_1 + r_2)$ & $\dn$ &
Chengsong
parents: 35
diff changeset
   512
     $\textit{let}\,(v, bs_1) = \textit{decode}'\,bs\,r_2\;\textit{in}\;
Chengsong
parents: 35
diff changeset
   513
       (\Right\,v, bs_1)$\\                           
Chengsong
parents: 35
diff changeset
   514
  $\textit{decode}'\,bs\;(r_1\cdot r_2)$ & $\dn$ &
Chengsong
parents: 35
diff changeset
   515
        $\textit{let}\,(v_1, bs_1) = \textit{decode}'\,bs\,r_1\;\textit{in}$\\
Chengsong
parents: 35
diff changeset
   516
  & &   $\textit{let}\,(v_2, bs_2) = \textit{decode}'\,bs_1\,r_2$\\
Chengsong
parents: 35
diff changeset
   517
  & &   \hspace{35mm}$\textit{in}\;(\Seq\,v_1\,v_2, bs_2)$\\
Chengsong
parents: 35
diff changeset
   518
  $\textit{decode}'\,(\Z\!::\!bs)\,(r^*)$ & $\dn$ & $(\Stars\,[], bs)$\\
Chengsong
parents: 35
diff changeset
   519
  $\textit{decode}'\,(\S\!::\!bs)\,(r^*)$ & $\dn$ & 
Chengsong
parents: 35
diff changeset
   520
         $\textit{let}\,(v, bs_1) = \textit{decode}'\,bs\,r\;\textit{in}$\\
Chengsong
parents: 35
diff changeset
   521
  & &   $\textit{let}\,(\Stars\,vs, bs_2) = \textit{decode}'\,bs_1\,r^*$\\
Chengsong
parents: 35
diff changeset
   522
  & &   \hspace{35mm}$\textit{in}\;(\Stars\,v\!::\!vs, bs_2)$\bigskip\\
Chengsong
parents: 35
diff changeset
   523
  
Chengsong
parents: 35
diff changeset
   524
  $\textit{decode}\,bs\,r$ & $\dn$ &
Chengsong
parents: 35
diff changeset
   525
     $\textit{let}\,(v, bs') = \textit{decode}'\,bs\,r\;\textit{in}$\\
Chengsong
parents: 35
diff changeset
   526
  & & $\textit{if}\;bs' = []\;\textit{then}\;\textit{Some}\,v\;
Chengsong
parents: 35
diff changeset
   527
       \textit{else}\;\textit{None}$                       
Chengsong
parents: 35
diff changeset
   528
\end{tabular}    
Chengsong
parents: 35
diff changeset
   529
\end{center}    
Chengsong
parents: 35
diff changeset
   530
\end{definition}
30
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   531
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   532
To do lexing using annotated regular expressions, we shall first transform the
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   533
usual (un-annotated) regular expressions into annotated regular
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   534
expressions:\\
36
Chengsong
parents: 35
diff changeset
   535
\begin{definition}
Chengsong
parents: 35
diff changeset
   536
\begin{center}
Chengsong
parents: 35
diff changeset
   537
\begin{tabular}{lcl}
Chengsong
parents: 35
diff changeset
   538
  $(\ZERO)^\uparrow$ & $\dn$ & $\textit{ZERO}$\\
Chengsong
parents: 35
diff changeset
   539
  $(\ONE)^\uparrow$ & $\dn$ & $\textit{ONE}\,[]$\\
Chengsong
parents: 35
diff changeset
   540
  $(c)^\uparrow$ & $\dn$ & $\textit{CHAR}\,[]\,c$\\
Chengsong
parents: 35
diff changeset
   541
  $(r_1 + r_2)^\uparrow$ & $\dn$ &
Chengsong
parents: 35
diff changeset
   542
         $\textit{ALT}\;[]\,(\textit{fuse}\,[\Z]\,r_1^\uparrow)\,
Chengsong
parents: 35
diff changeset
   543
                            (\textit{fuse}\,[\S]\,r_2^\uparrow)$\\
Chengsong
parents: 35
diff changeset
   544
  $(r_1\cdot r_2)^\uparrow$ & $\dn$ &
Chengsong
parents: 35
diff changeset
   545
         $\textit{SEQ}\;[]\,r_1^\uparrow\,r_2^\uparrow$\\
Chengsong
parents: 35
diff changeset
   546
  $(r^*)^\uparrow$ & $\dn$ &
Chengsong
parents: 35
diff changeset
   547
         $\textit{STAR}\;[]\,r^\uparrow$\\
Chengsong
parents: 35
diff changeset
   548
\end{tabular}    
Chengsong
parents: 35
diff changeset
   549
\end{center}    
Chengsong
parents: 35
diff changeset
   550
\end{definition}
30
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   551
Then we do successive derivative operations on the annotated regular expression. This derivative operation is the same as what we previously have for the simple regular expressions, except that we take special care of the bits to store the parse tree information:\\
36
Chengsong
parents: 35
diff changeset
   552
\begin{definition}{bder}
Chengsong
parents: 35
diff changeset
   553
\begin{center}
Chengsong
parents: 35
diff changeset
   554
  \begin{tabular}{@{}lcl@{}}
Chengsong
parents: 35
diff changeset
   555
  $(\textit{ZERO})\backslash c$ & $\dn$ & $\textit{ZERO}$\\  
Chengsong
parents: 35
diff changeset
   556
  $(\textit{ONE}\;bs)\backslash c$ & $\dn$ & $\textit{ZERO}$\\  
Chengsong
parents: 35
diff changeset
   557
  $(\textit{CHAR}\;bs\,d)\backslash c$ & $\dn$ &
Chengsong
parents: 35
diff changeset
   558
        $\textit{if}\;c=d\; \;\textit{then}\;
Chengsong
parents: 35
diff changeset
   559
         \textit{ONE}\;bs\;\textit{else}\;\textit{ZERO}$\\  
Chengsong
parents: 35
diff changeset
   560
  $(\textit{ALT}\;bs\,a_1\,a_2)\backslash c$ & $\dn$ &
Chengsong
parents: 35
diff changeset
   561
        $\textit{ALT}\,bs\,(a_1\backslash c)\,(a_2\backslash c)$\\
Chengsong
parents: 35
diff changeset
   562
  $(\textit{SEQ}\;bs\,a_1\,a_2)\backslash c$ & $\dn$ &
Chengsong
parents: 35
diff changeset
   563
     $\textit{if}\;\textit{bnullable}\,a_1$\\
Chengsong
parents: 35
diff changeset
   564
  & &$\textit{then}\;\textit{ALT}\,bs\,(\textit{SEQ}\,[]\,(a_1\backslash c)\,a_2)$\\
Chengsong
parents: 35
diff changeset
   565
  & &$\phantom{\textit{then}\;\textit{ALT}\,bs\,}(\textit{fuse}\,(\textit{bmkeps}\,a_1)\,(a_2\backslash c))$\\
Chengsong
parents: 35
diff changeset
   566
  & &$\textit{else}\;\textit{SEQ}\,bs\,(a_1\backslash c)\,a_2$\\
Chengsong
parents: 35
diff changeset
   567
  $(\textit{STAR}\,bs\,a)\backslash c$ & $\dn$ &
Chengsong
parents: 35
diff changeset
   568
      $\textit{SEQ}\;bs\,(\textit{fuse}\, [\Z] (r\backslash c))\,
Chengsong
parents: 35
diff changeset
   569
       (\textit{STAR}\,[]\,r)$
Chengsong
parents: 35
diff changeset
   570
\end{tabular}    
Chengsong
parents: 35
diff changeset
   571
\end{center}    
Chengsong
parents: 35
diff changeset
   572
\end{definition}
30
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   573
This way, we do not have to use an injection function and a second phase, but instead only need to collect the bits while running $mkeps$:
36
Chengsong
parents: 35
diff changeset
   574
\begin{definition}[\textit{bmkeps}]\mbox{}
Chengsong
parents: 35
diff changeset
   575
\begin{center}
Chengsong
parents: 35
diff changeset
   576
\begin{tabular}{lcl}
Chengsong
parents: 35
diff changeset
   577
  $\textit{bmkeps}\,(\textit{ONE}\,bs)$ & $\dn$ & $bs$\\
Chengsong
parents: 35
diff changeset
   578
  $\textit{bmkeps}\,(\textit{ALT}\,bs\,a_1\,a_2)$ & $\dn$ &
Chengsong
parents: 35
diff changeset
   579
     $\textit{if}\;\textit{bnullable}\,a_1$\\
Chengsong
parents: 35
diff changeset
   580
  & &$\textit{then}\;bs\,@\,\textit{bmkeps}\,a_1$\\
Chengsong
parents: 35
diff changeset
   581
  & &$\textit{else}\;bs\,@\,\textit{bmkeps}\,a_2$\\
Chengsong
parents: 35
diff changeset
   582
  $\textit{bmkeps}\,(\textit{SEQ}\,bs\,a_1\,a_2)$ & $\dn$ &
Chengsong
parents: 35
diff changeset
   583
     $bs \,@\,\textit{bmkeps}\,a_1\,@\, \textit{bmkeps}\,a_2$\\
Chengsong
parents: 35
diff changeset
   584
  $\textit{bmkeps}\,(\textit{STAR}\,bs\,a)$ & $\dn$ &
Chengsong
parents: 35
diff changeset
   585
     $bs \,@\, [\S]$
Chengsong
parents: 35
diff changeset
   586
\end{tabular}    
Chengsong
parents: 35
diff changeset
   587
\end{center}    
Chengsong
parents: 35
diff changeset
   588
\end{definition}
30
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   589
and then decode the bits using the regular expression. The whole process looks like this:\\
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   590
r
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   591
\\
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   592
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   593
The main point of the bitsequences and annotated regular expressions
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   594
is that we can apply rather aggressive (in terms of size)
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   595
simplification rules in order to keep derivatives small.  
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   596
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   597
We have
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   598
developed such ``aggressive'' simplification rules and generated test
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   599
data that show that the expected bound can be achieved. Obviously we
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   600
could only partially cover  the search space as there are infinitely
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   601
many regular expressions and strings. One modification we introduced
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   602
is to allow a list of annotated regular expressions in the
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   603
\textit{ALTS} constructor. This allows us to not just delete
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   604
unnecessary $\ZERO$s and $\ONE$s from regular expressions, but also
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   605
unnecessary ``copies'' of regular expressions (very similar to
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   606
simplifying $r + r$ to just $r$, but in a more general
35
f70e9ab4e680 psuedocode added
Chengsong
parents: 34
diff changeset
   607
setting). 
f70e9ab4e680 psuedocode added
Chengsong
parents: 34
diff changeset
   608
A psuedocode version of our algorithm is given below:\\
f70e9ab4e680 psuedocode added
Chengsong
parents: 34
diff changeset
   609
f70e9ab4e680 psuedocode added
Chengsong
parents: 34
diff changeset
   610
\begin{algorithm}
f70e9ab4e680 psuedocode added
Chengsong
parents: 34
diff changeset
   611
\caption{simplification of annotated regular expression}\label{euclid}
f70e9ab4e680 psuedocode added
Chengsong
parents: 34
diff changeset
   612
\begin{algorithmic}[1]
f70e9ab4e680 psuedocode added
Chengsong
parents: 34
diff changeset
   613
\Procedure{$Simp$}{$areg$}
f70e9ab4e680 psuedocode added
Chengsong
parents: 34
diff changeset
   614
\Switch{$areg$}
f70e9ab4e680 psuedocode added
Chengsong
parents: 34
diff changeset
   615
	\Case{$ALTS(bs, rs)$}
f70e9ab4e680 psuedocode added
Chengsong
parents: 34
diff changeset
   616
		\For{\textit{rs[i] in array rs}}
f70e9ab4e680 psuedocode added
Chengsong
parents: 34
diff changeset
   617
        			\State $\textit{rs[i]} \gets$ \textit{Simp(rs[i])}
f70e9ab4e680 psuedocode added
Chengsong
parents: 34
diff changeset
   618
      		\EndFor
f70e9ab4e680 psuedocode added
Chengsong
parents: 34
diff changeset
   619
		\For{\textit{rs[i] in array rs}}
f70e9ab4e680 psuedocode added
Chengsong
parents: 34
diff changeset
   620
        			\If{$rs[i] == ALTS(bs', rs')$}
f70e9ab4e680 psuedocode added
Chengsong
parents: 34
diff changeset
   621
				\State $rs'' \gets$ attach bits $bs'$ to all elements in $rs'$
f70e9ab4e680 psuedocode added
Chengsong
parents: 34
diff changeset
   622
				\State Insert $rs''$ into $rs$ at position $i$ ($rs[i]$ is destroyed, replaced by its list of children regular expressions)
f70e9ab4e680 psuedocode added
Chengsong
parents: 34
diff changeset
   623
			\EndIf
f70e9ab4e680 psuedocode added
Chengsong
parents: 34
diff changeset
   624
      		\EndFor
f70e9ab4e680 psuedocode added
Chengsong
parents: 34
diff changeset
   625
		\State Remove all duplicates in $rs$, only keeping the first copy for multiple occurrences of the same regular expression
f70e9ab4e680 psuedocode added
Chengsong
parents: 34
diff changeset
   626
		\State Remove all $0$s in $rs$
f70e9ab4e680 psuedocode added
Chengsong
parents: 34
diff changeset
   627
		\If{$ rs.length == 0$} \Return $ZERO$ \EndIf
f70e9ab4e680 psuedocode added
Chengsong
parents: 34
diff changeset
   628
		\If {$ rs.length == 1$} \Return$ rs[0] $\EndIf
f70e9ab4e680 psuedocode added
Chengsong
parents: 34
diff changeset
   629
	\EndCase
f70e9ab4e680 psuedocode added
Chengsong
parents: 34
diff changeset
   630
	\Case{$SEQ(bs, r_1, r_2)$}
f70e9ab4e680 psuedocode added
Chengsong
parents: 34
diff changeset
   631
		\If{$ r_1$ or $r_2$ is $ZERO$} \Return ZERO \EndIf
f70e9ab4e680 psuedocode added
Chengsong
parents: 34
diff changeset
   632
		\State update $r_1$ and $r_2$ by attaching $bs$ to their front
f70e9ab4e680 psuedocode added
Chengsong
parents: 34
diff changeset
   633
		\If {$r_1$ or $r_2$ is $ONE(bs')$} \Return $r_2$ or $r_1$ \EndIf
f70e9ab4e680 psuedocode added
Chengsong
parents: 34
diff changeset
   634
	\EndCase
f70e9ab4e680 psuedocode added
Chengsong
parents: 34
diff changeset
   635
	\Case{$Others$}
f70e9ab4e680 psuedocode added
Chengsong
parents: 34
diff changeset
   636
		\Return $areg$ as it is
f70e9ab4e680 psuedocode added
Chengsong
parents: 34
diff changeset
   637
	\EndCase
f70e9ab4e680 psuedocode added
Chengsong
parents: 34
diff changeset
   638
\EndSwitch
f70e9ab4e680 psuedocode added
Chengsong
parents: 34
diff changeset
   639
\EndProcedure
f70e9ab4e680 psuedocode added
Chengsong
parents: 34
diff changeset
   640
\end{algorithmic}
f70e9ab4e680 psuedocode added
Chengsong
parents: 34
diff changeset
   641
\end{algorithm}
36
Chengsong
parents: 35
diff changeset
   642
With this simplification our previous $(a + aa)^*$ example's 8000 nodes will be reduced to only 6.
35
f70e9ab4e680 psuedocode added
Chengsong
parents: 34
diff changeset
   643
f70e9ab4e680 psuedocode added
Chengsong
parents: 34
diff changeset
   644
Another modification is that we use simplification rules
30
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   645
inspired by Antimirov's work on partial derivatives. They maintain the
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   646
idea that only the first ``copy'' of a regular expression in an
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   647
alternative contributes to the calculation of a POSIX value. All
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   648
subsequent copies can be pruned from the regular expression.
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   649
35
f70e9ab4e680 psuedocode added
Chengsong
parents: 34
diff changeset
   650
30
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   651
We are currently engaged with proving that our simplification rules
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   652
actually do not affect the POSIX value that should be generated by the
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   653
algorithm according to the specification of a POSIX value and
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   654
furthermore that our derivatives stay small for all derivatives. For
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   655
this proof we use the theorem prover Isabelle. Once completed, this
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   656
result will advance the state-of-the-art: Sulzmann and Lu wrote in
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   657
their paper \cite{Sulzmann2014} about the bitcoded ``incremental
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   658
parsing method'' (that is the matching algorithm outlined in this
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   659
section):
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   660
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   661
\begin{quote}\it
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   662
  ``Correctness Claim: We further claim that the incremental parsing
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   663
  method in Figure~5 in combination with the simplification steps in
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   664
  Figure 6 yields POSIX parse trees. We have tested this claim
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   665
  extensively by using the method in Figure~3 as a reference but yet
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   666
  have to work out all proof details.''
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   667
\end{quote}  
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   668
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   669
\noindent
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   670
We would settle the correctness claim and furthermore obtain a much
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   671
tighter bound on the sizes of derivatives. The result is that our
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   672
algorithm should be correct and faster on all inputs.  The original
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   673
blow-up, as observed in JavaScript, Python and Java, would be excluded
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   674
from happening in our algorithm.
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   675
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   676
\section{Conclusion}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   677
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   678
In this PhD-project we are interested in fast algorithms for regular
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   679
expression matching. While this seems to be a ``settled'' area, in
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   680
fact interesting research questions are popping up as soon as one steps
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   681
outside the classic automata theory (for example in terms of what kind
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   682
of regular expressions are supported). The reason why it is
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   683
interesting for us to look at the derivative approach introduced by
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   684
Brzozowski for regular expression matching, and then much further
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   685
developed by Sulzmann and Lu, is that derivatives can elegantly deal
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   686
with some of the regular expressions that are of interest in ``real
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   687
life''. This includes the not-regular expression, written $\neg\,r$
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   688
(that is all strings that are not recognised by $r$), but also bounded
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   689
regular expressions such as $r^{\{n\}}$ and $r^{\{n..m\}}$). There is
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   690
also hope that the derivatives can provide another angle for how to
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   691
deal more efficiently with back-references, which are one of the
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   692
reasons why regular expression engines in JavaScript, Python and Java
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   693
choose to not implement the classic automata approach of transforming
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   694
regular expressions into NFAs and then DFAs---because we simply do not
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   695
know how such back-references can be represented by DFAs.
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   696
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   697
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   698
\bibliographystyle{plain}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   699
\bibliography{root}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   700
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   701
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   702
\end{document}