ninems/ninems.tex
author Chengsong
Tue, 16 Jul 2019 22:20:11 +0100
changeset 76 f575cf219377
parent 75 24d9d64c2a95
parent 74 9e791ef6022f
child 77 058133a9ffe0
permissions -rw-r--r--
merged
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
45
60cb82639691 spell check
Christian Urban <urbanc@in.tum.de>
parents: 44
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}
63
d3c22f809dde more proof-reading
Christian Urban <urbanc@in.tum.de>
parents: 62
diff changeset
     5
%\usepackage{algorithm}
35
f70e9ab4e680 psuedocode added
Chengsong
parents: 34
diff changeset
     6
\usepackage{amsmath}
f70e9ab4e680 psuedocode added
Chengsong
parents: 34
diff changeset
     7
\usepackage[noend]{algpseudocode}
42
Chengsong
parents: 41
diff changeset
     8
\usepackage{enumitem}
70
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
     9
\usepackage{nccmath}
63
d3c22f809dde more proof-reading
Christian Urban <urbanc@in.tum.de>
parents: 62
diff changeset
    10
d3c22f809dde more proof-reading
Christian Urban <urbanc@in.tum.de>
parents: 62
diff changeset
    11
\definecolor{darkblue}{rgb}{0,0,0.6}
d3c22f809dde more proof-reading
Christian Urban <urbanc@in.tum.de>
parents: 62
diff changeset
    12
\hypersetup{colorlinks=true,allcolors=darkblue}
70
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
    13
