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