ninems/ninems.tex
author Christian Urban <urbanc@in.tum.de>
Thu, 18 Jul 2019 15:06:50 +0100
changeset 77 058133a9ffe0
parent 76 f575cf219377
child 79 481c8000de6d
permissions -rw-r--r--
proof-read
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
77
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
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
77
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   184
exhibit this exponential behaviour.  But unfortunately, such regular
64
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 
77
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   207
home page of Stack Exchange to respond not fast enough to
75
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 
77
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   210
requests. This made the whole site become unavailable.
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   211
Another very recent example is a global outage of all Cloudflare servers
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   212
on 2 July 2019. A poorly written regular expression exhibited
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   213
exponential behaviour and exhausted CPUs that serve HTTP traffic.
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   214
Although the outage had several causes, at the heart was a regular
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   215
expression that was used to monitor network
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   216
traffic.\footnote{\url{https://blog.cloudflare.com/details-of-the-cloudflare-outage-on-july-2-2019/}}
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   217
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   218
The underlying problem is that many ``real life'' regular expression
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   219
matching engines do not use DFAs for matching. This is because they
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   220
support regular expressions that are not covered by the classical
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   221
automata theory, and in this more general setting there are quite a few
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   222
research questions still unanswered and fast algorithms still need to be
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   223
developed (for example how to treat bounded repetitions, negation and
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   224
back-references efficiently).
64
afd0d702a4fe some changes
Chengsong
parents: 63
diff changeset
   225
%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
   226
%how do they avoid dfas exponential states if they use them for fast matching?
77
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   227
30
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   228
There is also another under-researched problem to do with regular
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   229
expressions and lexing, i.e.~the process of breaking up strings into
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   230
sequences of tokens according to some regular expressions. In this
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   231
setting one is not just interested in whether or not a regular
64
afd0d702a4fe some changes
Chengsong
parents: 63
diff changeset
   232
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
   233
$r_{key}$ for recognising keywords such as \textit{if}, \textit{then}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   234
and so on; and a regular expression $r_{id}$ for recognising
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   235
identifiers (say, a single character followed by characters or
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   236
numbers). One can then form the compound regular expression
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   237
$(r_{key} + r_{id})^*$ and use it to tokenise strings.  But then how
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   238
should the string \textit{iffoo} be tokenised?  It could be tokenised
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   239
as a keyword followed by an identifier, or the entire string as a
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   240
single identifier.  Similarly, how should the string \textit{if} be
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   241
tokenised? Both regular expressions, $r_{key}$ and $r_{id}$, would
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   242
``fire''---so is it an identifier or a keyword?  While in applications
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   243
there is a well-known strategy to decide these questions, called POSIX
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   244
matching, only relatively recently precise definitions of what POSIX
64
afd0d702a4fe some changes
Chengsong
parents: 63
diff changeset
   245
matching actually means has been formalised
46
9b48724ec609 proofread
Christian Urban <urbanc@in.tum.de>
parents: 45
diff changeset
   246
\cite{AusafDyckhoffUrban2016,OkuiSuzuki2010,Vansummeren2006}. 
9b48724ec609 proofread
Christian Urban <urbanc@in.tum.de>
parents: 45
diff changeset
   247
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
   248
corresponding correctness proof turned out to be  faulty \cite{AusafDyckhoffUrban2016}.
9b48724ec609 proofread
Christian Urban <urbanc@in.tum.de>
parents: 45
diff changeset
   249
Roughly, POSIX matching means matching the longest initial substring.
64
afd0d702a4fe some changes
Chengsong
parents: 63
diff changeset
   250
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
   251
regular expressions (e.g.~keywords have a higher priority than
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   252
identifiers). This sounds rather simple, but according to Grathwohl et
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   253
al \cite[Page 36]{CrashCourse2014} this is not the case. They wrote:
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   254
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   255
\begin{quote}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   256
\it{}``The POSIX strategy is more complicated than the greedy because of 
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   257
the dependence on information about the length of matched strings in the 
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   258
various subexpressions.''
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   259
\end{quote}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   260
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   261
\noindent
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   262
This is also supported by evidence collected by Kuklewicz
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   263
\cite{Kuklewicz} who noticed that a number of POSIX regular expression
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   264
matchers calculate incorrect results.
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   265
77
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   266
Our focus in this project is on an algorithm introduced by Sulzmann and
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   267
Lu in 2014 for regular expression matching according to the POSIX
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   268
strategy \cite{Sulzmann2014}. Their algorithm is based on an older
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   269
algorithm by Brzozowski from 1964 where he introduced the notion of
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   270
derivatives of regular expressions~\cite{Brzozowski1964}. We shall
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   271
briefly explain this algorithm next.
30
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   272
46
9b48724ec609 proofread
Christian Urban <urbanc@in.tum.de>
parents: 45
diff changeset
   273
\section{The Algorithm by Brzozowski based on Derivatives of Regular
9b48724ec609 proofread
Christian Urban <urbanc@in.tum.de>
parents: 45
diff changeset
   274
Expressions}
30
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   275
40
8063792920ef proof reading
Christian Urban <urbanc@in.tum.de>
parents: 39
diff changeset
   276
Suppose (basic) regular expressions are given by the following grammar:
38
b5363c0dcd99 half easy changes
Chengsong
parents: 37
diff changeset
   277
\[			r ::=   \ZERO \mid  \ONE
b5363c0dcd99 half easy changes
Chengsong
parents: 37
diff changeset
   278
			 \mid  c  
b5363c0dcd99 half easy changes
Chengsong
parents: 37
diff changeset
   279
			 \mid  r_1 \cdot r_2
b5363c0dcd99 half easy changes
Chengsong
parents: 37
diff changeset
   280
			 \mid  r_1 + r_2   
b5363c0dcd99 half easy changes
Chengsong
parents: 37
diff changeset
   281
			 \mid r^*         
b5363c0dcd99 half easy changes
Chengsong
parents: 37
diff changeset
   282
\]
30
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   283
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   284
\noindent
46
9b48724ec609 proofread
Christian Urban <urbanc@in.tum.de>
parents: 45
diff changeset
   285
The intended meaning of the constructors is as follows: $\ZERO$
30
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   286
cannot match any string, $\ONE$ can match the empty string, the
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   287
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
   288
on.
8063792920ef proof reading
Christian Urban <urbanc@in.tum.de>
parents: 39
diff changeset
   289
58
f0360e17080e proofread
Christian Urban <urbanc@in.tum.de>
parents: 57
diff changeset
   290
The ingenious contribution by Brzozowski is the notion of
30
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   291
\emph{derivatives} of regular expressions.  The idea behind this
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   292
notion is as follows: suppose a regular expression $r$ can match a
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   293
string of the form $c\!::\! s$ (that is a list of characters starting
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   294
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
   295
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
   296
with the definition of $nullable$:
36
Chengsong
parents: 35
diff changeset
   297
\begin{center}
Chengsong
parents: 35
diff changeset
   298
		\begin{tabular}{lcl}
Chengsong
parents: 35
diff changeset
   299
			$\nullable(\ZERO)$     & $\dn$ & $\mathit{false}$ \\  
Chengsong
parents: 35
diff changeset
   300
			$\nullable(\ONE)$      & $\dn$ & $\mathit{true}$ \\
Chengsong
parents: 35
diff changeset
   301
			$\nullable(c)$ 	       & $\dn$ & $\mathit{false}$ \\
Chengsong
parents: 35
diff changeset
   302
			$\nullable(r_1 + r_2)$ & $\dn$ & $\nullable(r_1) \vee \nullable(r_2)$ \\
Chengsong
parents: 35
diff changeset
   303
			$\nullable(r_1\cdot r_2)$  & $\dn$ & $\nullable(r_1) \wedge \nullable(r_2)$ \\
Chengsong
parents: 35
diff changeset
   304
			$\nullable(r^*)$       & $\dn$ & $\mathit{true}$ \\
Chengsong
parents: 35
diff changeset
   305
		\end{tabular}
Chengsong
parents: 35
diff changeset
   306
	\end{center}
38
b5363c0dcd99 half easy changes
Chengsong
parents: 37
diff changeset
   307
This function simply tests whether the empty string is in $L(r)$.
36
Chengsong
parents: 35
diff changeset
   308
He then defined
30
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   309
the following operation on regular expressions, written
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   310
$r\backslash c$ (the derivative of $r$ w.r.t.~the character $c$):
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   311
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   312
\begin{center}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   313
\begin{tabular}{lcl}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   314
		$\ZERO \backslash c$ & $\dn$ & $\ZERO$\\  
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   315
		$\ONE \backslash c$  & $\dn$ & $\ZERO$\\
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   316
		$d \backslash c$     & $\dn$ & 
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   317
		$\mathit{if} \;c = d\;\mathit{then}\;\ONE\;\mathit{else}\;\ZERO$\\
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   318
$(r_1 + r_2)\backslash c$     & $\dn$ & $r_1 \backslash c \,+\, r_2 \backslash c$\\
36
Chengsong
parents: 35
diff changeset
   319
$(r_1 \cdot r_2)\backslash c$ & $\dn$ & $\mathit{if} \, nullable(r_1)$\\
30
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   320
	&   & $\mathit{then}\;(r_1\backslash c) \cdot r_2 \,+\, r_2\backslash c$\\
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   321
	&   & $\mathit{else}\;(r_1\backslash c) \cdot r_2$\\
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   322
	$(r^*)\backslash c$           & $\dn$ & $(r\backslash c) \cdot r^*$\\
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   323
\end{tabular}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   324
\end{center}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   325
46
9b48724ec609 proofread
Christian Urban <urbanc@in.tum.de>
parents: 45
diff changeset
   326
%Assuming the classic notion of a
9b48724ec609 proofread
Christian Urban <urbanc@in.tum.de>
parents: 45
diff changeset
   327
%\emph{language} of a regular expression, written $L(\_)$, t
30
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   328
40
8063792920ef proof reading
Christian Urban <urbanc@in.tum.de>
parents: 39
diff changeset
   329
\noindent
8063792920ef proof reading
Christian Urban <urbanc@in.tum.de>
parents: 39
diff changeset
   330
The main property of the derivative operation is that
30
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   331
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   332
\begin{center}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   333
$c\!::\!s \in L(r)$ holds
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   334
if and only if $s \in L(r\backslash c)$.
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   335
\end{center}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   336
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   337
\noindent
46
9b48724ec609 proofread
Christian Urban <urbanc@in.tum.de>
parents: 45
diff changeset
   338
For us the main advantage is that derivatives can be
38
b5363c0dcd99 half easy changes
Chengsong
parents: 37
diff changeset
   339
straightforwardly implemented in any functional programming language,
b5363c0dcd99 half easy changes
Chengsong
parents: 37
diff changeset
   340
and are easily definable and reasoned about in theorem provers---the
b5363c0dcd99 half easy changes
Chengsong
parents: 37
diff changeset
   341
definitions just consist of inductive datatypes and simple recursive
b5363c0dcd99 half easy changes
Chengsong
parents: 37
diff changeset
   342
functions. Moreover, the notion of derivatives can be easily
b5363c0dcd99 half easy changes
Chengsong
parents: 37
diff changeset
   343
generalised to cover extended regular expression constructors such as
b5363c0dcd99 half easy changes
Chengsong
parents: 37
diff changeset
   344
the not-regular expression, written $\neg\,r$, or bounded repetitions
b5363c0dcd99 half easy changes
Chengsong
parents: 37
diff changeset
   345
(for example $r^{\{n\}}$ and $r^{\{n..m\}}$), which cannot be so
b5363c0dcd99 half easy changes
Chengsong
parents: 37
diff changeset
   346
straightforwardly realised within the classic automata approach.
b5363c0dcd99 half easy changes
Chengsong
parents: 37
diff changeset
   347
For the moment however, we focus only on the usual basic regular expressions.
b5363c0dcd99 half easy changes
Chengsong
parents: 37
diff changeset
   348
b5363c0dcd99 half easy changes
Chengsong
parents: 37
diff changeset
   349
40
8063792920ef proof reading
Christian Urban <urbanc@in.tum.de>
parents: 39
diff changeset
   350
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
   351
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
   352
all the characters of the string $s$. Finally, test whether the
8063792920ef proof reading
Christian Urban <urbanc@in.tum.de>
parents: 39
diff changeset
   353
resulting regular expression can match the empty string.  If yes, then
8063792920ef proof reading
Christian Urban <urbanc@in.tum.de>
parents: 39
diff changeset
   354
$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
   355
we can generalise the derivative operation to strings like this:
46
9b48724ec609 proofread
Christian Urban <urbanc@in.tum.de>
parents: 45
diff changeset
   356
30
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   357
\begin{center}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   358
\begin{tabular}{lcl}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   359
$r \backslash (c\!::\!s) $ & $\dn$ & $(r \backslash c) \backslash s$ \\
40
8063792920ef proof reading
Christian Urban <urbanc@in.tum.de>
parents: 39
diff changeset
   360
$r \backslash [\,] $ & $\dn$ & $r$
30
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   361
\end{tabular}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   362
\end{center}
40
8063792920ef proof reading
Christian Urban <urbanc@in.tum.de>
parents: 39
diff changeset
   363
37
17d8e7599a01 new changes
Chengsong
parents: 36
diff changeset
   364
\noindent
46
9b48724ec609 proofread
Christian Urban <urbanc@in.tum.de>
parents: 45
diff changeset
   365
and then define as  regular-expression matching algorithm: 
30
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   366
\[
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   367
match\;s\;r \;\dn\; nullable(r\backslash s)
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   368
\]
40
8063792920ef proof reading
Christian Urban <urbanc@in.tum.de>
parents: 39
diff changeset
   369
8063792920ef proof reading
Christian Urban <urbanc@in.tum.de>
parents: 39
diff changeset
   370
\noindent
64
afd0d702a4fe some changes
Chengsong
parents: 63
diff changeset
   371
This algorithm looks graphically as follows:
46
9b48724ec609 proofread
Christian Urban <urbanc@in.tum.de>
parents: 45
diff changeset
   372
\begin{equation}\label{graph:*}
9b48724ec609 proofread
Christian Urban <urbanc@in.tum.de>
parents: 45
diff changeset
   373
\begin{tikzcd}
9b48724ec609 proofread
Christian Urban <urbanc@in.tum.de>
parents: 45
diff changeset
   374
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
   375
\end{tikzcd}
46
9b48724ec609 proofread
Christian Urban <urbanc@in.tum.de>
parents: 45
diff changeset
   376
\end{equation}
40
8063792920ef proof reading
Christian Urban <urbanc@in.tum.de>
parents: 39
diff changeset
   377
8063792920ef proof reading
Christian Urban <urbanc@in.tum.de>
parents: 39
diff changeset
   378
\noindent
46
9b48724ec609 proofread
Christian Urban <urbanc@in.tum.de>
parents: 45
diff changeset
   379
where we start with  a regular expression  $r_0$, build successive
9b48724ec609 proofread
Christian Urban <urbanc@in.tum.de>
parents: 45
diff changeset
   380
derivatives until we exhaust the string and then use \textit{nullable}
9b48724ec609 proofread
Christian Urban <urbanc@in.tum.de>
parents: 45
diff changeset
   381
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
   382
relatively  easily shown that this matcher is correct  (that is given
64
afd0d702a4fe some changes
Chengsong
parents: 63
diff changeset
   383
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
   384
9b48724ec609 proofread
Christian Urban <urbanc@in.tum.de>
parents: 45
diff changeset
   385
 
9b48724ec609 proofread
Christian Urban <urbanc@in.tum.de>
parents: 45
diff changeset
   386
\section{Values and the Algorithm by Sulzmann and Lu}
38
b5363c0dcd99 half easy changes
Chengsong
parents: 37
diff changeset
   387
77
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   388
One limitation of Brzozowski's algorithm is that it only produces a
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   389
YES/NO answer for whether a string is being matched by a regular
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   390
expression.  Sulzmann and Lu~\cite{Sulzmann2014} extended this algorithm
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   391
to allow generation of an actual matching, called a \emph{value} or
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   392
sometimes also \emph{lexical values}.  These values and regular
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   393
expressions correspond to each other as illustrated in the following
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   394
table:
46
9b48724ec609 proofread
Christian Urban <urbanc@in.tum.de>
parents: 45
diff changeset
   395
30
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   396
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   397
\begin{center}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   398
	\begin{tabular}{c@{\hspace{20mm}}c}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   399
		\begin{tabular}{@{}rrl@{}}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   400
			\multicolumn{3}{@{}l}{\textbf{Regular Expressions}}\medskip\\
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   401
			$r$ & $::=$  & $\ZERO$\\
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   402
			& $\mid$ & $\ONE$   \\
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   403
			& $\mid$ & $c$          \\
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   404
			& $\mid$ & $r_1 \cdot r_2$\\
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   405
			& $\mid$ & $r_1 + r_2$   \\
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   406
			\\
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   407
			& $\mid$ & $r^*$         \\
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   408
		\end{tabular}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   409
		&
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   410
		\begin{tabular}{@{\hspace{0mm}}rrl@{}}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   411
			\multicolumn{3}{@{}l}{\textbf{Values}}\medskip\\
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   412
			$v$ & $::=$  & \\
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   413
			&        & $\Empty$   \\
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   414
			& $\mid$ & $\Char(c)$          \\
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   415
			& $\mid$ & $\Seq\,v_1\, v_2$\\
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   416
			& $\mid$ & $\Left(v)$   \\
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   417
			& $\mid$ & $\Right(v)$  \\
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   418
			& $\mid$ & $\Stars\,[v_1,\ldots\,v_n]$ \\
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   419
		\end{tabular}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   420
	\end{tabular}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   421
\end{center}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   422
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   423
\noindent
64
afd0d702a4fe some changes
Chengsong
parents: 63
diff changeset
   424
No value  corresponds to $\ZERO$; $\Empty$ corresponds to
63
d3c22f809dde more proof-reading
Christian Urban <urbanc@in.tum.de>
parents: 62
diff changeset
   425
$\ONE$; $\Char$ to the character regular expression; $\Seq$ to the
d3c22f809dde more proof-reading
Christian Urban <urbanc@in.tum.de>
parents: 62
diff changeset
   426
sequence regular expression and so on. The idea of values is to encode
72
83b021fc7d29 interesting?
Chengsong
parents: 71
diff changeset
   427
a kind of lexical value for how the sub-parts of a regular expression match
64
afd0d702a4fe some changes
Chengsong
parents: 63
diff changeset
   428
the sub-parts of a string. To see this, suppose a \emph{flatten} operation, written
72
83b021fc7d29 interesting?
Chengsong
parents: 71
diff changeset
   429
$|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
   430
$v$. For example, $|\mathit{Seq} \, (\textit{Char x}) \, (\textit{Char
d3c22f809dde more proof-reading
Christian Urban <urbanc@in.tum.de>
parents: 62
diff changeset
   431
y})|$ is the string $xy$.  Using flatten, we can describe how values
64
afd0d702a4fe some changes
Chengsong
parents: 63
diff changeset
   432
encode parse trees: $\Seq\,v_1\, v_2$ encodes a tree with 2 children nodes
afd0d702a4fe some changes
Chengsong
parents: 63
diff changeset
   433
that tells how the string $|v_1| @
63
d3c22f809dde more proof-reading
Christian Urban <urbanc@in.tum.de>
parents: 62
diff changeset
   434
|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
   435
substring $|v_1|$ and, respectively, $r_2$ matches the substring
d3c22f809dde more proof-reading
Christian Urban <urbanc@in.tum.de>
parents: 62
diff changeset
   436
$|v_2|$. Exactly how these two are matched is contained in the
64
afd0d702a4fe some changes
Chengsong
parents: 63
diff changeset
   437
children nodes $v_1$ and $v_2$ of parent $\textit{Seq}$ . 
30
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   438
77
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   439
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
   440
and the regular expression $(x + (y + xy))^*$. We can view this regular
30
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   441
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
   442
``iterations'', then the $x$ is matched by the left-most alternative in
9b48724ec609 proofread
Christian Urban <urbanc@in.tum.de>
parents: 45
diff changeset
   443
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
   444
record this matching as
30
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   445
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   446
\begin{center}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   447
$\Stars\,[\Left\,(\Char\,x), \Right(\Left(\Char\,y))]$
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   448
\end{center}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   449
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   450
\noindent
72
83b021fc7d29 interesting?
Chengsong
parents: 71
diff changeset
   451
where $\Stars \; [\ldots]$ records all the
64
afd0d702a4fe some changes
Chengsong
parents: 63
diff changeset
   452
iterations; and $\Left$, respectively $\Right$, which
30
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   453
alternative is used. The value for
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   454
matching $xy$ in a single ``iteration'', i.e.~the POSIX value,
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   455
would look as follows
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   456
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   457
\begin{center}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   458
$\Stars\,[\Seq\,(\Char\,x)\,(\Char\,y)]$
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   459
\end{center}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   460
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   461
\noindent
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   462
where $\Stars$ has only a single-element list for the single iteration
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   463
and $\Seq$ indicates that $xy$ is matched by a sequence regular
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   464
expression.
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   465
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   466
The contribution of Sulzmann and Lu is an extension of Brzozowski's
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   467
algorithm by a second phase (the first phase being building successive
46
9b48724ec609 proofread
Christian Urban <urbanc@in.tum.de>
parents: 45
diff changeset
   468
derivatives---see \eqref{graph:*}). In this second phase, a POSIX value 
72
83b021fc7d29 interesting?
Chengsong
parents: 71
diff changeset
   469
is generated in case the regular expression matches  the string. 
83b021fc7d29 interesting?
Chengsong
parents: 71
diff changeset
   470
Pictorially, the Sulzmann and Lu algorithm is as follows:
46
9b48724ec609 proofread
Christian Urban <urbanc@in.tum.de>
parents: 45
diff changeset
   471
70
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   472
\begin{ceqn}
59
8ff7b7508824 changes1
Chengsong
parents: 58
diff changeset
   473
\begin{equation}\label{graph:2}
30
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   474
\begin{tikzcd}
36
Chengsong
parents: 35
diff changeset
   475
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
   476
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
   477
\end{tikzcd}
59
8ff7b7508824 changes1
Chengsong
parents: 58
diff changeset
   478
\end{equation}
70
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   479
\end{ceqn}
37
17d8e7599a01 new changes
Chengsong
parents: 36
diff changeset
   480
46
9b48724ec609 proofread
Christian Urban <urbanc@in.tum.de>
parents: 45
diff changeset
   481
\noindent
77
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   482
For convenience, we shall employ the following notations: the regular
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   483
expression we start with is $r_0$, and the given string $s$ is composed
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   484
of characters $c_0 c_1 \ldots c_{n-1}$. In  the first phase from the
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   485
left to right, we build the derivatives $r_1$, $r_2$, \ldots  according
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   486
to the characters $c_0$, $c_1$  until we exhaust the string and obtain
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   487
the derivative $r_n$. We test whether this derivative is
46
9b48724ec609 proofread
Christian Urban <urbanc@in.tum.de>
parents: 45
diff changeset
   488
$\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
   489
$r$ and no value needs to be generated. If yes, we start building the
77
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   490
values incrementally by \emph{injecting} back the characters into the
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   491
earlier values $v_n, \ldots, v_0$. This is the second phase of the
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   492
algorithm from the right to left. For the first value $v_n$, we call the
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   493
function $\textit{mkeps}$, which builds the parse tree for how the empty
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   494
string has been matched by the (nullable) regular expression $r_n$. This
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   495
function is defined as
30
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   496
51
5df7faf69238 added mkeps and pder, still have not proof read it
Chengsong
parents: 50
diff changeset
   497
	\begin{center}
5df7faf69238 added mkeps and pder, still have not proof read it
Chengsong
parents: 50
diff changeset
   498
		\begin{tabular}{lcl}
5df7faf69238 added mkeps and pder, still have not proof read it
Chengsong
parents: 50
diff changeset
   499
			$\mkeps(\ONE)$ 		& $\dn$ & $\Empty$ \\
5df7faf69238 added mkeps and pder, still have not proof read it
Chengsong
parents: 50
diff changeset
   500
			$\mkeps(r_{1}+r_{2})$	& $\dn$ 
5df7faf69238 added mkeps and pder, still have not proof read it
Chengsong
parents: 50
diff changeset
   501
			& \textit{if} $\nullable(r_{1})$\\ 
5df7faf69238 added mkeps and pder, still have not proof read it
Chengsong
parents: 50
diff changeset
   502
			& & \textit{then} $\Left(\mkeps(r_{1}))$\\ 
5df7faf69238 added mkeps and pder, still have not proof read it
Chengsong
parents: 50
diff changeset
   503
			& & \textit{else} $\Right(\mkeps(r_{2}))$\\
5df7faf69238 added mkeps and pder, still have not proof read it
Chengsong
parents: 50
diff changeset
   504
			$\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
   505
			$mkeps(r^*)$	        & $\dn$ & $\Stars\,[]$
5df7faf69238 added mkeps and pder, still have not proof read it
Chengsong
parents: 50
diff changeset
   506
		\end{tabular}
5df7faf69238 added mkeps and pder, still have not proof read it
Chengsong
parents: 50
diff changeset
   507
	\end{center}
41
a1f90febbc7f example
Chengsong
parents: 40
diff changeset
   508
59
8ff7b7508824 changes1
Chengsong
parents: 58
diff changeset
   509
8ff7b7508824 changes1
Chengsong
parents: 58
diff changeset
   510
\noindent There are no cases for $\ZERO$ and $c$, since
8ff7b7508824 changes1
Chengsong
parents: 58
diff changeset
   511
these regular expression cannot match the empty string. Note
8ff7b7508824 changes1
Chengsong
parents: 58
diff changeset
   512
also that in case of alternatives we give preference to the
8ff7b7508824 changes1
Chengsong
parents: 58
diff changeset
   513
regular expression on the left-hand side. This will become
8ff7b7508824 changes1
Chengsong
parents: 58
diff changeset
   514
important later on.
8ff7b7508824 changes1
Chengsong
parents: 58
diff changeset
   515
8ff7b7508824 changes1
Chengsong
parents: 58
diff changeset
   516
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
   517
the parse tree $v_i$ for how the regex $r_i$ matches the string $s_i$
77
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   518
($s_i = c_i \ldots c_{n-1}$ ) from the previous parse tree $v_{i+1}$.
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   519
After injecting back $n$ characters, we get the parse tree for how $r_0$
63
d3c22f809dde more proof-reading
Christian Urban <urbanc@in.tum.de>
parents: 62
diff changeset
   520
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
   521
the ``chopping off'' of characters during the derivative phase. The
77
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   522
corresponding function is called \emph{injection}, written
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   523
$\textit{inj}$; it takes three arguments: the first one is a regular
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   524
expression ${r_{i-1}}$, before the character is chopped off, the second
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   525
is a character ${c_{i-1}}$, the character we want to inject and the
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   526
third argument is the value ${v_i}$, into which one wants to inject the
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   527
character (it corresponds to the regular expression after the character
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   528
has been chopped off). The result of this function is a new value. The
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   529
definition of $\textit{inj}$ is as follows: 
59
8ff7b7508824 changes1
Chengsong
parents: 58
diff changeset
   530
8ff7b7508824 changes1
Chengsong
parents: 58
diff changeset
   531
\begin{center}
8ff7b7508824 changes1
Chengsong
parents: 58
diff changeset
   532
\begin{tabular}{l@{\hspace{1mm}}c@{\hspace{1mm}}l}
8ff7b7508824 changes1
Chengsong
parents: 58
diff changeset
   533
  $\textit{inj}\,(c)\,c\,Empty$            & $\dn$ & $Char\,c$\\
8ff7b7508824 changes1
Chengsong
parents: 58
diff changeset
   534
  $\textit{inj}\,(r_1 + r_2)\,c\,\Left(v)$ & $\dn$ & $\Left(\textit{inj}\,r_1\,c\,v)$\\
8ff7b7508824 changes1
Chengsong
parents: 58
diff changeset
   535
  $\textit{inj}\,(r_1 + r_2)\,c\,Right(v)$ & $\dn$ & $Right(\textit{inj}\,r_2\,c\,v)$\\
8ff7b7508824 changes1
Chengsong
parents: 58
diff changeset
   536
  $\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
   537
  $\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
   538
  $\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
   539
  $\textit{inj}\,(r^*)\,c\,Seq(v,Stars\,vs)$         & $\dn$  & $Stars((\textit{inj}\,r\,c\,v)\,::\,vs)$\\
8ff7b7508824 changes1
Chengsong
parents: 58
diff changeset
   540
\end{tabular}
8ff7b7508824 changes1
Chengsong
parents: 58
diff changeset
   541
\end{center}
8ff7b7508824 changes1
Chengsong
parents: 58
diff changeset
   542
63
d3c22f809dde more proof-reading
Christian Urban <urbanc@in.tum.de>
parents: 62
diff changeset
   543
\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
   544
expressions and values. To understands this definition better consider
d3c22f809dde more proof-reading
Christian Urban <urbanc@in.tum.de>
parents: 62
diff changeset
   545
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
   546
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
   547
``hole'' in $r_i$ and its corresponding value $v_i$. 
83b021fc7d29 interesting?
Chengsong
parents: 71
diff changeset
   548
To calculate $v_{i-1}$, we need to
64
afd0d702a4fe some changes
Chengsong
parents: 63
diff changeset
   549
locate where that hole is and fill it. 
afd0d702a4fe some changes
Chengsong
parents: 63
diff changeset
   550
We can find this location by
63
d3c22f809dde more proof-reading
Christian Urban <urbanc@in.tum.de>
parents: 62
diff changeset
   551
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
   552
$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
   553
%
d3c22f809dde more proof-reading
Christian Urban <urbanc@in.tum.de>
parents: 62
diff changeset
   554
\[ (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
   555
d3c22f809dde more proof-reading
Christian Urban <urbanc@in.tum.de>
parents: 62
diff changeset
   556
\noindent
59
8ff7b7508824 changes1
Chengsong
parents: 58
diff changeset
   557
otherwise if $r_a$ is not nullable,
63
d3c22f809dde more proof-reading
Christian Urban <urbanc@in.tum.de>
parents: 62
diff changeset
   558
\[ (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
   559
d3c22f809dde more proof-reading
Christian Urban <urbanc@in.tum.de>
parents: 62
diff changeset
   560
\noindent
64
afd0d702a4fe some changes
Chengsong
parents: 63
diff changeset
   561
the value $v_i$ should be  $\Seq(\ldots)$, contradicting the fact that
afd0d702a4fe some changes
Chengsong
parents: 63
diff changeset
   562
$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
   563
$\Left(\ldots)$ instead of $\Right(\ldots)$, we know that the left
64
afd0d702a4fe some changes
Chengsong
parents: 63
diff changeset
   564
branch of \[ (r_a \cdot r_b)\backslash c =
afd0d702a4fe some changes
Chengsong
parents: 63
diff changeset
   565
\bold{\underline{ (r_a\backslash c) \cdot r_b} }\,+\, r_b\backslash c,\](underlined)
afd0d702a4fe some changes
Chengsong
parents: 63
diff changeset
   566
 is taken instead of the right one. This means $c$ is chopped off 
afd0d702a4fe some changes
Chengsong
parents: 63
diff changeset
   567
from $r_a$ rather than $r_b$.
afd0d702a4fe some changes
Chengsong
parents: 63
diff changeset
   568
We have therefore found out 
63
d3c22f809dde more proof-reading
Christian Urban <urbanc@in.tum.de>
parents: 62
diff changeset
   569
that the hole will be on $r_a$. So we recursively call $\inj\, 
64
afd0d702a4fe some changes
Chengsong
parents: 63
diff changeset
   570
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
   571
$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
   572
Other clauses can be understood in a similar way.
59
8ff7b7508824 changes1
Chengsong
parents: 58
diff changeset
   573
71
0573615e41a3 new changes?
Chengsong
parents: 70
diff changeset
   574
%\comment{Other word: insight?}
0573615e41a3 new changes?
Chengsong
parents: 70
diff changeset
   575
The following example gives an insight of $\textit{inj}$'s effect
65
df2e0faccb23 moew changes
Chengsong
parents: 64
diff changeset
   576
and how Sulzmann and Lu's algorithm works as a whole.
df2e0faccb23 moew changes
Chengsong
parents: 64
diff changeset
   577
 Suppose we have a
df2e0faccb23 moew changes
Chengsong
parents: 64
diff changeset
   578
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
   579
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
   580
standard way of expressing it should be $a \cdot (b \cdot c)$. We omit
65
df2e0faccb23 moew changes
Chengsong
parents: 64
diff changeset
   581
the parentheses and dots here for readability). 
df2e0faccb23 moew changes
Chengsong
parents: 64
diff changeset
   582
This algorithm returns a POSIX value, which means it
df2e0faccb23 moew changes
Chengsong
parents: 64
diff changeset
   583
will go for the longest matching, i.e.~it should match the string
df2e0faccb23 moew changes
Chengsong
parents: 64
diff changeset
   584
$abc$ in one star iteration, using the longest alternative $abc$ in the
df2e0faccb23 moew changes
Chengsong
parents: 64
diff changeset
   585
sub-expression $((((a+b)+ab)+c)+abc)$ (we use $r$ to denote this sub-expression
64
afd0d702a4fe some changes
Chengsong
parents: 63
diff changeset
   586
for conciseness). 
65
df2e0faccb23 moew changes
Chengsong
parents: 64
diff changeset
   587
Before $\textit{inj}$ comes into play, 
df2e0faccb23 moew changes
Chengsong
parents: 64
diff changeset
   588
our lexer first builds derivative using string $abc$ (we simplified some regular expressions like
df2e0faccb23 moew changes
Chengsong
parents: 64
diff changeset
   589
$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
   590
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
   591
%Similarly, we allow
c737a0259194 sorry not all done, need a few more mins for last few changes
Chengsong
parents: 59
diff changeset
   592
%$\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
   593
%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
   594
%$\textit{ALT}$
c737a0259194 sorry not all done, need a few more mins for last few changes
Chengsong
parents: 59
diff changeset
   595
\begin{center}
63
d3c22f809dde more proof-reading
Christian Urban <urbanc@in.tum.de>
parents: 62
diff changeset
   596
\begin{tabular}{lcl}
72
83b021fc7d29 interesting?
Chengsong
parents: 71
diff changeset
   597
$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
   598
      & $\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
   599
      & $\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
   600
      &                              & $\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
   601
\end{tabular}
60
c737a0259194 sorry not all done, need a few more mins for last few changes
Chengsong
parents: 59
diff changeset
   602
\end{center}
63
d3c22f809dde more proof-reading
Christian Urban <urbanc@in.tum.de>
parents: 62
diff changeset
   603
d3c22f809dde more proof-reading
Christian Urban <urbanc@in.tum.de>
parents: 62
diff changeset
   604
\noindent
72
83b021fc7d29 interesting?
Chengsong
parents: 71
diff changeset
   605
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
   606
to construct a parse tree for how $r_3$ matched the string $abc$. 
72
83b021fc7d29 interesting?
Chengsong
parents: 71
diff changeset
   607
$\textit{mkeps}$ gives the following value $v_3$: 
65
df2e0faccb23 moew changes
Chengsong
parents: 64
diff changeset
   608
\begin{center}
df2e0faccb23 moew changes
Chengsong
parents: 64
diff changeset
   609
$\Left(\Left(\Seq(\Right(\Seq(\Empty, \Seq(\Empty,\Empty))), \Stars [])))$
df2e0faccb23 moew changes
Chengsong
parents: 64
diff changeset
   610
\end{center}
df2e0faccb23 moew changes
Chengsong
parents: 64
diff changeset
   611
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
   612
65
df2e0faccb23 moew changes
Chengsong
parents: 64
diff changeset
   613
\begin{center}
72
83b021fc7d29 interesting?
Chengsong
parents: 71
diff changeset
   614
   $( \underline{(\ZERO+\ZERO+\ZERO+ \ZERO+ \ONE \cdot \ONE \cdot \ONE) \cdot r^*} + (\ZERO+\ZERO+\ZERO + \ONE + \ZERO)
83b021fc7d29 interesting?
Chengsong
parents: 71
diff changeset
   615
  \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
   616
 \end{center}
70
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   617
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   618
\noindent
72
83b021fc7d29 interesting?
Chengsong
parents: 71
diff changeset
   619
 Note that the leftmost location of term $((\ZERO+\ZERO+\ZERO + \ZERO + \ONE \cdot \ONE \cdot
83b021fc7d29 interesting?
Chengsong
parents: 71
diff changeset
   620
 \ONE) \cdot r^*$ (which corresponds to the initial sub-match $abc$) allows
83b021fc7d29 interesting?
Chengsong
parents: 71
diff changeset
   621
 $\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
   622
 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
   623
 preferred over $a$ or $ab$. This $\Left(\Left(\ldots))$ location is
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   624
 naturally generated by two applications of the splitting clause
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   625
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   626
\begin{center}
65
df2e0faccb23 moew changes
Chengsong
parents: 64
diff changeset
   627
     $(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
   628
\end{center}
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   629
       
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   630
\noindent
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   631
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
   632
$\textit{front}$ and $r_2 \backslash c$ at the $\textit{back}$. This
72
83b021fc7d29 interesting?
Chengsong
parents: 71
diff changeset
   633
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
   634
initial sub-match. Removing the outside $\Left(\Left(...))$, the inside
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   635
sub-value 
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   636
 
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   637
\begin{center}
65
df2e0faccb23 moew changes
Chengsong
parents: 64
diff changeset
   638
 $\Seq(\Right(\Seq(\Empty, \Seq(\Empty, \Empty))), \Stars [])$
70
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   639
\end{center}
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   640
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   641
\noindent
72
83b021fc7d29 interesting?
Chengsong
parents: 71
diff changeset
   642
tells us how the empty string $[]$ is matched with $(\ZERO+\ZERO+\ZERO + \ZERO + \ONE \cdot
83b021fc7d29 interesting?
Chengsong
parents: 71
diff changeset
   643
\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
   644
expressions. The first one is an alternative, we take the rightmost
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   645
alternative---whose language contains the empty string. The second
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   646
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
   647
generates the nullable regular expression: by 0 iterations to form
72
83b021fc7d29 interesting?
Chengsong
parents: 71
diff changeset
   648
$\ONE$. Now $\textit{inj}$ injects characters back and incrementally
70
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   649
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
   650
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
   651
the string $[c]$ : $\textit{inj} \; r_2 \; c \; v_3$ gives us
65
df2e0faccb23 moew changes
Chengsong
parents: 64
diff changeset
   652
 \begin{center}
df2e0faccb23 moew changes
Chengsong
parents: 64
diff changeset
   653
 $v_2 = \Left(\Seq(\Right(\Seq(\Empty, \Seq(\Empty, c))), \Stars [])),$
df2e0faccb23 moew changes
Chengsong
parents: 64
diff changeset
   654
 \end{center}
df2e0faccb23 moew changes
Chengsong
parents: 64
diff changeset
   655
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
   656
\begin{center}
df2e0faccb23 moew changes
Chengsong
parents: 64
diff changeset
   657
$v_1 = \Seq(\Right(\Seq(\Empty, \Seq(b, c))), \Stars [])$
df2e0faccb23 moew changes
Chengsong
parents: 64
diff changeset
   658
\end{center}
61
580c7b84f900 hi finished
Chengsong
parents: 60
diff changeset
   659
 for how 
65
df2e0faccb23 moew changes
Chengsong
parents: 64
diff changeset
   660
 \begin{center}
72
83b021fc7d29 interesting?
Chengsong
parents: 71
diff changeset
   661
 $r_1= (\ONE+\ZERO+\ONE \cdot b + \ZERO + \ONE \cdot b \cdot c) \cdot r*$
65
df2e0faccb23 moew changes
Chengsong
parents: 64
diff changeset
   662
 \end{center}
61
580c7b84f900 hi finished
Chengsong
parents: 60
diff changeset
   663
  matched  the string $bc$ before it split into 2 pieces. 
580c7b84f900 hi finished
Chengsong
parents: 60
diff changeset
   664
  Finally, after injecting character $a$ back to $v_1$, 
65
df2e0faccb23 moew changes
Chengsong
parents: 64
diff changeset
   665
  we get  the parse tree 
df2e0faccb23 moew changes
Chengsong
parents: 64
diff changeset
   666
  \begin{center}
df2e0faccb23 moew changes
Chengsong
parents: 64
diff changeset
   667
  $v_0= \Stars [\Right(\Seq(a, \Seq(b, c)))]$
df2e0faccb23 moew changes
Chengsong
parents: 64
diff changeset
   668
  \end{center}
df2e0faccb23 moew changes
Chengsong
parents: 64
diff changeset
   669
   for how $r$ matched $abc$. This completes the algorithm.
df2e0faccb23 moew changes
Chengsong
parents: 64
diff changeset
   670
   
61
580c7b84f900 hi finished
Chengsong
parents: 60
diff changeset
   671
%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
   672
Readers might have noticed that the parse tree information 
580c7b84f900 hi finished
Chengsong
parents: 60
diff changeset
   673
is actually already available when doing derivatives. 
580c7b84f900 hi finished
Chengsong
parents: 60
diff changeset
   674
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
   675
 we can either take the initial match to be 
65
df2e0faccb23 moew changes
Chengsong
parents: 64
diff changeset
   676
 \begin{center}
42
Chengsong
parents: 41
diff changeset
   677
\begin{enumerate}
Chengsong
parents: 41
diff changeset
   678
    \item[1)] just $a$ or
Chengsong
parents: 41
diff changeset
   679
    \item[2)] string $ab$ or 
Chengsong
parents: 41
diff changeset
   680
    \item[3)] string $abc$.
Chengsong
parents: 41
diff changeset
   681
\end{enumerate}
65
df2e0faccb23 moew changes
Chengsong
parents: 64
diff changeset
   682
\end{center}
70
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   683
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   684
\noindent
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   685
In order to differentiate between these choices, we just need to
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   686
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
   687
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
   688
later does not affect their relative position because our algorithm does
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   689
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
   690
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
   691
traversing this information twice. This leads to an optimisation---if we
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   692
store the information for parse trees inside the regular expression,
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   693
update it when we do derivative on them, and collect the information
72
83b021fc7d29 interesting?
Chengsong
parents: 71
diff changeset
   694
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
   695
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
   696
doing the rest $n$ injections. This leads to Sulzmann and Lu's novel
71
0573615e41a3 new changes?
Chengsong
parents: 70
diff changeset
   697
idea of using bitcodes in derivatives.
42
Chengsong
parents: 41
diff changeset
   698
72
83b021fc7d29 interesting?
Chengsong
parents: 71
diff changeset
   699
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
   700
process of simplification of regular expressions. This is needed in
30
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   701
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
   702
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
   703
state-of-the-art.
30
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   704
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   705
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   706
\section{Simplification of Regular Expressions}
63
d3c22f809dde more proof-reading
Christian Urban <urbanc@in.tum.de>
parents: 62
diff changeset
   707
70
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   708
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
   709
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
   710
efficient regular expression parsing using DFAs~\cite{nielson11bcre}.
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   711
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
   712
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
   713
this project is that we want to introduce more aggressive
77
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   714
simplification rules in order to keep the size of derivatives small
70
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   715
throughout. This is because the main drawback of building successive
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   716
derivatives according to Brzozowski's definition is that they can grow
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   717
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
   718
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
   719
derivatives.  As a result, if implemented naively both algorithms by
70
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   720
Brzozowski and by Sulzmann and Lu are excruciatingly slow. For example
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   721
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
   722
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
   723
derivative regular expression with more than 8000 nodes (when viewed as
77
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   724
a tree). Operations like $\textit{der}$ and $\nullable$ need to traverse
63
d3c22f809dde more proof-reading
Christian Urban <urbanc@in.tum.de>
parents: 62
diff changeset
   725
such trees and consequently the bigger the size of the derivative the
66
8c8c82c0515f good to proofread
Chengsong
parents: 65
diff changeset
   726
slower the algorithm. 
35
f70e9ab4e680 psuedocode added
Chengsong
parents: 34
diff changeset
   727
70
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   728
Fortunately, one can simplify regular expressions after each derivative
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   729
step. Various simplifications of regular expressions are possible, such
77
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   730
as the simplification of $\ZERO + r$, $r + \ZERO$, $\ONE\cdot r$, $r
70
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   731
\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
   732
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
   733
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
   734
regular expressions match strings---although the latter is much harder
71
0573615e41a3 new changes?
Chengsong
parents: 70
diff changeset
   735
to establish. Some initial results in this regard have been
70
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   736
obtained in \cite{AusafDyckhoffUrban2016}. 
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   737
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   738
Unfortunately, the simplification rules outlined above  are not
77
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   739
sufficient to prevent a size explosion in all cases. We
70
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   740
believe a tighter bound can be achieved that prevents an explosion in
77
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   741
\emph{all} cases. Such a tighter bound is suggested by work of Antimirov who
70
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   742
proved that (partial) derivatives can be bound by the number of
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   743
characters contained in the initial regular expression
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   744
\cite{Antimirov95}. He defined the \emph{partial derivatives} of regular
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   745
expressions as follows:
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   746
52
25bbbb8b0e90 just in case of some accidents from erasing my work
Chengsong
parents: 51
diff changeset
   747
\begin{center}
25bbbb8b0e90 just in case of some accidents from erasing my work
Chengsong
parents: 51
diff changeset
   748
\begin{tabular}{lcl}
25bbbb8b0e90 just in case of some accidents from erasing my work
Chengsong
parents: 51
diff changeset
   749
 $\textit{pder} \; c \; 0$ & $\dn$ & $\emptyset$\\
25bbbb8b0e90 just in case of some accidents from erasing my work
Chengsong
parents: 51
diff changeset
   750
 $\textit{pder} \; c \; 1$ & $\dn$ & $\emptyset$ \\
25bbbb8b0e90 just in case of some accidents from erasing my work
Chengsong
parents: 51
diff changeset
   751
 $\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
   752
  $\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
   753
   $\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
   754
     & & $\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
   755
     & & $\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
   756
     $\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
   757
 \end{tabular}
25bbbb8b0e90 just in case of some accidents from erasing my work
Chengsong
parents: 51
diff changeset
   758
 \end{center}
70
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   759
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   760
\noindent
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   761
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
   762
regular expressions that are either $r$'s children expressions or a
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   763
concatenation of them. Antimirov has proved a tight bound of the size of
77
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   764
\emph{all} partial derivatives no matter what the string looks like.
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   765
Roughly speaking the size will be quadruple in the size of the regular
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   766
expression. If we want the size of derivatives in Sulzmann and Lu's
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   767
algorithm to stay equal or below this bound, we would need more
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   768
aggressive simplifications. Essentially we need to delete useless
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   769
$\ZERO$s and $\ONE$s, as well as deleting duplicates whenever possible.
71
0573615e41a3 new changes?
Chengsong
parents: 70
diff changeset
   770
For example, the parentheses in $(a+b) \cdot c + bc$ can be opened up to
77
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   771
get $a\cdot c +  b \cdot c + b \cdot c$, and then simplified to just $a \cdot
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   772
c + b \cdot c$. Another example is simplifying $(a^*+a) + (a^*+ \ONE) + (a
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   773
+\ONE)$ to just $a^*+a+\ONE$. Adding these more aggressive simplification
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   774
rules helps us to achieve the same size bound as that of the partial
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   775
derivatives. In order to implement the idea of ``spilling out alternatives''
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   776
and to make them compatible with the $\text{inj}$-mechanism, we use \emph{bitcodes}.
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   777
Bits and bitcodes (lists of bits) are just:
71
0573615e41a3 new changes?
Chengsong
parents: 70
diff changeset
   778
%This allows us to prove a tight
0573615e41a3 new changes?
Chengsong
parents: 70
diff changeset
   779
%bound on the size of regular expression during the running time of the
0573615e41a3 new changes?
Chengsong
parents: 70
diff changeset
   780
%algorithm if we can establish the connection between our simplification
0573615e41a3 new changes?
Chengsong
parents: 70
diff changeset
   781
%rules and partial derivatives.
35
f70e9ab4e680 psuedocode added
Chengsong
parents: 34
diff changeset
   782
f70e9ab4e680 psuedocode added
Chengsong
parents: 34
diff changeset
   783
 %We believe, and have generated test
f70e9ab4e680 psuedocode added
Chengsong
parents: 34
diff changeset
   784
%data, that a similar bound can be obtained for the derivatives in
f70e9ab4e680 psuedocode added
Chengsong
parents: 34
diff changeset
   785
%Sulzmann and Lu's algorithm. Let us give some details about this next.
30
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   786
72
83b021fc7d29 interesting?
Chengsong
parents: 71
diff changeset
   787
67
e974c5477a8c anotehr update
Chengsong
parents: 66
diff changeset
   788
\begin{center}
77
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   789
		$b ::=   S \mid  Z \qquad
43
Chengsong
parents: 42
diff changeset
   790
bs ::= [] \mid b:bs    
67
e974c5477a8c anotehr update
Chengsong
parents: 66
diff changeset
   791
$
e974c5477a8c anotehr update
Chengsong
parents: 66
diff changeset
   792
\end{center}
77
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   793
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   794
\noindent
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   795
The names $S$ and $Z$  here are quite arbitrary in order to avoid 
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   796
confusion with the regular expressions $\ZERO$ and $\ONE$. Bitcodes (or
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   797
bit-lists) can be used to encode values (or incomplete values) in a
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   798
compact form. This can be straightforwardly seen in the following
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   799
coding function from values to bitcodes: 
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   800
30
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   801
\begin{center}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   802
\begin{tabular}{lcl}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   803
  $\textit{code}(\Empty)$ & $\dn$ & $[]$\\
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   804
  $\textit{code}(\Char\,c)$ & $\dn$ & $[]$\\
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   805
  $\textit{code}(\Left\,v)$ & $\dn$ & $\Z :: code(v)$\\
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   806
  $\textit{code}(\Right\,v)$ & $\dn$ & $\S :: code(v)$\\
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   807
  $\textit{code}(\Seq\,v_1\,v_2)$ & $\dn$ & $code(v_1) \,@\, code(v_2)$\\
68
3c73d95cbfef more upd
Chengsong
parents: 67
diff changeset
   808
  $\textit{code}(\Stars\,[])$ & $\dn$ & $[\Z]$\\
3c73d95cbfef more upd
Chengsong
parents: 67
diff changeset
   809
  $\textit{code}(\Stars\,(v\!::\!vs))$ & $\dn$ & $\S :: code(v) \;@\;
30
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   810
                                                 code(\Stars\,vs)$
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   811
\end{tabular}    
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   812
\end{center} 
70
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   813
77
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   814
\noindent
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   815
Here $\textit{code}$ encodes a value into a bitcodes by converting
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   816
$\Left$ into $\Z$, $\Right$ into $\S$, the start point of a non-empty
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   817
star iteration into $\S$, and the border where a local star terminates
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   818
into $\Z$. This coding is lossy, as it throws away the information about
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   819
characters, and also does not encode the ``boundary'' between two
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   820
sequence values. Moreover, with only the bitcode we cannot even tell
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   821
whether the $\S$s and $\Z$s are for $\Left/\Right$ or $\Stars$. The
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   822
reason for choosing this compact way of storing information is that the
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   823
relatively small size of bits can be easily manipulated and ``moved
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   824
around'' in a regular expression. In order to recover values, we will 
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   825
need the corresponding regular expression as an extra information. This
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   826
means the decoding function is defined as:
70
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   827
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   828
37
17d8e7599a01 new changes
Chengsong
parents: 36
diff changeset
   829
%\begin{definition}[Bitdecoding of Values]\mbox{}
36
Chengsong
parents: 35
diff changeset
   830
\begin{center}
Chengsong
parents: 35
diff changeset
   831
\begin{tabular}{@{}l@{\hspace{1mm}}c@{\hspace{1mm}}l@{}}
Chengsong
parents: 35
diff changeset
   832
  $\textit{decode}'\,bs\,(\ONE)$ & $\dn$ & $(\Empty, bs)$\\
Chengsong
parents: 35
diff changeset
   833
  $\textit{decode}'\,bs\,(c)$ & $\dn$ & $(\Char\,c, bs)$\\
Chengsong
parents: 35
diff changeset
   834
  $\textit{decode}'\,(\Z\!::\!bs)\;(r_1 + r_2)$ & $\dn$ &
Chengsong
parents: 35
diff changeset
   835
     $\textit{let}\,(v, bs_1) = \textit{decode}'\,bs\,r_1\;\textit{in}\;
Chengsong
parents: 35
diff changeset
   836
       (\Left\,v, bs_1)$\\
Chengsong
parents: 35
diff changeset
   837
  $\textit{decode}'\,(\S\!::\!bs)\;(r_1 + r_2)$ & $\dn$ &
Chengsong
parents: 35
diff changeset
   838
     $\textit{let}\,(v, bs_1) = \textit{decode}'\,bs\,r_2\;\textit{in}\;
Chengsong
parents: 35
diff changeset
   839
       (\Right\,v, bs_1)$\\                           
Chengsong
parents: 35
diff changeset
   840
  $\textit{decode}'\,bs\;(r_1\cdot r_2)$ & $\dn$ &
Chengsong
parents: 35
diff changeset
   841
        $\textit{let}\,(v_1, bs_1) = \textit{decode}'\,bs\,r_1\;\textit{in}$\\
Chengsong
parents: 35
diff changeset
   842
  & &   $\textit{let}\,(v_2, bs_2) = \textit{decode}'\,bs_1\,r_2$\\
Chengsong
parents: 35
diff changeset
   843
  & &   \hspace{35mm}$\textit{in}\;(\Seq\,v_1\,v_2, bs_2)$\\
Chengsong
parents: 35
diff changeset
   844
  $\textit{decode}'\,(\Z\!::\!bs)\,(r^*)$ & $\dn$ & $(\Stars\,[], bs)$\\
Chengsong
parents: 35
diff changeset
   845
  $\textit{decode}'\,(\S\!::\!bs)\,(r^*)$ & $\dn$ & 
Chengsong
parents: 35
diff changeset
   846
         $\textit{let}\,(v, bs_1) = \textit{decode}'\,bs\,r\;\textit{in}$\\
Chengsong
parents: 35
diff changeset
   847
  & &   $\textit{let}\,(\Stars\,vs, bs_2) = \textit{decode}'\,bs_1\,r^*$\\
Chengsong
parents: 35
diff changeset
   848
  & &   \hspace{35mm}$\textit{in}\;(\Stars\,v\!::\!vs, bs_2)$\bigskip\\
Chengsong
parents: 35
diff changeset
   849
  
Chengsong
parents: 35
diff changeset
   850
  $\textit{decode}\,bs\,r$ & $\dn$ &
Chengsong
parents: 35
diff changeset
   851
     $\textit{let}\,(v, bs') = \textit{decode}'\,bs\,r\;\textit{in}$\\
Chengsong
parents: 35
diff changeset
   852
  & & $\textit{if}\;bs' = []\;\textit{then}\;\textit{Some}\,v\;
Chengsong
parents: 35
diff changeset
   853
       \textit{else}\;\textit{None}$                       
Chengsong
parents: 35
diff changeset
   854
\end{tabular}    
Chengsong
parents: 35
diff changeset
   855
\end{center}    
37
17d8e7599a01 new changes
Chengsong
parents: 36
diff changeset
   856
%\end{definition}
30
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
   857
77
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   858
Sulzmann and Lu's integrated the bitcodes into regular expressions to
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   859
create annotated regular expressions \cite{Sulzmann2014}.
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   860
\emph{Annotated regular expressions} are defined by the following
70
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   861
grammar:
43
Chengsong
parents: 42
diff changeset
   862
Chengsong
parents: 42
diff changeset
   863
\begin{center}
Chengsong
parents: 42
diff changeset
   864
\begin{tabular}{lcl}
Chengsong
parents: 42
diff changeset
   865
  $\textit{a}$ & $::=$  & $\textit{ZERO}$\\
Chengsong
parents: 42
diff changeset
   866
                  & $\mid$ & $\textit{ONE}\;\;bs$\\
Chengsong
parents: 42
diff changeset
   867
                  & $\mid$ & $\textit{CHAR}\;\;bs\,c$\\
72
83b021fc7d29 interesting?
Chengsong
parents: 71
diff changeset
   868
                  & $\mid$ & $\textit{ALT}\;\;bs\,a_1 \, a_2$\\
43
Chengsong
parents: 42
diff changeset
   869
                  & $\mid$ & $\textit{SEQ}\;\;bs\,a_1\,a_2$\\
Chengsong
parents: 42
diff changeset
   870
                  & $\mid$ & $\textit{STAR}\;\;bs\,a$
Chengsong
parents: 42
diff changeset
   871
\end{tabular}    
Chengsong
parents: 42
diff changeset
   872
\end{center}  
72
83b021fc7d29 interesting?
Chengsong
parents: 71
diff changeset
   873
%(in \textit{ALT})
77
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   874
43
Chengsong
parents: 42
diff changeset
   875
\noindent
77
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   876
where $bs$ stands for bitcodes, and $a$  for $\bold{a}$nnotated regular
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   877
expressions. We will show that these bitcodes encode information about
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   878
the (POSIX) value that should be generated by the Sulzmann and Lu
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   879
algorithm.
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   880
43
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
77
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   905
We use up arrows here to indicate that the basic un-annotated regular
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   906
expressions are ``lifted up'' into something slightly more complex. In the
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   907
fourth clause, $\textit{fuse}$ is an auxiliary function that helps to
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   908
attach bits to the front of an annotated regular expression. Its
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   909
definition is as follows:
70
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   910
44
4d674a971852 another changes. have written more. but havent typed them. tomorrow will continue.
Chengsong
parents: 43
diff changeset
   911
\begin{center}
4d674a971852 another changes. have written more. but havent typed them. tomorrow will continue.
Chengsong
parents: 43
diff changeset
   912
\begin{tabular}{lcl}
77
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   913
  $\textit{fuse}\;bs\,(\textit{ZERO})$ & $\dn$ & $\textit{ZERO}$\\
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   914
  $\textit{fuse}\;bs\,(\textit{ONE}\,bs')$ & $\dn$ &
44
4d674a971852 another changes. have written more. but havent typed them. tomorrow will continue.
Chengsong
parents: 43
diff changeset
   915
     $\textit{ONE}\,(bs\,@\,bs')$\\
77
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   916
  $\textit{fuse}\;bs\,(\textit{CHAR}\,bs'\,c)$ & $\dn$ &
44
4d674a971852 another changes. have written more. but havent typed them. tomorrow will continue.
Chengsong
parents: 43
diff changeset
   917
     $\textit{CHAR}\,(bs\,@\,bs')\,c$\\
77
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   918
  $\textit{fuse}\;bs\,(\textit{ALT}\,bs'\,a_1\,a_2)$ & $\dn$ &
44
4d674a971852 another changes. have written more. but havent typed them. tomorrow will continue.
Chengsong
parents: 43
diff changeset
   919
     $\textit{ALT}\,(bs\,@\,bs')\,a_1\,a_2$\\
77
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   920
  $\textit{fuse}\;bs\,(\textit{SEQ}\,bs'\,a_1\,a_2)$ & $\dn$ &
44
4d674a971852 another changes. have written more. but havent typed them. tomorrow will continue.
Chengsong
parents: 43
diff changeset
   921
     $\textit{SEQ}\,(bs\,@\,bs')\,a_1\,a_2$\\
77
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   922
  $\textit{fuse}\;bs\,(\textit{STAR}\,bs'\,a)$ & $\dn$ &
44
4d674a971852 another changes. have written more. but havent typed them. tomorrow will continue.
Chengsong
parents: 43
diff changeset
   923
     $\textit{STAR}\,(bs\,@\,bs')\,a$
4d674a971852 another changes. have written more. but havent typed them. tomorrow will continue.
Chengsong
parents: 43
diff changeset
   924
\end{tabular}    
4d674a971852 another changes. have written more. but havent typed them. tomorrow will continue.
Chengsong
parents: 43
diff changeset
   925
\end{center}  
4d674a971852 another changes. have written more. but havent typed them. tomorrow will continue.
Chengsong
parents: 43
diff changeset
   926
70
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   927
\noindent
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   928
After internalise we do successive derivative operations on the
77
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   929
annotated regular expressions. This derivative operation is the same as
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   930
what we previously have for the simple regular expressions, except that
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   931
we beed to take special care of the bitcodes:\comment{You need to be consitent with  ALTS and ALT; ALT is just 
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   932
an abbreviation; derivations and so on are defined for ALTS}
70
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   933
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   934
 %\begin{definition}{bder}
36
Chengsong
parents: 35
diff changeset
   935
\begin{center}
Chengsong
parents: 35
diff changeset
   936
  \begin{tabular}{@{}lcl@{}}
77
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   937
  $(\textit{ZERO})\,\backslash c$ & $\dn$ & $\textit{ZERO}$\\  
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   938
  $(\textit{ONE}\;bs)\,\backslash c$ & $\dn$ & $\textit{ZERO}$\\  
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   939
  $(\textit{CHAR}\;bs\,d)\,\backslash c$ & $\dn$ &
36
Chengsong
parents: 35
diff changeset
   940
        $\textit{if}\;c=d\; \;\textit{then}\;
Chengsong
parents: 35
diff changeset
   941
         \textit{ONE}\;bs\;\textit{else}\;\textit{ZERO}$\\  
77
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   942
  $(\textit{ALT}\;bs\,a_1\,a_2)\,\backslash c$ & $\dn$ &
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   943
        $\textit{ALT}\;bs\,(a_1\,\backslash c)\,(a_2\,\backslash c)$\\
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   944
  $(\textit{SEQ}\;bs\,a_1\,a_2)\,\backslash c$ & $\dn$ &
36
Chengsong
parents: 35
diff changeset
   945
     $\textit{if}\;\textit{bnullable}\,a_1$\\
77
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   946
  & &$\textit{then}\;\textit{ALT}\,bs\,(\textit{SEQ}\,[]\,(a_1\,\backslash c)\,a_2)$\\
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   947
  & &$\phantom{\textit{then}\;\textit{ALT}\,bs\,}(\textit{fuse}\,(\textit{bmkeps}\,a_1)\,(a_2\,\backslash c))$\\
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   948
  & &$\textit{else}\;\textit{SEQ}\,bs\,(a_1\,\backslash c)\,a_2$\\
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   949
  $(\textit{STAR}\,bs\,a)\,\backslash c$ & $\dn$ &
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   950
      $\textit{SEQ}\;bs\,(\textit{fuse}\, [\Z] (r\,\backslash c))\,
36
Chengsong
parents: 35
diff changeset
   951
       (\textit{STAR}\,[]\,r)$
Chengsong
parents: 35
diff changeset
   952
\end{tabular}    
Chengsong
parents: 35
diff changeset
   953
\end{center}    
37
17d8e7599a01 new changes
Chengsong
parents: 36
diff changeset
   954
%\end{definition}
74
9e791ef6022f just a merge - no changes
Christian Urban <urbanc@in.tum.de>
parents: 72
diff changeset
   955
77
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   956
\noindent
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   957
For instance, when we unfold $\textit{STAR} \; bs \; a$ into a sequence,
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   958
we need to attach an additional bit $Z$ to the front of $r \backslash c$
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   959
to indicate that there is one more star iteration. Also the $SEQ$ clause
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   960
is more subtle---when $a_1$ is $\textit{bnullable}$ (here
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   961
\textit{bnullable} is exactly the same as $\textit{nullable}$, except
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   962
that it is for annotated regular expressions, therefore we omit the
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   963
definition). Assume that $bmkeps$ correctly extracts the bitcode for how
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   964
$a_1$ matches the string prior to character $c$ (more on this later),
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   965
then the right branch of $ALTS$, which is $fuse \; bmkeps \;  a_1 (a_2
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   966
\backslash c)$ will collapse the regular expression $a_1$(as it has
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   967
already been fully matched) and store the parsing information at the
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   968
head of the regular expression $a_2 \backslash c$ by fusing to it. The
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   969
bitsequence $bs$, which was initially attached to the head of $SEQ$, has
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   970
now been elevated to the top-level of ALT, as this information will be
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   971
needed whichever way the $SEQ$ is matched--no matter whether $c$ belongs
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   972
to $a_1$ or $ a_2$. After building these derivatives and maintaining all
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   973
the lexing information, we complete the lexing by collecting the
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   974
bitcodes using a generalised version of the $\textit{mkeps}$ function
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   975
for annotated regular expressions, called $\textit{bmkeps}$:
44
4d674a971852 another changes. have written more. but havent typed them. tomorrow will continue.
Chengsong
parents: 43
diff changeset
   976
4d674a971852 another changes. have written more. but havent typed them. tomorrow will continue.
Chengsong
parents: 43
diff changeset
   977
37
17d8e7599a01 new changes
Chengsong
parents: 36
diff changeset
   978
%\begin{definition}[\textit{bmkeps}]\mbox{}
36
Chengsong
parents: 35
diff changeset
   979
\begin{center}
Chengsong
parents: 35
diff changeset
   980
\begin{tabular}{lcl}
77
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   981
  $\textit{bmkeps}\,(\textit{ONE}\;bs)$ & $\dn$ & $bs$\\
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   982
  $\textit{bmkeps}\,(\textit{ALT}\;bs\,a_1\,a_2)$ & $\dn$ &
36
Chengsong
parents: 35
diff changeset
   983
     $\textit{if}\;\textit{bnullable}\,a_1$\\
Chengsong
parents: 35
diff changeset
   984
  & &$\textit{then}\;bs\,@\,\textit{bmkeps}\,a_1$\\
Chengsong
parents: 35
diff changeset
   985
  & &$\textit{else}\;bs\,@\,\textit{bmkeps}\,a_2$\\
77
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   986
  $\textit{bmkeps}\,(\textit{SEQ}\;bs\,a_1\,a_2)$ & $\dn$ &
36
Chengsong
parents: 35
diff changeset
   987
     $bs \,@\,\textit{bmkeps}\,a_1\,@\, \textit{bmkeps}\,a_2$\\
77
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   988
  $\textit{bmkeps}\,(\textit{STAR}\;bs\,a)$ & $\dn$ &
36
Chengsong
parents: 35
diff changeset
   989
     $bs \,@\, [\S]$
Chengsong
parents: 35
diff changeset
   990
\end{tabular}    
Chengsong
parents: 35
diff changeset
   991
\end{center}    
37
17d8e7599a01 new changes
Chengsong
parents: 36
diff changeset
   992
%\end{definition}
70
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   993
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   994
\noindent
77
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   995
This function completes the value information by travelling along the
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   996
path of the regular expression that corresponds to a POSIX value and
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   997
collecting all the bitcodes, and using $S$ to indicate the end of star
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   998
iterations. If we take the bitcodes produced by $\textit{bmkeps}$ and
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   999
decode them, we get the value we expect. The corresponding lexing
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
  1000
algorithm looks as follows:
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
  1001
37
17d8e7599a01 new changes
Chengsong
parents: 36
diff changeset
  1002
\begin{center}
17d8e7599a01 new changes
Chengsong
parents: 36
diff changeset
  1003
\begin{tabular}{lcl}
17d8e7599a01 new changes
Chengsong
parents: 36
diff changeset
  1004
  $\textit{blexer}\;r\,s$ & $\dn$ &
17d8e7599a01 new changes
Chengsong
parents: 36
diff changeset
  1005
      $\textit{let}\;a = (r^\uparrow)\backslash s\;\textit{in}$\\                
17d8e7599a01 new changes
Chengsong
parents: 36
diff changeset
  1006
  & & $\;\;\textit{if}\; \textit{bnullable}(a)$\\
17d8e7599a01 new changes
Chengsong
parents: 36
diff changeset
  1007
  & & $\;\;\textit{then}\;\textit{decode}\,(\textit{bmkeps}\,a)\,r$\\
17d8e7599a01 new changes
Chengsong
parents: 36
diff changeset
  1008
  & & $\;\;\textit{else}\;\textit{None}$
17d8e7599a01 new changes
Chengsong
parents: 36
diff changeset
  1009
\end{tabular}
17d8e7599a01 new changes
Chengsong
parents: 36
diff changeset
  1010
\end{center}
77
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
  1011
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
  1012
\noindent
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
  1013
In this definition $_\backslash s$ is the  generalisation  of the derivative
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
  1014
operation from characters to strings (just like the derivatives for un-annotated
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
  1015
regular expressions).
30
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
  1016
77
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
  1017
The main point of the bitcodes and annotated regular expressions is that
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
  1018
we can apply rather aggressive (in terms of size) simplification rules
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
  1019
in order to keep derivatives small. We have developed such
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
  1020
``aggressive'' simplification rules and generated test data that show
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
  1021
that the expected bound can be achieved. Obviously we could only
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
  1022
partially cover  the search space as there are infinitely many regular
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
  1023
expressions and strings. 
30
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
  1024
77
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
  1025
One modification we introduced is to allow a list of annotated regular
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
  1026
expressions in the \textit{ALTS} constructor. This allows us to not just
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
  1027
delete unnecessary $\ZERO$s and $\ONE$s from regular expressions, but
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
  1028
also unnecessary ``copies'' of regular expressions (very similar to
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
  1029
simplifying $r + r$ to just $r$, but in a more general setting). Another
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
  1030
modification is that we use simplification rules inspired by Antimirov's
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
  1031
work on partial derivatives. They maintain the idea that only the first
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
  1032
``copy'' of a regular expression in an alternative contributes to the
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
  1033
calculation of a POSIX value. All subsequent copies can be pruned away from
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
  1034
the regular expression. A recursive definition of our  simplification function 
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
  1035
that looks somewhat similar to our Scala code is given below:\comment{Use $\ZERO$, $\ONE$ and so on. 
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
  1036
Is it $ALT$ or $ALTS$?}\\
49
d256aabe88f3 still wont comiple hhh
Chengsong
parents: 48
diff changeset
  1037
52
25bbbb8b0e90 just in case of some accidents from erasing my work
Chengsong
parents: 51
diff changeset
  1038
\begin{center}
25bbbb8b0e90 just in case of some accidents from erasing my work
Chengsong
parents: 51
diff changeset
  1039
  \begin{tabular}{@{}lcl@{}}
77
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
  1040
   
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
  1041
  $\textit{simp} \; (\textit{SEQ}\;bs\,a_1\,a_2)$ & $\dn$ & $ (\textit{simp} \; a_1, \textit{simp}  \; a_2) \; \textit{match} $ \\
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
  1042
   &&$\quad\textit{case} \; (0, \_) \Rightarrow  0$ \\
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
  1043
   &&$\quad\textit{case} \; (\_, 0) \Rightarrow  0$ \\
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
  1044
   &&$\quad\textit{case} \;  (1, a_2') \Rightarrow  \textit{fuse} \; bs \;  a_2'$ \\
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
  1045
   &&$\quad\textit{case} \; (a_1', 1) \Rightarrow  \textit{fuse} \; bs \;  a_1'$ \\
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
  1046
   &&$\quad\textit{case} \; (a_1', a_2') \Rightarrow  \textit{SEQ} \; bs \; a_1' \;  a_2'$ \\
52
25bbbb8b0e90 just in case of some accidents from erasing my work
Chengsong
parents: 51
diff changeset
  1047
77
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
  1048
  $\textit{simp} \; (\textit{ALTS}\;bs\,as)$ & $\dn$ & $\textit{distinct}( \textit{flatten} ( \textit{map simp as})) \; \textit{match} $ \\
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
  1049
  &&$\quad\textit{case} \; [] \Rightarrow  0$ \\
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
  1050
   &&$\quad\textit{case} \; a :: [] \Rightarrow  \textit{fuse bs a}$ \\
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
  1051
   &&$\quad\textit{case} \;  as' \Rightarrow  \textit{ALT}\;bs\;as'$\\ 
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
  1052
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
  1053
   $\textit{simp} \; a$ & $\dn$ & $\textit{a} \qquad \textit{otherwise}$   
52
25bbbb8b0e90 just in case of some accidents from erasing my work
Chengsong
parents: 51
diff changeset
  1054
\end{tabular}    
25bbbb8b0e90 just in case of some accidents from erasing my work
Chengsong
parents: 51
diff changeset
  1055
\end{center}    
47
d2a7e87ea6e1 will not compile, just text
Chengsong
parents: 46
diff changeset
  1056
77
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
  1057
\noindent
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
  1058
The simplification does a pattern matching on the regular expression.
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
  1059
When it detected that the regular expression is an alternative or
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
  1060
sequence, it will try to simplify its children regular expressions
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
  1061
recursively and then see if one of the children turn into $\ZERO$ or
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
  1062
$\ONE$, which might trigger further simplification at the current level.
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
  1063
The most involved part is the $\textit{ALTS}$ clause, where we use two
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
  1064
auxiliary functions flatten and distinct to open up nested
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
  1065
$\textit{ALTS}$ and reduce as many duplicates as possible. Function
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
  1066
distinct  keeps the first occurring copy only and remove all later ones
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
  1067
when detected duplicates. Function flatten opens up nested \textit{ALT}.
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
  1068
Its recursive definition is given below:
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
  1069
53
3ec403f650a8 readable version
Chengsong
parents: 52
diff changeset
  1070
 \begin{center}
3ec403f650a8 readable version
Chengsong
parents: 52
diff changeset
  1071
  \begin{tabular}{@{}lcl@{}}
70
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
  1072
  $\textit{flatten} \; (\textit{ALT}\;bs\,as) :: as'$ & $\dn$ & $(\textit{map} \;
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
  1073
     (\textit{fuse}\;bs)\; \textit{as}) \; @ \; \textit{flatten} \; as' $ \\
53
3ec403f650a8 readable version
Chengsong
parents: 52
diff changeset
  1074
  $\textit{flatten} \; \textit{ZERO} :: as'$ & $\dn$ & $ \textit{flatten} \;  as' $ \\
70
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
  1075
    $\textit{flatten} \; a :: as'$ & $\dn$ & $a :: \textit{flatten} \; as'$ \quad(otherwise) 
53
3ec403f650a8 readable version
Chengsong
parents: 52
diff changeset
  1076
\end{tabular}    
3ec403f650a8 readable version
Chengsong
parents: 52
diff changeset
  1077
\end{center}  
3ec403f650a8 readable version
Chengsong
parents: 52
diff changeset
  1078
70
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
  1079
\noindent
77
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
  1080
Here flatten behaves like the traditional functional programming flatten
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
  1081
function, except that it also removes $\ZERO$s. What it does is
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
  1082
basically removing parentheses like changing $a+(b+c)$ into $a+b+c$.
47
d2a7e87ea6e1 will not compile, just text
Chengsong
parents: 46
diff changeset
  1083
77
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
  1084
Suppose we apply simplification after each derivative step, and view
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
  1085
these two operations as an atomic one: $a \backslash_{simp}\,c \dn
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
  1086
\textit{simp}(a \backslash c)$. Then we can use the previous natural
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
  1087
extension from derivative w.r.t.~character to derivative
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
  1088
w.r.t.~string:\comment{simp in  the [] case?}
53
3ec403f650a8 readable version
Chengsong
parents: 52
diff changeset
  1089
3ec403f650a8 readable version
Chengsong
parents: 52
diff changeset
  1090
\begin{center}
3ec403f650a8 readable version
Chengsong
parents: 52
diff changeset
  1091
\begin{tabular}{lcl}
77
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
  1092
$r \backslash_{simp} (c\!::\!s) $ & $\dn$ & $(r \backslash_{simp}\, c) \backslash_{simp}\, s$ \\
53
3ec403f650a8 readable version
Chengsong
parents: 52
diff changeset
  1093
$r \backslash [\,] $ & $\dn$ & $r$
3ec403f650a8 readable version
Chengsong
parents: 52
diff changeset
  1094
\end{tabular}
3ec403f650a8 readable version
Chengsong
parents: 52
diff changeset
  1095
\end{center}
3ec403f650a8 readable version
Chengsong
parents: 52
diff changeset
  1096
77
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
  1097
\noindent
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
  1098
we obtain an optimised version of the algorithm:
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
  1099
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
  1100
 \begin{center}
53
3ec403f650a8 readable version
Chengsong
parents: 52
diff changeset
  1101
\begin{tabular}{lcl}
3ec403f650a8 readable version
Chengsong
parents: 52
diff changeset
  1102
  $\textit{blexer\_simp}\;r\,s$ & $\dn$ &
77
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
  1103
      $\textit{let}\;a = (r^\uparrow)\backslash_{simp}\, s\;\textit{in}$\\                
53
3ec403f650a8 readable version
Chengsong
parents: 52
diff changeset
  1104
  & & $\;\;\textit{if}\; \textit{bnullable}(a)$\\
3ec403f650a8 readable version
Chengsong
parents: 52
diff changeset
  1105
  & & $\;\;\textit{then}\;\textit{decode}\,(\textit{bmkeps}\,a)\,r$\\
3ec403f650a8 readable version
Chengsong
parents: 52
diff changeset
  1106
  & & $\;\;\textit{else}\;\textit{None}$
3ec403f650a8 readable version
Chengsong
parents: 52
diff changeset
  1107
\end{tabular}
3ec403f650a8 readable version
Chengsong
parents: 52
diff changeset
  1108
\end{center}
48
bbefcf7351f2 still will not compile
Chengsong
parents: 47
diff changeset
  1109
77
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
  1110
\noindent
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
  1111
This algorithm keeps the regular expression size small, for example,
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
  1112
with this simplification our previous $(a + aa)^*$ example's 8000 nodes
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
  1113
will be reduced to just 6 and stays constant, no matter how long the
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
  1114
input string is.
35
f70e9ab4e680 psuedocode added
Chengsong
parents: 34
diff changeset
  1115
30
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
  1116
35
f70e9ab4e680 psuedocode added
Chengsong
parents: 34
diff changeset
  1117
70
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
  1118
\section{Current Work}
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
  1119
77
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
  1120
We are currently engaged in two tasks related to this algorithm. The
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
  1121
first task is proving that our simplification rules actually do not
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
  1122
affect the POSIX value that should be generated by the algorithm
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
  1123
according to the specification of a POSIX value and furthermore obtain a
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
  1124
much tighter bound on the sizes of derivatives. The result is that our
49
d256aabe88f3 still wont comiple hhh
Chengsong
parents: 48
diff changeset
  1125
algorithm should be correct and faster on all inputs.  The original
d256aabe88f3 still wont comiple hhh
Chengsong
parents: 48
diff changeset
  1126
blow-up, as observed in JavaScript, Python and Java, would be excluded
77
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
  1127
from happening in our algorithm. For this proof we use the theorem prover
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
  1128
Isabelle. Once completed, this result will advance the state-of-the-art:
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
  1129
Sulzmann and Lu wrote in their paper~\cite{Sulzmann2014} about the
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
  1130
bitcoded ``incremental parsing method'' (that is the lexing algorithm
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
  1131
outlined in this section):
30
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
  1132
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
  1133
\begin{quote}\it
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
  1134
  ``Correctness Claim: We further claim that the incremental parsing
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
  1135
  method in Figure~5 in combination with the simplification steps in
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
  1136
  Figure 6 yields POSIX parse trees. We have tested this claim
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
  1137
  extensively by using the method in Figure~3 as a reference but yet
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
  1138
  have to work out all proof details.''
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
  1139
\end{quote}  
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
  1140
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
  1141
\noindent
77
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
  1142
We would settle this correctness claim. It is relatively straightforward
74
9e791ef6022f just a merge - no changes
Christian Urban <urbanc@in.tum.de>
parents: 72
diff changeset
  1143
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
  1144
derivative that corresponds to a POSIX value remains intact and can
77
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
  1145
still be collected, in other words, we can show that\comment{Double-check....I think this  is not the case}
74
9e791ef6022f just a merge - no changes
Christian Urban <urbanc@in.tum.de>
parents: 72
diff changeset
  1146
71
0573615e41a3 new changes?
Chengsong
parents: 70
diff changeset
  1147
\begin{center}
0573615e41a3 new changes?
Chengsong
parents: 70
diff changeset
  1148
$\textit{bmkeps} \; r = \textit{bmkeps} \; \textit{simp} \; r\;( r\; \textit{nullable})$
0573615e41a3 new changes?
Chengsong
parents: 70
diff changeset
  1149
\end{center}
74
9e791ef6022f just a merge - no changes
Christian Urban <urbanc@in.tum.de>
parents: 72
diff changeset
  1150
9e791ef6022f just a merge - no changes
Christian Urban <urbanc@in.tum.de>
parents: 72
diff changeset
  1151
\noindent
9e791ef6022f just a merge - no changes
Christian Urban <urbanc@in.tum.de>
parents: 72
diff changeset
  1152
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
  1153
additional $r$ in $r+r$  does not delete important POSIX information in
77
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
  1154
a regular expression. The hard part of this proof is to establish that
74
9e791ef6022f just a merge - no changes
Christian Urban <urbanc@in.tum.de>
parents: 72
diff changeset
  1155
71
0573615e41a3 new changes?
Chengsong
parents: 70
diff changeset
  1156
\begin{center}
0573615e41a3 new changes?
Chengsong
parents: 70
diff changeset
  1157
$\textit{bmkeps} \; \textit{blexer}\_{simp} \; r = \textit{bmkeps} \; \textit{blexer} \; \textit{simp} \; r$
0573615e41a3 new changes?
Chengsong
parents: 70
diff changeset
  1158
\end{center}
74
9e791ef6022f just a merge - no changes
Christian Urban <urbanc@in.tum.de>
parents: 72
diff changeset
  1159
77
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
  1160
\noindent\comment{OK from here on you still need to work. Did not read.}
71
0573615e41a3 new changes?
Chengsong
parents: 70
diff changeset
  1161
That is, if we do derivative on regular expression r and the simplified version, 
0573615e41a3 new changes?
Chengsong
parents: 70
diff changeset
  1162
they can still provide the same POSIX value if there is one . 
0573615e41a3 new changes?
Chengsong
parents: 70
diff changeset
  1163
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
  1164
  might become very different regular expressions after repeated application of $\textit{simp}$ and derivative.
0573615e41a3 new changes?
Chengsong
parents: 70
diff changeset
  1165
The crucial point is to find the indispensable information of 
0573615e41a3 new changes?
Chengsong
parents: 70
diff changeset
  1166
a regular expression and how it is kept intact during simplification so that it performs 
0573615e41a3 new changes?
Chengsong
parents: 70
diff changeset
  1167
as good as a regular expression that has not been simplified in the subsequent derivative operations.
0573615e41a3 new changes?
Chengsong
parents: 70
diff changeset
  1168
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
  1169
\\definition of retrieve\\
77
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
  1170
 
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
  1171
This function assembled the bitcode that corresponds to a parse tree for
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
  1172
how the current derivative matches the suffix of the string(the
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
  1173
characters that have not yet appeared, but is stored in the value).
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
  1174
Sulzmann and Lu used this to connect the bitcoded algorithm to the older
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
  1175
algorithm by the following equation:
058133a9ffe0 proof-read
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
  1176
 
72
83b021fc7d29 interesting?
Chengsong
parents: 71
diff changeset
  1177
 \begin{center}
83b021fc7d29 interesting?
Chengsong
parents: 71
diff changeset
  1178
 $inj \;a\; c \; v = \textit{decode} \; (\textit{retrieve}\; ((\textit{internalise}\; r)\backslash_{simp} c) v)$
83b021fc7d29 interesting?
Chengsong
parents: 71
diff changeset
  1179
 \end{center}
83b021fc7d29 interesting?
Chengsong
parents: 71
diff changeset
  1180
 A little fact that needs to be stated to help comprehension:
83b021fc7d29 interesting?
Chengsong
parents: 71
diff changeset
  1181
 \begin{center}
83b021fc7d29 interesting?
Chengsong
parents: 71
diff changeset
  1182
 $r^\uparrow = a$($a$ stands for $\textit{annotated}).$
83b021fc7d29 interesting?
Chengsong
parents: 71
diff changeset
  1183
 \end{center}
83b021fc7d29 interesting?
Chengsong
parents: 71
diff changeset
  1184
 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
  1185
 Our purpose of using this, however, is try to establish \\
53
3ec403f650a8 readable version
Chengsong
parents: 52
diff changeset
  1186
$ \textit{retrieve} \; a \; v \;=\; \textit{retrieve}  \; \textit{simp}(a) \; v'.$\\
3ec403f650a8 readable version
Chengsong
parents: 52
diff changeset
  1187
 The idea is that using $v'$,
71
0573615e41a3 new changes?
Chengsong
parents: 70
diff changeset
  1188
  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
  1189
 After establishing this, we might be able to finally bridge the gap of proving\\
3ec403f650a8 readable version
Chengsong
parents: 52
diff changeset
  1190
 $\textit{retrieve} \; r   \backslash  s \; v = \;\textit{retrieve} \; \textit{simp}(r)  \backslash  s \; v'$\\
3ec403f650a8 readable version
Chengsong
parents: 52
diff changeset
  1191
 and subsequently\\
3ec403f650a8 readable version
Chengsong
parents: 52
diff changeset
  1192
 $\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
  1193
 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
  1194
72
83b021fc7d29 interesting?
Chengsong
parents: 71
diff changeset
  1195
70
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
  1196
The second task is to speed up the more aggressive simplification.
cab5eab1f6f1 more proofreading
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
  1197
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
  1198
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
  1199
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
  1200
again the connection to DFAs. This is very much work in progress.
30
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
  1201
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
  1202
\section{Conclusion}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
  1203
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
  1204
In this PhD-project we are interested in fast algorithms for regular
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
  1205
expression matching. While this seems to be a ``settled'' area, in
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
  1206
fact interesting research questions are popping up as soon as one steps
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
  1207
outside the classic automata theory (for example in terms of what kind
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
  1208
of regular expressions are supported). The reason why it is
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
  1209
interesting for us to look at the derivative approach introduced by
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
  1210
Brzozowski for regular expression matching, and then much further
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
  1211
developed by Sulzmann and Lu, is that derivatives can elegantly deal
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
  1212
with some of the regular expressions that are of interest in ``real
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
  1213
life''. This includes the not-regular expression, written $\neg\,r$
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
  1214
(that is all strings that are not recognised by $r$), but also bounded
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
  1215
regular expressions such as $r^{\{n\}}$ and $r^{\{n..m\}}$). There is
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
  1216
also hope that the derivatives can provide another angle for how to
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
  1217
deal more efficiently with back-references, which are one of the
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
  1218
reasons why regular expression engines in JavaScript, Python and Java
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
  1219
choose to not implement the classic automata approach of transforming
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
  1220
regular expressions into NFAs and then DFAs---because we simply do not
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
  1221
know how such back-references can be represented by DFAs.
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
  1222
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
  1223
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
  1224
\bibliographystyle{plain}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
  1225
\bibliography{root}
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
  1226
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
  1227
bd9eb959dbce changed file name to ninems
Chengsong
parents:
diff changeset
  1228
\end{document}