\newcommand{\comment}[1]%
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
    14
{{\color{red}$\Rightarrow$}\marginpar{\raggedright\small{\bf\color{red}#1}}}
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
    15
30
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    16
% \documentclass{article}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    17
%\usepackage[utf8]{inputenc}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    18
%\usepackage[english]{babel}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    19
%\usepackage{listings}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    20
% \usepackage{amsthm}
63
d3c22f809dde more proof-reading
Christian Urban <urbanc@in.tum.de>
parents: 62
diff changeset
    21
%\usepackage{hyperref}
30
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    22
% \usepackage[margin=0.5in]{geometry}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    23
%\usepackage{pmboxdraw}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    24
 
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    25
\title{POSIX Regular Expression Matching and Lexing}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    26
\author{Chengsong Tan}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    27
\affil{King's College London\\
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    28
London, UK\\
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    29
\texttt{chengsong.tan@kcl.ac.uk}}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    30
\authorrunning{Chengsong Tan}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    31
\Copyright{Chengsong Tan}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    32
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    33
\newcommand{\dn}{\stackrel{\mbox{\scriptsize def}}{=}}%
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    34
\newcommand{\ZERO}{\mbox{\bf 0}}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    35
\newcommand{\ONE}{\mbox{\bf 1}}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    36
\def\lexer{\mathit{lexer}}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    37
\def\mkeps{\mathit{mkeps}}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    38
\def\inj{\mathit{inj}}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    39
\def\Empty{\mathit{Empty}}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    40
\def\Left{\mathit{Left}}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    41
\def\Right{\mathit{Right}}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    42
\def\Stars{\mathit{Stars}}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    43
\def\Char{\mathit{Char}}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    44
\def\Seq{\mathit{Seq}}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    45
\def\Der{\mathit{Der}}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    46
\def\nullable{\mathit{nullable}}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    47
\def\Z{\mathit{Z}}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    48
\def\S{\mathit{S}}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    49
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    50
%\theoremstyle{theorem}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    51
%\newtheorem{theorem}{Theorem}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    52
%\theoremstyle{lemma}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    53
%\newtheorem{lemma}{Lemma}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    54
%\newcommand{\lemmaautorefname}{Lemma}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    55
%\theoremstyle{definition}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    56
%\newtheorem{definition}{Definition}
35
f70e9ab4e680 psuedocode added
Chengsong
parents: 34
diff changeset
    57
\algnewcommand\algorithmicswitch{\textbf{switch}}
f70e9ab4e680 psuedocode added
Chengsong
parents: 34
diff changeset
    58
\algnewcommand\algorithmiccase{\textbf{case}}
f70e9ab4e680 psuedocode added
Chengsong
parents: 34
diff changeset
    59
\algnewcommand\algorithmicassert{\texttt{assert}}
f70e9ab4e680 psuedocode added
Chengsong
parents: 34
diff changeset
    60
\algnewcommand\Assert[1]{\State \algorithmicassert(#1)}%
f70e9ab4e680 psuedocode added
Chengsong
parents: 34
diff changeset
    61
% New "environments"
f70e9ab4e680 psuedocode added
Chengsong
parents: 34
diff changeset
    62
\algdef{SE}[SWITCH]{Switch}{EndSwitch}[1]{\algorithmicswitch\ #1\ \algorithmicdo}{\algorithmicend\ \algorithmicswitch}%
f70e9ab4e680 psuedocode added
Chengsong
parents: 34
diff changeset
    63
\algdef{SE}[CASE]{Case}{EndCase}[1]{\algorithmiccase\ #1}{\algorithmicend\ \algorithmiccase}%
f70e9ab4e680 psuedocode added
Chengsong
parents: 34
diff changeset
    64
\algtext*{EndSwitch}%
f70e9ab4e680 psuedocode added
Chengsong
parents: 34
diff changeset
    65
\algtext*{EndCase}%
30
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    66
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    67
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    68
\begin{document}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    69
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    70
\maketitle
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    71
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    72
\begin{abstract}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    73
  Brzozowski introduced in 1964 a beautifully simple algorithm for
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    74
  regular expression matching based on the notion of derivatives of
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    75
  regular expressions. In 2014, Sulzmann and Lu extended this
40
8063792920ef proof reading
Christian Urban <urbanc@in.tum.de>
parents: 39
diff changeset
    76
  algorithm to not just give a YES/NO answer for whether or not a
64
afd0d702a4fe some changes
Chengsong
parents: 63
diff changeset
    77
  regular expression matches a string, but in case it does also
58
f0360e17080e proofread
Christian Urban <urbanc@in.tum.de>
parents: 57
diff changeset
    78
  answers with \emph{how} it matches the string.  This is important for
40
8063792920ef proof reading
Christian Urban <urbanc@in.tum.de>
parents: 39
diff changeset
    79
  applications such as lexing (tokenising a string). The problem is to
8063792920ef proof reading
Christian Urban <urbanc@in.tum.de>
parents: 39
diff changeset
    80
  make the algorithm by Sulzmann and Lu fast on all inputs without
8063792920ef proof reading
Christian Urban <urbanc@in.tum.de>
parents: 39
diff changeset
    81
  breaking its correctness. We have already developed some
59
8ff7b7508824 changes1
Chengsong
parents: 58
diff changeset
    82
  simplification rules for this, but have not yet proved that they
40
8063792920ef proof reading
Christian Urban <urbanc@in.tum.de>
parents: 39
diff changeset
    83
  preserve the correctness of the algorithm. We also have not yet
8063792920ef proof reading
Christian Urban <urbanc@in.tum.de>
parents: 39
diff changeset
    84
  looked at extended regular expressions, such as bounded repetitions,
8063792920ef proof reading
Christian Urban <urbanc@in.tum.de>
parents: 39
diff changeset
    85
  negation and back-references.
30
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    86
\end{abstract}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    87
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    88
\section{Introduction}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    89
70
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
    90
30
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    91
This PhD-project is about regular expression matching and
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    92
lexing. Given the maturity of this topic, the reader might wonder:
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    93
Surely, regular expressions must have already been studied to death?
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    94
What could possibly be \emph{not} known in this area? And surely all
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    95
implemented algorithms for regular expression matching are blindingly
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    96
fast?
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    97
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    98
Unfortunately these preconceptions are not supported by evidence: Take
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
    99
for example the regular expression $(a^*)^*\,b$ and ask whether
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   100
strings of the form $aa..a$ match this regular
64
afd0d702a4fe some changes
Chengsong
parents: 63
diff changeset
   101
expression. Obviously not---the expected $b$ in the last
30
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   102
position is missing. One would expect that modern regular expression
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   103
matching engines can find this out very quickly. Alas, if one tries
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   104
this example in JavaScript, Python or Java 8 with strings like 28
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   105
$a$'s, one discovers that this decision takes around 30 seconds and
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   106
takes considerably longer when adding a few more $a$'s, as the graphs
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   107
below show:
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   108
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   109
\begin{center}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   110
\begin{tabular}{@{}c@{\hspace{0mm}}c@{\hspace{0mm}}c@{}}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   111
\begin{tikzpicture}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   112
\begin{axis}[
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   113
    xlabel={$n$},
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   114
    x label style={at={(1.05,-0.05)}},
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   115
    ylabel={time in secs},
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   116
    enlargelimits=false,
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   117
    xtick={0,5,...,30},
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   118
    xmax=33,
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   119
    ymax=35,
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   120
    ytick={0,5,...,30},
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   121
    scaled ticks=false,
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   122
    axis lines=left,
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   123
    width=5cm,
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   124
    height=4cm, 
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   125
    legend entries={JavaScript},  
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   126
    legend pos=north west,
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   127
    legend cell align=left]
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   128
\addplot[red,mark=*, mark options={fill=white}] table {re-js.data};
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   129
\end{axis}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   130
\end{tikzpicture}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   131
  &
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   132
\begin{tikzpicture}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   133
\begin{axis}[
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   134
    xlabel={$n$},
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   135
    x label style={at={(1.05,-0.05)}},
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   136
    %ylabel={time in secs},
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   137
    enlargelimits=false,
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   138
    xtick={0,5,...,30},
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   139
    xmax=33,
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   140
    ymax=35,
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   141
    ytick={0,5,...,30},
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   142
    scaled ticks=false,
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   143
    axis lines=left,
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   144
    width=5cm,
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   145
    height=4cm, 
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   146
    legend entries={Python},  
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   147
    legend pos=north west,
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   148
    legend cell align=left]
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   149
\addplot[blue,mark=*, mark options={fill=white}] table {re-python2.data};
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   150
\end{axis}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   151
\end{tikzpicture}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   152
  &
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   153
\begin{tikzpicture}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   154
\begin{axis}[
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   155
    xlabel={$n$},
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   156
    x label style={at={(1.05,-0.05)}},
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   157
    %ylabel={time in secs},
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   158
    enlargelimits=false,
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   159
    xtick={0,5,...,30},
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   160
    xmax=33,
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   161
    ymax=35,
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   162
    ytick={0,5,...,30},
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   163
    scaled ticks=false,
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   164
    axis lines=left,
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   165
    width=5cm,
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   166
    height=4cm, 
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   167
    legend entries={Java 8},  
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   168
    legend pos=north west,
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   169
    legend cell align=left]
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   170
\addplot[cyan,mark=*, mark options={fill=white}] table {re-java.data};
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   171
\end{axis}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   172
\end{tikzpicture}\\
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   173
\multicolumn{3}{c}{Graphs: Runtime for matching $(a^*)^*\,b$ with strings 
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   174
           of the form $\underbrace{aa..a}_{n}$.}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   175
\end{tabular}    
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   176
\end{center}  
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   177
58
f0360e17080e proofread
Christian Urban <urbanc@in.tum.de>
parents: 57
diff changeset
   178
\noindent These are clearly abysmal and possibly surprising results. One
64
afd0d702a4fe some changes
Chengsong
parents: 63
diff changeset
   179
would expect these systems to do  much better than that---after all,
58
f0360e17080e proofread
Christian Urban <urbanc@in.tum.de>
parents: 57
diff changeset
   180
given a DFA and a string, deciding whether a string is matched by this
f0360e17080e proofread
Christian Urban <urbanc@in.tum.de>
parents: 57
diff changeset
   181
DFA should be linear.
30
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   182
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   183
Admittedly, the regular expression $(a^*)^*\,b$ is carefully chosen to
64
afd0d702a4fe some changes
Chengsong
parents: 63
diff changeset
   184
exhibit this exponential behaviour.  Unfortunately, such regular
afd0d702a4fe some changes
Chengsong
parents: 63
diff changeset
   185
expressions are not just a few outliers. They are actually 
afd0d702a4fe some changes
Chengsong
parents: 63
diff changeset
   186
frequent enough to have a separate name created for
30
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   187
them---\emph{evil regular expressions}. In empiric work, Davis et al
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   188
report that they have found thousands of such evil regular expressions
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   189
in the JavaScript and Python ecosystems \cite{Davis18}.
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   190
58
f0360e17080e proofread
Christian Urban <urbanc@in.tum.de>
parents: 57
diff changeset
   191
This exponential blowup in matching algorithms sometimes causes
63
d3c22f809dde more proof-reading
Christian Urban <urbanc@in.tum.de>
parents: 62
diff changeset
   192
considerable grief in real life: for example on 20 July 2016 one evil
58
f0360e17080e proofread
Christian Urban <urbanc@in.tum.de>
parents: 57
diff changeset
   193
regular expression brought the webpage
f0360e17080e proofread
Christian Urban <urbanc@in.tum.de>
parents: 57
diff changeset
   194
\href{http://stackexchange.com}{Stack Exchange} to its
63
d3c22f809dde more proof-reading
Christian Urban <urbanc@in.tum.de>
parents: 62
diff changeset
   195
knees.\footnote{\url{https://stackstatus.net/post/147710624694/outage-postmortem-july-20-2016}}
30
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   196
In this instance, a regular expression intended to just trim white
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   197
spaces from the beginning and the end of a line actually consumed
64
afd0d702a4fe some changes
Chengsong
parents: 63
diff changeset
   198
massive amounts of CPU-resources---causing web servers to
afd0d702a4fe some changes
Chengsong
parents: 63
diff changeset
   199
grind to a halt. This happened when a post with 20,000 white spaces was
58
f0360e17080e proofread
Christian Urban <urbanc@in.tum.de>
parents: 57
diff changeset
   200
submitted, but importantly the white spaces were neither at the
75
24d9d64c2a95 added the cloudfare eg.
Chengsong
parents: 72
diff changeset
   201
beginning nor at the end. 
24d9d64c2a95 added the cloudfare eg.
Chengsong
parents: 72
diff changeset
   202
As a result, the regular expression matching
24d9d64c2a95 added the cloudfare eg.
Chengsong
parents: 72
diff changeset
   203
engine needed to backtrack over many choices.
24d9d64c2a95 added the cloudfare eg.
Chengsong
parents: 72
diff changeset
   204
In this example, the time needed to process the string is not 
24d9d64c2a95 added the cloudfare eg.
Chengsong
parents: 72
diff changeset
   205
exactly the classical exponential case, but rather $O(n^2)$
24d9d64c2a95 added the cloudfare eg.
Chengsong
parents: 72
diff changeset
   206
with respect to the string length. But this is enough for the 
24d9d64c2a95 added the cloudfare eg.
Chengsong
parents: 72
diff changeset
   207
home page of stackexchnge to respond not fast enough to
24d9d64c2a95 added the cloudfare eg.
Chengsong
parents: 72
diff changeset
   208
the load balancer, which thought that there must be some
24d9d64c2a95 added the cloudfare eg.
Chengsong
parents: 72
diff changeset
   209
attack and therefore stopped the servers from responding to 
24d9d64c2a95 added the cloudfare eg.
Chengsong
parents: 72
diff changeset
   210
requests. This makes the whole site become unavailable.
24d9d64c2a95 added the cloudfare eg.
Chengsong
parents: 72
diff changeset
   211
Another fresh example that just came out of the oven
24d9d64c2a95 added the cloudfare eg.
Chengsong
parents: 72
diff changeset
   212
is the cloudfare outage incident. A poorly written
24d9d64c2a95 added the cloudfare eg.
Chengsong
parents: 72
diff changeset
   213
regular expression exhibited exponential behaviour
24d9d64c2a95 added the cloudfare eg.
Chengsong
parents: 72
diff changeset
   214
and exhausted CPUs that serve HTTP traffic on 2 July 2019,
24d9d64c2a95 added the cloudfare eg.
Chengsong
parents: 72
diff changeset
   215
 resulting in a 27-minute outage. The regular expression contained 
24d9d64c2a95 added the cloudfare eg.
Chengsong
parents: 72
diff changeset
   216
adjacent Kleene stars, which is the source of the exponential number
24d9d64c2a95 added the cloudfare eg.
Chengsong
parents: 72
diff changeset
   217
of backtracking possibilities. Although this outage has a series of
24d9d64c2a95 added the cloudfare eg.
Chengsong
parents: 72
diff changeset
   218
causes that came from different vulnerabilities within the system 
24d9d64c2a95 added the cloudfare eg.
Chengsong
parents: 72
diff changeset
   219
of cloudfare, the heart of the problem lies within regular expression.
24d9d64c2a95 added the cloudfare eg.
Chengsong
parents: 72
diff changeset
   220
Such outages could be excluded from happening if the matching 
24d9d64c2a95 added the cloudfare eg.
Chengsong
parents: 72
diff changeset
   221
algorithm is guaranteed to be fast.\footnote{\url{https://blog.cloudflare.com/details-of-the-cloudflare-outage-on-july-2-2019/}}
24d9d64c2a95 added the cloudfare eg.
Chengsong
parents: 72
diff changeset
   222
 The underlying problem is
58
f0360e17080e proofread
Christian Urban <urbanc@in.tum.de>
parents: 57
diff changeset
   223
that many ``real life'' regular expression matching engines do not use
75
24d9d64c2a95 added the cloudfare eg.
Chengsong
parents: 72
diff changeset
   224
DFAs for matching. 
24d9d64c2a95 added the cloudfare eg.
Chengsong
parents: 72
diff changeset
   225
This is because they support regular expressions that
58
f0360e17080e proofread
Christian Urban <urbanc@in.tum.de>
parents: 57
diff changeset
   226
are not covered by the classical automata theory, and in this more
f0360e17080e proofread
Christian Urban <urbanc@in.tum.de>
parents: 57
diff changeset
   227
general setting there are quite a few research questions still
f0360e17080e proofread
Christian Urban <urbanc@in.tum.de>
parents: 57
diff changeset
   228
unanswered and fast algorithms still need to be developed (for example
63
d3c22f809dde more proof-reading
Christian Urban <urbanc@in.tum.de>
parents: 62
diff changeset
   229
how to treat bounded repetitions, negation and  back-references
d3c22f809dde more proof-reading
Christian Urban <urbanc@in.tum.de>
parents: 62
diff changeset
   230
efficiently).
64
afd0d702a4fe some changes
Chengsong
parents: 63
diff changeset
   231
%question: dfa can have exponential states. isn't this the actual reason why they do not use dfas?
afd0d702a4fe some changes
Chengsong
parents: 63
diff changeset
   232
%how do they avoid dfas exponential states if they use them for fast matching?
30
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   233
There is also another under-researched problem to do with regular
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   234
expressions and lexing, i.e.~the process of breaking up strings into
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   235
sequences of tokens according to some regular expressions. In this
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   236
setting one is not just interested in whether or not a regular
64
afd0d702a4fe some changes
Chengsong
parents: 63
diff changeset
   237
expression matches a string, but also in \emph{how}.  Consider for example a regular expression
30
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   238
$r_{key}$ for recognising keywords such as \textit{if}, \textit{then}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   239
and so on; and a regular expression $r_{id}$ for recognising
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   240
identifiers (say, a single character followed by characters or
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   241
numbers). One can then form the compound regular expression
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   242
$(r_{key} + r_{id})^*$ and use it to tokenise strings.  But then how
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   243
should the string \textit{iffoo} be tokenised?  It could be tokenised
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   244
as a keyword followed by an identifier, or the entire string as a
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   245
single identifier.  Similarly, how should the string \textit{if} be
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   246
tokenised? Both regular expressions, $r_{key}$ and $r_{id}$, would
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   247
``fire''---so is it an identifier or a keyword?  While in applications
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   248
there is a well-known strategy to decide these questions, called POSIX
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   249
matching, only relatively recently precise definitions of what POSIX
64
afd0d702a4fe some changes
Chengsong
parents: 63
diff changeset
   250
matching actually means has been formalised
46
9b48724ec609 proofread
Christian Urban <urbanc@in.tum.de>
parents: 45
diff changeset
   251
\cite{AusafDyckhoffUrban2016,OkuiSuzuki2010,Vansummeren2006}. 
9b48724ec609 proofread
Christian Urban <urbanc@in.tum.de>
parents: 45
diff changeset
   252
Such a definition has also been given by Sulzmann and  Lu \cite{Sulzmann2014}, but the
9b48724ec609 proofread
Christian Urban <urbanc@in.tum.de>
parents: 45
diff changeset
   253
corresponding correctness proof turned out to be  faulty \cite{AusafDyckhoffUrban2016}.
9b48724ec609 proofread
Christian Urban <urbanc@in.tum.de>
parents: 45
diff changeset
   254
Roughly, POSIX matching means matching the longest initial substring.
64
afd0d702a4fe some changes
Chengsong
parents: 63
diff changeset
   255
In the case of a tie, the initial sub-match is chosen according to some priorities attached to the
30
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   256
regular expressions (e.g.~keywords have a higher priority than
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   257
identifiers). This sounds rather simple, but according to Grathwohl et
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   258
al \cite[Page 36]{CrashCourse2014} this is not the case. They wrote:
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   259
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   260
\begin{quote}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   261
\it{}``The POSIX strategy is more complicated than the greedy because of 
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   262
the dependence on information about the length of matched strings in the 
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   263
various subexpressions.''
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   264
\end{quote}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   265
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   266
\noindent
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   267
This is also supported by evidence collected by Kuklewicz
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   268
\cite{Kuklewicz} who noticed that a number of POSIX regular expression
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   269
matchers calculate incorrect results.
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   270
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   271
Our focus is on an algorithm introduced by Sulzmann and Lu in 2014 for
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   272
regular expression matching according to the POSIX strategy
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   273
\cite{Sulzmann2014}. Their algorithm is based on an older algorithm by
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   274
Brzozowski from 1964 where he introduced the notion of derivatives of
72
83b021fc7d29 interesting?
Chengsong
parents: 71
diff changeset
   275
regular expressions~\cite{Brzozowski1964}. We shall briefly explain
58
f0360e17080e proofread
Christian Urban <urbanc@in.tum.de>
parents: 57
diff changeset
   276
this algorithm next.
30
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   277
46
9b48724ec609 proofread
Christian Urban <urbanc@in.tum.de>
parents: 45
diff changeset
   278
\section{The Algorithm by Brzozowski based on Derivatives of Regular
9b48724ec609 proofread
Christian Urban <urbanc@in.tum.de>
parents: 45
diff changeset
   279
Expressions}
30
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   280
40
8063792920ef proof reading
Christian Urban <urbanc@in.tum.de>
parents: 39
diff changeset
   281
Suppose (basic) regular expressions are given by the following grammar:
38
b5363c0dcd99 half easy changes
Chengsong
parents: 37
diff changeset
   282
\[			r ::=   \ZERO \mid  \ONE
b5363c0dcd99 half easy changes
Chengsong
parents: 37
diff changeset
   283
			 \mid  c  
b5363c0dcd99 half easy changes
Chengsong
parents: 37
diff changeset
   284
			 \mid  r_1 \cdot r_2
b5363c0dcd99 half easy changes
Chengsong
parents: 37
diff changeset
   285
			 \mid  r_1 + r_2   
b5363c0dcd99 half easy changes
Chengsong
parents: 37
diff changeset
   286
			 \mid r^*         
b5363c0dcd99 half easy changes
Chengsong
parents: 37
diff changeset
   287
\]
30
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   288
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   289
\noindent
46
9b48724ec609 proofread
Christian Urban <urbanc@in.tum.de>
parents: 45
diff changeset
   290
The intended meaning of the constructors is as follows: $\ZERO$
30
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   291
cannot match any string, $\ONE$ can match the empty string, the
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   292
character regular expression $c$ can match the character $c$, and so
40
8063792920ef proof reading
Christian Urban <urbanc@in.tum.de>
parents: 39
diff changeset
   293
on.
8063792920ef proof reading
Christian Urban <urbanc@in.tum.de>
parents: 39
diff changeset
   294
58
f0360e17080e proofread
Christian Urban <urbanc@in.tum.de>
parents: 57
diff changeset
   295
The ingenious contribution by Brzozowski is the notion of
30
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   296
\emph{derivatives} of regular expressions.  The idea behind this
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   297
notion is as follows: suppose a regular expression $r$ can match a
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   298
string of the form $c\!::\! s$ (that is a list of characters starting
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   299
with $c$), what does the regular expression look like that can match
40
8063792920ef proof reading
Christian Urban <urbanc@in.tum.de>
parents: 39
diff changeset
   300
just $s$? Brzozowski gave a neat answer to this question. He started
8063792920ef proof reading
Christian Urban <urbanc@in.tum.de>
parents: 39
diff changeset
   301
with the definition of $nullable$:
36
Chengsong
parents: 35
diff changeset
   302
\begin{center}
Chengsong
parents: 35
diff changeset
   303
		\begin{tabular}{lcl}
Chengsong
parents: 35
diff changeset
   304
			$\nullable(\ZERO)$     & $\dn$ & $\mathit{false}$ \\  
Chengsong
parents: 35
diff changeset
   305
			$\nullable(\ONE)$      & $\dn$ & $\mathit{true}$ \\
Chengsong
parents: 35
diff changeset
   306
			$\nullable(c)$ 	       & $\dn$ & $\mathit{false}$ \\
Chengsong
parents: 35
diff changeset
   307
			$\nullable(r_1 + r_2)$ & $\dn$ & $\nullable(r_1) \vee \nullable(r_2)$ \\
Chengsong
parents: 35
diff changeset
   308
			$\nullable(r_1\cdot r_2)$  & $\dn$ & $\nullable(r_1) \wedge \nullable(r_2)$ \\
Chengsong
parents: 35
diff changeset
   309
			$\nullable(r^*)$       & $\dn$ & $\mathit{true}$ \\
Chengsong
parents: 35
diff changeset
   310
		\end{tabular}
Chengsong
parents: 35
diff changeset
   311
	\end{center}
38
b5363c0dcd99 half easy changes
Chengsong
parents: 37
diff changeset
   312
This function simply tests whether the empty string is in $L(r)$.
36
Chengsong
parents: 35
diff changeset
   313
He then defined
30
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   314
the following operation on regular expressions, written
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   315
$r\backslash c$ (the derivative of $r$ w.r.t.~the character $c$):
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   316
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   317
\begin{center}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   318
\begin{tabular}{lcl}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   319
		$\ZERO \backslash c$ & $\dn$ & $\ZERO$\\  
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   320
		$\ONE \backslash c$  & $\dn$ & $\ZERO$\\
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   321
		$d \backslash c$     & $\dn$ & 
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   322
		$\mathit{if} \;c = d\;\mathit{then}\;\ONE\;\mathit{else}\;\ZERO$\\
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   323
$(r_1 + r_2)\backslash c$     & $\dn$ & $r_1 \backslash c \,+\, r_2 \backslash c$\\
36
Chengsong
parents: 35
diff changeset
   324
$(r_1 \cdot r_2)\backslash c$ & $\dn$ & $\mathit{if} \, nullable(r_1)$\\
30
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   325
	&   & $\mathit{then}\;(r_1\backslash c) \cdot r_2 \,+\, r_2\backslash c$\\
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   326
	&   & $\mathit{else}\;(r_1\backslash c) \cdot r_2$\\
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   327
	$(r^*)\backslash c$           & $\dn$ & $(r\backslash c) \cdot r^*$\\
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   328
\end{tabular}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   329
\end{center}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   330
46
9b48724ec609 proofread
Christian Urban <urbanc@in.tum.de>
parents: 45
diff changeset
   331
%Assuming the classic notion of a
9b48724ec609 proofread
Christian Urban <urbanc@in.tum.de>
parents: 45
diff changeset
   332
%\emph{language} of a regular expression, written $L(\_)$, t
30
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   333
40
8063792920ef proof reading
Christian Urban <urbanc@in.tum.de>
parents: 39
diff changeset
   334
\noindent
8063792920ef proof reading
Christian Urban <urbanc@in.tum.de>
parents: 39
diff changeset
   335
The main property of the derivative operation is that
30
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   336
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   337
\begin{center}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   338
$c\!::\!s \in L(r)$ holds
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   339
if and only if $s \in L(r\backslash c)$.
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   340
\end{center}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   341
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   342
\noindent
46
9b48724ec609 proofread
Christian Urban <urbanc@in.tum.de>
parents: 45
diff changeset
   343
For us the main advantage is that derivatives can be
38
b5363c0dcd99 half easy changes
Chengsong
parents: 37
diff changeset
   344
straightforwardly implemented in any functional programming language,
b5363c0dcd99 half easy changes
Chengsong
parents: 37
diff changeset
   345
and are easily definable and reasoned about in theorem provers---the
b5363c0dcd99 half easy changes
Chengsong
parents: 37
diff changeset
   346
definitions just consist of inductive datatypes and simple recursive
b5363c0dcd99 half easy changes
Chengsong
parents: 37
diff changeset
   347
functions. Moreover, the notion of derivatives can be easily
b5363c0dcd99 half easy changes
Chengsong
parents: 37
diff changeset
   348
generalised to cover extended regular expression constructors such as
b5363c0dcd99 half easy changes
Chengsong
parents: 37
diff changeset
   349
the not-regular expression, written $\neg\,r$, or bounded repetitions
b5363c0dcd99 half easy changes
Chengsong
parents: 37
diff changeset
   350
(for example $r^{\{n\}}$ and $r^{\{n..m\}}$), which cannot be so
b5363c0dcd99 half easy changes
Chengsong
parents: 37
diff changeset
   351
straightforwardly realised within the classic automata approach.
b5363c0dcd99 half easy changes
Chengsong
parents: 37
diff changeset
   352
For the moment however, we focus only on the usual basic regular expressions.
b5363c0dcd99 half easy changes
Chengsong
parents: 37
diff changeset
   353
b5363c0dcd99 half easy changes
Chengsong
parents: 37
diff changeset
   354
40
8063792920ef proof reading
Christian Urban <urbanc@in.tum.de>
parents: 39
diff changeset
   355
Now if we want to find out whether a string $s$ matches with a regular
8063792920ef proof reading
Christian Urban <urbanc@in.tum.de>
parents: 39
diff changeset
   356
expression $r$, build the derivatives of $r$ w.r.t.\ (in succession)
8063792920ef proof reading
Christian Urban <urbanc@in.tum.de>
parents: 39
diff changeset
   357
all the characters of the string $s$. Finally, test whether the
8063792920ef proof reading
Christian Urban <urbanc@in.tum.de>
parents: 39
diff changeset
   358
resulting regular expression can match the empty string.  If yes, then
8063792920ef proof reading
Christian Urban <urbanc@in.tum.de>
parents: 39
diff changeset
   359
$r$ matches $s$, and no in the negative case. To implement this idea
8063792920ef proof reading
Christian Urban <urbanc@in.tum.de>
parents: 39
diff changeset
   360
we can generalise the derivative operation to strings like this:
46
9b48724ec609 proofread
Christian Urban <urbanc@in.tum.de>
parents: 45
diff changeset
   361
30
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   362
\begin{center}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   363
\begin{tabular}{lcl}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   364
$r \backslash (c\!::\!s) $ & $\dn$ & $(r \backslash c) \backslash s$ \\
40
8063792920ef proof reading
Christian Urban <urbanc@in.tum.de>
parents: 39
diff changeset
   365
$r \backslash [\,] $ & $\dn$ & $r$
30
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   366
\end{tabular}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   367
\end{center}
40
8063792920ef proof reading
Christian Urban <urbanc@in.tum.de>
parents: 39
diff changeset
   368
37
17d8e7599a01 new changes
Chengsong
parents: 36
diff changeset
   369
\noindent
46
9b48724ec609 proofread
Christian Urban <urbanc@in.tum.de>
parents: 45
diff changeset
   370
and then define as  regular-expression matching algorithm: 
30
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   371
\[
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   372
match\;s\;r \;\dn\; nullable(r\backslash s)
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   373
\]
40
8063792920ef proof reading
Christian Urban <urbanc@in.tum.de>
parents: 39
diff changeset
   374
8063792920ef proof reading
Christian Urban <urbanc@in.tum.de>
parents: 39
diff changeset
   375
\noindent
64
afd0d702a4fe some changes
Chengsong
parents: 63
diff changeset
   376
This algorithm looks graphically as follows:
46
9b48724ec609 proofread
Christian Urban <urbanc@in.tum.de>
parents: 45
diff changeset
   377
\begin{equation}\label{graph:*}
9b48724ec609 proofread
Christian Urban <urbanc@in.tum.de>
parents: 45
diff changeset
   378
\begin{tikzcd}
9b48724ec609 proofread
Christian Urban <urbanc@in.tum.de>
parents: 45
diff changeset
   379
r_0 \arrow[r, "\backslash c_0"]  & r_1 \arrow[r, "\backslash c_1"] & r_2 \arrow[r, dashed]  & r_n  \arrow[r,"\textit{nullable}?"] & \;\textrm{YES}/\textrm{NO}
38
b5363c0dcd99 half easy changes
Chengsong
parents: 37
diff changeset
   380
\end{tikzcd}
46
9b48724ec609 proofread
Christian Urban <urbanc@in.tum.de>
parents: 45
diff changeset
   381
\end{equation}
40
8063792920ef proof reading
Christian Urban <urbanc@in.tum.de>
parents: 39
diff changeset
   382
8063792920ef proof reading
Christian Urban <urbanc@in.tum.de>
parents: 39
diff changeset
   383
\noindent
46
9b48724ec609 proofread
Christian Urban <urbanc@in.tum.de>
parents: 45
diff changeset
   384
where we start with  a regular expression  $r_0$, build successive
9b48724ec609 proofread
Christian Urban <urbanc@in.tum.de>
parents: 45
diff changeset
   385
derivatives until we exhaust the string and then use \textit{nullable}
9b48724ec609 proofread
Christian Urban <urbanc@in.tum.de>
parents: 45
diff changeset
   386
to test whether the result can match the empty string. It can  be
9b48724ec609 proofread
Christian Urban <urbanc@in.tum.de>
parents: 45
diff changeset
   387
relatively  easily shown that this matcher is correct  (that is given
64
afd0d702a4fe some changes
Chengsong
parents: 63
diff changeset
   388
an $s = c_0...c_{n-1}$ and an $r_0$, it generates YES if and only if $s \in L(r_0)$).
46
9b48724ec609 proofread
Christian Urban <urbanc@in.tum.de>
parents: 45
diff changeset
   389
9b48724ec609 proofread
Christian Urban <urbanc@in.tum.de>
parents: 45
diff changeset
   390
 
9b48724ec609 proofread
Christian Urban <urbanc@in.tum.de>
parents: 45
diff changeset
   391
\section{Values and the Algorithm by Sulzmann and Lu}
38
b5363c0dcd99 half easy changes
Chengsong
parents: 37
diff changeset
   392
30
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   393
One limitation, however, of Brzozowski's algorithm is that it only
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   394
produces a YES/NO answer for whether a string is being matched by a
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   395
regular expression.  Sulzmann and Lu~\cite{Sulzmann2014} extended this
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   396
algorithm to allow generation of an actual matching, called a
72
83b021fc7d29 interesting?
Chengsong
parents: 71
diff changeset
   397
\emph{value} or sometimes lexical values.  These values and regular expressions correspond to each 
46
9b48724ec609 proofread
Christian Urban <urbanc@in.tum.de>
parents: 45
diff changeset
   398
other as illustrated in the following table:
9b48724ec609 proofread
Christian Urban <urbanc@in.tum.de>
parents: 45
diff changeset
   399
30
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   400
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   401
\begin{center}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   402
	\begin{tabular}{c@{\hspace{20mm}}c}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   403
		\begin{tabular}{@{}rrl@{}}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   404
			\multicolumn{3}{@{}l}{\textbf{Regular Expressions}}\medskip\\
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   405
			$r$ & $::=$  & $\ZERO$\\
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   406
			& $\mid$ & $\ONE$   \\
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   407
			& $\mid$ & $c$          \\
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   408
			& $\mid$ & $r_1 \cdot r_2$\\
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   409
			& $\mid$ & $r_1 + r_2$   \\
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   410
			\\
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   411
			& $\mid$ & $r^*$         \\
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   412
		\end{tabular}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   413
		&
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   414
		\begin{tabular}{@{\hspace{0mm}}rrl@{}}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   415
			\multicolumn{3}{@{}l}{\textbf{Values}}\medskip\\
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   416
			$v$ & $::=$  & \\
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   417
			&        & $\Empty$   \\
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   418
			& $\mid$ & $\Char(c)$          \\
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   419
			& $\mid$ & $\Seq\,v_1\, v_2$\\
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   420
			& $\mid$ & $\Left(v)$   \\
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   421
			& $\mid$ & $\Right(v)$  \\
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   422
			& $\mid$ & $\Stars\,[v_1,\ldots\,v_n]$ \\
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   423
		\end{tabular}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   424
	\end{tabular}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   425
\end{center}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   426
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   427
\noindent
64
afd0d702a4fe some changes
Chengsong
parents: 63
diff changeset
   428
No value  corresponds to $\ZERO$; $\Empty$ corresponds to
63
d3c22f809dde more proof-reading
Christian Urban <urbanc@in.tum.de>
parents: 62
diff changeset
   429
$\ONE$; $\Char$ to the character regular expression; $\Seq$ to the
d3c22f809dde more proof-reading
Christian Urban <urbanc@in.tum.de>
parents: 62
diff changeset
   430
sequence regular expression and so on. The idea of values is to encode
72
83b021fc7d29 interesting?
Chengsong
parents: 71
diff changeset
   431
a kind of lexical value for how the sub-parts of a regular expression match
64
afd0d702a4fe some changes
Chengsong
parents: 63
diff changeset
   432
the sub-parts of a string. To see this, suppose a \emph{flatten} operation, written
72
83b021fc7d29 interesting?
Chengsong
parents: 71
diff changeset
   433
$|v|$ for values. We can use this function to extract the underlying string of a value
63
d3c22f809dde more proof-reading
Christian Urban <urbanc@in.tum.de>
parents: 62
diff changeset
   434
$v$. For example, $|\mathit{Seq} \, (\textit{Char x}) \, (\textit{Char
d3c22f809dde more proof-reading
Christian Urban <urbanc@in.tum.de>
parents: 62
diff changeset
   435
y})|$ is the string $xy$.  Using flatten, we can describe how values
64
afd0d702a4fe some changes
Chengsong
parents: 63
diff changeset
   436
encode parse trees: $\Seq\,v_1\, v_2$ encodes a tree with 2 children nodes
afd0d702a4fe some changes
Chengsong
parents: 63
diff changeset
   437
that tells how the string $|v_1| @
63
d3c22f809dde more proof-reading
Christian Urban <urbanc@in.tum.de>
parents: 62
diff changeset
   438
|v_2|$ matches the regex $r_1 \cdot r_2$ whereby $r_1$ matches the
d3c22f809dde more proof-reading
Christian Urban <urbanc@in.tum.de>
parents: 62
diff changeset
   439
substring $|v_1|$ and, respectively, $r_2$ matches the substring
d3c22f809dde more proof-reading
Christian Urban <urbanc@in.tum.de>
parents: 62
diff changeset
   440
$|v_2|$. Exactly how these two are matched is contained in the
64
afd0d702a4fe some changes
Chengsong
parents: 63
diff changeset
   441
children nodes $v_1$ and $v_2$ of parent $\textit{Seq}$ . 
30
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   442
72
83b021fc7d29 interesting?
Chengsong
parents: 71
diff changeset
   443
 To give a concrete example of how values work, consider the string $xy$
46
9b48724ec609 proofread
Christian Urban <urbanc@in.tum.de>
parents: 45
diff changeset
   444
and the regular expression $(x + (y + xy))^*$. We can view this regular
30
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   445
expression as a tree and if the string $xy$ is matched by two Star
46
9b48724ec609 proofread
Christian Urban <urbanc@in.tum.de>
parents: 45
diff changeset
   446
``iterations'', then the $x$ is matched by the left-most alternative in
9b48724ec609 proofread
Christian Urban <urbanc@in.tum.de>
parents: 45
diff changeset
   447
this tree and the $y$ by the right-left alternative. This suggests to
9b48724ec609 proofread
Christian Urban <urbanc@in.tum.de>
parents: 45
diff changeset
   448
record this matching as
30
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   449
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   450
\begin{center}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   451
$\Stars\,[\Left\,(\Char\,x), \Right(\Left(\Char\,y))]$
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   452
\end{center}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   453
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   454
\noindent
72
83b021fc7d29 interesting?
Chengsong
parents: 71
diff changeset
   455
where $\Stars \; [\ldots]$ records all the
64
afd0d702a4fe some changes
Chengsong
parents: 63
diff changeset
   456
iterations; and $\Left$, respectively $\Right$, which
30
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   457
alternative is used. The value for
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   458
matching $xy$ in a single ``iteration'', i.e.~the POSIX value,
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   459
would look as follows
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   460
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   461
\begin{center}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   462
$\Stars\,[\Seq\,(\Char\,x)\,(\Char\,y)]$
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   463
\end{center}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   464
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   465
\noindent
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   466
where $\Stars$ has only a single-element list for the single iteration
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   467
and $\Seq$ indicates that $xy$ is matched by a sequence regular
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   468
expression.
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   469
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   470
The contribution of Sulzmann and Lu is an extension of Brzozowski's
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   471
algorithm by a second phase (the first phase being building successive
46
9b48724ec609 proofread
Christian Urban <urbanc@in.tum.de>
parents: 45
diff changeset
   472
derivatives---see \eqref{graph:*}). In this second phase, a POSIX value 
72
83b021fc7d29 interesting?
Chengsong
parents: 71
diff changeset
   473
is generated in case the regular expression matches  the string. 
83b021fc7d29 interesting?
Chengsong
parents: 71
diff changeset
   474
Pictorially, the Sulzmann and Lu algorithm is as follows:
46
9b48724ec609 proofread
Christian Urban <urbanc@in.tum.de>
parents: 45
diff changeset
   475
70
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   476
\begin{ceqn}
59
8ff7b7508824 changes1
Chengsong
parents: 58
diff changeset
   477
\begin{equation}\label{graph:2}
30
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   478
\begin{tikzcd}
36
Chengsong
parents: 35
diff changeset
   479
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
   480
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
   481
\end{tikzcd}
59
8ff7b7508824 changes1
Chengsong
parents: 58
diff changeset
   482
\end{equation}
70
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   483
\end{ceqn}
37
17d8e7599a01 new changes
Chengsong
parents: 36
diff changeset
   484
46
9b48724ec609 proofread
Christian Urban <urbanc@in.tum.de>
parents: 45
diff changeset
   485
\noindent
59
8ff7b7508824 changes1
Chengsong
parents: 58
diff changeset
   486
For convenience, we shall employ the following notations: the regular expression we
58
f0360e17080e proofread
Christian Urban <urbanc@in.tum.de>
parents: 57
diff changeset
   487
start with is $r_0$, and the given string $s$ is composed of characters $c_0 c_1
64
afd0d702a4fe some changes
Chengsong
parents: 63
diff changeset
   488
\ldots c_{n-1}$. In  the first phase, we build the derivatives $r_1$, $r_2$, \ldots  according to
72
83b021fc7d29 interesting?
Chengsong
parents: 71
diff changeset
   489
the characters $c_0$, $c_1$  until we exhaust the string and
83b021fc7d29 interesting?
Chengsong
parents: 71
diff changeset
   490
obtain the derivative $r_n$. We test whether this derivative is
46
9b48724ec609 proofread
Christian Urban <urbanc@in.tum.de>
parents: 45
diff changeset
   491
$\textit{nullable}$ or not. If not, we know the string does not match
9b48724ec609 proofread
Christian Urban <urbanc@in.tum.de>
parents: 45
diff changeset
   492
$r$ and no value needs to be generated. If yes, we start building the
72
83b021fc7d29 interesting?
Chengsong
parents: 71
diff changeset
   493
values incrementally by \emph{injecting} back the characters into
83b021fc7d29 interesting?
Chengsong
parents: 71
diff changeset
   494
the earlier values $v_n, \ldots, v_0$. For the first value $v_0$, we call the function
46
9b48724ec609 proofread
Christian Urban <urbanc@in.tum.de>
parents: 45
diff changeset
   495
$\textit{mkeps}$, which builds the parse tree for how the empty string
72
83b021fc7d29 interesting?
Chengsong
parents: 71
diff changeset
   496
has been matched by the (nullable) regular expression $r_n$. This function is defined
46
9b48724ec609 proofread
Christian Urban <urbanc@in.tum.de>
parents: 45
diff changeset
   497
as
30
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   498
51
5df7faf69238 added mkeps and pder, still have not proof read it
Chengsong
parents: 50
diff changeset
   499
	\begin{center}
5df7faf69238 added mkeps and pder, still have not proof read it
Chengsong
parents: 50
diff changeset
   500
		\begin{tabular}{lcl}
5df7faf69238 added mkeps and pder, still have not proof read it
Chengsong
parents: 50
diff changeset
   501
			$\mkeps(\ONE)$ 		& $\dn$ & $\Empty$ \\
5df7faf69238 added mkeps and pder, still have not proof read it
Chengsong
parents: 50
diff changeset
   502
			$\mkeps(r_{1}+r_{2})$	& $\dn$ 
5df7faf69238 added mkeps and pder, still have not proof read it
Chengsong
parents: 50
diff changeset
   503
			& \textit{if} $\nullable(r_{1})$\\ 
5df7faf69238 added mkeps and pder, still have not proof read it
Chengsong
parents: 50
diff changeset
   504
			& & \textit{then} $\Left(\mkeps(r_{1}))$\\ 
5df7faf69238 added mkeps and pder, still have not proof read it
Chengsong
parents: 50
diff changeset
   505
			& & \textit{else} $\Right(\mkeps(r_{2}))$\\
5df7faf69238 added mkeps and pder, still have not proof read it
Chengsong
parents: 50
diff changeset
   506
			$\mkeps(r_1\cdot r_2)$ 	& $\dn$ & $\Seq\,(\mkeps\,r_1)\,(\mkeps\,r_2)$\\
5df7faf69238 added mkeps and pder, still have not proof read it
Chengsong
parents: 50
diff changeset
   507
			$mkeps(r^*)$	        & $\dn$ & $\Stars\,[]$
5df7faf69238 added mkeps and pder, still have not proof read it
Chengsong
parents: 50
diff changeset
   508
		\end{tabular}
5df7faf69238 added mkeps and pder, still have not proof read it
Chengsong
parents: 50
diff changeset
   509
	\end{center}
41
a1f90febbc7f example
Chengsong
parents: 40
diff changeset
   510
59
8ff7b7508824 changes1
Chengsong
parents: 58
diff changeset
   511
8ff7b7508824 changes1
Chengsong
parents: 58
diff changeset
   512
\noindent There are no cases for $\ZERO$ and $c$, since
8ff7b7508824 changes1
Chengsong
parents: 58
diff changeset
   513
these regular expression cannot match the empty string. Note
8ff7b7508824 changes1
Chengsong
parents: 58
diff changeset
   514
also that in case of alternatives we give preference to the
8ff7b7508824 changes1
Chengsong
parents: 58
diff changeset
   515
regular expression on the left-hand side. This will become
8ff7b7508824 changes1
Chengsong
parents: 58
diff changeset
   516
important later on.
8ff7b7508824 changes1
Chengsong
parents: 58
diff changeset
   517
8ff7b7508824 changes1
Chengsong
parents: 58
diff changeset
   518
After this, we inject back the characters one by one in order to build
63
d3c22f809dde more proof-reading
Christian Urban <urbanc@in.tum.de>
parents: 62
diff changeset
   519
the parse tree $v_i$ for how the regex $r_i$ matches the string $s_i$
64
afd0d702a4fe some changes
Chengsong
parents: 63
diff changeset
   520
($s_i = c_i \ldots c_{n-1}$ ) from the previous parse tree $v_{i+1}$. After
63
d3c22f809dde more proof-reading
Christian Urban <urbanc@in.tum.de>
parents: 62
diff changeset
   521
injecting back $n$ characters, we get the parse tree for how $r_0$
d3c22f809dde more proof-reading
Christian Urban <urbanc@in.tum.de>
parents: 62
diff changeset
   522
matches $s$. For this Sulzmann and Lu defined a function that reverses
d3c22f809dde more proof-reading
Christian Urban <urbanc@in.tum.de>
parents: 62
diff changeset
   523
the ``chopping off'' of characters during the derivative phase. The
d3c22f809dde more proof-reading
Christian Urban <urbanc@in.tum.de>
parents: 62
diff changeset
   524
corresponding function is called $\textit{inj}$; it takes three
d3c22f809dde more proof-reading
Christian Urban <urbanc@in.tum.de>
parents: 62
diff changeset
   525
arguments: the first one is a regular expression ${r_{i-1}}$, before the
d3c22f809dde more proof-reading
Christian Urban <urbanc@in.tum.de>
parents: 62
diff changeset
   526
character is chopped off, the second is a character ${c_{i-1}}$, the
d3c22f809dde more proof-reading
Christian Urban <urbanc@in.tum.de>
parents: 62
diff changeset
   527
character we want to inject and the third argument is the value
64
afd0d702a4fe some changes
Chengsong
parents: 63
diff changeset
   528
${v_i}$, into which one wants to inject the character (it
63
d3c22f809dde more proof-reading
Christian Urban <urbanc@in.tum.de>
parents: 62
diff changeset
   529
corresponds to the regular expression after the character has been
d3c22f809dde more proof-reading
Christian Urban <urbanc@in.tum.de>
parents: 62
diff changeset
   530
chopped off). The result of this function is a new value. The definition
d3c22f809dde more proof-reading
Christian Urban <urbanc@in.tum.de>
parents: 62
diff changeset
   531
of $\textit{inj}$ is as follows: 
59
8ff7b7508824 changes1
Chengsong
parents: 58
diff changeset
   532
8ff7b7508824 changes1
Chengsong
parents: 58
diff changeset
   533
\begin{center}
8ff7b7508824 changes1
Chengsong
parents: 58
diff changeset
   534
\begin{tabular}{l@{\hspace{1mm}}c@{\hspace{1mm}}l}
8ff7b7508824 changes1
Chengsong
parents: 58
diff changeset
   535
  $\textit{inj}\,(c)\,c\,Empty$            & $\dn$ & $Char\,c$\\
8ff7b7508824 changes1
Chengsong
parents: 58
diff changeset
   536
  $\textit{inj}\,(r_1 + r_2)\,c\,\Left(v)$ & $\dn$ & $\Left(\textit{inj}\,r_1\,c\,v)$\\
8ff7b7508824 changes1
Chengsong
parents: 58
diff changeset
   537
  $\textit{inj}\,(r_1 + r_2)\,c\,Right(v)$ & $\dn$ & $Right(\textit{inj}\,r_2\,c\,v)$\\
8ff7b7508824 changes1
Chengsong
parents: 58
diff changeset
   538
  $\textit{inj}\,(r_1 \cdot r_2)\,c\,Seq(v_1,v_2)$ & $\dn$  & $Seq(\textit{inj}\,r_1\,c\,v_1,v_2)$\\
8ff7b7508824 changes1
Chengsong
parents: 58
diff changeset
   539
  $\textit{inj}\,(r_1 \cdot r_2)\,c\,\Left(Seq(v_1,v_2))$ & $\dn$  & $Seq(\textit{inj}\,r_1\,c\,v_1,v_2)$\\
8ff7b7508824 changes1
Chengsong
parents: 58
diff changeset
   540
  $\textit{inj}\,(r_1 \cdot r_2)\,c\,Right(v)$ & $\dn$  & $Seq(\textit{mkeps}(r_1),\textit{inj}\,r_2\,c\,v)$\\
8ff7b7508824 changes1
Chengsong
parents: 58
diff changeset
   541
  $\textit{inj}\,(r^*)\,c\,Seq(v,Stars\,vs)$         & $\dn$  & $Stars((\textit{inj}\,r\,c\,v)\,::\,vs)$\\
8ff7b7508824 changes1
Chengsong
parents: 58
diff changeset
   542
\end{tabular}
8ff7b7508824 changes1
Chengsong
parents: 58
diff changeset
   543
\end{center}
8ff7b7508824 changes1
Chengsong
parents: 58
diff changeset
   544
63
d3c22f809dde more proof-reading
Christian Urban <urbanc@in.tum.de>
parents: 62
diff changeset
   545
\noindent This definition is by recursion on the ``shape'' of regular
d3c22f809dde more proof-reading
Christian Urban <urbanc@in.tum.de>
parents: 62
diff changeset
   546
expressions and values. To understands this definition better consider
d3c22f809dde more proof-reading
Christian Urban <urbanc@in.tum.de>
parents: 62
diff changeset
   547
the situation when we build the derivative on regular expression $r_{i-1}$.
d3c22f809dde more proof-reading
Christian Urban <urbanc@in.tum.de>
parents: 62
diff changeset
   548
For this we chop off a character from $r_{i-1}$ to form $r_i$. This leaves a
72
83b021fc7d29 interesting?
Chengsong
parents: 71
diff changeset
   549
``hole'' in $r_i$ and its corresponding value $v_i$. 
83b021fc7d29 interesting?
Chengsong
parents: 71
diff changeset
   550
To calculate $v_{i-1}$, we need to
64
afd0d702a4fe some changes
Chengsong
parents: 63
diff changeset
   551
locate where that hole is and fill it. 
afd0d702a4fe some changes
Chengsong
parents: 63
diff changeset
   552
We can find this location by
63
d3c22f809dde more proof-reading
Christian Urban <urbanc@in.tum.de>
parents: 62
diff changeset
   553
comparing $r_{i-1}$ and $v_i$. For instance, if $r_{i-1}$ is of shape
64
afd0d702a4fe some changes
Chengsong
parents: 63
diff changeset
   554
$r_a \cdot r_b$, and $v_i$ is of shape $\Left(Seq(v_1,v_2))$, we know immediately that 
63
d3c22f809dde more proof-reading
Christian Urban <urbanc@in.tum.de>
parents: 62
diff changeset
   555
%
d3c22f809dde more proof-reading
Christian Urban <urbanc@in.tum.de>
parents: 62
diff changeset
   556
\[ (r_a \cdot r_b)\backslash c = (r_a\backslash c) \cdot r_b \,+\, r_b\backslash c,\]
d3c22f809dde more proof-reading
Christian Urban <urbanc@in.tum.de>
parents: 62
diff changeset
   557
d3c22f809dde more proof-reading
Christian Urban <urbanc@in.tum.de>
parents: 62
diff changeset
   558
\noindent
59
8ff7b7508824 changes1
Chengsong
parents: 58
diff changeset
   559
otherwise if $r_a$ is not nullable,
63
d3c22f809dde more proof-reading
Christian Urban <urbanc@in.tum.de>
parents: 62
diff changeset
   560
\[ (r_a \cdot r_b)\backslash c = (r_a\backslash c) \cdot r_b,\]
d3c22f809dde more proof-reading
Christian Urban <urbanc@in.tum.de>
parents: 62
diff changeset
   561
d3c22f809dde more proof-reading
Christian Urban <urbanc@in.tum.de>
parents: 62
diff changeset
   562
\noindent
64
afd0d702a4fe some changes
Chengsong
parents: 63
diff changeset
   563
the value $v_i$ should be  $\Seq(\ldots)$, contradicting the fact that
afd0d702a4fe some changes
Chengsong
parents: 63
diff changeset
   564
$v_i$ is actually of shape $\Left(\ldots)$. Furthermore, since $v_i$ is of shape
63
d3c22f809dde more proof-reading
Christian Urban <urbanc@in.tum.de>
parents: 62
diff changeset
   565
$\Left(\ldots)$ instead of $\Right(\ldots)$, we know that the left
64
afd0d702a4fe some changes
Chengsong
parents: 63
diff changeset
   566
branch of \[ (r_a \cdot r_b)\backslash c =
afd0d702a4fe some changes
Chengsong
parents: 63
diff changeset
   567
\bold{\underline{ (r_a\backslash c) \cdot r_b} }\,+\, r_b\backslash c,\](underlined)
afd0d702a4fe some changes
Chengsong
parents: 63
diff changeset
   568
 is taken instead of the right one. This means $c$ is chopped off 
afd0d702a4fe some changes
Chengsong
parents: 63
diff changeset
   569
from $r_a$ rather than $r_b$.
afd0d702a4fe some changes
Chengsong
parents: 63
diff changeset
   570
We have therefore found out 
63
d3c22f809dde more proof-reading
Christian Urban <urbanc@in.tum.de>
parents: 62
diff changeset
   571
that the hole will be on $r_a$. So we recursively call $\inj\, 
64
afd0d702a4fe some changes
Chengsong
parents: 63
diff changeset
   572
r_a\,c\,v_a$ to fill that hole in $v_a$. After injection, the value 
63
d3c22f809dde more proof-reading
Christian Urban <urbanc@in.tum.de>
parents: 62
diff changeset
   573
$v_i$ for $r_i = r_a \cdot r_b$ should be $\Seq\,(\inj\,r_a\,c\,v_a)\,v_b$.
60
c737a0259194 sorry not all done, need a few more mins for last few changes
Chengsong
parents: 59
diff changeset
   574
Other clauses can be understood in a similar way.
59
8ff7b7508824 changes1
Chengsong
parents: 58
diff changeset
   575
71
0573615e41a3 new changes?
Chengsong
parents: 70
diff changeset
   576
%\comment{Other word: insight?}
0573615e41a3 new changes?
Chengsong
parents: 70
diff changeset
   577
The following example gives an insight of $\textit{inj}$'s effect
65
df2e0faccb23 moew changes
Chengsong
parents: 64
diff changeset
   578
and how Sulzmann and Lu's algorithm works as a whole.
df2e0faccb23 moew changes
Chengsong
parents: 64
diff changeset
   579
 Suppose we have a
df2e0faccb23 moew changes
Chengsong
parents: 64
diff changeset
   580
regular expression $((((a+b)+ab)+c)+abc)^*$, and want to match it against
63
d3c22f809dde more proof-reading
Christian Urban <urbanc@in.tum.de>
parents: 62
diff changeset
   581
the string $abc$ (when $abc$ is written as a regular expression, the most
d3c22f809dde more proof-reading
Christian Urban <urbanc@in.tum.de>
parents: 62
diff changeset
   582
standard way of expressing it should be $a \cdot (b \cdot c)$. We omit
65
df2e0faccb23 moew changes
Chengsong
parents: 64
diff changeset
   583
the parentheses and dots here for readability). 
df2e0faccb23 moew changes
Chengsong
parents: 64
diff changeset
   584
This algorithm returns a POSIX value, which means it
df2e0faccb23 moew changes
Chengsong
parents: 64
diff changeset
   585
will go for the longest matching, i.e.~it should match the string
df2e0faccb23 moew changes
Chengsong
parents: 64
diff changeset
   586
$abc$ in one star iteration, using the longest alternative $abc$ in the
df2e0faccb23 moew changes
Chengsong
parents: 64
diff changeset
   587
sub-expression $((((a+b)+ab)+c)+abc)$ (we use $r$ to denote this sub-expression
64
afd0d702a4fe some changes
Chengsong
parents: 63
diff changeset
   588
for conciseness). 
65
df2e0faccb23 moew changes
Chengsong
parents: 64
diff changeset
   589
Before $\textit{inj}$ comes into play, 
df2e0faccb23 moew changes
Chengsong
parents: 64
diff changeset
   590
our lexer first builds derivative using string $abc$ (we simplified some regular expressions like
df2e0faccb23 moew changes
Chengsong
parents: 64
diff changeset
   591
$0 \cdot b$ to $0$ for conciseness; we also omit parentheses if
63
d3c22f809dde more proof-reading
Christian Urban <urbanc@in.tum.de>
parents: 62
diff changeset
   592
they are clear from the context):
60
c737a0259194 sorry not all done, need a few more mins for last few changes
Chengsong
parents: 59
diff changeset
   593
%Similarly, we allow
c737a0259194 sorry not all done, need a few more mins for last few changes
Chengsong
parents: 59
diff changeset
   594
%$\textit{ALT}$ to take a list of regular expressions as an argument
c737a0259194 sorry not all done, need a few more mins for last few changes
Chengsong
parents: 59
diff changeset
   595
%instead of just 2 operands to reduce the nested depth of
c737a0259194 sorry not all done, need a few more mins for last few changes
Chengsong
parents: 59
diff changeset
   596
%$\textit{ALT}$
c737a0259194 sorry not all done, need a few more mins for last few changes
Chengsong
parents: 59
diff changeset
   597
\begin{center}
63
d3c22f809dde more proof-reading
Christian Urban <urbanc@in.tum.de>
parents: 62
diff changeset
   598
\begin{tabular}{lcl}
72
83b021fc7d29 interesting?
Chengsong
parents: 71
diff changeset
   599
$r^*$ & $\xrightarrow{\backslash a}$ & $r_1 = (\ONE+\ZERO+\ONE \cdot b + \ZERO + \ONE \cdot b \cdot c) \cdot r^*$\\
83b021fc7d29 interesting?
Chengsong
parents: 71
diff changeset
   600
      & $\xrightarrow{\backslash b}$ & $r_2 = (\ZERO+\ZERO+\ONE \cdot \ONE + \ZERO + \ONE \cdot \ONE \cdot c) \cdot r^* +(\ZERO+\ONE+\ZERO  + \ZERO + \ZERO) \cdot r^*$\\
83b021fc7d29 interesting?
Chengsong
parents: 71
diff changeset
   601
      & $\xrightarrow{\backslash c}$ & $r_3 = ((\ZERO+\ZERO+\ZERO + \ZERO + \ONE \cdot \ONE \cdot \ONE) \cdot r^* + (\ZERO+\ZERO+\ZERO  + \ONE + \ZERO) \cdot r^*) + $\\ 
83b021fc7d29 interesting?
Chengsong
parents: 71
diff changeset
   602
      &                              & $\phantom{r_3 = (} ((\ZERO+\ONE+\ZERO  + \ZERO + \ZERO) \cdot r^* + (\ZERO+\ZERO+\ZERO  + \ONE + \ZERO) \cdot r^* )$
63
d3c22f809dde more proof-reading
Christian Urban <urbanc@in.tum.de>
parents: 62
diff changeset
   603
\end{tabular}
60
c737a0259194 sorry not all done, need a few more mins for last few changes
Chengsong
parents: 59
diff changeset
   604
\end{center}
63
d3c22f809dde more proof-reading
Christian Urban <urbanc@in.tum.de>
parents: 62
diff changeset
   605
d3c22f809dde more proof-reading
Christian Urban <urbanc@in.tum.de>
parents: 62
diff changeset
   606
\noindent
72
83b021fc7d29 interesting?
Chengsong
parents: 71
diff changeset
   607
In  case $r_3$ is nullable, we can call $\textit{mkeps}$ 
60
c737a0259194 sorry not all done, need a few more mins for last few changes
Chengsong
parents: 59
diff changeset
   608
to construct a parse tree for how $r_3$ matched the string $abc$. 
72
83b021fc7d29 interesting?
Chengsong
parents: 71
diff changeset
   609
$\textit{mkeps}$ gives the following value $v_3$: 
65
df2e0faccb23 moew changes
Chengsong
parents: 64
diff changeset
   610
\begin{center}
df2e0faccb23 moew changes
Chengsong
parents: 64
diff changeset
   611
$\Left(\Left(\Seq(\Right(\Seq(\Empty, \Seq(\Empty,\Empty))), \Stars [])))$
df2e0faccb23 moew changes
Chengsong
parents: 64
diff changeset
   612
\end{center}
df2e0faccb23 moew changes
Chengsong
parents: 64
diff changeset
   613
The outer $\Left(\Left(\ldots))$ tells us the leftmost nullable part of $r_3$(underlined):
70
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   614
65
df2e0faccb23 moew changes
Chengsong
parents: 64
diff changeset
   615
\begin{center}
72
83b021fc7d29 interesting?
Chengsong
parents: 71
diff changeset
   616
   $( \underline{(\ZERO+\ZERO+\ZERO+ \ZERO+ \ONE \cdot \ONE \cdot \ONE) \cdot r^*} + (\ZERO+\ZERO+\ZERO + \ONE + \ZERO)
83b021fc7d29 interesting?
Chengsong
parents: 71
diff changeset
   617
  \cdot r^*) +((\ZERO+\ONE+\ZERO  + \ZERO + \ZERO) \cdot r^*+(\ZERO+\ZERO+\ZERO  + \ONE + \ZERO) \cdot r^* ).$
65
df2e0faccb23 moew changes
Chengsong
parents: 64
diff changeset
   618
 \end{center}
70
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   619
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   620
\noindent
72
83b021fc7d29 interesting?
Chengsong
parents: 71
diff changeset
   621
 Note that the leftmost location of term $((\ZERO+\ZERO+\ZERO + \ZERO + \ONE \cdot \ONE \cdot
83b021fc7d29 interesting?
Chengsong
parents: 71
diff changeset
   622
 \ONE) \cdot r^*$ (which corresponds to the initial sub-match $abc$) allows
83b021fc7d29 interesting?
Chengsong
parents: 71
diff changeset
   623
 $\textit{mkeps}$ to pick it up because $\textit{mkeps}$ is defined to always choose the
70
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   624
 left one when it is nullable. In the case of this example, $abc$ is
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   625
 preferred over $a$ or $ab$. This $\Left(\Left(\ldots))$ location is
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   626
 naturally generated by two applications of the splitting clause
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   627
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   628
\begin{center}
65
df2e0faccb23 moew changes
Chengsong
parents: 64
diff changeset
   629
     $(r_1 \cdot r_2)\backslash c  (when \; r_1 \; nullable) \, = (r_1\backslash c) \cdot r_2 \,+\, r_2\backslash c.$
70
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   630
\end{center}
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   631
       
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   632
\noindent
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   633
By this clause, we put $r_1 \backslash c \cdot r_2 $ at the
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   634
$\textit{front}$ and $r_2 \backslash c$ at the $\textit{back}$. This
72
83b021fc7d29 interesting?
Chengsong
parents: 71
diff changeset
   635
allows $\textit{mkeps}$ to always pick up among two matches the one with a longer
70
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   636
initial sub-match. Removing the outside $\Left(\Left(...))$, the inside
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   637
sub-value 
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   638
 
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   639
\begin{center}
65
df2e0faccb23 moew changes
Chengsong
parents: 64
diff changeset
   640
 $\Seq(\Right(\Seq(\Empty, \Seq(\Empty, \Empty))), \Stars [])$
70
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   641
\end{center}
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   642
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   643
\noindent
72
83b021fc7d29 interesting?
Chengsong
parents: 71
diff changeset
   644
tells us how the empty string $[]$ is matched with $(\ZERO+\ZERO+\ZERO + \ZERO + \ONE \cdot
83b021fc7d29 interesting?
Chengsong
parents: 71
diff changeset
   645
\ONE \cdot \ONE) \cdot r^*$. We match $[]$ by a sequence of 2 nullable regular
70
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   646
expressions. The first one is an alternative, we take the rightmost
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   647
alternative---whose language contains the empty string. The second
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   648
nullable regular expression is a Kleene star. $\Stars$ tells us how it
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   649
generates the nullable regular expression: by 0 iterations to form
72
83b021fc7d29 interesting?
Chengsong
parents: 71
diff changeset
   650
$\ONE$. Now $\textit{inj}$ injects characters back and incrementally
70
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   651
builds a parse tree based on $v_3$. Using the value $v_3$, the character
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   652
c, and the regular expression $r_2$, we can recover how $r_2$ matched
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   653
the string $[c]$ : $\textit{inj} \; r_2 \; c \; v_3$ gives us
65
df2e0faccb23 moew changes
Chengsong
parents: 64
diff changeset
   654
 \begin{center}
df2e0faccb23 moew changes
Chengsong
parents: 64
diff changeset
   655
 $v_2 = \Left(\Seq(\Right(\Seq(\Empty, \Seq(\Empty, c))), \Stars [])),$
df2e0faccb23 moew changes
Chengsong
parents: 64
diff changeset
   656
 \end{center}
df2e0faccb23 moew changes
Chengsong
parents: 64
diff changeset
   657
which tells us how $r_2$ matched $[c]$. After this we inject back the character $b$, and get
df2e0faccb23 moew changes
Chengsong
parents: 64
diff changeset
   658
\begin{center}
df2e0faccb23 moew changes
Chengsong
parents: 64
diff changeset
   659
$v_1 = \Seq(\Right(\Seq(\Empty, \Seq(b, c))), \Stars [])$
df2e0faccb23 moew changes
Chengsong
parents: 64
diff changeset
   660
\end{center}
61
580c7b84f900 hi finished
Chengsong
parents: 60
diff changeset
   661
 for how 
65
df2e0faccb23 moew changes
Chengsong
parents: 64
diff changeset
   662
 \begin{center}
72
83b021fc7d29 interesting?
Chengsong
parents: 71
diff changeset
   663
 $r_1= (\ONE+\ZERO+\ONE \cdot b + \ZERO + \ONE \cdot b \cdot c) \cdot r*$
65
df2e0faccb23 moew changes
Chengsong
parents: 64
diff changeset
   664
 \end{center}
61
580c7b84f900 hi finished
Chengsong
parents: 60
diff changeset
   665
  matched  the string $bc$ before it split into 2 pieces. 
580c7b84f900 hi finished
Chengsong
parents: 60
diff changeset
   666
  Finally, after injecting character $a$ back to $v_1$, 
65
df2e0faccb23 moew changes
Chengsong
parents: 64
diff changeset
   667
  we get  the parse tree 
df2e0faccb23 moew changes
Chengsong
parents: 64
diff changeset
   668
  \begin{center}
df2e0faccb23 moew changes
Chengsong
parents: 64
diff changeset
   669
  $v_0= \Stars [\Right(\Seq(a, \Seq(b, c)))]$
df2e0faccb23 moew changes
Chengsong
parents: 64
diff changeset
   670
  \end{center}
df2e0faccb23 moew changes
Chengsong
parents: 64
diff changeset
   671
   for how $r$ matched $abc$. This completes the algorithm.
df2e0faccb23 moew changes
Chengsong
parents: 64
diff changeset
   672
   
61
580c7b84f900 hi finished
Chengsong
parents: 60
diff changeset
   673
%We omit the details of injection function, which is provided by Sulzmann and Lu's paper \cite{Sulzmann2014}. 
580c7b84f900 hi finished
Chengsong
parents: 60
diff changeset
   674
Readers might have noticed that the parse tree information 
580c7b84f900 hi finished
Chengsong
parents: 60
diff changeset
   675
is actually already available when doing derivatives. 
580c7b84f900 hi finished
Chengsong
parents: 60
diff changeset
   676
For example, immediately after the operation $\backslash a$ we know that if we want to match a string that starts with $a$,
580c7b84f900 hi finished
Chengsong
parents: 60
diff changeset
   677
 we can either take the initial match to be 
65
df2e0faccb23 moew changes
Chengsong
parents: 64
diff changeset
   678
 \begin{center}
42
Chengsong
parents: 41
diff changeset
   679
\begin{enumerate}
Chengsong
parents: 41
diff changeset
   680
    \item[1)] just $a$ or
Chengsong
parents: 41
diff changeset
   681
    \item[2)] string $ab$ or 
Chengsong
parents: 41
diff changeset
   682
    \item[3)] string $abc$.
Chengsong
parents: 41
diff changeset
   683
\end{enumerate}
65
df2e0faccb23 moew changes
Chengsong
parents: 64
diff changeset
   684
\end{center}
70
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   685
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   686
\noindent
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   687
In order to differentiate between these choices, we just need to
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   688
remember their positions--$a$ is on the left, $ab$ is in the middle ,
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   689
and $abc$ is on the right. Which one of these alternatives is chosen
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   690
later does not affect their relative position because our algorithm does
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   691
not change this order. If this parsing information can be determined and
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   692
does not change because of later derivatives, there is no point in
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   693
traversing this information twice. This leads to an optimisation---if we
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   694
store the information for parse trees inside the regular expression,
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   695
update it when we do derivative on them, and collect the information
72
83b021fc7d29 interesting?
Chengsong
parents: 71
diff changeset
   696
when finished with derivatives and call $\textit{mkeps}$ for deciding which
70
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   697
branch is POSIX, we can generate the parse tree in one pass, instead of
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   698
doing the rest $n$ injections. This leads to Sulzmann and Lu's novel
71
0573615e41a3 new changes?
Chengsong
parents: 70
diff changeset
   699
idea of using bitcodes in derivatives.
42
Chengsong
parents: 41
diff changeset
   700
72
83b021fc7d29 interesting?
Chengsong
parents: 71
diff changeset
   701
In the next section, we shall focus on the bitcoded algorithm and the
63
d3c22f809dde more proof-reading
Christian Urban <urbanc@in.tum.de>
parents: 62
diff changeset
   702
process of simplification of regular expressions. This is needed in
30
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   703
order to obtain \emph{fast} versions of the Brzozowski's, and Sulzmann
63
d3c22f809dde more proof-reading
Christian Urban <urbanc@in.tum.de>
parents: 62
diff changeset
   704
and Lu's algorithms.  This is where the PhD-project aims to advance the
d3c22f809dde more proof-reading
Christian Urban <urbanc@in.tum.de>
parents: 62
diff changeset
   705
state-of-the-art.
30
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   706
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   707
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   708
\section{Simplification of Regular Expressions}
63
d3c22f809dde more proof-reading
Christian Urban <urbanc@in.tum.de>
parents: 62
diff changeset
   709
70
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   710
Using bitcodes to guide  parsing is not a novel idea. It was applied to
63
d3c22f809dde more proof-reading
Christian Urban <urbanc@in.tum.de>
parents: 62
diff changeset
   711
context free grammars and then adapted by Henglein and Nielson for
70
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   712
efficient regular expression parsing using DFAs~\cite{nielson11bcre}.
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   713
Sulzmann and Lu took this idea of bitcodes a step further by integrating
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   714
bitcodes into derivatives. The reason why we want to use bitcodes in
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   715
this project is that we want to introduce more aggressive
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   716
simplifications in order to keep the size of derivatives small
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   717
throughout. This is because the main drawback of building successive
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   718
derivatives according to Brzozowski's definition is that they can grow
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   719
very quickly in size. This is mainly due to the fact that the derivative
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   720
operation generates often ``useless'' $\ZERO$s and $\ONE$s in
63
d3c22f809dde more proof-reading
Christian Urban <urbanc@in.tum.de>
parents: 62
diff changeset
   721
derivatives.  As a result, if implemented naively both algorithms by
70
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   722
Brzozowski and by Sulzmann and Lu are excruciatingly slow. For example
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   723
when starting with the regular expression $(a + aa)^*$ and building 12
63
d3c22f809dde more proof-reading
Christian Urban <urbanc@in.tum.de>
parents: 62
diff changeset
   724
successive derivatives w.r.t.~the character $a$, one obtains a
d3c22f809dde more proof-reading
Christian Urban <urbanc@in.tum.de>
parents: 62
diff changeset
   725
derivative regular expression with more than 8000 nodes (when viewed as
d3c22f809dde more proof-reading
Christian Urban <urbanc@in.tum.de>
parents: 62
diff changeset
   726
a tree). Operations like derivative and $\nullable$ need to traverse
d3c22f809dde more proof-reading
Christian Urban <urbanc@in.tum.de>
parents: 62
diff changeset
   727
such trees and consequently the bigger the size of the derivative the
66
8c8c82c0515f good to proofread
Chengsong
parents: 65
diff changeset
   728
slower the algorithm. 
35
f70e9ab4e680 psuedocode added
Chengsong
parents: 34
diff changeset
   729
70
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   730
Fortunately, one can simplify regular expressions after each derivative
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   731
step. Various simplifications of regular expressions are possible, such
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   732
as the simplifications of $\ZERO + r$, $r + \ZERO$, $\ONE\cdot r$, $r
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   733
\cdot \ONE$, and $r + r$ to just $r$. These simplifications do not
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   734
affect the answer for whether a regular expression matches a string or
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   735
not, but fortunately also do not affect the POSIX strategy of how
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   736
regular expressions match strings---although the latter is much harder
71
0573615e41a3 new changes?
Chengsong
parents: 70
diff changeset
   737
to establish. Some initial results in this regard have been
70
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   738
obtained in \cite{AusafDyckhoffUrban2016}. 
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   739
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   740
Unfortunately, the simplification rules outlined above  are not
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   741
sufficient to prevent an explosion for all regular expression. We
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   742
believe a tighter bound can be achieved that prevents an explosion in
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   743
all cases. Such a tighter bound is suggested by work of Antimirov who
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   744
proved that (partial) derivatives can be bound by the number of
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   745
characters contained in the initial regular expression
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   746
\cite{Antimirov95}. He defined the \emph{partial derivatives} of regular
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   747
expressions as follows:
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   748
52
25bbbb8b0e90 just in case of some accidents from erasing my work
Chengsong
parents: 51
diff changeset
   749
\begin{center}
25bbbb8b0e90 just in case of some accidents from erasing my work
Chengsong
parents: 51
diff changeset
   750
\begin{tabular}{lcl}
25bbbb8b0e90 just in case of some accidents from erasing my work
Chengsong
parents: 51
diff changeset
   751
 $\textit{pder} \; c \; 0$ & $\dn$ & $\emptyset$\\
25bbbb8b0e90 just in case of some accidents from erasing my work
Chengsong
parents: 51
diff changeset
   752
 $\textit{pder} \; c \; 1$ & $\dn$ & $\emptyset$ \\
25bbbb8b0e90 just in case of some accidents from erasing my work
Chengsong
parents: 51
diff changeset
   753
 $\textit{pder} \; c \; d$ & $\dn$ & $\textit{if} \; c \,=\, d \; \{  1   \}  \; \textit{else} \; \emptyset$ \\ 
25bbbb8b0e90 just in case of some accidents from erasing my work
Chengsong
parents: 51
diff changeset
   754
  $\textit{pder} \; c \; r_1+r_2$ & $\dn$ & $pder \; c \; r_1 \cup pder \; c \;  r_2$ \\
70
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   755
   $\textit{pder} \; c \; r_1 \cdot r_2$ & $\dn$ & $\textit{if} \; nullable \; r_1 $\\
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   756
     & & $\textit{then} \; \{  r \cdot r_2 \mid r \in pder \; c \; r_1   \}  \cup pder \; c \; r_2 \;$\\
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   757
     & & $\textit{else} \; \{  r \cdot r_2 \mid r \in pder \; c \; r_1   \} $ \\ 
52
25bbbb8b0e90 just in case of some accidents from erasing my work
Chengsong
parents: 51
diff changeset
   758
     $\textit{pder} \; c \; r^*$ & $\dn$ & $ \{  r' \cdot r^* \mid r' \in pder \; c \; r   \}  $ \\  
25bbbb8b0e90 just in case of some accidents from erasing my work
Chengsong
parents: 51
diff changeset
   759
 \end{tabular}
25bbbb8b0e90 just in case of some accidents from erasing my work
Chengsong
parents: 51
diff changeset
   760
 \end{center}
70
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   761
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   762
\noindent
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   763
A partial derivative of a regular expression $r$ is essentially a set of
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   764
regular expressions that are either $r$'s children expressions or a
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   765
concatenation of them. Antimirov has proved a tight bound of the size of
71
0573615e41a3 new changes?
Chengsong
parents: 70
diff changeset
   766
partial derivatives. Roughly
72
83b021fc7d29 interesting?
Chengsong
parents: 71
diff changeset
   767
speaking the size will be quadruple in the size of the regular expression.
83b021fc7d29 interesting?
Chengsong
parents: 71
diff changeset
   768
 If we want the size of derivatives 
71
0573615e41a3 new changes?
Chengsong
parents: 70
diff changeset
   769
to stay below this bound, we would need more aggressive simplifications
0573615e41a3 new changes?
Chengsong
parents: 70
diff changeset
   770
such as opening up alternatives to achieve the maximum level of duplicates
0573615e41a3 new changes?
Chengsong
parents: 70
diff changeset
   771
cancellation.
0573615e41a3 new changes?
Chengsong
parents: 70
diff changeset
   772
For example, the parentheses in $(a+b) \cdot c + bc$ can be opened up to
0573615e41a3 new changes?
Chengsong
parents: 70
diff changeset
   773
get $a\cdot c +b \cdot c
0573615e41a3 new changes?
Chengsong
parents: 70
diff changeset
   774
+ b \cdot c$, and then simplified to $a \cdot c+b \cdot c$. Another example is from
72
83b021fc7d29 interesting?
Chengsong
parents: 71
diff changeset
   775
$(a^*+a) + (a^*+ \ONE) + (a +\ONE)$ to $a^*+a+\ONE$.
71
0573615e41a3 new changes?
Chengsong
parents: 70
diff changeset
   776
Adding these more aggressive simplification rules
0573615e41a3 new changes?
Chengsong
parents: 70
diff changeset
   777
 helped us to achieve the same size bound as that of the partial derivatives.
0573615e41a3 new changes?
Chengsong
parents: 70
diff changeset
   778
To introduce these "spilling out alternatives" simplifications
0573615e41a3 new changes?
Chengsong
parents: 70
diff changeset
   779
 and make the correctness proof easier,
0573615e41a3 new changes?
Chengsong
parents: 70
diff changeset
   780
we used bitcodes. 
72
83b021fc7d29 interesting?
Chengsong
parents: 71
diff changeset
   781
Bitcodes look like this:
71
0573615e41a3 new changes?
Chengsong
parents: 70
diff changeset
   782
%This allows us to prove a tight
0573615e41a3 new changes?
Chengsong
parents: 70
diff changeset
   783
%bound on the size of regular expression during the running time of the
0573615e41a3 new changes?
Chengsong
parents: 70
diff changeset
   784
%algorithm if we can establish the connection between our simplification
0573615e41a3 new changes?
Chengsong
parents: 70
diff changeset
   785
%rules and partial derivatives.
35
f70e9ab4e680 psuedocode added
Chengsong
parents: 34
diff changeset
   786
f70e9ab4e680 psuedocode added
Chengsong
parents: 34
diff changeset
   787
 %We believe, and have generated test
f70e9ab4e680 psuedocode added
Chengsong
parents: 34
diff changeset
   788
%data, that a similar bound can be obtained for the derivatives in
f70e9ab4e680 psuedocode added
Chengsong
parents: 34
diff changeset
   789
%Sulzmann and Lu's algorithm. Let us give some details about this next.
30
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   790
72
83b021fc7d29 interesting?
Chengsong
parents: 71
diff changeset
   791
67
e974c5477a8c anotehr update
Chengsong
parents: 66
diff changeset
   792
\begin{center}
e974c5477a8c anotehr update
Chengsong
parents: 66
diff changeset
   793
		$b ::=   S \mid  Z \; \;\;
43
Chengsong
parents: 42
diff changeset
   794
bs ::= [] \mid b:bs    
67
e974c5477a8c anotehr update
Chengsong
parents: 66
diff changeset
   795
$
e974c5477a8c anotehr update
Chengsong
parents: 66
diff changeset
   796
\end{center}
71
0573615e41a3 new changes?
Chengsong
parents: 70
diff changeset
   797
They are just a string of bits, 
0573615e41a3 new changes?
Chengsong
parents: 70
diff changeset
   798
the names $S$ and $Z$  here are quite arbitrary, we can use 0 and 1 
0573615e41a3 new changes?
Chengsong
parents: 70
diff changeset
   799
or any other set of binary symbols to substitute them. 
0573615e41a3 new changes?
Chengsong
parents: 70
diff changeset
   800
Bitcodes(or bit-sequences) are a compact form of parse trees.
43
Chengsong
parents: 42
diff changeset
   801
Bitcodes are essentially incomplete values.
30
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   802
This can be straightforwardly seen in the following transformation: 
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   803
\begin{center}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   804
\begin{tabular}{lcl}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   805
  $\textit{code}(\Empty)$ & $\dn$ & $[]$\\
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   806
  $\textit{code}(\Char\,c)$ & $\dn$ & $[]$\\
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   807
  $\textit{code}(\Left\,v)$ & $\dn$ & $\Z :: code(v)$\\
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   808
  $\textit{code}(\Right\,v)$ & $\dn$ & $\S :: code(v)$\\
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   809
  $\textit{code}(\Seq\,v_1\,v_2)$ & $\dn$ & $code(v_1) \,@\, code(v_2)$\\
68
3c73d95cbfef more upd
Chengsong
parents: 67
diff changeset
   810
  $\textit{code}(\Stars\,[])$ & $\dn$ & $[\Z]$\\
3c73d95cbfef more upd
Chengsong
parents: 67
diff changeset
   811
  $\textit{code}(\Stars\,(v\!::\!vs))$ & $\dn$ & $\S :: code(v) \;@\;
30
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   812
                                                 code(\Stars\,vs)$
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   813
\end{tabular}    
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   814
\end{center} 
70
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   815
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   816
Here code encodes a value into a bit-sequence by converting Left into
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   817
$\Z$, Right into $\S$, the start point of a non-empty star iteration
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   818
into $\S$, and the border where a local star terminates into $\Z$. This
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   819
conversion is apparently lossy, as it throws away the character
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   820
information, and does not decode the boundary between the two operands
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   821
of the sequence constructor. Moreover, with only the bitcode we cannot
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   822
even tell whether the $\S$s and $\Z$s are for $\Left/\Right$ or
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   823
$\Stars$. The reason for choosing this compact way of storing
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   824
information is that the relatively small size of bits can be easily
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   825
moved around. In order to recover the bitcode back into values, we will
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   826
need the regular expression as the extra information and decode it back
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   827
into value:\\
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   828
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   829
37
17d8e7599a01 new changes
Chengsong
parents: 36
diff changeset
   830
%\begin{definition}[Bitdecoding of Values]\mbox{}
36
Chengsong
parents: 35
diff changeset
   831
\begin{center}
Chengsong
parents: 35
diff changeset
   832
\begin{tabular}{@{}l@{\hspace{1mm}}c@{\hspace{1mm}}l@{}}
Chengsong
parents: 35
diff changeset
   833
  $\textit{decode}'\,bs\,(\ONE)$ & $\dn$ & $(\Empty, bs)$\\
Chengsong
parents: 35
diff changeset
   834
  $\textit{decode}'\,bs\,(c)$ & $\dn$ & $(\Char\,c, bs)$\\
Chengsong
parents: 35
diff changeset
   835
  $\textit{decode}'\,(\Z\!::\!bs)\;(r_1 + r_2)$ & $\dn$ &
Chengsong
parents: 35
diff changeset
   836
     $\textit{let}\,(v, bs_1) = \textit{decode}'\,bs\,r_1\;\textit{in}\;
Chengsong
parents: 35
diff changeset
   837
       (\Left\,v, bs_1)$\\
Chengsong
parents: 35
diff changeset
   838
  $\textit{decode}'\,(\S\!::\!bs)\;(r_1 + r_2)$ & $\dn$ &
Chengsong
parents: 35
diff changeset
   839
     $\textit{let}\,(v, bs_1) = \textit{decode}'\,bs\,r_2\;\textit{in}\;
Chengsong
parents: 35
diff changeset
   840
       (\Right\,v, bs_1)$\\                           
Chengsong
parents: 35
diff changeset
   841
  $\textit{decode}'\,bs\;(r_1\cdot r_2)$ & $\dn$ &
Chengsong
parents: 35
diff changeset
   842
        $\textit{let}\,(v_1, bs_1) = \textit{decode}'\,bs\,r_1\;\textit{in}$\\
Chengsong
parents: 35
diff changeset
   843
  & &   $\textit{let}\,(v_2, bs_2) = \textit{decode}'\,bs_1\,r_2$\\
Chengsong
parents: 35
diff changeset
   844
  & &   \hspace{35mm}$\textit{in}\;(\Seq\,v_1\,v_2, bs_2)$\\
Chengsong
parents: 35
diff changeset
   845
  $\textit{decode}'\,(\Z\!::\!bs)\,(r^*)$ & $\dn$ & $(\Stars\,[], bs)$\\
Chengsong
parents: 35
diff changeset
   846
  $\textit{decode}'\,(\S\!::\!bs)\,(r^*)$ & $\dn$ & 
Chengsong
parents: 35
diff changeset
   847
         $\textit{let}\,(v, bs_1) = \textit{decode}'\,bs\,r\;\textit{in}$\\
Chengsong
parents: 35
diff changeset
   848
  & &   $\textit{let}\,(\Stars\,vs, bs_2) = \textit{decode}'\,bs_1\,r^*$\\
Chengsong
parents: 35
diff changeset
   849
  & &   \hspace{35mm}$\textit{in}\;(\Stars\,v\!::\!vs, bs_2)$\bigskip\\
Chengsong
parents: 35
diff changeset
   850
  
Chengsong
parents: 35
diff changeset
   851
  $\textit{decode}\,bs\,r$ & $\dn$ &
Chengsong
parents: 35
diff changeset
   852
     $\textit{let}\,(v, bs') = \textit{decode}'\,bs\,r\;\textit{in}$\\
Chengsong
parents: 35
diff changeset
   853
  & & $\textit{if}\;bs' = []\;\textit{then}\;\textit{Some}\,v\;
Chengsong
parents: 35
diff changeset
   854
       \textit{else}\;\textit{None}$                       
Chengsong
parents: 35
diff changeset
   855
\end{tabular}    
Chengsong
parents: 35
diff changeset
   856
\end{center}    
37
17d8e7599a01 new changes
Chengsong
parents: 36
diff changeset
   857
%\end{definition}
30
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   858
71
0573615e41a3 new changes?
Chengsong
parents: 70
diff changeset
   859
Sulzmann and Lu's integrated the bitcodes into regular
0573615e41a3 new changes?
Chengsong
parents: 70
diff changeset
   860
expressions to create annotated regular expressions.
0573615e41a3 new changes?
Chengsong
parents: 70
diff changeset
   861
It is by attaching them to the head of every substructure of a
0573615e41a3 new changes?
Chengsong
parents: 70
diff changeset
   862
regular expression\cite{Sulzmann2014}. Annotated regular expressions
0573615e41a3 new changes?
Chengsong
parents: 70
diff changeset
   863
 are defined by the following
70
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   864
grammar:
43
Chengsong
parents: 42
diff changeset
   865
Chengsong
parents: 42
diff changeset
   866
\begin{center}
Chengsong
parents: 42
diff changeset
   867
\begin{tabular}{lcl}
Chengsong
parents: 42
diff changeset
   868
  $\textit{a}$ & $::=$  & $\textit{ZERO}$\\
Chengsong
parents: 42
diff changeset
   869
                  & $\mid$ & $\textit{ONE}\;\;bs$\\
Chengsong
parents: 42
diff changeset
   870
                  & $\mid$ & $\textit{CHAR}\;\;bs\,c$\\
72
83b021fc7d29 interesting?
Chengsong
parents: 71
diff changeset
   871
                  & $\mid$ & $\textit{ALT}\;\;bs\,a_1 \, a_2$\\
43
Chengsong
parents: 42
diff changeset
   872
                  & $\mid$ & $\textit{SEQ}\;\;bs\,a_1\,a_2$\\
Chengsong
parents: 42
diff changeset
   873
                  & $\mid$ & $\textit{STAR}\;\;bs\,a$
Chengsong
parents: 42
diff changeset
   874
\end{tabular}    
Chengsong
parents: 42
diff changeset
   875
\end{center}  
72
83b021fc7d29 interesting?
Chengsong
parents: 71
diff changeset
   876
%(in \textit{ALT})
43
Chengsong
parents: 42
diff changeset
   877
\noindent
72
83b021fc7d29 interesting?
Chengsong
parents: 71
diff changeset
   878
where $bs$ stands for bit-sequences, and $a$  for $\bold{a}$nnotated regular expressions. These bit-sequences encode
43
Chengsong
parents: 42
diff changeset
   879
information about the (POSIX) value that should be generated by the
Chengsong
parents: 42
diff changeset
   880
Sulzmann and Lu algorithm. 
Chengsong
parents: 42
diff changeset
   881
70
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   882
To do lexing using annotated regular expressions, we shall first
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   883
transform the usual (un-annotated) regular expressions into annotated
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   884
regular expressions. This operation is called \emph{internalisation} and
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   885
defined as follows:
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   886
37
17d8e7599a01 new changes
Chengsong
parents: 36
diff changeset
   887
%\begin{definition}
36
Chengsong
parents: 35
diff changeset
   888
\begin{center}
Chengsong
parents: 35
diff changeset
   889
\begin{tabular}{lcl}
Chengsong
parents: 35
diff changeset
   890
  $(\ZERO)^\uparrow$ & $\dn$ & $\textit{ZERO}$\\
Chengsong
parents: 35
diff changeset
   891
  $(\ONE)^\uparrow$ & $\dn$ & $\textit{ONE}\,[]$\\
Chengsong
parents: 35
diff changeset
   892
  $(c)^\uparrow$ & $\dn$ & $\textit{CHAR}\,[]\,c$\\
Chengsong
parents: 35
diff changeset
   893
  $(r_1 + r_2)^\uparrow$ & $\dn$ &
Chengsong
parents: 35
diff changeset
   894
         $\textit{ALT}\;[]\,(\textit{fuse}\,[\Z]\,r_1^\uparrow)\,
Chengsong
parents: 35
diff changeset
   895
                            (\textit{fuse}\,[\S]\,r_2^\uparrow)$\\
Chengsong
parents: 35
diff changeset
   896
  $(r_1\cdot r_2)^\uparrow$ & $\dn$ &
Chengsong
parents: 35
diff changeset
   897
         $\textit{SEQ}\;[]\,r_1^\uparrow\,r_2^\uparrow$\\
Chengsong
parents: 35
diff changeset
   898
  $(r^*)^\uparrow$ & $\dn$ &
Chengsong
parents: 35
diff changeset
   899
         $\textit{STAR}\;[]\,r^\uparrow$\\
Chengsong
parents: 35
diff changeset
   900
\end{tabular}    
Chengsong
parents: 35
diff changeset
   901
\end{center}    
37
17d8e7599a01 new changes
Chengsong
parents: 36
diff changeset
   902
%\end{definition}
44
4d674a971852 another changes. have written more. but havent typed them. tomorrow will continue.
Chengsong
parents: 43
diff changeset
   903
70
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   904
\noindent
72
83b021fc7d29 interesting?
Chengsong
parents: 71
diff changeset
   905
We use up arrows here to imply that the basic un-annotated regular expressions
83b021fc7d29 interesting?
Chengsong
parents: 71
diff changeset
   906
are "lifted up" into something slightly more complex.
83b021fc7d29 interesting?
Chengsong
parents: 71
diff changeset
   907
In the fourth clause, $\textit{fuse}$ is an auxiliary function that helps to attach bits to the
70
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   908
front of an annotated regular expression. Its definition is as follows:
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   909
44
4d674a971852 another changes. have written more. but havent typed them. tomorrow will continue.
Chengsong
parents: 43
diff changeset
   910
\begin{center}
4d674a971852 another changes. have written more. but havent typed them. tomorrow will continue.
Chengsong
parents: 43
diff changeset
   911
\begin{tabular}{lcl}
4d674a971852 another changes. have written more. but havent typed them. tomorrow will continue.
Chengsong
parents: 43
diff changeset
   912
  $\textit{fuse}\,bs\,(\textit{ZERO})$ & $\dn$ & $\textit{ZERO}$\\
4d674a971852 another changes. have written more. but havent typed them. tomorrow will continue.
Chengsong
parents: 43
diff changeset
   913
  $\textit{fuse}\,bs\,(\textit{ONE}\,bs')$ & $\dn$ &
4d674a971852 another changes. have written more. but havent typed them. tomorrow will continue.
Chengsong
parents: 43
diff changeset
   914
     $\textit{ONE}\,(bs\,@\,bs')$\\
4d674a971852 another changes. have written more. but havent typed them. tomorrow will continue.
Chengsong
parents: 43
diff changeset
   915
  $\textit{fuse}\,bs\,(\textit{CHAR}\,bs'\,c)$ & $\dn$ &
4d674a971852 another changes. have written more. but havent typed them. tomorrow will continue.
Chengsong
parents: 43
diff changeset
   916
     $\textit{CHAR}\,(bs\,@\,bs')\,c$\\
4d674a971852 another changes. have written more. but havent typed them. tomorrow will continue.
Chengsong
parents: 43
diff changeset
   917
  $\textit{fuse}\,bs\,(\textit{ALT}\,bs'\,a_1\,a_2)$ & $\dn$ &
4d674a971852 another changes. have written more. but havent typed them. tomorrow will continue.
Chengsong
parents: 43
diff changeset
   918
     $\textit{ALT}\,(bs\,@\,bs')\,a_1\,a_2$\\
4d674a971852 another changes. have written more. but havent typed them. tomorrow will continue.
Chengsong
parents: 43
diff changeset
   919
  $\textit{fuse}\,bs\,(\textit{SEQ}\,bs'\,a_1\,a_2)$ & $\dn$ &
4d674a971852 another changes. have written more. but havent typed them. tomorrow will continue.
Chengsong
parents: 43
diff changeset
   920
     $\textit{SEQ}\,(bs\,@\,bs')\,a_1\,a_2$\\
4d674a971852 another changes. have written more. but havent typed them. tomorrow will continue.
Chengsong
parents: 43
diff changeset
   921
  $\textit{fuse}\,bs\,(\textit{STAR}\,bs'\,a)$ & $\dn$ &
4d674a971852 another changes. have written more. but havent typed them. tomorrow will continue.
Chengsong
parents: 43
diff changeset
   922
     $\textit{STAR}\,(bs\,@\,bs')\,a$
4d674a971852 another changes. have written more. but havent typed them. tomorrow will continue.
Chengsong
parents: 43
diff changeset
   923
\end{tabular}    
4d674a971852 another changes. have written more. but havent typed them. tomorrow will continue.
Chengsong
parents: 43
diff changeset
   924
\end{center}  
4d674a971852 another changes. have written more. but havent typed them. tomorrow will continue.
Chengsong
parents: 43
diff changeset
   925
70
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   926
\noindent
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   927
After internalise we do successive derivative operations on the
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   928
 annotated regular expression. This derivative operation is the same as
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   929
 what we previously have for the simple regular expressions, except that
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   930
 we take special care of the bits :\\
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   931
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   932
 %\begin{definition}{bder}
36
Chengsong
parents: 35
diff changeset
   933
\begin{center}
Chengsong
parents: 35
diff changeset
   934
  \begin{tabular}{@{}lcl@{}}
Chengsong
parents: 35
diff changeset
   935
  $(\textit{ZERO})\backslash c$ & $\dn$ & $\textit{ZERO}$\\  
Chengsong
parents: 35
diff changeset
   936
  $(\textit{ONE}\;bs)\backslash c$ & $\dn$ & $\textit{ZERO}$\\  
Chengsong
parents: 35
diff changeset
   937
  $(\textit{CHAR}\;bs\,d)\backslash c$ & $\dn$ &
Chengsong
parents: 35
diff changeset
   938
        $\textit{if}\;c=d\; \;\textit{then}\;
Chengsong
parents: 35
diff changeset
   939
         \textit{ONE}\;bs\;\textit{else}\;\textit{ZERO}$\\  
Chengsong
parents: 35
diff changeset
   940
  $(\textit{ALT}\;bs\,a_1\,a_2)\backslash c$ & $\dn$ &
Chengsong
parents: 35
diff changeset
   941
        $\textit{ALT}\,bs\,(a_1\backslash c)\,(a_2\backslash c)$\\
Chengsong
parents: 35
diff changeset
   942
  $(\textit{SEQ}\;bs\,a_1\,a_2)\backslash c$ & $\dn$ &
Chengsong
parents: 35
diff changeset
   943
     $\textit{if}\;\textit{bnullable}\,a_1$\\
Chengsong
parents: 35
diff changeset
   944
  & &$\textit{then}\;\textit{ALT}\,bs\,(\textit{SEQ}\,[]\,(a_1\backslash c)\,a_2)$\\
Chengsong
parents: 35
diff changeset
   945
  & &$\phantom{\textit{then}\;\textit{ALT}\,bs\,}(\textit{fuse}\,(\textit{bmkeps}\,a_1)\,(a_2\backslash c))$\\
Chengsong
parents: 35
diff changeset
   946
  & &$\textit{else}\;\textit{SEQ}\,bs\,(a_1\backslash c)\,a_2$\\
Chengsong
parents: 35
diff changeset
   947
  $(\textit{STAR}\,bs\,a)\backslash c$ & $\dn$ &
Chengsong
parents: 35
diff changeset
   948
      $\textit{SEQ}\;bs\,(\textit{fuse}\, [\Z] (r\backslash c))\,
Chengsong
parents: 35
diff changeset
   949
       (\textit{STAR}\,[]\,r)$
Chengsong
parents: 35
diff changeset
   950
\end{tabular}    
Chengsong
parents: 35
diff changeset
   951
\end{center}    
37
17d8e7599a01 new changes
Chengsong
parents: 36
diff changeset
   952
%\end{definition}
74
9e791ef6022f just a merge - no changes
Christian Urban <urbanc@in.tum.de>
parents: 72
diff changeset
   953
9e791ef6022f just a merge - no changes
Christian Urban <urbanc@in.tum.de>
parents: 72
diff changeset
   954
For instance, when we unfold $STAR \; bs \; a$ into a sequence, we
9e791ef6022f just a merge - no changes
Christian Urban <urbanc@in.tum.de>
parents: 72
diff changeset
   955
attach an additional bit Z to the front of $r \backslash c$ to indicate
9e791ef6022f just a merge - no changes
Christian Urban <urbanc@in.tum.de>
parents: 72
diff changeset
   956
that there is one more star iteration. The other example, the $SEQ$
9e791ef6022f just a merge - no changes
Christian Urban <urbanc@in.tum.de>
parents: 72
diff changeset
   957
clause is more subtle-- when $a_1$ is $bnullable$(here bnullable is
9e791ef6022f just a merge - no changes
Christian Urban <urbanc@in.tum.de>
parents: 72
diff changeset
   958
exactly the same as nullable, except that it is for annotated regular
9e791ef6022f just a merge - no changes
Christian Urban <urbanc@in.tum.de>
parents: 72
diff changeset
   959
expressions, therefore we omit the definition). Assume that $bmkeps$
9e791ef6022f just a merge - no changes
Christian Urban <urbanc@in.tum.de>
parents: 72
diff changeset
   960
correctly extracts the bitcode for how $a_1$ matches the string prior to
9e791ef6022f just a merge - no changes
Christian Urban <urbanc@in.tum.de>
parents: 72
diff changeset
   961
character c(more on this later), then the right branch of $ALTS$, which
9e791ef6022f just a merge - no changes
Christian Urban <urbanc@in.tum.de>
parents: 72
diff changeset
   962
is $fuse \; bmkeps \;  a_1 (a_2 \backslash c)$ will collapse the regular
9e791ef6022f just a merge - no changes
Christian Urban <urbanc@in.tum.de>
parents: 72
diff changeset
   963
expression $a_1$(as it has already been fully matched) and store the
9e791ef6022f just a merge - no changes
Christian Urban <urbanc@in.tum.de>
parents: 72
diff changeset
   964
parsing information at the head of the regular expression $a_2
9e791ef6022f just a merge - no changes
Christian Urban <urbanc@in.tum.de>
parents: 72
diff changeset
   965
\backslash c$ by fusing to it. The bitsequence $bs$, which was initially
9e791ef6022f just a merge - no changes
Christian Urban <urbanc@in.tum.de>
parents: 72
diff changeset
   966
attached to the head of $SEQ$, has now been elevated to the top-level of
9e791ef6022f just a merge - no changes
Christian Urban <urbanc@in.tum.de>
parents: 72
diff changeset
   967
ALT, as this information will be needed whichever way the $SEQ$ is
9e791ef6022f just a merge - no changes
Christian Urban <urbanc@in.tum.de>
parents: 72
diff changeset
   968
matched--no matter whether c belongs to $a_1$ or $ a_2$. After carefully
9e791ef6022f just a merge - no changes
Christian Urban <urbanc@in.tum.de>
parents: 72
diff changeset
   969
doing these derivatives and maintaining all the parsing information, we
9e791ef6022f just a merge - no changes
Christian Urban <urbanc@in.tum.de>
parents: 72
diff changeset
   970
complete the parsing by collecting the bits using a special $mkeps$
9e791ef6022f just a merge - no changes
Christian Urban <urbanc@in.tum.de>
parents: 72
diff changeset
   971
function for annotated regular expressions--$bmkeps$:
44
4d674a971852 another changes. have written more. but havent typed them. tomorrow will continue.
Chengsong
parents: 43
diff changeset
   972
4d674a971852 another changes. have written more. but havent typed them. tomorrow will continue.
Chengsong
parents: 43
diff changeset
   973
37
17d8e7599a01 new changes
Chengsong
parents: 36
diff changeset
   974
%\begin{definition}[\textit{bmkeps}]\mbox{}
36
Chengsong
parents: 35
diff changeset
   975
\begin{center}
Chengsong
parents: 35
diff changeset
   976
\begin{tabular}{lcl}
Chengsong
parents: 35
diff changeset
   977
  $\textit{bmkeps}\,(\textit{ONE}\,bs)$ & $\dn$ & $bs$\\
Chengsong
parents: 35
diff changeset
   978
  $\textit{bmkeps}\,(\textit{ALT}\,bs\,a_1\,a_2)$ & $\dn$ &
Chengsong
parents: 35
diff changeset
   979
     $\textit{if}\;\textit{bnullable}\,a_1$\\
Chengsong
parents: 35
diff changeset
   980
  & &$\textit{then}\;bs\,@\,\textit{bmkeps}\,a_1$\\
Chengsong
parents: 35
diff changeset
   981
  & &$\textit{else}\;bs\,@\,\textit{bmkeps}\,a_2$\\
Chengsong
parents: 35
diff changeset
   982
  $\textit{bmkeps}\,(\textit{SEQ}\,bs\,a_1\,a_2)$ & $\dn$ &
Chengsong
parents: 35
diff changeset
   983
     $bs \,@\,\textit{bmkeps}\,a_1\,@\, \textit{bmkeps}\,a_2$\\
Chengsong
parents: 35
diff changeset
   984
  $\textit{bmkeps}\,(\textit{STAR}\,bs\,a)$ & $\dn$ &
Chengsong
parents: 35
diff changeset
   985
     $bs \,@\, [\S]$
Chengsong
parents: 35
diff changeset
   986
\end{tabular}    
Chengsong
parents: 35
diff changeset
   987
\end{center}    
37
17d8e7599a01 new changes
Chengsong
parents: 36
diff changeset
   988
%\end{definition}
70
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   989
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   990
\noindent
44
4d674a971852 another changes. have written more. but havent typed them. tomorrow will continue.
Chengsong
parents: 43
diff changeset
   991
This function completes the parse tree information by 
45
60cb82639691 spell check
Christian Urban <urbanc@in.tum.de>
parents: 44
diff changeset
   992
travelling along the path on the regular expression that corresponds to a POSIX value snd collect all the bits, and
72
83b021fc7d29 interesting?
Chengsong
parents: 71
diff changeset
   993
using S to indicate the end of star iterations. If we take the bits produced by $bmkeps$ and decode it, 
44
4d674a971852 another changes. have written more. but havent typed them. tomorrow will continue.
Chengsong
parents: 43
diff changeset
   994
we get the parse tree we need, the working flow looks like this:\\
37
17d8e7599a01 new changes
Chengsong
parents: 36
diff changeset
   995
\begin{center}
17d8e7599a01 new changes
Chengsong
parents: 36
diff changeset
   996
\begin{tabular}{lcl}
17d8e7599a01 new changes
Chengsong
parents: 36
diff changeset
   997
  $\textit{blexer}\;r\,s$ & $\dn$ &
17d8e7599a01 new changes
Chengsong
parents: 36
diff changeset
   998
      $\textit{let}\;a = (r^\uparrow)\backslash s\;\textit{in}$\\                
17d8e7599a01 new changes
Chengsong
parents: 36
diff changeset
   999
  & & $\;\;\textit{if}\; \textit{bnullable}(a)$\\
17d8e7599a01 new changes
Chengsong
parents: 36
diff changeset
  1000
  & & $\;\;\textit{then}\;\textit{decode}\,(\textit{bmkeps}\,a)\,r$\\
17d8e7599a01 new changes
Chengsong
parents: 36
diff changeset
  1001
  & & $\;\;\textit{else}\;\textit{None}$
17d8e7599a01 new changes
Chengsong
parents: 36
diff changeset
  1002
\end{tabular}
17d8e7599a01 new changes
Chengsong
parents: 36
diff changeset
  1003
\end{center}
53
3ec403f650a8 readable version
Chengsong
parents: 52
diff changeset
  1004
Here $(r^\uparrow)\backslash s$ is similar to what we have previously defined for 
3ec403f650a8 readable version
Chengsong
parents: 52
diff changeset
  1005
$r\backslash s$.
30
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
  1006
71
0573615e41a3 new changes?
Chengsong
parents: 70
diff changeset
  1007
The main point of the bit-sequences and annotated regular expressions
30
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
  1008
is that we can apply rather aggressive (in terms of size)
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
  1009
simplification rules in order to keep derivatives small.  
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
  1010
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
  1011
We have
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
  1012
developed such ``aggressive'' simplification rules and generated test
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
  1013
data that show that the expected bound can be achieved. Obviously we
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
  1014
could only partially cover  the search space as there are infinitely
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
  1015
many regular expressions and strings. One modification we introduced
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
  1016
is to allow a list of annotated regular expressions in the
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
  1017
\textit{ALTS} constructor. This allows us to not just delete
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
  1018
unnecessary $\ZERO$s and $\ONE$s from regular expressions, but also
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
  1019
unnecessary ``copies'' of regular expressions (very similar to
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
  1020
simplifying $r + r$ to just $r$, but in a more general
35
f70e9ab4e680 psuedocode added
Chengsong
parents: 34
diff changeset
  1021
setting). 
49
d256aabe88f3 still wont comiple hhh
Chengsong
parents: 48
diff changeset
  1022
Another modification is that we use simplification rules
d256aabe88f3 still wont comiple hhh
Chengsong
parents: 48
diff changeset
  1023
inspired by Antimirov's work on partial derivatives. They maintain the
d256aabe88f3 still wont comiple hhh
Chengsong
parents: 48
diff changeset
  1024
idea that only the first ``copy'' of a regular expression in an
d256aabe88f3 still wont comiple hhh
Chengsong
parents: 48
diff changeset
  1025
alternative contributes to the calculation of a POSIX value. All
d256aabe88f3 still wont comiple hhh
Chengsong
parents: 48
diff changeset
  1026
subsequent copies can be pruned from the regular expression.
d256aabe88f3 still wont comiple hhh
Chengsong
parents: 48
diff changeset
  1027
52
25bbbb8b0e90 just in case of some accidents from erasing my work
Chengsong
parents: 51
diff changeset
  1028
A recursive definition of simplification function that looks similar to scala code is given below:\\
25bbbb8b0e90 just in case of some accidents from erasing my work
Chengsong
parents: 51
diff changeset
  1029
\begin{center}
25bbbb8b0e90 just in case of some accidents from erasing my work
Chengsong
parents: 51
diff changeset
  1030
  \begin{tabular}{@{}lcl@{}}
25bbbb8b0e90 just in case of some accidents from erasing my work
Chengsong
parents: 51
diff changeset
  1031
  $\textit{simp} \; a$ & $\dn$ & $\textit{a} \; \textit{if} \; a  =  (\textit{ONE} \; bs) \; or\; (\textit{CHAR} \, bs \; c) \; or\; (\textit{STAR}\; bs\; a_1)$\\  
25bbbb8b0e90 just in case of some accidents from erasing my work
Chengsong
parents: 51
diff changeset
  1032
  
25bbbb8b0e90 just in case of some accidents from erasing my work
Chengsong
parents: 51
diff changeset
  1033
  $\textit{simp} \; \textit{SEQ}\;bs\,a_1\,a_2$ & $\dn$ & $ (\textit{simp} \; a_1, \textit{simp}  \; a_2) \; \textit{match} $ \\
25bbbb8b0e90 just in case of some accidents from erasing my work
Chengsong
parents: 51
diff changeset
  1034
  &&$\textit{case} \; (0, \_) \Rightarrow  0$ \\
25bbbb8b0e90 just in case of some accidents from erasing my work
Chengsong
parents: 51
diff changeset
  1035
   &&$ \textit{case} \; (\_, 0) \Rightarrow  0$ \\
25bbbb8b0e90 just in case of some accidents from erasing my work
Chengsong
parents: 51
diff changeset
  1036
   &&$ \textit{case} \;  (1, a_2') \Rightarrow  \textit{fuse} \; bs \;  a_2'$ \\
25bbbb8b0e90 just in case of some accidents from erasing my work
Chengsong
parents: 51
diff changeset
  1037
   &&$ \textit{case} \; (a_1', 1) \Rightarrow  \textit{fuse} \; bs \;  a_1'$ \\
25bbbb8b0e90 just in case of some accidents from erasing my work
Chengsong
parents: 51
diff changeset
  1038
   &&$ \textit{case} \; (a_1', a_2') \Rightarrow  \textit{SEQ} \; bs \; a_1' \;  a_2'$ \\
25bbbb8b0e90 just in case of some accidents from erasing my work
Chengsong
parents: 51
diff changeset
  1039
72
83b021fc7d29 interesting?
Chengsong
parents: 71
diff changeset
  1040
  $\textit{simp} \; \textit{ALTS}\;bs\,as$ & $\dn$ & $\textit{ distinct}( \textit{flatten} ( \textit{map simp as})) \; \textit{match} $ \\
52
25bbbb8b0e90 just in case of some accidents from erasing my work
Chengsong
parents: 51
diff changeset
  1041
  &&$\textit{case} \; [] \Rightarrow  0$ \\
25bbbb8b0e90 just in case of some accidents from erasing my work
Chengsong
parents: 51
diff changeset
  1042
   &&$ \textit{case} \; a :: [] \Rightarrow  \textit{fuse bs a}$ \\
25bbbb8b0e90 just in case of some accidents from erasing my work
Chengsong
parents: 51
diff changeset
  1043
   &&$ \textit{case} \;  as' \Rightarrow  \textit{ALT bs as'}$ 
25bbbb8b0e90 just in case of some accidents from erasing my work
Chengsong
parents: 51
diff changeset
  1044
\end{tabular}    
25bbbb8b0e90 just in case of some accidents from erasing my work
Chengsong
parents: 51
diff changeset
  1045
\end{center}    
47
d2a7e87ea6e1 will not compile, just text
Chengsong
parents: 46
diff changeset
  1046
d2a7e87ea6e1 will not compile, just text
Chengsong
parents: 46
diff changeset
  1047
The simplification does a pattern matching on the regular expression. When it detected that
72
83b021fc7d29 interesting?
Chengsong
parents: 71
diff changeset
  1048
the regular expression is an alternative or sequence, 
83b021fc7d29 interesting?
Chengsong
parents: 71
diff changeset
  1049
it will try to simplify its children regular expressions
83b021fc7d29 interesting?
Chengsong
parents: 71
diff changeset
  1050
recursively and then see if one of the children turn 
83b021fc7d29 interesting?
Chengsong
parents: 71
diff changeset
  1051
into $\ZERO$ or $\ONE$, which might trigger further simplification
83b021fc7d29 interesting?
Chengsong
parents: 71
diff changeset
  1052
 at the current level. The most involved part is the $\textit{ALTS}$
83b021fc7d29 interesting?
Chengsong
parents: 71
diff changeset
  1053
  clause, where we use two auxiliary functions 
83b021fc7d29 interesting?
Chengsong
parents: 71
diff changeset
  1054
 flatten and distinct to open up nested $\textit{ALTS}$ and 
83b021fc7d29 interesting?
Chengsong
parents: 71
diff changeset
  1055
 reduce as many duplicates as possible.
83b021fc7d29 interesting?
Chengsong
parents: 71
diff changeset
  1056
 Function distinct  keeps the first occurring copy only and 
83b021fc7d29 interesting?
Chengsong
parents: 71
diff changeset
  1057
 remove all later ones when detected duplicates.
83b021fc7d29 interesting?
Chengsong
parents: 71
diff changeset
  1058
 Function flatten opens up nested \textit{ALT}. Its recursive
83b021fc7d29 interesting?
Chengsong
parents: 71
diff changeset
  1059
  definition is given below:
53
3ec403f650a8 readable version
Chengsong
parents: 52
diff changeset
  1060
 \begin{center}
3ec403f650a8 readable version
Chengsong
parents: 52
diff changeset
  1061
  \begin{tabular}{@{}lcl@{}}
70
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
  1062
  $\textit{flatten} \; (\textit{ALT}\;bs\,as) :: as'$ & $\dn$ & $(\textit{map} \;
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
  1063
     (\textit{fuse}\;bs)\; \textit{as}) \; @ \; \textit{flatten} \; as' $ \\
53
3ec403f650a8 readable version
Chengsong
parents: 52
diff changeset
  1064
  $\textit{flatten} \; \textit{ZERO} :: as'$ & $\dn$ & $ \textit{flatten} \;  as' $ \\
70
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
  1065
    $\textit{flatten} \; a :: as'$ & $\dn$ & $a :: \textit{flatten} \; as'$ \quad(otherwise) 
53
3ec403f650a8 readable version
Chengsong
parents: 52
diff changeset
  1066
\end{tabular}    
3ec403f650a8 readable version
Chengsong
parents: 52
diff changeset
  1067
\end{center}  
3ec403f650a8 readable version
Chengsong
parents: 52
diff changeset
  1068
70
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
  1069
\noindent
71
0573615e41a3 new changes?
Chengsong
parents: 70
diff changeset
  1070
 Here flatten behaves like the traditional functional programming flatten function, except that it also removes $\ZERO$s.
0573615e41a3 new changes?
Chengsong
parents: 70
diff changeset
  1071
 What it does is basically removing parentheses like changing $a+(b+c)$ into $a+b+c$.
47
d2a7e87ea6e1 will not compile, just text
Chengsong
parents: 46
diff changeset
  1072
53
3ec403f650a8 readable version
Chengsong
parents: 52
diff changeset
  1073
Suppose we apply simplification after each derivative step,
3ec403f650a8 readable version
Chengsong
parents: 52
diff changeset
  1074
and view these two operations as an atomic one: $a \backslash_{simp} c \dn \textit{simp}(a \backslash c)$.
3ec403f650a8 readable version
Chengsong
parents: 52
diff changeset
  1075
Then we can use the previous natural extension from derivative w.r.t   character to derivative w.r.t string:
3ec403f650a8 readable version
Chengsong
parents: 52
diff changeset
  1076
3ec403f650a8 readable version
Chengsong
parents: 52
diff changeset
  1077
\begin{center}
3ec403f650a8 readable version
Chengsong
parents: 52
diff changeset
  1078
\begin{tabular}{lcl}
3ec403f650a8 readable version
Chengsong
parents: 52
diff changeset
  1079
$r \backslash_{simp} (c\!::\!s) $ & $\dn$ & $(r \backslash_{simp} c) \backslash_{simp} s$ \\
3ec403f650a8 readable version
Chengsong
parents: 52
diff changeset
  1080
$r \backslash [\,] $ & $\dn$ & $r$
3ec403f650a8 readable version
Chengsong
parents: 52
diff changeset
  1081
\end{tabular}
3ec403f650a8 readable version
Chengsong
parents: 52
diff changeset
  1082
\end{center}
3ec403f650a8 readable version
Chengsong
parents: 52
diff changeset
  1083
3ec403f650a8 readable version
Chengsong
parents: 52
diff changeset
  1084
 we get an optimized version of the algorithm:
3ec403f650a8 readable version
Chengsong
parents: 52
diff changeset
  1085
\begin{center}
3ec403f650a8 readable version
Chengsong
parents: 52
diff changeset
  1086
\begin{tabular}{lcl}
3ec403f650a8 readable version
Chengsong
parents: 52
diff changeset
  1087
  $\textit{blexer\_simp}\;r\,s$ & $\dn$ &
3ec403f650a8 readable version
Chengsong
parents: 52
diff changeset
  1088
      $\textit{let}\;a = (r^\uparrow)\backslash_{simp} s\;\textit{in}$\\                
3ec403f650a8 readable version
Chengsong
parents: 52
diff changeset
  1089
  & & $\;\;\textit{if}\; \textit{bnullable}(a)$\\
3ec403f650a8 readable version
Chengsong
parents: 52
diff changeset
  1090
  & & $\;\;\textit{then}\;\textit{decode}\,(\textit{bmkeps}\,a)\,r$\\
3ec403f650a8 readable version
Chengsong
parents: 52
diff changeset
  1091
  & & $\;\;\textit{else}\;\textit{None}$
3ec403f650a8 readable version
Chengsong
parents: 52
diff changeset
  1092
\end{tabular}
3ec403f650a8 readable version
Chengsong
parents: 52
diff changeset
  1093
\end{center}
48
bbefcf7351f2 still will not compile
Chengsong
parents: 47
diff changeset
  1094
bbefcf7351f2 still will not compile
Chengsong
parents: 47
diff changeset
  1095
This algorithm effectively keeps the regular expression size small, for example,
bbefcf7351f2 still will not compile
Chengsong
parents: 47
diff changeset
  1096
with this simplification our previous $(a + aa)^*$ example's 8000 nodes will be reduced to only 6 and stay constant, however long the input string is.
35
f70e9ab4e680 psuedocode added
Chengsong
parents: 34
diff changeset
  1097
30
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
  1098
35
f70e9ab4e680 psuedocode added
Chengsong
parents: 34
diff changeset
  1099
70
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
  1100
\section{Current Work}
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
  1101
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
  1102
We are currently engaged in two tasks related to this algorithm. 
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
  1103
72
83b021fc7d29 interesting?
Chengsong
parents: 71
diff changeset
  1104
49
d256aabe88f3 still wont comiple hhh
Chengsong
parents: 48
diff changeset
  1105
The first one is proving that our simplification rules
30
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
  1106
actually do not affect the POSIX value that should be generated by the
49
d256aabe88f3 still wont comiple hhh
Chengsong
parents: 48
diff changeset
  1107
algorithm according to the specification of a POSIX value
d256aabe88f3 still wont comiple hhh
Chengsong
parents: 48
diff changeset
  1108
 and furthermore obtain a much
d256aabe88f3 still wont comiple hhh
Chengsong
parents: 48
diff changeset
  1109
tighter bound on the sizes of derivatives. The result is that our
d256aabe88f3 still wont comiple hhh
Chengsong
parents: 48
diff changeset
  1110
algorithm should be correct and faster on all inputs.  The original
d256aabe88f3 still wont comiple hhh
Chengsong
parents: 48
diff changeset
  1111
blow-up, as observed in JavaScript, Python and Java, would be excluded
d256aabe88f3 still wont comiple hhh
Chengsong
parents: 48
diff changeset
  1112
from happening in our algorithm.For
30
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
  1113
this proof we use the theorem prover Isabelle. Once completed, this
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
  1114
result will advance the state-of-the-art: Sulzmann and Lu wrote in
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
  1115
their paper \cite{Sulzmann2014} about the bitcoded ``incremental
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
  1116
parsing method'' (that is the matching algorithm outlined in this
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
  1117
section):
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
  1118
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
  1119
\begin{quote}\it
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
  1120
  ``Correctness Claim: We further claim that the incremental parsing
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
  1121
  method in Figure~5 in combination with the simplification steps in
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
  1122
  Figure 6 yields POSIX parse trees. We have tested this claim
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
  1123
  extensively by using the method in Figure~3 as a reference but yet
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
  1124
  have to work out all proof details.''
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
  1125
\end{quote}  
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
  1126
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
  1127
\noindent
74
9e791ef6022f just a merge - no changes
Christian Urban <urbanc@in.tum.de>
parents: 72
diff changeset
  1128
We would settle the correctness claim. It is relatively straightforward
9e791ef6022f just a merge - no changes
Christian Urban <urbanc@in.tum.de>
parents: 72
diff changeset
  1129
to establish that after one simplification step, the part of a nullable
9e791ef6022f just a merge - no changes
Christian Urban <urbanc@in.tum.de>
parents: 72
diff changeset
  1130
derivative that corresponds to a POSIX value remains intact and can
9e791ef6022f just a merge - no changes
Christian Urban <urbanc@in.tum.de>
parents: 72
diff changeset
  1131
still be collected, in other words,
9e791ef6022f just a merge - no changes
Christian Urban <urbanc@in.tum.de>
parents: 72
diff changeset
  1132
71
0573615e41a3 new changes?
Chengsong
parents: 70
diff changeset
  1133
\begin{center}
0573615e41a3 new changes?
Chengsong
parents: 70
diff changeset
  1134
$\textit{bmkeps} \; r = \textit{bmkeps} \; \textit{simp} \; r\;( r\; \textit{nullable})$
0573615e41a3 new changes?
Chengsong
parents: 70
diff changeset
  1135
\end{center}
74
9e791ef6022f just a merge - no changes
Christian Urban <urbanc@in.tum.de>
parents: 72
diff changeset
  1136
9e791ef6022f just a merge - no changes
Christian Urban <urbanc@in.tum.de>
parents: 72
diff changeset
  1137
\noindent
9e791ef6022f just a merge - no changes
Christian Urban <urbanc@in.tum.de>
parents: 72
diff changeset
  1138
as this basically comes down to proving actions like removing the
9e791ef6022f just a merge - no changes
Christian Urban <urbanc@in.tum.de>
parents: 72
diff changeset
  1139
additional $r$ in $r+r$  does not delete important POSIX information in
9e791ef6022f just a merge - no changes
Christian Urban <urbanc@in.tum.de>
parents: 72
diff changeset
  1140
a regular expression. The hardcore of this problem is to prove that
9e791ef6022f just a merge - no changes
Christian Urban <urbanc@in.tum.de>
parents: 72
diff changeset
  1141
71
0573615e41a3 new changes?
Chengsong
parents: 70
diff changeset
  1142
\begin{center}
0573615e41a3 new changes?
Chengsong
parents: 70
diff changeset
  1143
$\textit{bmkeps} \; \textit{blexer}\_{simp} \; r = \textit{bmkeps} \; \textit{blexer} \; \textit{simp} \; r$
0573615e41a3 new changes?
Chengsong
parents: 70
diff changeset
  1144
\end{center}
74
9e791ef6022f just a merge - no changes
Christian Urban <urbanc@in.tum.de>
parents: 72
diff changeset
  1145
9e791ef6022f just a merge - no changes
Christian Urban <urbanc@in.tum.de>
parents: 72
diff changeset
  1146
\noindent
71
0573615e41a3 new changes?
Chengsong
parents: 70
diff changeset
  1147
That is, if we do derivative on regular expression r and the simplified version, 
0573615e41a3 new changes?
Chengsong
parents: 70
diff changeset
  1148
they can still provide the same POSIX value if there is one . 
0573615e41a3 new changes?
Chengsong
parents: 70
diff changeset
  1149
This is not as straightforward as the previous proposition, as the two regular expressions $r$ and $\textit{simp}\; r$
0573615e41a3 new changes?
Chengsong
parents: 70
diff changeset
  1150
  might become very different regular expressions after repeated application of $\textit{simp}$ and derivative.
0573615e41a3 new changes?
Chengsong
parents: 70
diff changeset
  1151
The crucial point is to find the indispensable information of 
0573615e41a3 new changes?
Chengsong
parents: 70
diff changeset
  1152
a regular expression and how it is kept intact during simplification so that it performs 
0573615e41a3 new changes?
Chengsong
parents: 70
diff changeset
  1153
as good as a regular expression that has not been simplified in the subsequent derivative operations.
0573615e41a3 new changes?
Chengsong
parents: 70
diff changeset
  1154
To aid this, we use the helping function retrieve described by Sulzmann and Lu:
49
d256aabe88f3 still wont comiple hhh
Chengsong
parents: 48
diff changeset
  1155
\\definition of retrieve\\
72
83b021fc7d29 interesting?
Chengsong
parents: 71
diff changeset
  1156
 This function assembled the bitcode that corresponds to a parse tree for how the current 
71
0573615e41a3 new changes?
Chengsong
parents: 70
diff changeset
  1157
 derivative matches the suffix of the string(the characters that have not yet appeared, but is stored in the value).
72
83b021fc7d29 interesting?
Chengsong
parents: 71
diff changeset
  1158
 Sulzmann and Lu used this to connect the bitcoded algorithm to the older algorithm by the following equation:
83b021fc7d29 interesting?
Chengsong
parents: 71
diff changeset
  1159
 \begin{center}
83b021fc7d29 interesting?
Chengsong
parents: 71
diff changeset
  1160
 $inj \;a\; c \; v = \textit{decode} \; (\textit{retrieve}\; ((\textit{internalise}\; r)\backslash_{simp} c) v)$
83b021fc7d29 interesting?
Chengsong
parents: 71
diff changeset
  1161
 \end{center}
83b021fc7d29 interesting?
Chengsong
parents: 71
diff changeset
  1162
 A little fact that needs to be stated to help comprehension:
83b021fc7d29 interesting?
Chengsong
parents: 71
diff changeset
  1163
 \begin{center}
83b021fc7d29 interesting?
Chengsong
parents: 71
diff changeset
  1164
 $r^\uparrow = a$($a$ stands for $\textit{annotated}).$
83b021fc7d29 interesting?
Chengsong
parents: 71
diff changeset
  1165
 \end{center}
83b021fc7d29 interesting?
Chengsong
parents: 71
diff changeset
  1166
 Ausaf and Urban also used this fact to prove  the correctness of bitcoded algorithm without simplification.
50
866eda9ba66a now will compile
Chengsong
parents: 49
diff changeset
  1167
 Our purpose of using this, however, is try to establish \\
53
3ec403f650a8 readable version
Chengsong
parents: 52
diff changeset
  1168
$ \textit{retrieve} \; a \; v \;=\; \textit{retrieve}  \; \textit{simp}(a) \; v'.$\\
3ec403f650a8 readable version
Chengsong
parents: 52
diff changeset
  1169
 The idea is that using $v'$,
71
0573615e41a3 new changes?
Chengsong
parents: 70
diff changeset
  1170
  a simplified version of $v$ that possibly had gone through the same simplification step as $\textit{simp}(a)$ we are still  able to extract the bit-sequence that gives the same parsing information as the unsimplified one.
53
3ec403f650a8 readable version
Chengsong
parents: 52
diff changeset
  1171
 After establishing this, we might be able to finally bridge the gap of proving\\
3ec403f650a8 readable version
Chengsong
parents: 52
diff changeset
  1172
 $\textit{retrieve} \; r   \backslash  s \; v = \;\textit{retrieve} \; \textit{simp}(r)  \backslash  s \; v'$\\
3ec403f650a8 readable version
Chengsong
parents: 52
diff changeset
  1173
 and subsequently\\
3ec403f650a8 readable version
Chengsong
parents: 52
diff changeset
  1174
 $\textit{retrieve} \; r \backslash  s \; v\; = \; \textit{retrieve} \; r  \backslash_{simp}   s \; v'$.\\
58
f0360e17080e proofread
Christian Urban <urbanc@in.tum.de>
parents: 57
diff changeset
  1175
 This proves that our simplified version of regular expression still contains all the bitcodes needed.
49
d256aabe88f3 still wont comiple hhh
Chengsong
parents: 48
diff changeset
  1176
72
83b021fc7d29 interesting?
Chengsong
parents: 71
diff changeset
  1177
70
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
  1178
The second task is to speed up the more aggressive simplification.
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
  1179
Currently it is slower than a naive simplification(the naive version as
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
  1180
implemented in ADU of course can explode in some cases). So it needs to
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
  1181
be explored how to make it faster. Our possibility would be to explore
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
  1182
again the connection to DFAs. This is very much work in progress.
30
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
  1183
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
  1184
\section{Conclusion}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
  1185
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
  1186
In this PhD-project we are interested in fast algorithms for regular
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
  1187
expression matching. While this seems to be a ``settled'' area, in
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
  1188
fact interesting research questions are popping up as soon as one steps
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
  1189
outside the classic automata theory (for example in terms of what kind
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
  1190
of regular expressions are supported). The reason why it is
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
  1191
interesting for us to look at the derivative approach introduced by
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
  1192
Brzozowski for regular expression matching, and then much further
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
  1193
developed by Sulzmann and Lu, is that derivatives can elegantly deal
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
  1194
with some of the regular expressions that are of interest in ``real
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
  1195
life''. This includes the not-regular expression, written $\neg\,r$
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
  1196
(that is all strings that are not recognised by $r$), but also bounded
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
  1197
regular expressions such as $r^{\{n\}}$ and $r^{\{n..m\}}$). There is
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
  1198
also hope that the derivatives can provide another angle for how to
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
  1199
deal more efficiently with back-references, which are one of the
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
  1200
reasons why regular expression engines in JavaScript, Python and Java
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
  1201
choose to not implement the classic automata approach of transforming
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
  1202
regular expressions into NFAs and then DFAs---because we simply do not
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
  1203
know how such back-references can be represented by DFAs.
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
  1204
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
  1205
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
  1206
\bibliographystyle{plain}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
  1207
\bibliography{root}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
  1208
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
  1209
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
  1210
\end{document}