ChengsongPhdThesis/ChengsongPhDThesis.tex
author Christian Urban <christian.urban@kcl.ac.uk>
Tue, 22 Mar 2022 11:08:43 +0000
changeset 461 c4b6906068a9
parent 453 d68b9db4c9ec
permissions -rw-r--r--
updated paper
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
438
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
     1
\documentclass[a4paper,UKenglish]{lipics}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
     2
\usepackage{graphic}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
     3
\usepackage{data}
453
Chengsong
parents: 444
diff changeset
     4
438
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
     5
%\usepackage{algorithm}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
     6
\usepackage{amsmath}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
     7
\usepackage[noend]{algpseudocode}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
     8
\usepackage{enumitem}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
     9
\usepackage{nccmath}
453
Chengsong
parents: 444
diff changeset
    10
\usepackage{tikz-cd}
438
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
    11
\usetikzlibrary{positioning}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
    12
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
    13
\definecolor{darkblue}{rgb}{0,0,0.6}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
    14
\hypersetup{colorlinks=true,allcolors=darkblue}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
    15
\newcommand{\comment}[1]%
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
    16
{{\color{red}$\Rightarrow$}\marginpar{\raggedright\small{\bf\color{red}#1}}}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
    17
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
    18
% \documentclass{article}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
    19
%\usepackage[utf8]{inputenc}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
    20
%\usepackage[english]{babel}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
    21
%\usepackage{listings}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
    22
% \usepackage{amsthm}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
    23
%\usepackage{hyperref}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
    24
% \usepackage[margin=0.5in]{geometry}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
    25
%\usepackage{pmboxdraw}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
    26
 
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
    27
\title{POSIX Regular Expression Matching and Lexing}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
    28
\author{Chengsong Tan}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
    29
\affil{King's College London\\
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
    30
London, UK\\
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
    31
\texttt{chengsong.tan@kcl.ac.uk}}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
    32
\authorrunning{Chengsong Tan}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
    33
\Copyright{Chengsong Tan}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
    34
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
    35
\newcommand{\dn}{\stackrel{\mbox{\scriptsize def}}{=}}%
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
    36
\newcommand{\ZERO}{\mbox{\bf 0}}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
    37
\newcommand{\ONE}{\mbox{\bf 1}}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
    38
\def\lexer{\mathit{lexer}}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
    39
\def\mkeps{\mathit{mkeps}}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
    40
444
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
    41
\def\DFA{\textit{DFA}}
441
Chengsong
parents: 440
diff changeset
    42
\def\bmkeps{\textit{bmkeps}}
Chengsong
parents: 440
diff changeset
    43
\def\retrieve{\textit{retrieve}}
Chengsong
parents: 440
diff changeset
    44
\def\blexer{\textit{blexer}}
Chengsong
parents: 440
diff changeset
    45
\def\flex{\textit{flex}}
438
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
    46
\def\inj{\mathit{inj}}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
    47
\def\Empty{\mathit{Empty}}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
    48
\def\Left{\mathit{Left}}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
    49
\def\Right{\mathit{Right}}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
    50
\def\Stars{\mathit{Stars}}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
    51
\def\Char{\mathit{Char}}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
    52
\def\Seq{\mathit{Seq}}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
    53
\def\Der{\mathit{Der}}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
    54
\def\nullable{\mathit{nullable}}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
    55
\def\Z{\mathit{Z}}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
    56
\def\S{\mathit{S}}
441
Chengsong
parents: 440
diff changeset
    57
\def\rup{r^\uparrow}
438
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
    58
444
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
    59
\newcommand{\PDER}{\textit{PDER}}
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
    60
\newcommand{\flts}{\textit{flts}}
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
    61
\newcommand{\distinctBy}{\textit{distinctBy}}
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
    62
\newcommand{\map}{\textit{map}}
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
    63
\newcommand{\size}{\textit{size}}
438
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
    64
\def\awidth{\mathit{awidth}}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
    65
\def\pder{\mathit{pder}}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
    66
\def\maxterms{\mathit{maxterms}}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
    67
\def\bsimp{\mathit{bsimp}}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
    68
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
    69
%\theoremstyle{theorem}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
    70
%\newtheorem{theorem}{Theorem}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
    71
%\theoremstyle{lemma}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
    72
%\newtheorem{lemma}{Lemma}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
    73
%\newcommand{\lemmaautorefname}{Lemma}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
    74
%\theoremstyle{definition}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
    75
%\newtheorem{definition}{Definition}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
    76
\algnewcommand\algorithmicswitch{\textbf{switch}}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
    77
\algnewcommand\algorithmiccase{\textbf{case}}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
    78
\algnewcommand\algorithmicassert{\texttt{assert}}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
    79
\algnewcommand\Assert[1]{\State \algorithmicassert(#1)}%
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
    80
% New "environments"
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
    81
\algdef{SE}[SWITCH]{Switch}{EndSwitch}[1]{\algorithmicswitch\ #1\ \algorithmicdo}{\algorithmicend\ \algorithmicswitch}%
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
    82
\algdef{SE}[CASE]{Case}{EndCase}[1]{\algorithmiccase\ #1}{\algorithmicend\ \algorithmiccase}%
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
    83
\algtext*{EndSwitch}%
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
    84
\algtext*{EndCase}%
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
    85
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
    86
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
    87
\begin{document}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
    88
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
    89
\maketitle
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
    90
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
    91
\begin{abstract}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
    92
  Brzozowski introduced in 1964 a beautifully simple algorithm for
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
    93
  regular expression matching based on the notion of derivatives of
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
    94
  regular expressions. In 2014, Sulzmann and Lu extended this
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
    95
  algorithm to not just give a YES/NO answer for whether or not a
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
    96
  regular expression matches a string, but in case it does also
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
    97
  answers with \emph{how} it matches the string.  This is important for
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
    98
  applications such as lexing (tokenising a string). The problem is to
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
    99
  make the algorithm by Sulzmann and Lu fast on all inputs without
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   100
  breaking its correctness. We have already developed some
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   101
  simplification rules for this, but have not yet proved that they
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   102
  preserve the correctness of the algorithm. We also have not yet
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   103
  looked at extended regular expressions, such as bounded repetitions,
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   104
  negation and back-references.
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   105
\end{abstract}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   106
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   107
\section{Introduction}
440
0856fbf8bda7 bonestruct
Chengsong
parents: 438
diff changeset
   108
\subsection{Basic Regex Introduction}
444
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   109
440
0856fbf8bda7 bonestruct
Chengsong
parents: 438
diff changeset
   110
Suppose (basic) regular expressions are given by the following grammar:
0856fbf8bda7 bonestruct
Chengsong
parents: 438
diff changeset
   111
\[			r ::=   \ZERO \mid  \ONE
0856fbf8bda7 bonestruct
Chengsong
parents: 438
diff changeset
   112
			 \mid  c  
0856fbf8bda7 bonestruct
Chengsong
parents: 438
diff changeset
   113
			 \mid  r_1 \cdot r_2
0856fbf8bda7 bonestruct
Chengsong
parents: 438
diff changeset
   114
			 \mid  r_1 + r_2   
0856fbf8bda7 bonestruct
Chengsong
parents: 438
diff changeset
   115
			 \mid r^*         
0856fbf8bda7 bonestruct
Chengsong
parents: 438
diff changeset
   116
\]
0856fbf8bda7 bonestruct
Chengsong
parents: 438
diff changeset
   117
0856fbf8bda7 bonestruct
Chengsong
parents: 438
diff changeset
   118
Problem of matching:
438
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   119
440
0856fbf8bda7 bonestruct
Chengsong
parents: 438
diff changeset
   120
\begin{center}
0856fbf8bda7 bonestruct
Chengsong
parents: 438
diff changeset
   121
\begin{tabular}{lcr}
0856fbf8bda7 bonestruct
Chengsong
parents: 438
diff changeset
   122
$\textit{Match}(r, s)$ & $ =  $ & $\textit{if}\; s \in L(r)\; \textit{output} \; \textit{YES}$\\
0856fbf8bda7 bonestruct
Chengsong
parents: 438
diff changeset
   123
&				& $\textit{else} \; \textit{output} \; \textit{NO}$
0856fbf8bda7 bonestruct
Chengsong
parents: 438
diff changeset
   124
\end{tabular}
0856fbf8bda7 bonestruct
Chengsong
parents: 438
diff changeset
   125
\end{center}
444
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   126
Omnipresent use of regexes in modern 
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   127
software. 
440
0856fbf8bda7 bonestruct
Chengsong
parents: 438
diff changeset
   128
Examples: Snort, Bro, etc?
0856fbf8bda7 bonestruct
Chengsong
parents: 438
diff changeset
   129
\subsubsection{The rules for network intrusion analysis tools }
0856fbf8bda7 bonestruct
Chengsong
parents: 438
diff changeset
   130
TODO: read rules libraries such as Snort and the explanation for some of the rules
0856fbf8bda7 bonestruct
Chengsong
parents: 438
diff changeset
   131
TODO: pcre/pcre2?
0856fbf8bda7 bonestruct
Chengsong
parents: 438
diff changeset
   132
TODO: any other libraries?
0856fbf8bda7 bonestruct
Chengsong
parents: 438
diff changeset
   133
0856fbf8bda7 bonestruct
Chengsong
parents: 438
diff changeset
   134
444
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   135
There has been many widely used libraries such as 
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   136
Henry Spencer's regexp(3), RE2, etc.
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   137
They are fast and successful, but ugly corner cases
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   138
allowing the $\textit{ReDoS}$ attack exist, and
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   139
is a non-negligible protion.
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   140
\subsection{The practical problem}
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   141
These corner cases either
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   142
\begin{itemize}
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   143
\item
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   144
go unnoticed until they
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   145
cause considerable grief in real life
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   146
\item
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   147
or force the regex library writers to pose
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   148
restrictions on the input, limiting the 
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   149
choice a programmer has when using regexes.
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   150
\end{itemize}
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   151
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   152
Motivation:
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   153
We want some library that supports as many constructs as possible,
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   154
but still gives formal guarantees on the correctness and running
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   155
time.
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   156
440
0856fbf8bda7 bonestruct
Chengsong
parents: 438
diff changeset
   157
\subsection{Regexes that brought down CloudFlare}
0856fbf8bda7 bonestruct
Chengsong
parents: 438
diff changeset
   158
0856fbf8bda7 bonestruct
Chengsong
parents: 438
diff changeset
   159
438
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   160
matching some string $s$ with a regex
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   161
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   162
\begin{verbatim}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   163
(?:(?:\"|'|\]|\}|\\|\d|
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   164
(?:nan|infinity|true|false|null|undefined|symbol|math)
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   165
|\`|\-|\+)+[)]*;?((?:\s|-|~|!|{}|\|\||\+)*.*(?:.*=.*))) 
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   166
\end{verbatim}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   167
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   168
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   169
%Could be from a network intrusion detection algorithm.
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   170
%Checking whether there is some malicious code 
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   171
%in the network data blocks being routed.
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   172
%If so, discard the data and identify the sender for future alert.
440
0856fbf8bda7 bonestruct
Chengsong
parents: 438
diff changeset
   173
\section{Existing approaches}
0856fbf8bda7 bonestruct
Chengsong
parents: 438
diff changeset
   174
\subsection{Shortcomings of different methods}
438
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   175
440
0856fbf8bda7 bonestruct
Chengsong
parents: 438
diff changeset
   176
0856fbf8bda7 bonestruct
Chengsong
parents: 438
diff changeset
   177
\subsubsection{ NFA's}
441
Chengsong
parents: 440
diff changeset
   178
$\bold{Problems With This:}$
Chengsong
parents: 440
diff changeset
   179
\begin{itemize}
Chengsong
parents: 440
diff changeset
   180
\item
440
0856fbf8bda7 bonestruct
Chengsong
parents: 438
diff changeset
   181
Can be slow especially when many states are active.
441
Chengsong
parents: 440
diff changeset
   182
\item
Chengsong
parents: 440
diff changeset
   183
Want Lexing Results: Can have  Exponential different matching results.
Chengsong
parents: 440
diff changeset
   184
\end{itemize}
Chengsong
parents: 440
diff changeset
   185
Chengsong
parents: 440
diff changeset
   186
Chengsong
parents: 440
diff changeset
   187
One regular expression can have multiple lexical values. For example
Chengsong
parents: 440
diff changeset
   188
for the regular expression $(a+b)^*$, it has a infinite list of
Chengsong
parents: 440
diff changeset
   189
values corresponding to it: $\Stars\,[]$, $\Stars\,[\Left(Char(a))]$,
Chengsong
parents: 440
diff changeset
   190
$\Stars\,[\Right(Char(b))]$, $\Stars\,[\Left(Char(a),\,\Right(Char(b))]$,
Chengsong
parents: 440
diff changeset
   191
$\ldots$, and vice versa.
Chengsong
parents: 440
diff changeset
   192
Even for the regular expression matching a certain string, there could 
Chengsong
parents: 440
diff changeset
   193
still be more than one value corresponding to it.
Chengsong
parents: 440
diff changeset
   194
Take the example where $r= (a^*\cdot a^*)^*$ and the string 
Chengsong
parents: 440
diff changeset
   195
$s=\underbrace{aa\ldots a}_\text{n \textit{a}s}$.
Chengsong
parents: 440
diff changeset
   196
The number of different ways of matching 
Chengsong
parents: 440
diff changeset
   197
without allowing any value under a star to be flattened
Chengsong
parents: 440
diff changeset
   198
to an empty string can be given by the following formula:
Chengsong
parents: 440
diff changeset
   199
\begin{center}
Chengsong
parents: 440
diff changeset
   200
	$C_n = (n+1)+n C_1+\ldots + 2 C_{n-1}$
Chengsong
parents: 440
diff changeset
   201
\end{center}
Chengsong
parents: 440
diff changeset
   202
and a closed form formula can be calculated to be
Chengsong
parents: 440
diff changeset
   203
\begin{equation}
Chengsong
parents: 440
diff changeset
   204
	C_n =\frac{(2+\sqrt{2})^n - (2-\sqrt{2})^n}{4\sqrt{2}}
Chengsong
parents: 440
diff changeset
   205
\end{equation}
Chengsong
parents: 440
diff changeset
   206
which is clearly in exponential order.
Chengsong
parents: 440
diff changeset
   207
A lexer aimed at getting all the possible values has an exponential
Chengsong
parents: 440
diff changeset
   208
worst case runtime. Therefore it is impractical to try to generate
Chengsong
parents: 440
diff changeset
   209
all possible matches in a run. In practice, we are usually 
Chengsong
parents: 440
diff changeset
   210
interested about POSIX values, which by intuition always
Chengsong
parents: 440
diff changeset
   211
match the leftmost regular expression when there is a choice
Chengsong
parents: 440
diff changeset
   212
and always match a sub part as much as possible before proceeding
Chengsong
parents: 440
diff changeset
   213
to the next token. For example, the above example has the POSIX value
Chengsong
parents: 440
diff changeset
   214
$ \Stars\,[\Seq(Stars\,[\underbrace{\Char(a),\ldots,\Char(a)}_\text{n iterations}], Stars\,[])]$.
Chengsong
parents: 440
diff changeset
   215
The output of an algorithm we want would be a POSIX matching
Chengsong
parents: 440
diff changeset
   216
encoded as a value.\\
Chengsong
parents: 440
diff changeset
   217
$\mathbf{TODO:}$
Chengsong
parents: 440
diff changeset
   218
\begin{itemize}
Chengsong
parents: 440
diff changeset
   219
\item
Chengsong
parents: 440
diff changeset
   220
Illustrate graphically how you can match $a*a**$ with $aaa$ in different ways. 
Chengsong
parents: 440
diff changeset
   221
\item
Chengsong
parents: 440
diff changeset
   222
Give a backtracking algorithm, and explain briefly why this can be exponentially slow.
Chengsong
parents: 440
diff changeset
   223
(When there is a matching, it finds straight away; where there is not one, this fails to 
Chengsong
parents: 440
diff changeset
   224
recognize immediately that a match cannot be possibly found, and tries out all remaining 
Chengsong
parents: 440
diff changeset
   225
possibilities, etc.)
Chengsong
parents: 440
diff changeset
   226
\item
Chengsong
parents: 440
diff changeset
   227
From the above point, are there statical analysis tools that single out those malicious 
Chengsong
parents: 440
diff changeset
   228
patterns and tell before a lexer is even run?
Chengsong
parents: 440
diff changeset
   229
Have a more thorough survey of the Birmingham paper.
Chengsong
parents: 440
diff changeset
   230
Give out the suitable scenarios for such static analysis algorithms.
Chengsong
parents: 440
diff changeset
   231
Chengsong
parents: 440
diff changeset
   232
\end{itemize}
438
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   233
440
0856fbf8bda7 bonestruct
Chengsong
parents: 438
diff changeset
   234
\subsubsection{DFAs}
0856fbf8bda7 bonestruct
Chengsong
parents: 438
diff changeset
   235
The tool JFLEX uses it.
0856fbf8bda7 bonestruct
Chengsong
parents: 438
diff changeset
   236
Advantages: super fast on most regexes \\
0856fbf8bda7 bonestruct
Chengsong
parents: 438
diff changeset
   237
TODO: show it being fast on a lot of inputs\\
0856fbf8bda7 bonestruct
Chengsong
parents: 438
diff changeset
   238
Disavantages:
0856fbf8bda7 bonestruct
Chengsong
parents: 438
diff changeset
   239
state explosion for bounded repetitions due to 
0856fbf8bda7 bonestruct
Chengsong
parents: 438
diff changeset
   240
theoretic bottleneck of having to remember exactly what the
0856fbf8bda7 bonestruct
Chengsong
parents: 438
diff changeset
   241
suffix up to length $n$ of input string is.
0856fbf8bda7 bonestruct
Chengsong
parents: 438
diff changeset
   242
"Countdown States activation problem":
0856fbf8bda7 bonestruct
Chengsong
parents: 438
diff changeset
   243
$.*a.{100}$ requires $2^100$ + DFA states.
444
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   244
Example:
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   245
Converting $((a|b )*b.{10}){3}$ to a $\DFA$
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   246
gives the error:
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   247
\begin{verbatim}
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   248
147972 states before minimization, 79107 states in minimized DFA
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   249
Old file "search.java" saved as "search.java~"
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   250
Writing code to "search.java"
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   251
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   252
Unexpected exception encountered. This indicates a bug in JFlex.
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   253
Please consider filing an issue at http://github.com/jflex-de/jflex/issues/new
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   254
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   255
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   256
character value expected
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   257
java.lang.IllegalArgumentException: character value expected
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   258
        at jflex.generator.PackEmitter.emitUC(PackEmitter.java:105)
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   259
        at jflex.generator.CountEmitter.emit(CountEmitter.java:116)
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   260
        at jflex.generator.Emitter.emitDynamicInit(Emitter.java:530)
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   261
        at jflex.generator.Emitter.emit(Emitter.java:1369)
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   262
        at jflex.generator.LexGenerator.generate(LexGenerator.java:115)
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   263
        at jflex.Main.generate(Main.java:320)
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   264
        at jflex.Main.main(Main.java:336)
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   265
\end{verbatim}
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   266
440
0856fbf8bda7 bonestruct
Chengsong
parents: 438
diff changeset
   267
\subsubsection{variant of DFA's}
0856fbf8bda7 bonestruct
Chengsong
parents: 438
diff changeset
   268
counting set automata 
0856fbf8bda7 bonestruct
Chengsong
parents: 438
diff changeset
   269
\\
0856fbf8bda7 bonestruct
Chengsong
parents: 438
diff changeset
   270
TODO: microsoft 2020 oopsla CsA work, need to add bibli entry, and read, understand key novelty, learn to benchmark like it
0856fbf8bda7 bonestruct
Chengsong
parents: 438
diff changeset
   271
\\
0856fbf8bda7 bonestruct
Chengsong
parents: 438
diff changeset
   272
TODO: find weakness of such counting set automata?
0856fbf8bda7 bonestruct
Chengsong
parents: 438
diff changeset
   273
\\
0856fbf8bda7 bonestruct
Chengsong
parents: 438
diff changeset
   274
Other variants?
0856fbf8bda7 bonestruct
Chengsong
parents: 438
diff changeset
   275
0856fbf8bda7 bonestruct
Chengsong
parents: 438
diff changeset
   276
\subsubsection{NFA and Regex: isomorphic structure}
0856fbf8bda7 bonestruct
Chengsong
parents: 438
diff changeset
   277
TODO: define mathematically an isomorphism?\\
0856fbf8bda7 bonestruct
Chengsong
parents: 438
diff changeset
   278
438
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   279
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   280
440
0856fbf8bda7 bonestruct
Chengsong
parents: 438
diff changeset
   281
\subsubsection{variants of NFA's}
0856fbf8bda7 bonestruct
Chengsong
parents: 438
diff changeset
   282
How about acting on regular expressions themselves? Certain copies represent verbose info--that they will always match the same string--prune away!
0856fbf8bda7 bonestruct
Chengsong
parents: 438
diff changeset
   283
0856fbf8bda7 bonestruct
Chengsong
parents: 438
diff changeset
   284
\subsection{Brzozowski's derivatives}
0856fbf8bda7 bonestruct
Chengsong
parents: 438
diff changeset
   285
0856fbf8bda7 bonestruct
Chengsong
parents: 438
diff changeset
   286
\subsection{Sulzmann and Lu's algorithm}
0856fbf8bda7 bonestruct
Chengsong
parents: 438
diff changeset
   287
0856fbf8bda7 bonestruct
Chengsong
parents: 438
diff changeset
   288
\subsection{Bit-coded algorithm}
0856fbf8bda7 bonestruct
Chengsong
parents: 438
diff changeset
   289
+bitcodes!
0856fbf8bda7 bonestruct
Chengsong
parents: 438
diff changeset
   290
Built on top of derivatives, but with auxiliary bits
0856fbf8bda7 bonestruct
Chengsong
parents: 438
diff changeset
   291
\subsection{Correctness Proof}
441
Chengsong
parents: 440
diff changeset
   292
Chengsong
parents: 440
diff changeset
   293
Not proven by Sulzmann  and Lu
Chengsong
parents: 440
diff changeset
   294
Chengsong
parents: 440
diff changeset
   295
Proven by Ausaf and Urban!!
Chengsong
parents: 440
diff changeset
   296
Chengsong
parents: 440
diff changeset
   297
Chengsong
parents: 440
diff changeset
   298
For this we have started with looking at the proof of
Chengsong
parents: 440
diff changeset
   299
\begin{equation}\label{lexer}
Chengsong
parents: 440
diff changeset
   300
\blexer \; (r^\uparrow)  s = \lexer \;r \;s,
Chengsong
parents: 440
diff changeset
   301
\end{equation}
Chengsong
parents: 440
diff changeset
   302
Chengsong
parents: 440
diff changeset
   303
%\noindent
Chengsong
parents: 440
diff changeset
   304
%might provide us insight into proving 
Chengsong
parents: 440
diff changeset
   305
%\begin{center}
Chengsong
parents: 440
diff changeset
   306
%$\blexer \; r^\uparrow \;s = \blexers \; r^\uparrow \;s$
Chengsong
parents: 440
diff changeset
   307
%\end{center}
Chengsong
parents: 440
diff changeset
   308
Chengsong
parents: 440
diff changeset
   309
\noindent
Chengsong
parents: 440
diff changeset
   310
which established that the bit-sequence algorithm produces the same
Chengsong
parents: 440
diff changeset
   311
result as the original algorithm, which does not use 
Chengsong
parents: 440
diff changeset
   312
bit-sequences.
Chengsong
parents: 440
diff changeset
   313
The proof uses two ``tricks''. One is that it uses a \flex-function
Chengsong
parents: 440
diff changeset
   314
Chengsong
parents: 440
diff changeset
   315
\begin{center}
Chengsong
parents: 440
diff changeset
   316
\begin{tabular}{lcl}
Chengsong
parents: 440
diff changeset
   317
$\textit{flex} \;r\; f\; (c\!::\!s) $ & $\dn$ & $\textit{flex} \;  (r\backslash c) \;(\lambda v. f (inj \; r \; c \; v)) \;s$ \\
Chengsong
parents: 440
diff changeset
   318
$\textit{flex} \;r\; f\;  [\,] $ & $\dn$ & $f$
Chengsong
parents: 440
diff changeset
   319
\end{tabular}
Chengsong
parents: 440
diff changeset
   320
\end{center}
Chengsong
parents: 440
diff changeset
   321
Chengsong
parents: 440
diff changeset
   322
\noindent
Chengsong
parents: 440
diff changeset
   323
Chengsong
parents: 440
diff changeset
   324
The intuition behind the $\flex$ function is that
Chengsong
parents: 440
diff changeset
   325
 it  accumulates a series of $\inj$ function applications when doing derivatives
Chengsong
parents: 440
diff changeset
   326
 in a $\mathit{LIFO}$ manner. The arguments of the $\inj$ functions are kept by
Chengsong
parents: 440
diff changeset
   327
  remembering which character
Chengsong
parents: 440
diff changeset
   328
 was chopped off and what the regular expression looks like before
Chengsong
parents: 440
diff changeset
   329
 chopping off that character.
Chengsong
parents: 440
diff changeset
   330
 The $\mathit{LIFO}$ order was achieved by putting the newest $\inj$ application
Chengsong
parents: 440
diff changeset
   331
 always before the application of $f$, the previously accumulated function applications.\\
Chengsong
parents: 440
diff changeset
   332
Therefore, the function $\flex$, when acted on a string $s@[c]$ where the last
Chengsong
parents: 440
diff changeset
   333
character is $c$, by nature can have its last injection function revealed already: 
Chengsong
parents: 440
diff changeset
   334
\begin{equation}\label{flex}
Chengsong
parents: 440
diff changeset
   335
\flex \; r \; id \; (s@[c]) \; v = \flex \;  r \; id \; s \; (inj \; (r\backslash s) \; c\; v).
Chengsong
parents: 440
diff changeset
   336
\end{equation}
Chengsong
parents: 440
diff changeset
   337
that the last character can be taken off, and the injection it causes be applied to 
Chengsong
parents: 440
diff changeset
   338
the argument value $v$.
Chengsong
parents: 440
diff changeset
   339
Chengsong
parents: 440
diff changeset
   340
Ausaf and Urban proved that the Sulzmann and Lu's lexers
Chengsong
parents: 440
diff changeset
   341
can be charactarized by the $\flex$ function:
Chengsong
parents: 440
diff changeset
   342
\begin{center}
Chengsong
parents: 440
diff changeset
   343
$\lexer \;r\; s = \flex \;\textit{id} \; r\;s \;(\mkeps \; (r\backslash s))$.
Chengsong
parents: 440
diff changeset
   344
\end{center}
Chengsong
parents: 440
diff changeset
   345
Chengsong
parents: 440
diff changeset
   346
\noindent
Chengsong
parents: 440
diff changeset
   347
This property says that the Sulzmann and Lu's $\lexer$ does lexing by
Chengsong
parents: 440
diff changeset
   348
stacking up injection functions while doing derivatives,
Chengsong
parents: 440
diff changeset
   349
explicitly showing the order of characters being
Chengsong
parents: 440
diff changeset
   350
injected back in each step.
Chengsong
parents: 440
diff changeset
   351
Chengsong
parents: 440
diff changeset
   352
\noindent
Chengsong
parents: 440
diff changeset
   353
The other trick, which is the crux in the existing proof, 
Chengsong
parents: 440
diff changeset
   354
is the use of the $\retrieve$-function:
Chengsong
parents: 440
diff changeset
   355
\begin{center}
Chengsong
parents: 440
diff changeset
   356
\begin{tabular}{@{}l@{\hspace{2mm}}c@{\hspace{2mm}}l@{}}
Chengsong
parents: 440
diff changeset
   357
  $\textit{retrieve}\,(_{bs}\ONE)\,\Empty$ & $\dn$ & $bs$\\
Chengsong
parents: 440
diff changeset
   358
  $\textit{retrieve}\,(_{bs}{\bf c})\,(\Char\,d)$ & $\dn$ & $bs$\\
Chengsong
parents: 440
diff changeset
   359
  $\textit{retrieve}\,(_{bs}\sum a::as)\,(\Left\,v)$ & $\dn$ &
Chengsong
parents: 440
diff changeset
   360
     $bs \,@\, \textit{retrieve}\,a\,v$\\
Chengsong
parents: 440
diff changeset
   361
  $\textit{retrieve}\,(_{bs}\sum a::as)\,(\Right\,v)$ & $\dn$ &
Chengsong
parents: 440
diff changeset
   362
  $\textit{bs} \,@\, \textit{retrieve}\,(_{[]}\sum as)\,v$\\
Chengsong
parents: 440
diff changeset
   363
  $\textit{retrieve}\,(_{bs}a_1\cdot a_2)\,(\Seq\,v_1\,v_2)$ & $\dn$ &
Chengsong
parents: 440
diff changeset
   364
     $bs \,@\,\textit{retrieve}\,a_1\,v_1\,@\, \textit{retrieve}\,a_2\,v_2$\\
Chengsong
parents: 440
diff changeset
   365
  $\textit{retrieve}\,(_{bs}a^*)\,(\Stars\,[])$ & $\dn$ &
Chengsong
parents: 440
diff changeset
   366
     $bs \,@\, [0]$\\
Chengsong
parents: 440
diff changeset
   367
  $\textit{retrieve}\,(_{bs}a^*)\,(\Stars\,(v\!::\!vs))$ & $\dn$ &\\
Chengsong
parents: 440
diff changeset
   368
  \multicolumn{3}{l}{
Chengsong
parents: 440
diff changeset
   369
     \hspace{3cm}$bs \,@\, [1] \,@\, \textit{retrieve}\,a\,v\,@\,
Chengsong
parents: 440
diff changeset
   370
                    \textit{retrieve}\,(_{[]}a^*)\,(\Stars\,vs)$}\\
Chengsong
parents: 440
diff changeset
   371
\end{tabular}
Chengsong
parents: 440
diff changeset
   372
\end{center}
Chengsong
parents: 440
diff changeset
   373
Chengsong
parents: 440
diff changeset
   374
\noindent
Chengsong
parents: 440
diff changeset
   375
Sulzmann and Lu proposed this function, but did not prove
Chengsong
parents: 440
diff changeset
   376
anything about it. Ausaf and Urban made use of the
Chengsong
parents: 440
diff changeset
   377
fact about $\retrieve$ in their proof:
Chengsong
parents: 440
diff changeset
   378
 \begin{equation}\label{retrieve_reversible}
Chengsong
parents: 440
diff changeset
   379
 \retrieve\; \rup \backslash c \; v = \retrieve \;  \rup (\inj \;r \;c \; v)
Chengsong
parents: 440
diff changeset
   380
 \end{equation} 
Chengsong
parents: 440
diff changeset
   381
This says that $\retrieve$ will always pick up 
Chengsong
parents: 440
diff changeset
   382
partial information about a lexing value value and transform it into suitable bitcodes.
Chengsong
parents: 440
diff changeset
   383
If the information is in the regular expression (stored as bitcodes), it will keep those
Chengsong
parents: 440
diff changeset
   384
bitcodes with the guidance of the value,
Chengsong
parents: 440
diff changeset
   385
if the information is in the value, which has been injected back to the value,
Chengsong
parents: 440
diff changeset
   386
it will "digest" and transform that part of the value to bitcodes.
Chengsong
parents: 440
diff changeset
   387
Chengsong
parents: 440
diff changeset
   388
\noindent
Chengsong
parents: 440
diff changeset
   389
Chengsong
parents: 440
diff changeset
   390
Using this together with ~\eqref{flex}, we can prove that the bitcoded version of
Chengsong
parents: 440
diff changeset
   391
lexer is the same as Sulzmann and Lu's lexer:
Chengsong
parents: 440
diff changeset
   392
\begin{center} 
Chengsong
parents: 440
diff changeset
   393
$\lexer \; r \; s =  \flex \; r\; id\; s\; v = \textit{decode} \;( \textit{bmkeps}\; (\rup \backslash s) ) r = \blexer \; r \; s$
Chengsong
parents: 440
diff changeset
   394
\end{center}
Chengsong
parents: 440
diff changeset
   395
\noindent
Chengsong
parents: 440
diff changeset
   396
\begin{proof}
Chengsong
parents: 440
diff changeset
   397
We express $\bmkeps$ using $\retrieve$, and the theorem to prove becomes:
Chengsong
parents: 440
diff changeset
   398
\begin{center} 
Chengsong
parents: 440
diff changeset
   399
$ \flex \; r\; id\; s\; v = \textit{decode} \;( \textit{retrieve}\; (\rup \backslash s) \; v \;) r$
Chengsong
parents: 440
diff changeset
   400
\end{center}
Chengsong
parents: 440
diff changeset
   401
\noindent
Chengsong
parents: 440
diff changeset
   402
We prove the above by reverse induction on string $s$(meaning that the inductive step is on 
Chengsong
parents: 440
diff changeset
   403
$s @ [c]$ rather than $c :: s$).
Chengsong
parents: 440
diff changeset
   404
$v$ takes arbitrary values.\\
Chengsong
parents: 440
diff changeset
   405
The base case goes through trivially.\\
Chengsong
parents: 440
diff changeset
   406
For the inductive step, assuming
Chengsong
parents: 440
diff changeset
   407
$ \flex \; r\; id\; s\; v = \textit{decode} \;( \textit{retrieve}\; (\rup \backslash s) \; v \;) r$
Chengsong
parents: 440
diff changeset
   408
holds for all values $v$. Now we need to show that
Chengsong
parents: 440
diff changeset
   409
$ \flex \; r\; id\; s@[c]\; v = \textit{decode} \;( \textit{retrieve}\; (\rup \backslash (s@[c])) \; v \;) r$.\\
Chengsong
parents: 440
diff changeset
   410
~\eqref{flex} allows us to do the following rewrite:
Chengsong
parents: 440
diff changeset
   411
\begin{center} 
Chengsong
parents: 440
diff changeset
   412
$ \flex \; r\; id\; (s@[c])\; v = \flex \; r \; id\; s\; (\inj \; (r \backslash s) \; c\; v)=  \textit{decode} \;( \textit{retrieve}\; (\rup \backslash s) \; (\inj \; (r\backslash s) \;c\;v)\;) r$
Chengsong
parents: 440
diff changeset
   413
\end{center}
Chengsong
parents: 440
diff changeset
   414
~\eqref{retrieve_reversible} allows us  to further rewrite the $\mathit{RHS}$ of the above to
Chengsong
parents: 440
diff changeset
   415
\begin{center}
Chengsong
parents: 440
diff changeset
   416
$\textit{decode} \; (\textit{retrieve}\; (\rup \backslash (s @ [c])) \; v\;)  \;r$
Chengsong
parents: 440
diff changeset
   417
\end{center}
Chengsong
parents: 440
diff changeset
   418
Chengsong
parents: 440
diff changeset
   419
Chengsong
parents: 440
diff changeset
   420
\end{proof}
Chengsong
parents: 440
diff changeset
   421
Chengsong
parents: 440
diff changeset
   422
440
0856fbf8bda7 bonestruct
Chengsong
parents: 438
diff changeset
   423
0856fbf8bda7 bonestruct
Chengsong
parents: 438
diff changeset
   424
\section{My Work}
0856fbf8bda7 bonestruct
Chengsong
parents: 438
diff changeset
   425
0856fbf8bda7 bonestruct
Chengsong
parents: 438
diff changeset
   426
\subsection{an improved version of bit-coded algorithm: with simp!}
438
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   427
443
c6351a96bf80 writeupforclosedforms
Chengsong
parents: 441
diff changeset
   428
\subsection{a correctness proof for bitcoded algorithm}
440
0856fbf8bda7 bonestruct
Chengsong
parents: 438
diff changeset
   429
0856fbf8bda7 bonestruct
Chengsong
parents: 438
diff changeset
   430
\subsection{finiteness proof }
443
c6351a96bf80 writeupforclosedforms
Chengsong
parents: 441
diff changeset
   431
\subsubsection{closed form}
c6351a96bf80 writeupforclosedforms
Chengsong
parents: 441
diff changeset
   432
We can give the derivative of regular expressions
c6351a96bf80 writeupforclosedforms
Chengsong
parents: 441
diff changeset
   433
with respect to string a closed form with respect to simplification:
c6351a96bf80 writeupforclosedforms
Chengsong
parents: 441
diff changeset
   434
\begin{itemize}
c6351a96bf80 writeupforclosedforms
Chengsong
parents: 441
diff changeset
   435
\item
c6351a96bf80 writeupforclosedforms
Chengsong
parents: 441
diff changeset
   436
closed form for sequences:
c6351a96bf80 writeupforclosedforms
Chengsong
parents: 441
diff changeset
   437
\begin{verbatim}
c6351a96bf80 writeupforclosedforms
Chengsong
parents: 441
diff changeset
   438
lemma seq_closed_form: shows 
c6351a96bf80 writeupforclosedforms
Chengsong
parents: 441
diff changeset
   439
"rsimp (rders_simp (RSEQ r1 r2) s) = 
c6351a96bf80 writeupforclosedforms
Chengsong
parents: 441
diff changeset
   440
rsimp ( RALTS ( (RSEQ (rders_simp r1 s) r2) # 
c6351a96bf80 writeupforclosedforms
Chengsong
parents: 441
diff changeset
   441
                (map (rders r2) (vsuf s r1)) 
c6351a96bf80 writeupforclosedforms
Chengsong
parents: 441
diff changeset
   442
              )  
c6351a96bf80 writeupforclosedforms
Chengsong
parents: 441
diff changeset
   443
      )"
c6351a96bf80 writeupforclosedforms
Chengsong
parents: 441
diff changeset
   444
\end{verbatim}
c6351a96bf80 writeupforclosedforms
Chengsong
parents: 441
diff changeset
   445
where the recursive function $\textit{vsuf}$ is defined as
c6351a96bf80 writeupforclosedforms
Chengsong
parents: 441
diff changeset
   446
\begin{verbatim}
c6351a96bf80 writeupforclosedforms
Chengsong
parents: 441
diff changeset
   447
fun vsuf :: "char list -> rrexp -> char list list" where
c6351a96bf80 writeupforclosedforms
Chengsong
parents: 441
diff changeset
   448
"vsuf [] _ = []"
c6351a96bf80 writeupforclosedforms
Chengsong
parents: 441
diff changeset
   449
|"vsuf (c#cs) r1 = (if (rnullable r1) then  (vsuf cs (rder c r1)) @ [c # cs]
c6351a96bf80 writeupforclosedforms
Chengsong
parents: 441
diff changeset
   450
                                      else  (vsuf cs (rder c r1))
c6351a96bf80 writeupforclosedforms
Chengsong
parents: 441
diff changeset
   451
                   ) "
440
0856fbf8bda7 bonestruct
Chengsong
parents: 438
diff changeset
   452
443
c6351a96bf80 writeupforclosedforms
Chengsong
parents: 441
diff changeset
   453
\end{verbatim}
c6351a96bf80 writeupforclosedforms
Chengsong
parents: 441
diff changeset
   454
\item
c6351a96bf80 writeupforclosedforms
Chengsong
parents: 441
diff changeset
   455
closed form for stars:
c6351a96bf80 writeupforclosedforms
Chengsong
parents: 441
diff changeset
   456
\begin{verbatim}
c6351a96bf80 writeupforclosedforms
Chengsong
parents: 441
diff changeset
   457
lemma star_closed_form:
c6351a96bf80 writeupforclosedforms
Chengsong
parents: 441
diff changeset
   458
  shows "rders_simp (RSTAR r0) (c#s) = 
c6351a96bf80 writeupforclosedforms
Chengsong
parents: 441
diff changeset
   459
rsimp ( RALTS ( 
c6351a96bf80 writeupforclosedforms
Chengsong
parents: 441
diff changeset
   460
(map (\lambda s1. RSEQ (rders_simp r0 s1) (RSTAR r0) ) 
c6351a96bf80 writeupforclosedforms
Chengsong
parents: 441
diff changeset
   461
(star_updates s r [[c]]) ) ))"
c6351a96bf80 writeupforclosedforms
Chengsong
parents: 441
diff changeset
   462
\end{verbatim}
c6351a96bf80 writeupforclosedforms
Chengsong
parents: 441
diff changeset
   463
where the recursive function $\textit{star}\_\textit{updates}$ is defined as
c6351a96bf80 writeupforclosedforms
Chengsong
parents: 441
diff changeset
   464
\begin{verbatim}
c6351a96bf80 writeupforclosedforms
Chengsong
parents: 441
diff changeset
   465
fun star_update :: "char -> rrexp -> char list list -> char list list" where
c6351a96bf80 writeupforclosedforms
Chengsong
parents: 441
diff changeset
   466
"star_update c r [] = []"
c6351a96bf80 writeupforclosedforms
Chengsong
parents: 441
diff changeset
   467
|"star_update c r (s # Ss) = (if (rnullable (rders_simp r s)) 
c6351a96bf80 writeupforclosedforms
Chengsong
parents: 441
diff changeset
   468
                                then (s@[c]) # [c] # (star_update c r Ss) 
c6351a96bf80 writeupforclosedforms
Chengsong
parents: 441
diff changeset
   469
                               else   (s@[c]) # (star_update c r Ss) )"
c6351a96bf80 writeupforclosedforms
Chengsong
parents: 441
diff changeset
   470
c6351a96bf80 writeupforclosedforms
Chengsong
parents: 441
diff changeset
   471
fun star_updates :: "char list -> rrexp -> char list list -> char list list"
c6351a96bf80 writeupforclosedforms
Chengsong
parents: 441
diff changeset
   472
  where
c6351a96bf80 writeupforclosedforms
Chengsong
parents: 441
diff changeset
   473
"star_updates [] r Ss = Ss"
c6351a96bf80 writeupforclosedforms
Chengsong
parents: 441
diff changeset
   474
| "star_updates (c # cs) r Ss = star_updates cs r (star_update c r Ss)"
c6351a96bf80 writeupforclosedforms
Chengsong
parents: 441
diff changeset
   475
c6351a96bf80 writeupforclosedforms
Chengsong
parents: 441
diff changeset
   476
\end{verbatim}
c6351a96bf80 writeupforclosedforms
Chengsong
parents: 441
diff changeset
   477
c6351a96bf80 writeupforclosedforms
Chengsong
parents: 441
diff changeset
   478
c6351a96bf80 writeupforclosedforms
Chengsong
parents: 441
diff changeset
   479
\end{itemize}
c6351a96bf80 writeupforclosedforms
Chengsong
parents: 441
diff changeset
   480
These closed form is a formalization of the intuition 
c6351a96bf80 writeupforclosedforms
Chengsong
parents: 441
diff changeset
   481
 that we can push in the derivatives
c6351a96bf80 writeupforclosedforms
Chengsong
parents: 441
diff changeset
   482
of compound regular expressions to its sub-expressions, and the resulting
c6351a96bf80 writeupforclosedforms
Chengsong
parents: 441
diff changeset
   483
expression is a linear combination of those sub-expressions' derivatives.
c6351a96bf80 writeupforclosedforms
Chengsong
parents: 441
diff changeset
   484
\subsubsection{Estimation of closed forms' size}
c6351a96bf80 writeupforclosedforms
Chengsong
parents: 441
diff changeset
   485
And thanks to $\textit{distinctBy}$ helping with deduplication,
c6351a96bf80 writeupforclosedforms
Chengsong
parents: 441
diff changeset
   486
the linear combination can be  bounded by the set enumerating all 
c6351a96bf80 writeupforclosedforms
Chengsong
parents: 441
diff changeset
   487
regular expressions up to a certain size :
c6351a96bf80 writeupforclosedforms
Chengsong
parents: 441
diff changeset
   488
\begin{verbatim}
c6351a96bf80 writeupforclosedforms
Chengsong
parents: 441
diff changeset
   489
c6351a96bf80 writeupforclosedforms
Chengsong
parents: 441
diff changeset
   490
lemma star_closed_form_bounded_by_rdistinct_list_estimate:
c6351a96bf80 writeupforclosedforms
Chengsong
parents: 441
diff changeset
   491
  shows "rsize (rsimp ( RALTS ( (map (\lambda s1. RSEQ (rders_simp r0 s1) (RSTAR r0) )
c6351a96bf80 writeupforclosedforms
Chengsong
parents: 441
diff changeset
   492
         (star_updates s r [[c]]) ) ))) <=
c6351a96bf80 writeupforclosedforms
Chengsong
parents: 441
diff changeset
   493
        Suc (sum_list (map rsize (rdistinct (map (\lambda s1. RSEQ (rders_simp r0 s1) (RSTAR r0) )
c6351a96bf80 writeupforclosedforms
Chengsong
parents: 441
diff changeset
   494
         (star_updates s r [[c]]) ) {})  ) )"
c6351a96bf80 writeupforclosedforms
Chengsong
parents: 441
diff changeset
   495
         
c6351a96bf80 writeupforclosedforms
Chengsong
parents: 441
diff changeset
   496
         lemma distinct_list_rexp_up_to_certain_size_bouded_by_set_enumerating_up_to_that_size:
c6351a96bf80 writeupforclosedforms
Chengsong
parents: 441
diff changeset
   497
  shows "\forallr\in set rs. (rsize r ) <= N ==> sum_list (map rsize (rdistinct rs {})) <=
c6351a96bf80 writeupforclosedforms
Chengsong
parents: 441
diff changeset
   498
         (card (rexp_enum N))* N"
c6351a96bf80 writeupforclosedforms
Chengsong
parents: 441
diff changeset
   499
         
c6351a96bf80 writeupforclosedforms
Chengsong
parents: 441
diff changeset
   500
         lemma ind_hypo_on_ders_leads_to_stars_bounded:
c6351a96bf80 writeupforclosedforms
Chengsong
parents: 441
diff changeset
   501
  shows "\foralls. rsize (rders_simp r0 s) <= N ==>        
c6351a96bf80 writeupforclosedforms
Chengsong
parents: 441
diff changeset
   502
      (sum_list (map rsize (rdistinct (map (\lambda s1. RSEQ (rders_simp r0 s1) (RSTAR r0) )
c6351a96bf80 writeupforclosedforms
Chengsong
parents: 441
diff changeset
   503
         (star_updates s r [[c]]) ) {})  ) ) <= 
c6351a96bf80 writeupforclosedforms
Chengsong
parents: 441
diff changeset
   504
(card (rexp_enum (Suc (N + rsize (RSTAR r0))))) * (Suc (N + rsize (RSTAR r0)))
c6351a96bf80 writeupforclosedforms
Chengsong
parents: 441
diff changeset
   505
"
c6351a96bf80 writeupforclosedforms
Chengsong
parents: 441
diff changeset
   506
\end{verbatim}
c6351a96bf80 writeupforclosedforms
Chengsong
parents: 441
diff changeset
   507
c6351a96bf80 writeupforclosedforms
Chengsong
parents: 441
diff changeset
   508
With the above 3 lemmas, we can argue that the inductive hypothesis
c6351a96bf80 writeupforclosedforms
Chengsong
parents: 441
diff changeset
   509
$r_0$'s derivatives is bounded above  leads to $r_0^*$'s
c6351a96bf80 writeupforclosedforms
Chengsong
parents: 441
diff changeset
   510
derivatives being bounded above.
c6351a96bf80 writeupforclosedforms
Chengsong
parents: 441
diff changeset
   511
\begin{verbatim}
c6351a96bf80 writeupforclosedforms
Chengsong
parents: 441
diff changeset
   512
c6351a96bf80 writeupforclosedforms
Chengsong
parents: 441
diff changeset
   513
lemma r0_bounded_star_bounded:
c6351a96bf80 writeupforclosedforms
Chengsong
parents: 441
diff changeset
   514
  shows "\foralls. rsize (rders_simp r0 s) <= N ==>
c6351a96bf80 writeupforclosedforms
Chengsong
parents: 441
diff changeset
   515
             \foralls. rsize (rders_simp (RSTAR r0) s) <= 
c6351a96bf80 writeupforclosedforms
Chengsong
parents: 441
diff changeset
   516
(card (rexp_enum (Suc (N + rsize (RSTAR r0))))) * (Suc (N + rsize (RSTAR r0)))"
c6351a96bf80 writeupforclosedforms
Chengsong
parents: 441
diff changeset
   517
\end{verbatim}
c6351a96bf80 writeupforclosedforms
Chengsong
parents: 441
diff changeset
   518
c6351a96bf80 writeupforclosedforms
Chengsong
parents: 441
diff changeset
   519
c6351a96bf80 writeupforclosedforms
Chengsong
parents: 441
diff changeset
   520
And we have a similar argument for the sequence case.
444
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   521
\subsection{stronger simplification needed}
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   522
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   523
\subsubsection{Bounded List of Terms}
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   524
We have seen that without simplification the size of $(a+aa)^*$
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   525
grows exponentially and unbounded(where we omit certain nested
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   526
parentheses among the four terms in the last explicitly written out regex):
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   527
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   528
\def\ll{\stackrel{\_\backslash{} a}{\longrightarrow}}
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   529
\begin{center}
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   530
\begin{tabular}{rll}
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   531
$(a + aa)^*$ & $\ll$ & $(\ONE + \ONE{}a) \cdot (a + aa)^*$\\
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   532
& $\ll$ & $(\ZERO + \ZERO{}a + \ONE) \cdot (a + aa)^* \;+\; (\ONE + \ONE{}a) \cdot (a + aa)^*$\\
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   533
& $\ll$ & $(\ZERO + \ZERO{}a + \ZERO) \cdot (a + aa)^* + (\ONE + \ONE{}a) \cdot (a + aa)^* \;+\; $\\
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   534
& & $\qquad(\ZERO + \ZERO{}a + \ONE) \cdot (a + aa)^* + (\ONE + \ONE{}a) \cdot (a + aa)^*$\\
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   535
& $\ll$ & \ldots \hspace{15mm}(regular expressions of sizes 98, 169, 283, 468, 767, \ldots)
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   536
\end{tabular}
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   537
\end{center}
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   538
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   539
But if we look closely at the regex
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   540
\begin{center}
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   541
\begin{tabular}{rll}
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   542
& & $\qquad(\ZERO + \ZERO{}a + \ONE) \cdot (a + aa)^* + (\ONE + \ONE{}a) \cdot (a + aa)^*$\\
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   543
\end{tabular}
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   544
\end{center}
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   545
we realize that:
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   546
\begin{itemize}
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   547
\item
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   548
The regex is  equivalent to an alternative taking a long-flattened list, 
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   549
where each list is a sequence, and the second child of that sequence
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   550
is always $(a+aa)^*$. In other words, the regex is a "linear combination"
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   551
of terms of the form $(a+aa)\backslash s \cdot (a+aa)^*$ ($s$ is any string).
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   552
\item
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   553
The number of different terms of the shape $(a+aa) \backslash s \cdot (a+aa)^*$ is 
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   554
bounded because the first child $(a+aa) \backslash s$ can only be one of
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   555
$(\ZERO + \ZERO{}a + \ZERO)$, $(\ZERO + \ZERO{}a + \ONE)$, 
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   556
$(\ONE + \ONE{}a)$ and $(\ZERO + \ZERO{}a)$.
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   557
\item
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   558
With simplification we have that the regex is additionally reduced to,
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   559
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   560
where each term $\bsimp((a+aa)\backslash s )  $
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   561
is further reduced to only
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   562
$\ONE$, $\ONE + a$ and $\ZERO$.
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   563
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   564
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   565
\end{itemize}
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   566
Generalizing this to any regular expression of the form 
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   567
$\sum_{s\in L(r)} \bsimp(r\backslash s ) \cdot r^*$,
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   568
we have the closed-form for star regex's string derivative as below:
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   569
$\forall r \;s.\; \exists sl. \; s.t.\;\bsimp(r^* \backslash s) = \bsimp(\sum_{s'\in sl}(r\backslash s') \cdot r^* )$.
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   570
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   571
The regex $\bsimp(\sum_{s' \in sl}(r\backslash s') \cdot r^*)$ is bounded by
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   572
$\distinctBy(\flts(\sum_{s'\in sl}(\bsimp(r \backslash s')) \cdot r^*))$,
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   573
which again is bounded by $\distinctBy(\sum_{s'\in sl}(\bsimp(r\backslash s')) \cdot r^*)$.
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   574
This might give us a polynomial bound on the length of the list
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   575
$\distinctBy[(\bsimp(r\backslash s')) \cdot r^* | {s'\in sl} ]$, if the terms in 
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   576
$\distinctBy[(\bsimp (r\backslash s')) | {s' \in sl}]$ has a polynomial bound.
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   577
This is unfortunately not true under our current $\distinctBy$ function:
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   578
If we let $r_n = ( (aa)^* + (aaa)^* + \ldots + \underline{(a\ldots a)^*}{n \,a's}) $,
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   579
then we have that $\textit{maxterms} r_n = \textit{sup} (\textit{length} [\bsimp(r_n\backslash s') | s' \in sl]) = 
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   580
L.C.M(1,\ldots, n)$. According to \href{http://oeis.org/A003418}{OEISA003418}
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   581
this grows exponentially quickly. So we have found a regex $r_n$ where
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   582
$\textit{maxterms} (r_n ^* \backslash s) \geq 2^{(n-1)}$.
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   583
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   584
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   585
\subsubsection{stronger version of \distinctBy}
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   586
\href{https://www.researchgate.net/publication/340874991_Partial_derivatives_of_regular_expressions_and_finite_automaton_constructions}{Antimirove}
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   587
has proven a linear bound on the number of terms in the "partial derivatives" of a regular expression:
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   588
\begin{center}
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   589
$\size (\PDER(r))  \leq \awidth (r)$.
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   590
\end{center}
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   591
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   592
The proof is by structural induction on the regular expression r.
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   593
The hard cases are the sequence case $r_1\cdot r_2$ and star case $r^*$.
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   594
The central idea that allows the induction to go through for this bound is on the inclusion:
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   595
\begin{center}
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   596
$\pder_{s@[c]} (a\cdot b) \subseteq (\pder_{s@[c]} a ) \cdot b \cup (\bigcup_{s' \in Suf(s@[c])} (\pder_{s'} \; b))$
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   597
\end{center} 
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   598
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   599
This way, 
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   600
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   601
\begin{center}
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   602
\begin{tabular}{lcl}
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   603
$| \pder_{s@[c]} (a\cdot b) |$ & $ \leq$ & $ | (\pder_{s@[c]} a ) \cdot b \cup (\bigcup_{s' \in Suf(s@[c])} (\pder_{s'} \; b))|$\\
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   604
& $\leq$ & $| (\pder_{s@[c]} a ) \cdot b|  + | (\bigcup_{s' \in Suf(s@[c])} (\pder_{s'} \; b))|$\\
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   605
& $=$ & $\awidth(a) + \awidth(b)$ \\
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   606
& $=$ & $\awidth(a+b)$
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   607
\end{tabular}
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   608
\end{center} 
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   609
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   610
we have that a compound regular expression $a\cdot b$'s subterms
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   611
 is bounded by its sub-expression's derivatives terms.
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   612
 
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   613
This argument can be modified to bound the terms in 
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   614
our  version of regex with strong simplification:
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   615
\begin{center}
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   616
\begin{tabular}{lcl}
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   617
$| \maxterms (\bsimp  (a\cdot b) \backslash s)|$ & $=$ & $ |maxterms(\bsimp( (a\backslash s \cdot b) + \sum_{s'\in sl}(b\backslash s') ))|$\\
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   618
& $\leq$ & $| (\pder_{s@[c]} a ) \cdot b|  + | (\bigcup_{s' \in Suf(s@[c])} (\pder_{s'} \; b))|$\\
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   619
& $=$ & $\awidth(a) + \awidth(b)$ \\
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   620
& $=$ & $\awidth(a+b)$
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   621
\end{tabular}
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   622
\end{center} 
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   623
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   624
440
0856fbf8bda7 bonestruct
Chengsong
parents: 438
diff changeset
   625
0856fbf8bda7 bonestruct
Chengsong
parents: 438
diff changeset
   626
0856fbf8bda7 bonestruct
Chengsong
parents: 438
diff changeset
   627
\subsection{cubic bound}
444
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   628
Bounding the regex's subterms by
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   629
its alphabetic width.
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   630
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   631
The entire expression's size can be bounded by
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   632
number of subterms times each subterms' size.
440
0856fbf8bda7 bonestruct
Chengsong
parents: 438
diff changeset
   633
438
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   634
440
0856fbf8bda7 bonestruct
Chengsong
parents: 438
diff changeset
   635
0856fbf8bda7 bonestruct
Chengsong
parents: 438
diff changeset
   636
0856fbf8bda7 bonestruct
Chengsong
parents: 438
diff changeset
   637
444
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   638
\section{Support for bounded repetitions and other constructs}
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   639
Example: 
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   640
$.*a.\{100\}$ after translation to $\DFA$ and minimization will 
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   641
always take over $2^{100}$ states.
440
0856fbf8bda7 bonestruct
Chengsong
parents: 438
diff changeset
   642
444
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   643
\section{Towards a library with fast running time practically}
440
0856fbf8bda7 bonestruct
Chengsong
parents: 438
diff changeset
   644
444
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   645
registers and cache-related optimizations?
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   646
JVM related optimizations?
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   647
a7e98deebb5c restructured sizebound proof
Chengsong
parents: 443
diff changeset
   648
\section{Past Report materials}
438
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   649
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   650
Deciding whether a string is in the language of the regex
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   651
can be intuitively done by constructing an NFA\cite{Thompson_1968}:
443
c6351a96bf80 writeupforclosedforms
Chengsong
parents: 441
diff changeset
   652
and simulate the running of it.
438
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   653
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   654
Which should be simple enough that modern programmers
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   655
have no problems with it at all?
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   656
Not really:
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   657
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   658
Take $(a^*)^*\,b$ and ask whether
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   659
strings of the form $aa..a$ match this regular
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   660
expression. Obviously this is not the case---the expected $b$ in the last
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   661
position is missing. One would expect that modern regular expression
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   662
matching engines can find this out very quickly. Alas, if one tries
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   663
this example in JavaScript, Python or Java 8 with strings like 28
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   664
$a$'s, one discovers that this decision takes around 30 seconds and
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   665
takes considerably longer when adding a few more $a$'s, as the graphs
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   666
below show:
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   667
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   668
\begin{center}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   669
\begin{tabular}{@{}c@{\hspace{0mm}}c@{\hspace{0mm}}c@{}}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   670
\begin{tikzpicture}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   671
\begin{axis}[
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   672
    xlabel={$n$},
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   673
    x label style={at={(1.05,-0.05)}},
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   674
    ylabel={time in secs},
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   675
    enlargelimits=false,
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   676
    xtick={0,5,...,30},
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   677
    xmax=33,
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   678
    ymax=35,
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   679
    ytick={0,5,...,30},
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   680
    scaled ticks=false,
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   681
    axis lines=left,
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   682
    width=5cm,
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   683
    height=4cm, 
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   684
    legend entries={JavaScript},  
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   685
    legend pos=north west,
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   686
    legend cell align=left]
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   687
\addplot[red,mark=*, mark options={fill=white}] table {re-js.data};
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   688
\end{axis}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   689
\end{tikzpicture}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   690
  &
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   691
\begin{tikzpicture}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   692
\begin{axis}[
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   693
    xlabel={$n$},
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   694
    x label style={at={(1.05,-0.05)}},
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   695
    %ylabel={time in secs},
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   696
    enlargelimits=false,
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   697
    xtick={0,5,...,30},
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   698
    xmax=33,
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   699
    ymax=35,
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   700
    ytick={0,5,...,30},
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   701
    scaled ticks=false,
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   702
    axis lines=left,
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   703
    width=5cm,
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   704
    height=4cm, 
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   705
    legend entries={Python},  
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   706
    legend pos=north west,
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   707
    legend cell align=left]
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   708
\addplot[blue,mark=*, mark options={fill=white}] table {re-python2.data};
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   709
\end{axis}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   710
\end{tikzpicture}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   711
  &
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   712
\begin{tikzpicture}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   713
\begin{axis}[
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   714
    xlabel={$n$},
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   715
    x label style={at={(1.05,-0.05)}},
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   716
    %ylabel={time in secs},
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   717
    enlargelimits=false,
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   718
    xtick={0,5,...,30},
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   719
    xmax=33,
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   720
    ymax=35,
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   721
    ytick={0,5,...,30},
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   722
    scaled ticks=false,
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   723
    axis lines=left,
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   724
    width=5cm,
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   725
    height=4cm, 
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   726
    legend entries={Java 8},  
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   727
    legend pos=north west,
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   728
    legend cell align=left]
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   729
\addplot[cyan,mark=*, mark options={fill=white}] table {re-java.data};
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   730
\end{axis}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   731
\end{tikzpicture}\\
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   732
\multicolumn{3}{c}{Graphs: Runtime for matching $(a^*)^*\,b$ with strings 
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   733
           of the form $\underbrace{aa..a}_{n}$.}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   734
\end{tabular}    
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   735
\end{center}  
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   736
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   737
Why?
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   738
Using $\textit{NFA}$'s that can backtrack.
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   739
%TODO: what does it mean to do DFS BFS on NFA's
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   740
	
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   741
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   742
Then how about determinization?
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   743
\begin{itemize}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   744
\item
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   745
 Turning NFA's to DFA's can cause the size of the automata
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   746
to blow up exponentially.
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   747
\item
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   748
Want to extract submatch information.
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   749
For example, 
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   750
$r_1 \cdot r_2$ matches $s$,
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   751
want to know $s = s_1@s_2$ where $s_i$ 
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   752
corresponds to $r_i$. Where $s_i$ might be the
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   753
attacker's ip address.
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   754
\item
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   755
Variants such as counting automaton exist.
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   756
But usually made super fast on a certain class
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   757
of regexes like bounded repetitions:
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   758
\begin{verbatim}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   759
.*a.{100}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   760
\end{verbatim}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   761
On a lot of inputs this works very well.
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   762
On average good practical performance.
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   763
~10MiB per second.
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   764
But cannot be super fast on all inputs of regexes and strings,
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   765
can be imprecise (incorrect) when it comes to more complex regexes.
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   766
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   767
\end{itemize}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   768
%TODO: real world example?
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   769
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   770
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   771
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   772
\subsection{derivatives}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   773
Q:
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   774
Is there an efficient lexing algorithm with provable guarantees on 
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   775
correctness and running time?
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   776
Brzozowski Derivatives\cite{Brzozowski1964}!
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   777
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   778
\begin{center}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   779
		\begin{tabular}{lcl}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   780
			$\nullable(\ZERO)$     & $\dn$ & $\mathit{false}$ \\  
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   781
			$\nullable(\ONE)$      & $\dn$ & $\mathit{true}$ \\
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   782
			$\nullable(c)$ 	       & $\dn$ & $\mathit{false}$ \\
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   783
			$\nullable(r_1 + r_2)$ & $\dn$ & $\nullable(r_1) \vee \nullable(r_2)$ \\
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   784
			$\nullable(r_1\cdot r_2)$  & $\dn$ & $\nullable(r_1) \wedge \nullable(r_2)$ \\
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   785
			$\nullable(r^*)$       & $\dn$ & $\mathit{true}$ \\
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   786
		\end{tabular}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   787
	\end{center}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   788
	
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   789
	
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   790
	
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   791
This function simply tests whether the empty string is in $L(r)$.
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   792
He then defined
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   793
the following operation on regular expressions, written
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   794
$r\backslash c$ (the derivative of $r$ w.r.t.~the character $c$):
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   795
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   796
\begin{center}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   797
\begin{tabular}{lcl}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   798
		$\ZERO \backslash c$ & $\dn$ & $\ZERO$\\  
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   799
		$\ONE \backslash c$  & $\dn$ & $\ZERO$\\
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   800
		$d \backslash c$     & $\dn$ & 
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   801
		$\mathit{if} \;c = d\;\mathit{then}\;\ONE\;\mathit{else}\;\ZERO$\\
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   802
$(r_1 + r_2)\backslash c$     & $\dn$ & $r_1 \backslash c \,+\, r_2 \backslash c$\\
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   803
$(r_1 \cdot r_2)\backslash c$ & $\dn$ & $\mathit{if} \, nullable(r_1)$\\
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   804
	&   & $\mathit{then}\;(r_1\backslash c) \cdot r_2 \,+\, r_2\backslash c$\\
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   805
	&   & $\mathit{else}\;(r_1\backslash c) \cdot r_2$\\
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   806
	$(r^*)\backslash c$           & $\dn$ & $(r\backslash c) \cdot r^*$\\
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   807
\end{tabular}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   808
\end{center}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   809
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   810
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   811
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   812
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   813
\begin{ceqn}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   814
\begin{equation}\label{graph:01}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   815
\begin{tikzcd}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   816
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] \\
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   817
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]         
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   818
\end{tikzcd}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   819
\end{equation}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   820
\end{ceqn}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   821
Nicely functional, correctness easily provable, but suffers
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   822
from large stack size with long strings, and 
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   823
inability to perform even moderate simplification.
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   824
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   825
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   826
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   827
The Sulzmann and Lu's bit-coded algorithm:
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   828
\begin{figure}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   829
\centering
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   830
\includegraphics[scale=0.3]{bitcoded_sulzmann.png}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   831
\end{figure}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   832
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   833
This one-phase algorithm is free from the burden of large stack usage:
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   834
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   835
\begin{center}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   836
\begin{tikzpicture}[scale=2,node distance=1.9cm,
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   837
                    every node/.style={minimum size=7mm}]
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   838
\node (r0)  {$r_0$};
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   839
\node (r1) [right=of r0]{$r_1$};
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   840
\draw[->,line width=0.2mm](r0)--(r1) node[above,midway] {$\backslash\,c_0$};
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   841
\node (r2) [right=of r1]{$r_2$};
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   842
\draw[->, line width = 0.2mm](r1)--(r2) node[above,midway] {$\backslash\,c_1$};
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   843
\node (rn) [right=of r2]{$r_n$};
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   844
\draw[dashed,->,line width=0.2mm](r2)--(rn) node[above,midway] {} ;
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   845
\draw (rn) node[anchor=west] {\;\raisebox{3mm}{$\nullable$}};
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   846
\node (bs) [below=of rn]{$bs$};
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   847
\draw[->,line width=0.2mm](rn) -- (bs);
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   848
\node (v0) [left=of bs] {$v_0$};
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   849
\draw[->,line width=0.2mm](bs)--(v0) node[below,midway] {$\textit{decode}$};
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   850
\draw (rn) node[anchor=north west] {\;\raisebox{-8mm}{$\textit{collect bits}$}};
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   851
\draw[->, line width=0.2mm](v0)--(r0) node[below, midway] {};
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   852
\end{tikzpicture}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   853
\end{center}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   854
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   855
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   856
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   857
This is functional code, and easily provable (proof by Urban and Ausaf).
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   858
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   859
But it suffers from exponential blows even with the simplification steps:
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   860
\begin{figure}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   861
\centering
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   862
\includegraphics[scale= 0.3]{pics/nub_filter_simp.png}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   863
\end{figure}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   864
claim: Sulzmann and Lu claimed it linear $w.r.t$ input.
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   865
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   866
example that blows it up:
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   867
$(a+aa)^*$
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   868
\section{Contributions}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   869
\subsection{Our contribution 1}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   870
an improved version of the above algorithm that solves most blow up 
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   871
cases, including the above example.
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   872
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   873
a formalized closed-form for string derivatives:
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   874
\[ (\sum rs) \backslash_s s = simp(\sum_{r \in rs}(r \backslash_s s)) \]
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   875
\[ (r1\cdot r2) \backslash_s s = simp(r_1 \backslash_s s  \cdot r_2 + \sum_{s' \in Suffix(s)} r_2 \backslash_s s' )\]
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   876
\[r0^* \backslash_s s = simp(\sum_{s' \in substr(s)} (r0 \backslash_s s') \cdot r0^*) \]
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   877
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   878
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   879
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   880
Also with a size guarantee that make sure the size of the derivatives 
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   881
don't go up unbounded.
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   882
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   883
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   884
\begin{theorem}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   885
Given a regular expression r, we have 
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   886
\begin{center}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   887
$\exists N_r.\; s.t. \;\forall s. \; |r \backslash_s s| < N_r$
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   888
\end{center}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   889
\end{theorem}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   890
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   891
The proof for this is using partial derivative's terms to bound it.
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   892
\begin{center}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   893
\begin{tabular}{lcl}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   894
$| \maxterms (\bsimp  (a\cdot b) \backslash s)|$ & $=$ & $ |maxterms(\bsimp( (a\backslash s \cdot b) + \sum_{s'\in sl}(b\backslash s') ))|$\\
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   895
& $\leq$ & $| (\pder_{s@[c]} a ) \cdot b|  + | (\bigcup_{s' \in Suf(s@[c])} (\pder_{s'} \; b))|$\\
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   896
& $=$ & $\awidth(a) + \awidth(b)$ \\
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   897
& $=$ & $\awidth(a+b)$
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   898
\end{tabular}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   899
\end{center} 
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   900
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   901
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   902
\subsection{Our Contribution 2}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   903
more aggressive simplification that prunes away sub-parts
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   904
of a regex based on what terms has appeared before.
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   905
Which gives us a truly linear bound on the input length.
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   906
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   907
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   908
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   909
\section{To be completed}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   910
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   911
benchmarking our algorithm against JFLEX
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   912
counting set automata, Silex, other main regex engines (incorporate their ideas such
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   913
as zippers and other data structures reducing memory use).
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   914
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   915
extend to back references.
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   916
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   917
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   918
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   919
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   920
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   921
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   922
\noindent These are clearly abysmal and possibly surprising results. One
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   923
would expect these systems to do  much better than that---after all,
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   924
given a DFA and a string, deciding whether a string is matched by this
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   925
DFA should be linear in terms of the size of the regular expression and
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   926
the string?
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   927
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   928
Admittedly, the regular expression $(a^*)^*\,b$ is carefully chosen to
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   929
exhibit this super-linear behaviour.  But unfortunately, such regular
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   930
expressions are not just a few outliers. They are actually 
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   931
frequent enough to have a separate name created for
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   932
them---\emph{evil regular expressions}. In empiric work, Davis et al
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   933
report that they have found thousands of such evil regular expressions
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   934
in the JavaScript and Python ecosystems \cite{Davis18}. Static analysis
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   935
approach that is both sound and complete exists\cite{17Bir}, but the running 
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   936
time on certain examples in the RegExLib and Snort regular expressions
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   937
libraries is unacceptable. Therefore the problem of efficiency still remains.
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   938
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   939
This superlinear blowup in matching algorithms sometimes causes
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   940
considerable grief in real life: for example on 20 July 2016 one evil
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   941
regular expression brought the webpage
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   942
\href{http://stackexchange.com}{Stack Exchange} to its
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   943
knees.\footnote{\url{https://stackstatus.net/post/147710624694/outage-postmortem-july-20-2016}}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   944
In this instance, a regular expression intended to just trim white
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   945
spaces from the beginning and the end of a line actually consumed
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   946
massive amounts of CPU-resources---causing web servers to grind to a
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   947
halt. This happened when a post with 20,000 white spaces was submitted,
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   948
but importantly the white spaces were neither at the beginning nor at
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   949
the end. As a result, the regular expression matching engine needed to
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   950
backtrack over many choices. In this example, the time needed to process
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   951
the string was $O(n^2)$ with respect to the string length. This
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   952
quadratic overhead was enough for the homepage of Stack Exchange to
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   953
respond so slowly that the load balancer assumed there must be some
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   954
attack and therefore stopped the servers from responding to any
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   955
requests. This made the whole site become unavailable. Another very
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   956
recent example is a global outage of all Cloudflare servers on 2 July
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   957
2019. A poorly written regular expression exhibited exponential
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   958
behaviour and exhausted CPUs that serve HTTP traffic. Although the
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   959
outage had several causes, at the heart was a regular expression that
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   960
was used to monitor network
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   961
traffic.\footnote{\url{https://blog.cloudflare.com/details-of-the-cloudflare-outage-on-july-2-2019/}}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   962
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   963
The underlying problem is that many ``real life'' regular expression
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   964
matching engines do not use DFAs for matching. This is because they
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   965
support regular expressions that are not covered by the classical
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   966
automata theory, and in this more general setting there are quite a few
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   967
research questions still unanswered and fast algorithms still need to be
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   968
developed (for example how to treat efficiently bounded repetitions, negation and
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   969
back-references).
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   970
%question: dfa can have exponential states. isn't this the actual reason why they do not use dfas?
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   971
%how do they avoid dfas exponential states if they use them for fast matching?
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   972
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   973
There is also another under-researched problem to do with regular
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   974
expressions and lexing, i.e.~the process of breaking up strings into
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   975
sequences of tokens according to some regular expressions. In this
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   976
setting one is not just interested in whether or not a regular
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   977
expression matches a string, but also in \emph{how}.  Consider for
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   978
example a regular expression $r_{key}$ for recognising keywords such as
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   979
\textit{if}, \textit{then} and so on; and a regular expression $r_{id}$
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   980
for recognising identifiers (say, a single character followed by
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   981
characters or numbers). One can then form the compound regular
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   982
expression $(r_{key} + r_{id})^*$ and use it to tokenise strings.  But
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   983
then how should the string \textit{iffoo} be tokenised?  It could be
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   984
tokenised as a keyword followed by an identifier, or the entire string
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   985
as a single identifier.  Similarly, how should the string \textit{if} be
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   986
tokenised? Both regular expressions, $r_{key}$ and $r_{id}$, would
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   987
``fire''---so is it an identifier or a keyword?  While in applications
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   988
there is a well-known strategy to decide these questions, called POSIX
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   989
matching, only relatively recently precise definitions of what POSIX
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   990
matching actually means have been formalised
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   991
\cite{AusafDyckhoffUrban2016,OkuiSuzuki2010,Vansummeren2006}. Such a
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   992
definition has also been given by Sulzmann and  Lu \cite{Sulzmann2014},
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   993
but the corresponding correctness proof turned out to be  faulty
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   994
\cite{AusafDyckhoffUrban2016}. Roughly, POSIX matching means matching
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   995
the longest initial substring. In the case of a tie, the initial
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   996
sub-match is chosen according to some priorities attached to the regular
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   997
expressions (e.g.~keywords have a higher priority than identifiers).
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   998
This sounds rather simple, but according to Grathwohl et al \cite[Page
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
   999
36]{CrashCourse2014} this is not the case. They wrote:
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1000
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1001
\begin{quote}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1002
\it{}``The POSIX strategy is more complicated than the greedy because of 
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1003
the dependence on information about the length of matched strings in the 
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1004
various subexpressions.''
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1005
\end{quote}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1006
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1007
\noindent
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1008
This is also supported by evidence collected by Kuklewicz
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1009
\cite{Kuklewicz} who noticed that a number of POSIX regular expression
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1010
matchers calculate incorrect results.
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1011
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1012
Our focus in this project is on an algorithm introduced by Sulzmann and
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1013
Lu in 2014 for regular expression matching according to the POSIX
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1014
strategy \cite{Sulzmann2014}. Their algorithm is based on an older
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1015
algorithm by Brzozowski from 1964 where he introduced the notion of
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1016
derivatives of regular expressions~\cite{Brzozowski1964}. We shall
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1017
briefly explain this algorithm next.
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1018
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1019
\section{The Algorithm by Brzozowski based on Derivatives of Regular
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1020
Expressions}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1021
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1022
Suppose (basic) regular expressions are given by the following grammar:
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1023
\[			r ::=   \ZERO \mid  \ONE
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1024
			 \mid  c  
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1025
			 \mid  r_1 \cdot r_2
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1026
			 \mid  r_1 + r_2   
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1027
			 \mid r^*         
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1028
\]
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1029
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1030
\noindent
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1031
The intended meaning of the constructors is as follows: $\ZERO$
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1032
cannot match any string, $\ONE$ can match the empty string, the
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1033
character regular expression $c$ can match the character $c$, and so
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1034
on.
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1035
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1036
The ingenious contribution by Brzozowski is the notion of
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1037
\emph{derivatives} of regular expressions.  The idea behind this
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1038
notion is as follows: suppose a regular expression $r$ can match a
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1039
string of the form $c\!::\! s$ (that is a list of characters starting
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1040
with $c$), what does the regular expression look like that can match
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1041
just $s$? Brzozowski gave a neat answer to this question. He started
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1042
with the definition of $nullable$:
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1043
\begin{center}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1044
		\begin{tabular}{lcl}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1045
			$\nullable(\ZERO)$     & $\dn$ & $\mathit{false}$ \\  
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1046
			$\nullable(\ONE)$      & $\dn$ & $\mathit{true}$ \\
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1047
			$\nullable(c)$ 	       & $\dn$ & $\mathit{false}$ \\
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1048
			$\nullable(r_1 + r_2)$ & $\dn$ & $\nullable(r_1) \vee \nullable(r_2)$ \\
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1049
			$\nullable(r_1\cdot r_2)$  & $\dn$ & $\nullable(r_1) \wedge \nullable(r_2)$ \\
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1050
			$\nullable(r^*)$       & $\dn$ & $\mathit{true}$ \\
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1051
		\end{tabular}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1052
	\end{center}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1053
This function simply tests whether the empty string is in $L(r)$.
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1054
He then defined
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1055
the following operation on regular expressions, written
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1056
$r\backslash c$ (the derivative of $r$ w.r.t.~the character $c$):
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1057
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1058
\begin{center}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1059
\begin{tabular}{lcl}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1060
		$\ZERO \backslash c$ & $\dn$ & $\ZERO$\\  
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1061
		$\ONE \backslash c$  & $\dn$ & $\ZERO$\\
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1062
		$d \backslash c$     & $\dn$ & 
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1063
		$\mathit{if} \;c = d\;\mathit{then}\;\ONE\;\mathit{else}\;\ZERO$\\
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1064
$(r_1 + r_2)\backslash c$     & $\dn$ & $r_1 \backslash c \,+\, r_2 \backslash c$\\
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1065
$(r_1 \cdot r_2)\backslash c$ & $\dn$ & $\mathit{if} \, nullable(r_1)$\\
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1066
	&   & $\mathit{then}\;(r_1\backslash c) \cdot r_2 \,+\, r_2\backslash c$\\
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1067
	&   & $\mathit{else}\;(r_1\backslash c) \cdot r_2$\\
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1068
	$(r^*)\backslash c$           & $\dn$ & $(r\backslash c) \cdot r^*$\\
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1069
\end{tabular}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1070
\end{center}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1071
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1072
%Assuming the classic notion of a
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1073
%\emph{language} of a regular expression, written $L(\_)$, t
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1074
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1075
\noindent
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1076
The main property of the derivative operation is that
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1077
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1078
\begin{center}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1079
$c\!::\!s \in L(r)$ holds
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1080
if and only if $s \in L(r\backslash c)$.
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1081
\end{center}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1082
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1083
\noindent
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1084
For us the main advantage is that derivatives can be
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1085
straightforwardly implemented in any functional programming language,
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1086
and are easily definable and reasoned about in theorem provers---the
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1087
definitions just consist of inductive datatypes and simple recursive
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1088
functions. Moreover, the notion of derivatives can be easily
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1089
generalised to cover extended regular expression constructors such as
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1090
the not-regular expression, written $\neg\,r$, or bounded repetitions
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1091
(for example $r^{\{n\}}$ and $r^{\{n..m\}}$), which cannot be so
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1092
straightforwardly realised within the classic automata approach.
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1093
For the moment however, we focus only on the usual basic regular expressions.
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1094
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1095
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1096
Now if we want to find out whether a string $s$ matches with a regular
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1097
expression $r$, we can build the derivatives of $r$ w.r.t.\ (in succession)
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1098
all the characters of the string $s$. Finally, test whether the
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1099
resulting regular expression can match the empty string.  If yes, then
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1100
$r$ matches $s$, and no in the negative case. To implement this idea
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1101
we can generalise the derivative operation to strings like this:
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1102
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1103
\begin{center}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1104
\begin{tabular}{lcl}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1105
$r \backslash (c\!::\!s) $ & $\dn$ & $(r \backslash c) \backslash s$ \\
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1106
$r \backslash [\,] $ & $\dn$ & $r$
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1107
\end{tabular}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1108
\end{center}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1109
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1110
\noindent
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1111
and then define as  regular-expression matching algorithm: 
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1112
\[
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1113
match\;s\;r \;\dn\; nullable(r\backslash s)
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1114
\]
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1115
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1116
\noindent
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1117
This algorithm looks graphically as follows:
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1118
\begin{equation}\label{graph:*}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1119
\begin{tikzcd}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1120
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}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1121
\end{tikzcd}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1122
\end{equation}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1123
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1124
\noindent
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1125
where we start with  a regular expression  $r_0$, build successive
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1126
derivatives until we exhaust the string and then use \textit{nullable}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1127
to test whether the result can match the empty string. It can  be
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1128
relatively  easily shown that this matcher is correct  (that is given
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1129
an $s = c_0...c_{n-1}$ and an $r_0$, it generates YES if and only if $s \in L(r_0)$).
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1130
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1131
 
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1132
\section{Values and the Algorithm by Sulzmann and Lu}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1133
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1134
One limitation of Brzozowski's algorithm is that it only produces a
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1135
YES/NO answer for whether a string is being matched by a regular
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1136
expression.  Sulzmann and Lu~\cite{Sulzmann2014} extended this algorithm
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1137
to allow generation of an actual matching, called a \emph{value} or
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1138
sometimes also \emph{lexical value}.  These values and regular
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1139
expressions correspond to each other as illustrated in the following
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1140
table:
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1141
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1142
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1143
\begin{center}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1144
	\begin{tabular}{c@{\hspace{20mm}}c}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1145
		\begin{tabular}{@{}rrl@{}}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1146
			\multicolumn{3}{@{}l}{\textbf{Regular Expressions}}\medskip\\
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1147
			$r$ & $::=$  & $\ZERO$\\
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1148
			& $\mid$ & $\ONE$   \\
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1149
			& $\mid$ & $c$          \\
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1150
			& $\mid$ & $r_1 \cdot r_2$\\
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1151
			& $\mid$ & $r_1 + r_2$   \\
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1152
			\\
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1153
			& $\mid$ & $r^*$         \\
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1154
		\end{tabular}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1155
		&
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1156
		\begin{tabular}{@{\hspace{0mm}}rrl@{}}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1157
			\multicolumn{3}{@{}l}{\textbf{Values}}\medskip\\
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1158
			$v$ & $::=$  & \\
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1159
			&        & $\Empty$   \\
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1160
			& $\mid$ & $\Char(c)$          \\
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1161
			& $\mid$ & $\Seq\,v_1\, v_2$\\
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1162
			& $\mid$ & $\Left(v)$   \\
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1163
			& $\mid$ & $\Right(v)$  \\
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1164
			& $\mid$ & $\Stars\,[v_1,\ldots\,v_n]$ \\
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1165
		\end{tabular}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1166
	\end{tabular}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1167
\end{center}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1168
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1169
\noindent
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1170
No value  corresponds to $\ZERO$; $\Empty$ corresponds to $\ONE$;
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1171
$\Char$ to the character regular expression; $\Seq$ to the sequence
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1172
regular expression and so on. The idea of values is to encode a kind of
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1173
lexical value for how the sub-parts of a regular expression match the
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1174
sub-parts of a string. To see this, suppose a \emph{flatten} operation,
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1175
written $|v|$ for values. We can use this function to extract the
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1176
underlying string of a value $v$. For example, $|\mathit{Seq} \,
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1177
(\textit{Char x}) \, (\textit{Char y})|$ is the string $xy$.  Using
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1178
flatten, we can describe how values encode lexical values: $\Seq\,v_1\,
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1179
v_2$ encodes a tree with two children nodes that tells how the string
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1180
$|v_1| @ |v_2|$ matches the regex $r_1 \cdot r_2$ whereby $r_1$ matches
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1181
the substring $|v_1|$ and, respectively, $r_2$ matches the substring
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1182
$|v_2|$. Exactly how these two are matched is contained in the children
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1183
nodes $v_1$ and $v_2$ of parent $\textit{Seq}$. 
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1184
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1185
To give a concrete example of how values work, consider the string $xy$
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1186
and the regular expression $(x + (y + xy))^*$. We can view this regular
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1187
expression as a tree and if the string $xy$ is matched by two Star
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1188
``iterations'', then the $x$ is matched by the left-most alternative in
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1189
this tree and the $y$ by the right-left alternative. This suggests to
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1190
record this matching as
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1191
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1192
\begin{center}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1193
$\Stars\,[\Left\,(\Char\,x), \Right(\Left(\Char\,y))]$
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1194
\end{center}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1195
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1196
\noindent
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1197
where $\Stars \; [\ldots]$ records all the
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1198
iterations; and $\Left$, respectively $\Right$, which
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1199
alternative is used. The value for
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1200
matching $xy$ in a single ``iteration'', i.e.~the POSIX value,
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1201
would look as follows
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1202
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1203
\begin{center}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1204
$\Stars\,[\Seq\,(\Char\,x)\,(\Char\,y)]$
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1205
\end{center}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1206
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1207
\noindent
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1208
where $\Stars$ has only a single-element list for the single iteration
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1209
and $\Seq$ indicates that $xy$ is matched by a sequence regular
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1210
expression.
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1211
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1212
The contribution of Sulzmann and Lu is an extension of Brzozowski's
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1213
algorithm by a second phase (the first phase being building successive
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1214
derivatives---see \eqref{graph:*}). In this second phase, a POSIX value 
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1215
is generated in case the regular expression matches  the string. 
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1216
Pictorially, the Sulzmann and Lu algorithm is as follows:
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1217
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1218
\begin{ceqn}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1219
\begin{equation}\label{graph:2}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1220
\begin{tikzcd}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1221
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] \\
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1222
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]         
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1223
\end{tikzcd}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1224
\end{equation}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1225
\end{ceqn}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1226
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1227
\noindent
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1228
For convenience, we shall employ the following notations: the regular
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1229
expression we start with is $r_0$, and the given string $s$ is composed
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1230
of characters $c_0 c_1 \ldots c_{n-1}$. In  the first phase from the
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1231
left to right, we build the derivatives $r_1$, $r_2$, \ldots  according
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1232
to the characters $c_0$, $c_1$  until we exhaust the string and obtain
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1233
the derivative $r_n$. We test whether this derivative is
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1234
$\textit{nullable}$ or not. If not, we know the string does not match
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1235
$r$ and no value needs to be generated. If yes, we start building the
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1236
values incrementally by \emph{injecting} back the characters into the
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1237
earlier values $v_n, \ldots, v_0$. This is the second phase of the
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1238
algorithm from the right to left. For the first value $v_n$, we call the
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1239
function $\textit{mkeps}$, which builds the lexical value
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1240
for how the empty string has been matched by the (nullable) regular
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1241
expression $r_n$. This function is defined as
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1242
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1243
	\begin{center}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1244
		\begin{tabular}{lcl}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1245
			$\mkeps(\ONE)$ 		& $\dn$ & $\Empty$ \\
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1246
			$\mkeps(r_{1}+r_{2})$	& $\dn$ 
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1247
			& \textit{if} $\nullable(r_{1})$\\ 
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1248
			& & \textit{then} $\Left(\mkeps(r_{1}))$\\ 
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1249
			& & \textit{else} $\Right(\mkeps(r_{2}))$\\
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1250
			$\mkeps(r_1\cdot r_2)$ 	& $\dn$ & $\Seq\,(\mkeps\,r_1)\,(\mkeps\,r_2)$\\
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1251
			$mkeps(r^*)$	        & $\dn$ & $\Stars\,[]$
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1252
		\end{tabular}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1253
	\end{center}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1254
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1255
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1256
\noindent There are no cases for $\ZERO$ and $c$, since
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1257
these regular expression cannot match the empty string. Note
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1258
also that in case of alternatives we give preference to the
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1259
regular expression on the left-hand side. This will become
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1260
important later on about what value is calculated.
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1261
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1262
After the $\mkeps$-call, we inject back the characters one by one in order to build
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1263
the lexical value $v_i$ for how the regex $r_i$ matches the string $s_i$
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1264
($s_i = c_i \ldots c_{n-1}$ ) from the previous lexical value $v_{i+1}$.
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1265
After injecting back $n$ characters, we get the lexical value for how $r_0$
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1266
matches $s$. For this Sulzmann and Lu defined a function that reverses
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1267
the ``chopping off'' of characters during the derivative phase. The
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1268
corresponding function is called \emph{injection}, written
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1269
$\textit{inj}$; it takes three arguments: the first one is a regular
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1270
expression ${r_{i-1}}$, before the character is chopped off, the second
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1271
is a character ${c_{i-1}}$, the character we want to inject and the
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1272
third argument is the value ${v_i}$, into which one wants to inject the
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1273
character (it corresponds to the regular expression after the character
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1274
has been chopped off). The result of this function is a new value. The
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1275
definition of $\textit{inj}$ is as follows: 
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1276
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1277
\begin{center}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1278
\begin{tabular}{l@{\hspace{1mm}}c@{\hspace{1mm}}l}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1279
  $\textit{inj}\,(c)\,c\,Empty$            & $\dn$ & $Char\,c$\\
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1280
  $\textit{inj}\,(r_1 + r_2)\,c\,\Left(v)$ & $\dn$ & $\Left(\textit{inj}\,r_1\,c\,v)$\\
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1281
  $\textit{inj}\,(r_1 + r_2)\,c\,Right(v)$ & $\dn$ & $Right(\textit{inj}\,r_2\,c\,v)$\\
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1282
  $\textit{inj}\,(r_1 \cdot r_2)\,c\,Seq(v_1,v_2)$ & $\dn$  & $Seq(\textit{inj}\,r_1\,c\,v_1,v_2)$\\
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1283
  $\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)$\\
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1284
  $\textit{inj}\,(r_1 \cdot r_2)\,c\,Right(v)$ & $\dn$  & $Seq(\textit{mkeps}(r_1),\textit{inj}\,r_2\,c\,v)$\\
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1285
  $\textit{inj}\,(r^*)\,c\,Seq(v,Stars\,vs)$         & $\dn$  & $Stars((\textit{inj}\,r\,c\,v)\,::\,vs)$\\
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1286
\end{tabular}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1287
\end{center}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1288
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1289
\noindent This definition is by recursion on the ``shape'' of regular
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1290
expressions and values. To understands this definition better consider
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1291
the situation when we build the derivative on regular expression $r_{i-1}$.
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1292
For this we chop off a character from $r_{i-1}$ to form $r_i$. This leaves a
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1293
``hole'' in $r_i$ and its corresponding value $v_i$. 
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1294
To calculate $v_{i-1}$, we need to
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1295
locate where that hole is and fill it. 
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1296
We can find this location by
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1297
comparing $r_{i-1}$ and $v_i$. For instance, if $r_{i-1}$ is of shape
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1298
$r_a \cdot r_b$, and $v_i$ is of shape $\Left(Seq(v_1,v_2))$, we know immediately that 
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1299
%
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1300
\[ (r_a \cdot r_b)\backslash c = (r_a\backslash c) \cdot r_b \,+\, r_b\backslash c,\]
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1301
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1302
\noindent
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1303
otherwise if $r_a$ is not nullable,
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1304
\[ (r_a \cdot r_b)\backslash c = (r_a\backslash c) \cdot r_b,\]
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1305
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1306
\noindent
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1307
the value $v_i$ should be  $\Seq(\ldots)$, contradicting the fact that
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1308
$v_i$ is actually of shape $\Left(\ldots)$. Furthermore, since $v_i$ is of shape
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1309
$\Left(\ldots)$ instead of $\Right(\ldots)$, we know that the left
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1310
branch of \[ (r_a \cdot r_b)\backslash c =
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1311
\bold{\underline{ (r_a\backslash c) \cdot r_b} }\,+\, r_b\backslash c,\](underlined)
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1312
 is taken instead of the right one. This means $c$ is chopped off 
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1313
from $r_a$ rather than $r_b$.
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1314
We have therefore found out 
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1315
that the hole will be on $r_a$. So we recursively call $\inj\, 
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1316
r_a\,c\,v_a$ to fill that hole in $v_a$. After injection, the value 
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1317
$v_i$ for $r_i = r_a \cdot r_b$ should be $\Seq\,(\inj\,r_a\,c\,v_a)\,v_b$.
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1318
Other clauses can be understood in a similar way.
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1319
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1320
%\comment{Other word: insight?}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1321
The following example gives an insight of $\textit{inj}$'s effect and
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1322
how Sulzmann and Lu's algorithm works as a whole. Suppose we have a
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1323
regular expression $((((a+b)+ab)+c)+abc)^*$, and want to match it
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1324
against the string $abc$ (when $abc$ is written as a regular expression,
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1325
the standard way of expressing it is $a \cdot (b \cdot c)$. But we
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1326
usually omit the parentheses and dots here for better readability. This
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1327
algorithm returns a POSIX value, which means it will produce the longest
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1328
matching. Consequently, it matches the string $abc$ in one star
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1329
iteration, using the longest alternative $abc$ in the sub-expression (we shall use $r$ to denote this
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1330
sub-expression for conciseness):
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1331
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1332
\[((((a+b)+ab)+c)+\underbrace{abc}_r)\] 
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1333
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1334
\noindent
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1335
Before $\textit{inj}$ is called, our lexer first builds derivative using
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1336
string $abc$ (we simplified some regular expressions like $\ZERO \cdot
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1337
b$ to $\ZERO$ for conciseness; we also omit parentheses if they are
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1338
clear from the context):
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1339
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1340
%Similarly, we allow
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1341
%$\textit{ALT}$ to take a list of regular expressions as an argument
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1342
%instead of just 2 operands to reduce the nested depth of
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1343
%$\textit{ALT}$
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1344
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1345
\begin{center}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1346
\begin{tabular}{lcl}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1347
$r^*$ & $\xrightarrow{\backslash a}$ & $r_1 = (\ONE+\ZERO+\ONE \cdot b + \ZERO + \ONE \cdot b \cdot c) \cdot r^*$\\
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1348
      & $\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^*$\\
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1349
      & $\xrightarrow{\backslash c}$ & $r_3 = ((\ZERO+\ZERO+\ZERO + \ZERO + \ONE \cdot \ONE \cdot \ONE) \cdot r^* + (\ZERO+\ZERO+\ZERO  + \ONE + \ZERO) \cdot r^*) + $\\ 
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1350
      &                              & $\phantom{r_3 = (} ((\ZERO+\ONE+\ZERO  + \ZERO + \ZERO) \cdot r^* + (\ZERO+\ZERO+\ZERO  + \ONE + \ZERO) \cdot r^* )$
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1351
\end{tabular}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1352
\end{center}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1353
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1354
\noindent
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1355
In  case $r_3$ is nullable, we can call $\textit{mkeps}$ 
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1356
to construct a lexical value for how $r_3$ matched the string $abc$. 
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1357
This function gives the following value $v_3$: 
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1358
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1359
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1360
\begin{center}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1361
$\Left(\Left(\Seq(\Right(\Seq(\Empty, \Seq(\Empty,\Empty))), \Stars [])))$
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1362
\end{center}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1363
The outer $\Left(\Left(\ldots))$ tells us the leftmost nullable part of $r_3$(underlined):
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1364
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1365
\begin{center}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1366
	\begin{tabular}{l@{\hspace{2mm}}l}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1367
    & $\big(\underline{(\ZERO+\ZERO+\ZERO+ \ZERO+ \ONE \cdot \ONE \cdot \ONE) \cdot r^*} 
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1368
    \;+\; (\ZERO+\ZERO+\ZERO + \ONE + \ZERO) \cdot r^*\big)$ \smallskip\\
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1369
    $+$ & $\big((\ZERO+\ONE+\ZERO  + \ZERO + \ZERO) \cdot r^*
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1370
    \;+\; (\ZERO+\ZERO+\ZERO  + \ONE + \ZERO) \cdot r^* \big)$
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1371
  	\end{tabular}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1372
 \end{center}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1373
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1374
\noindent
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1375
 Note that the leftmost location of term $(\ZERO+\ZERO+\ZERO + \ZERO + \ONE \cdot \ONE \cdot
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1376
 \ONE) \cdot r^*$ (which corresponds to the initial sub-match $abc$) allows
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1377
 $\textit{mkeps}$ to pick it up because $\textit{mkeps}$ is defined to always choose the
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1378
 left one when it is nullable. In the case of this example, $abc$ is
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1379
 preferred over $a$ or $ab$. This $\Left(\Left(\ldots))$ location is
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1380
 generated by two applications of the splitting clause
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1381
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1382
\begin{center}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1383
     $(r_1 \cdot r_2)\backslash c  \;\;(when \; r_1 \; nullable) \, = (r_1\backslash c) \cdot r_2 \,+\, r_2\backslash c.$
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1384
\end{center}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1385
       
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1386
\noindent
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1387
By this clause, we put $r_1 \backslash c \cdot r_2 $ at the
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1388
$\textit{front}$ and $r_2 \backslash c$ at the $\textit{back}$. This
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1389
allows $\textit{mkeps}$ to always pick up among two matches the one with a longer
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1390
initial sub-match. Removing the outside $\Left(\Left(...))$, the inside
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1391
sub-value 
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1392
 
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1393
\begin{center}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1394
 $\Seq(\Right(\Seq(\Empty, \Seq(\Empty, \Empty))), \Stars [])$
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1395
\end{center}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1396
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1397
\noindent
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1398
tells us how the empty string $[]$ is matched with $(\ZERO+\ZERO+\ZERO + \ZERO + \ONE \cdot
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1399
\ONE \cdot \ONE) \cdot r^*$. We match $[]$ by a sequence of two nullable regular
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1400
expressions. The first one is an alternative, we take the rightmost
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1401
alternative---whose language contains the empty string. The second
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1402
nullable regular expression is a Kleene star. $\Stars$ tells us how it
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1403
generates the nullable regular expression: by 0 iterations to form
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1404
$\ONE$. Now $\textit{inj}$ injects characters back and incrementally
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1405
builds a lexical value based on $v_3$. Using the value $v_3$, the character
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1406
c, and the regular expression $r_2$, we can recover how $r_2$ matched
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1407
the string $[c]$ : $\textit{inj} \; r_2 \; c \; v_3$ gives us
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1408
 \begin{center}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1409
 $v_2 = \Left(\Seq(\Right(\Seq(\Empty, \Seq(\Empty, c))), \Stars [])),$
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1410
 \end{center}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1411
which tells us how $r_2$ matched $[c]$. After this we inject back the character $b$, and get
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1412
\begin{center}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1413
$v_1 = \Seq(\Right(\Seq(\Empty, \Seq(b, c))), \Stars [])$
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1414
\end{center}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1415
 for how 
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1416
 \begin{center}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1417
 $r_1= (\ONE+\ZERO+\ONE \cdot b + \ZERO + \ONE \cdot b \cdot c) \cdot r*$
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1418
 \end{center}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1419
  matched  the string $bc$ before it split into two substrings. 
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1420
  Finally, after injecting character $a$ back to $v_1$, 
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1421
  we get  the lexical value tree 
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1422
  \begin{center}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1423
  $v_0= \Stars [\Right(\Seq(a, \Seq(b, c)))]$
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1424
  \end{center}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1425
   for how $r$ matched $abc$. This completes the algorithm.
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1426
   
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1427
%We omit the details of injection function, which is provided by Sulzmann and Lu's paper \cite{Sulzmann2014}. 
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1428
Readers might have noticed that the lexical value information is actually
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1429
already available when doing derivatives. For example, immediately after
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1430
the operation $\backslash a$ we know that if we want to match a string
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1431
that starts with $a$, we can either take the initial match to be 
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1432
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1433
 \begin{center}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1434
\begin{enumerate}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1435
    \item[1)] just $a$ or
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1436
    \item[2)] string $ab$ or 
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1437
    \item[3)] string $abc$.
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1438
\end{enumerate}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1439
\end{center}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1440
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1441
\noindent
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1442
In order to differentiate between these choices, we just need to
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1443
remember their positions---$a$ is on the left, $ab$ is in the middle ,
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1444
and $abc$ is on the right. Which of these alternatives is chosen
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1445
later does not affect their relative position because the algorithm does
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1446
not change this order. If this parsing information can be determined and
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1447
does not change because of later derivatives, there is no point in
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1448
traversing this information twice. This leads to an optimisation---if we
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1449
store the information for lexical values inside the regular expression,
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1450
update it when we do derivative on them, and collect the information
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1451
when finished with derivatives and call $\textit{mkeps}$ for deciding which
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1452
branch is POSIX, we can generate the lexical value in one pass, instead of
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1453
doing the rest $n$ injections. This leads to Sulzmann and Lu's novel
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1454
idea of using bitcodes in derivatives.
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1455
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1456
In the next section, we shall focus on the bitcoded algorithm and the
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1457
process of simplification of regular expressions. This is needed in
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1458
order to obtain \emph{fast} versions of the Brzozowski's, and Sulzmann
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1459
and Lu's algorithms.  This is where the PhD-project aims to advance the
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1460
state-of-the-art.
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1461
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1462
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1463
\section{Simplification of Regular Expressions}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1464
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1465
Using bitcodes to guide  parsing is not a novel idea. It was applied to
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1466
context free grammars and then adapted by Henglein and Nielson for
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1467
efficient regular expression  lexing using DFAs~\cite{nielson11bcre}.
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1468
Sulzmann and Lu took this idea of bitcodes a step further by integrating
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1469
bitcodes into derivatives. The reason why we want to use bitcodes in
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1470
this project is that we want to introduce more aggressive simplification
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1471
rules in order to keep the size of derivatives small throughout. This is
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1472
because the main drawback of building successive derivatives according
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1473
to Brzozowski's definition is that they can grow very quickly in size.
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1474
This is mainly due to the fact that the derivative operation generates
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1475
often ``useless'' $\ZERO$s and $\ONE$s in derivatives.  As a result, if
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1476
implemented naively both algorithms by Brzozowski and by Sulzmann and Lu
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1477
are excruciatingly slow. For example when starting with the regular
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1478
expression $(a + aa)^*$ and building 12 successive derivatives
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1479
w.r.t.~the character $a$, one obtains a derivative regular expression
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1480
with more than 8000 nodes (when viewed as a tree). Operations like
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1481
$\textit{der}$ and $\nullable$ need to traverse such trees and
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1482
consequently the bigger the size of the derivative the slower the
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1483
algorithm. 
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1484
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1485
Fortunately, one can simplify regular expressions after each derivative
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1486
step. Various simplifications of regular expressions are possible, such
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1487
as the simplification of $\ZERO + r$, $r + \ZERO$, $\ONE\cdot r$, $r
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1488
\cdot \ONE$, and $r + r$ to just $r$. These simplifications do not
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1489
affect the answer for whether a regular expression matches a string or
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1490
not, but fortunately also do not affect the POSIX strategy of how
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1491
regular expressions match strings---although the latter is much harder
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1492
to establish. Some initial results in this regard have been
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1493
obtained in \cite{AusafDyckhoffUrban2016}. 
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1494
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1495
Unfortunately, the simplification rules outlined above  are not
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1496
sufficient to prevent a size explosion in all cases. We
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1497
believe a tighter bound can be achieved that prevents an explosion in
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1498
\emph{all} cases. Such a tighter bound is suggested by work of Antimirov who
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1499
proved that (partial) derivatives can be bound by the number of
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1500
characters contained in the initial regular expression
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1501
\cite{Antimirov95}. He defined the \emph{partial derivatives} of regular
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1502
expressions as follows:
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1503
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1504
\begin{center}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1505
\begin{tabular}{lcl}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1506
 $\textit{pder} \; c \; \ZERO$ & $\dn$ & $\emptyset$\\
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1507
 $\textit{pder} \; c \; \ONE$ & $\dn$ & $\emptyset$ \\
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1508
 $\textit{pder} \; c \; d$ & $\dn$ & $\textit{if} \; c \,=\, d \; \{  \ONE   \}  \; \textit{else} \; \emptyset$ \\ 
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1509
  $\textit{pder} \; c \; r_1+r_2$ & $\dn$ & $pder \; c \; r_1 \cup pder \; c \;  r_2$ \\
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1510
   $\textit{pder} \; c \; r_1 \cdot r_2$ & $\dn$ & $\textit{if} \; nullable \; r_1 $\\
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1511
     & & $\textit{then} \; \{  r \cdot r_2 \mid r \in pder \; c \; r_1   \}  \cup pder \; c \; r_2 \;$\\
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1512
     & & $\textit{else} \; \{  r \cdot r_2 \mid r \in pder \; c \; r_1   \} $ \\ 
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1513
     $\textit{pder} \; c \; r^*$ & $\dn$ & $ \{  r' \cdot r^* \mid r' \in pder \; c \; r   \}  $ \\  
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1514
 \end{tabular}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1515
 \end{center}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1516
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1517
\noindent
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1518
A partial derivative of a regular expression $r$ is essentially a set of
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1519
regular expressions that are either $r$'s children expressions or a
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1520
concatenation of them. Antimirov has proved a tight bound of the sum of
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1521
the size of \emph{all} partial derivatives no matter what the string
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1522
looks like. Roughly speaking the size sum will be at most cubic in the
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1523
size of the regular expression.
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1524
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1525
If we want the size of derivatives in Sulzmann and Lu's algorithm to
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1526
stay below this bound, we would need more aggressive simplifications.
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1527
Essentially we need to delete useless $\ZERO$s and $\ONE$s, as well as
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1528
deleting duplicates whenever possible. For example, the parentheses in
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1529
$(a+b) \cdot c + bc$ can be opened up to get $a\cdot c +  b \cdot c + b
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1530
\cdot c$, and then simplified to just $a \cdot c + b \cdot c$. Another
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1531
example is simplifying $(a^*+a) + (a^*+ \ONE) + (a +\ONE)$ to just
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1532
$a^*+a+\ONE$. Adding these more aggressive simplification rules helps us
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1533
to achieve the same size bound as that of the partial derivatives. 
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1534
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1535
In order to implement the idea of ``spilling out alternatives'' and to
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1536
make them compatible with the $\text{inj}$-mechanism, we use
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1537
\emph{bitcodes}. Bits and bitcodes (lists of bits) are just:
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1538
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1539
%This allows us to prove a tight
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1540
%bound on the size of regular expression during the running time of the
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1541
%algorithm if we can establish the connection between our simplification
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1542
%rules and partial derivatives.
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1543
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1544
 %We believe, and have generated test
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1545
%data, that a similar bound can be obtained for the derivatives in
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1546
%Sulzmann and Lu's algorithm. Let us give some details about this next.
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1547
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1548
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1549
\begin{center}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1550
		$b ::=   S \mid  Z \qquad
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1551
bs ::= [] \mid b:bs    
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1552
$
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1553
\end{center}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1554
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1555
\noindent
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1556
The $S$ and $Z$ are arbitrary names for the bits in order to avoid 
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1557
confusion with the regular expressions $\ZERO$ and $\ONE$. Bitcodes (or
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1558
bit-lists) can be used to encode values (or incomplete values) in a
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1559
compact form. This can be straightforwardly seen in the following
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1560
coding function from values to bitcodes: 
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1561
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1562
\begin{center}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1563
\begin{tabular}{lcl}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1564
  $\textit{code}(\Empty)$ & $\dn$ & $[]$\\
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1565
  $\textit{code}(\Char\,c)$ & $\dn$ & $[]$\\
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1566
  $\textit{code}(\Left\,v)$ & $\dn$ & $\Z :: code(v)$\\
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1567
  $\textit{code}(\Right\,v)$ & $\dn$ & $\S :: code(v)$\\
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1568
  $\textit{code}(\Seq\,v_1\,v_2)$ & $\dn$ & $code(v_1) \,@\, code(v_2)$\\
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1569
  $\textit{code}(\Stars\,[])$ & $\dn$ & $[\Z]$\\
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1570
  $\textit{code}(\Stars\,(v\!::\!vs))$ & $\dn$ & $\S :: code(v) \;@\;
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1571
                                                 code(\Stars\,vs)$
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1572
\end{tabular}    
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1573
\end{center} 
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1574
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1575
\noindent
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1576
Here $\textit{code}$ encodes a value into a bitcodes by converting
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1577
$\Left$ into $\Z$, $\Right$ into $\S$, the start point of a non-empty
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1578
star iteration into $\S$, and the border where a local star terminates
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1579
into $\Z$. This coding is lossy, as it throws away the information about
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1580
characters, and also does not encode the ``boundary'' between two
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1581
sequence values. Moreover, with only the bitcode we cannot even tell
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1582
whether the $\S$s and $\Z$s are for $\Left/\Right$ or $\Stars$. The
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1583
reason for choosing this compact way of storing information is that the
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1584
relatively small size of bits can be easily manipulated and ``moved
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1585
around'' in a regular expression. In order to recover values, we will 
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1586
need the corresponding regular expression as an extra information. This
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1587
means the decoding function is defined as:
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1588
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1589
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1590
%\begin{definition}[Bitdecoding of Values]\mbox{}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1591
\begin{center}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1592
\begin{tabular}{@{}l@{\hspace{1mm}}c@{\hspace{1mm}}l@{}}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1593
  $\textit{decode}'\,bs\,(\ONE)$ & $\dn$ & $(\Empty, bs)$\\
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1594
  $\textit{decode}'\,bs\,(c)$ & $\dn$ & $(\Char\,c, bs)$\\
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1595
  $\textit{decode}'\,(\Z\!::\!bs)\;(r_1 + r_2)$ & $\dn$ &
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1596
     $\textit{let}\,(v, bs_1) = \textit{decode}'\,bs\,r_1\;\textit{in}\;
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1597
       (\Left\,v, bs_1)$\\
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1598
  $\textit{decode}'\,(\S\!::\!bs)\;(r_1 + r_2)$ & $\dn$ &
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1599
     $\textit{let}\,(v, bs_1) = \textit{decode}'\,bs\,r_2\;\textit{in}\;
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1600
       (\Right\,v, bs_1)$\\                           
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1601
  $\textit{decode}'\,bs\;(r_1\cdot r_2)$ & $\dn$ &
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1602
        $\textit{let}\,(v_1, bs_1) = \textit{decode}'\,bs\,r_1\;\textit{in}$\\
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1603
  & &   $\textit{let}\,(v_2, bs_2) = \textit{decode}'\,bs_1\,r_2$\\
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1604
  & &   \hspace{35mm}$\textit{in}\;(\Seq\,v_1\,v_2, bs_2)$\\
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1605
  $\textit{decode}'\,(\Z\!::\!bs)\,(r^*)$ & $\dn$ & $(\Stars\,[], bs)$\\
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1606
  $\textit{decode}'\,(\S\!::\!bs)\,(r^*)$ & $\dn$ & 
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1607
         $\textit{let}\,(v, bs_1) = \textit{decode}'\,bs\,r\;\textit{in}$\\
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1608
  & &   $\textit{let}\,(\Stars\,vs, bs_2) = \textit{decode}'\,bs_1\,r^*$\\
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1609
  & &   \hspace{35mm}$\textit{in}\;(\Stars\,v\!::\!vs, bs_2)$\bigskip\\
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1610
  
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1611
  $\textit{decode}\,bs\,r$ & $\dn$ &
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1612
     $\textit{let}\,(v, bs') = \textit{decode}'\,bs\,r\;\textit{in}$\\
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1613
  & & $\textit{if}\;bs' = []\;\textit{then}\;\textit{Some}\,v\;
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1614
       \textit{else}\;\textit{None}$                       
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1615
\end{tabular}    
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1616
\end{center}    
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1617
%\end{definition}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1618
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1619
Sulzmann and Lu's integrated the bitcodes into regular expressions to
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1620
create annotated regular expressions \cite{Sulzmann2014}.
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1621
\emph{Annotated regular expressions} are defined by the following
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1622
grammar:%\comment{ALTS should have  an $as$ in  the definitions, not  just $a_1$ and $a_2$}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1623
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1624
\begin{center}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1625
\begin{tabular}{lcl}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1626
  $\textit{a}$ & $::=$  & $\textit{ZERO}$\\
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1627
                  & $\mid$ & $\textit{ONE}\;\;bs$\\
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1628
                  & $\mid$ & $\textit{CHAR}\;\;bs\,c$\\
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1629
                  & $\mid$ & $\textit{ALTS}\;\;bs\,as$\\
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1630
                  & $\mid$ & $\textit{SEQ}\;\;bs\,a_1\,a_2$\\
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1631
                  & $\mid$ & $\textit{STAR}\;\;bs\,a$
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1632
\end{tabular}    
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1633
\end{center}  
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1634
%(in \textit{ALTS})
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1635
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1636
\noindent
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1637
where $bs$ stands for bitcodes, $a$  for $\bold{a}$nnotated regular
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1638
expressions and $as$ for a list of annotated regular expressions.
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1639
The alternative constructor($\textit{ALTS}$) has been generalized to 
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1640
accept a list of annotated regular expressions rather than just 2.
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1641
We will show that these bitcodes encode information about
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1642
the (POSIX) value that should be generated by the Sulzmann and Lu
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1643
algorithm.
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1644
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1645
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1646
To do lexing using annotated regular expressions, we shall first
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1647
transform the usual (un-annotated) regular expressions into annotated
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1648
regular expressions. This operation is called \emph{internalisation} and
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1649
defined as follows:
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1650
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1651
%\begin{definition}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1652
\begin{center}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1653
\begin{tabular}{lcl}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1654
  $(\ZERO)^\uparrow$ & $\dn$ & $\textit{ZERO}$\\
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1655
  $(\ONE)^\uparrow$ & $\dn$ & $\textit{ONE}\,[]$\\
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1656
  $(c)^\uparrow$ & $\dn$ & $\textit{CHAR}\,[]\,c$\\
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1657
  $(r_1 + r_2)^\uparrow$ & $\dn$ &
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1658
  $\textit{ALTS}\;[]\,List((\textit{fuse}\,[\Z]\,r_1^\uparrow),\,
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1659
  (\textit{fuse}\,[\S]\,r_2^\uparrow))$\\
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1660
  $(r_1\cdot r_2)^\uparrow$ & $\dn$ &
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1661
         $\textit{SEQ}\;[]\,r_1^\uparrow\,r_2^\uparrow$\\
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1662
  $(r^*)^\uparrow$ & $\dn$ &
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1663
         $\textit{STAR}\;[]\,r^\uparrow$\\
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1664
\end{tabular}    
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1665
\end{center}    
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1666
%\end{definition}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1667
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1668
\noindent
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1669
We use up arrows here to indicate that the basic un-annotated regular
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1670
expressions are ``lifted up'' into something slightly more complex. In the
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1671
fourth clause, $\textit{fuse}$ is an auxiliary function that helps to
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1672
attach bits to the front of an annotated regular expression. Its
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1673
definition is as follows:
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1674
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1675
\begin{center}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1676
\begin{tabular}{lcl}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1677
  $\textit{fuse}\;bs\,(\textit{ZERO})$ & $\dn$ & $\textit{ZERO}$\\
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1678
  $\textit{fuse}\;bs\,(\textit{ONE}\,bs')$ & $\dn$ &
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1679
     $\textit{ONE}\,(bs\,@\,bs')$\\
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1680
  $\textit{fuse}\;bs\,(\textit{CHAR}\,bs'\,c)$ & $\dn$ &
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1681
     $\textit{CHAR}\,(bs\,@\,bs')\,c$\\
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1682
  $\textit{fuse}\;bs\,(\textit{ALTS}\,bs'\,as)$ & $\dn$ &
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1683
     $\textit{ALTS}\,(bs\,@\,bs')\,as$\\
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1684
  $\textit{fuse}\;bs\,(\textit{SEQ}\,bs'\,a_1\,a_2)$ & $\dn$ &
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1685
     $\textit{SEQ}\,(bs\,@\,bs')\,a_1\,a_2$\\
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1686
  $\textit{fuse}\;bs\,(\textit{STAR}\,bs'\,a)$ & $\dn$ &
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1687
     $\textit{STAR}\,(bs\,@\,bs')\,a$
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1688
\end{tabular}    
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1689
\end{center}  
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1690
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1691
\noindent
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1692
After internalising the regular expression, we perform successive
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1693
derivative operations on the annotated regular expressions. This
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1694
derivative operation is the same as what we had previously for the
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1695
basic regular expressions, except that we beed to take care of
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1696
the bitcodes:
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1697
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1698
 %\begin{definition}{bder}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1699
\begin{center}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1700
  \begin{tabular}{@{}lcl@{}}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1701
  $(\textit{ZERO})\,\backslash c$ & $\dn$ & $\textit{ZERO}$\\  
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1702
  $(\textit{ONE}\;bs)\,\backslash c$ & $\dn$ & $\textit{ZERO}$\\  
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1703
  $(\textit{CHAR}\;bs\,d)\,\backslash c$ & $\dn$ &
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1704
        $\textit{if}\;c=d\; \;\textit{then}\;
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1705
         \textit{ONE}\;bs\;\textit{else}\;\textit{ZERO}$\\  
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1706
  $(\textit{ALTS}\;bs\,as)\,\backslash c$ & $\dn$ &
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1707
  $\textit{ALTS}\;bs\,(as.map(\backslash c))$\\
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1708
  $(\textit{SEQ}\;bs\,a_1\,a_2)\,\backslash c$ & $\dn$ &
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1709
     $\textit{if}\;\textit{bnullable}\,a_1$\\
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1710
					       & &$\textit{then}\;\textit{ALTS}\,bs\,List((\textit{SEQ}\,[]\,(a_1\,\backslash c)\,a_2),$\\
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1711
					       & &$\phantom{\textit{then}\;\textit{ALTS}\,bs\,}(\textit{fuse}\,(\textit{bmkeps}\,a_1)\,(a_2\,\backslash c)))$\\
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1712
  & &$\textit{else}\;\textit{SEQ}\,bs\,(a_1\,\backslash c)\,a_2$\\
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1713
  $(\textit{STAR}\,bs\,a)\,\backslash c$ & $\dn$ &
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1714
      $\textit{SEQ}\;bs\,(\textit{fuse}\, [\Z] (r\,\backslash c))\,
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1715
       (\textit{STAR}\,[]\,r)$
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1716
\end{tabular}    
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1717
\end{center}    
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1718
%\end{definition}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1719
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1720
\noindent
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1721
For instance, when we unfold $\textit{STAR} \; bs \; a$ into a sequence,
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1722
we need to attach an additional bit $Z$ to the front of $r \backslash c$
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1723
to indicate that there is one more star iteration. Also the $SEQ$ clause
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1724
is more subtle---when $a_1$ is $\textit{bnullable}$ (here
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1725
\textit{bnullable} is exactly the same as $\textit{nullable}$, except
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1726
that it is for annotated regular expressions, therefore we omit the
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1727
definition). Assume that $bmkeps$ correctly extracts the bitcode for how
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1728
$a_1$ matches the string prior to character $c$ (more on this later),
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1729
then the right branch of $ALTS$, which is $fuse \; bmkeps \;  a_1 (a_2
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1730
\backslash c)$ will collapse the regular expression $a_1$(as it has
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1731
already been fully matched) and store the parsing information at the
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1732
head of the regular expression $a_2 \backslash c$ by fusing to it. The
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1733
bitsequence $bs$, which was initially attached to the head of $SEQ$, has
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1734
now been elevated to the top-level of $ALTS$, as this information will be
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1735
needed whichever way the $SEQ$ is matched---no matter whether $c$ belongs
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1736
to $a_1$ or $ a_2$. After building these derivatives and maintaining all
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1737
the lexing information, we complete the lexing by collecting the
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1738
bitcodes using a generalised version of the $\textit{mkeps}$ function
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1739
for annotated regular expressions, called $\textit{bmkeps}$:
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1740
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1741
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1742
%\begin{definition}[\textit{bmkeps}]\mbox{}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1743
\begin{center}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1744
\begin{tabular}{lcl}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1745
  $\textit{bmkeps}\,(\textit{ONE}\;bs)$ & $\dn$ & $bs$\\
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1746
  $\textit{bmkeps}\,(\textit{ALTS}\;bs\,a::as)$ & $\dn$ &
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1747
     $\textit{if}\;\textit{bnullable}\,a$\\
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1748
  & &$\textit{then}\;bs\,@\,\textit{bmkeps}\,a$\\
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1749
  & &$\textit{else}\;bs\,@\,\textit{bmkeps}\,(\textit{ALTS}\;bs\,as)$\\
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1750
  $\textit{bmkeps}\,(\textit{SEQ}\;bs\,a_1\,a_2)$ & $\dn$ &
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1751
     $bs \,@\,\textit{bmkeps}\,a_1\,@\, \textit{bmkeps}\,a_2$\\
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1752
  $\textit{bmkeps}\,(\textit{STAR}\;bs\,a)$ & $\dn$ &
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1753
     $bs \,@\, [\S]$
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1754
\end{tabular}    
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1755
\end{center}    
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1756
%\end{definition}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1757
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1758
\noindent
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1759
This function completes the value information by travelling along the
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1760
path of the regular expression that corresponds to a POSIX value and
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1761
collecting all the bitcodes, and using $S$ to indicate the end of star
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1762
iterations. If we take the bitcodes produced by $\textit{bmkeps}$ and
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1763
decode them, we get the value we expect. The corresponding lexing
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1764
algorithm looks as follows:
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1765
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1766
\begin{center}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1767
\begin{tabular}{lcl}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1768
  $\textit{blexer}\;r\,s$ & $\dn$ &
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1769
      $\textit{let}\;a = (r^\uparrow)\backslash s\;\textit{in}$\\                
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1770
  & & $\;\;\textit{if}\; \textit{bnullable}(a)$\\
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1771
  & & $\;\;\textit{then}\;\textit{decode}\,(\textit{bmkeps}\,a)\,r$\\
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1772
  & & $\;\;\textit{else}\;\textit{None}$
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1773
\end{tabular}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1774
\end{center}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1775
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1776
\noindent
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1777
In this definition $\_\backslash s$ is the  generalisation  of the derivative
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1778
operation from characters to strings (just like the derivatives for un-annotated
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1779
regular expressions).
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1780
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1781
The main point of the bitcodes and annotated regular expressions is that
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1782
we can apply rather aggressive (in terms of size) simplification rules
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1783
in order to keep derivatives small. We have developed such
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1784
``aggressive'' simplification rules and generated test data that show
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1785
that the expected bound can be achieved. Obviously we could only
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1786
partially cover  the search space as there are infinitely many regular
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1787
expressions and strings. 
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1788
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1789
One modification we introduced is to allow a list of annotated regular
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1790
expressions in the \textit{ALTS} constructor. This allows us to not just
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1791
delete unnecessary $\ZERO$s and $\ONE$s from regular expressions, but
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1792
also unnecessary ``copies'' of regular expressions (very similar to
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1793
simplifying $r + r$ to just $r$, but in a more general setting). Another
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1794
modification is that we use simplification rules inspired by Antimirov's
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1795
work on partial derivatives. They maintain the idea that only the first
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1796
``copy'' of a regular expression in an alternative contributes to the
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1797
calculation of a POSIX value. All subsequent copies can be pruned away from
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1798
the regular expression. A recursive definition of our  simplification function 
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1799
that looks somewhat similar to our Scala code is given below:
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1800
%\comment{Use $\ZERO$, $\ONE$ and so on. 
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1801
%Is it $ALTS$ or $ALTS$?}\\
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1802
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1803
\begin{center}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1804
  \begin{tabular}{@{}lcl@{}}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1805
   
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1806
  $\textit{simp} \; (\textit{SEQ}\;bs\,a_1\,a_2)$ & $\dn$ & $ (\textit{simp} \; a_1, \textit{simp}  \; a_2) \; \textit{match} $ \\
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1807
   &&$\quad\textit{case} \; (\ZERO, \_) \Rightarrow  \ZERO$ \\
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1808
   &&$\quad\textit{case} \; (\_, \ZERO) \Rightarrow  \ZERO$ \\
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1809
   &&$\quad\textit{case} \;  (\ONE, a_2') \Rightarrow  \textit{fuse} \; bs \;  a_2'$ \\
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1810
   &&$\quad\textit{case} \; (a_1', \ONE) \Rightarrow  \textit{fuse} \; bs \;  a_1'$ \\
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1811
   &&$\quad\textit{case} \; (a_1', a_2') \Rightarrow  \textit{SEQ} \; bs \; a_1' \;  a_2'$ \\
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1812
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1813
  $\textit{simp} \; (\textit{ALTS}\;bs\,as)$ & $\dn$ & $\textit{distinct}( \textit{flatten} ( \textit{map simp as})) \; \textit{match} $ \\
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1814
  &&$\quad\textit{case} \; [] \Rightarrow  \ZERO$ \\
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1815
   &&$\quad\textit{case} \; a :: [] \Rightarrow  \textit{fuse bs a}$ \\
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1816
   &&$\quad\textit{case} \;  as' \Rightarrow  \textit{ALTS}\;bs\;as'$\\ 
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1817
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1818
   $\textit{simp} \; a$ & $\dn$ & $\textit{a} \qquad \textit{otherwise}$   
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1819
\end{tabular}    
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1820
\end{center}    
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1821
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1822
\noindent
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1823
The simplification does a pattern matching on the regular expression.
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1824
When it detected that the regular expression is an alternative or
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1825
sequence, it will try to simplify its children regular expressions
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1826
recursively and then see if one of the children turn into $\ZERO$ or
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1827
$\ONE$, which might trigger further simplification at the current level.
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1828
The most involved part is the $\textit{ALTS}$ clause, where we use two
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1829
auxiliary functions $\textit{flatten}$ and $\textit{distinct}$ to open up nested
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1830
$\textit{ALTS}$ and reduce as many duplicates as possible. Function
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1831
$\textit{distinct}$  keeps the first occurring copy only and remove all later ones
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1832
when detected duplicates. Function $\textit{flatten}$ opens up nested \textit{ALTS}.
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1833
Its recursive definition is given below:
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1834
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1835
 \begin{center}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1836
  \begin{tabular}{@{}lcl@{}}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1837
  $\textit{flatten} \; (\textit{ALTS}\;bs\,as) :: as'$ & $\dn$ & $(\textit{map} \;
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1838
     (\textit{fuse}\;bs)\; \textit{as}) \; @ \; \textit{flatten} \; as' $ \\
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1839
  $\textit{flatten} \; \textit{ZERO} :: as'$ & $\dn$ & $ \textit{flatten} \;  as' $ \\
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1840
    $\textit{flatten} \; a :: as'$ & $\dn$ & $a :: \textit{flatten} \; as'$ \quad(otherwise) 
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1841
\end{tabular}    
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1842
\end{center}  
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1843
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1844
\noindent
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1845
Here $\textit{flatten}$ behaves like the traditional functional programming flatten
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1846
function, except that it also removes $\ZERO$s. Or in terms of regular expressions, it
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1847
removes parentheses, for example changing $a+(b+c)$ into $a+b+c$.
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1848
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1849
Suppose we apply simplification after each derivative step, and view
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1850
these two operations as an atomic one: $a \backslash_{simp}\,c \dn
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1851
\textit{simp}(a \backslash c)$. Then we can use the previous natural
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1852
extension from derivative w.r.t.~character to derivative
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1853
w.r.t.~string:%\comment{simp in  the [] case?}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1854
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1855
\begin{center}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1856
\begin{tabular}{lcl}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1857
$r \backslash_{simp} (c\!::\!s) $ & $\dn$ & $(r \backslash_{simp}\, c) \backslash_{simp}\, s$ \\
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1858
$r \backslash_{simp} [\,] $ & $\dn$ & $r$
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1859
\end{tabular}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1860
\end{center}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1861
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1862
\noindent
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1863
we obtain an optimised version of the algorithm:
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1864
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1865
 \begin{center}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1866
\begin{tabular}{lcl}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1867
  $\textit{blexer\_simp}\;r\,s$ & $\dn$ &
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1868
      $\textit{let}\;a = (r^\uparrow)\backslash_{simp}\, s\;\textit{in}$\\                
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1869
  & & $\;\;\textit{if}\; \textit{bnullable}(a)$\\
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1870
  & & $\;\;\textit{then}\;\textit{decode}\,(\textit{bmkeps}\,a)\,r$\\
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1871
  & & $\;\;\textit{else}\;\textit{None}$
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1872
\end{tabular}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1873
\end{center}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1874
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1875
\noindent
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1876
This algorithm keeps the regular expression size small, for example,
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1877
with this simplification our previous $(a + aa)^*$ example's 8000 nodes
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1878
will be reduced to just 6 and stays constant, no matter how long the
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1879
input string is.
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1880
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1881
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1882
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1883
\section{Current Work}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1884
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1885
We are currently engaged in two tasks related to this algorithm. The
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1886
first task is proving that our simplification rules actually do not
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1887
affect the POSIX value that should be generated by the algorithm
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1888
according to the specification of a POSIX value and furthermore obtain a
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1889
much tighter bound on the sizes of derivatives. The result is that our
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1890
algorithm should be correct and faster on all inputs.  The original
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1891
blow-up, as observed in JavaScript, Python and Java, would be excluded
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1892
from happening in our algorithm. For this proof we use the theorem prover
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1893
Isabelle. Once completed, this result will advance the state-of-the-art:
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1894
Sulzmann and Lu wrote in their paper~\cite{Sulzmann2014} about the
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1895
bitcoded ``incremental parsing method'' (that is the lexing algorithm
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1896
outlined in this section):
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1897
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1898
\begin{quote}\it
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1899
  ``Correctness Claim: We further claim that the incremental parsing
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1900
  method in Figure~5 in combination with the simplification steps in
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1901
  Figure 6 yields POSIX parse tree [our lexical values]. We have tested this claim
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1902
  extensively by using the method in Figure~3 as a reference but yet
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1903
  have to work out all proof details.''
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1904
\end{quote}  
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1905
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1906
\noindent 
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1907
We like to settle this correctness claim. It is relatively
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1908
straightforward to establish that after one simplification step, the part of a
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1909
nullable derivative that corresponds to a POSIX value remains intact and can
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1910
still be collected, in other words, we can show that
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1911
%\comment{Double-check....I
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1912
%think this  is not the case}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1913
%\comment{If i remember correctly, you have proved this lemma.
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1914
%I feel this is indeed not true because you might place arbitrary 
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1915
%bits on the regex r, however if this is the case, did i remember wrongly that
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1916
%you proved something like simplification does not affect $\textit{bmkeps}$ results?
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1917
%Anyway, i have amended this a little bit so it does not allow arbitrary bits attached
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1918
%to a regex. Maybe it works now.}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1919
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1920
\begin{center}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1921
	$\textit{bmkeps} \; a = \textit{bmkeps} \; \textit{bsimp} \; a\;($\textit{provided}$ \; a\; is \; \textit{bnullable} )$
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1922
\end{center} 
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1923
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1924
\noindent
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1925
as this basically comes down to proving actions like removing the
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1926
additional $r$ in $r+r$  does not delete important POSIX information in
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1927
a regular expression. The hard part of this proof is to establish that
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1928
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1929
\begin{center}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1930
	$ \textit{blexer}\_{simp}(r, \; s) =  \textit{blexer}(r, \; s)$
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1931
\end{center}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1932
%comment{This is not true either...look at the definion blexer/blexer-simp}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1933
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1934
\noindent That is, if we do derivative on regular expression $r$ and then
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1935
simplify it, and repeat this process until we exhaust the string, we get a
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1936
regular expression $r''$($\textit{LHS}$)  that provides the POSIX matching
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1937
information, which is exactly the same as the result $r'$($\textit{RHS}$ of the
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1938
normal derivative algorithm that only does derivative repeatedly and has no
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1939
simplification at all.  This might seem at first glance very unintuitive, as
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1940
the $r'$ could be exponentially larger than $r''$, but can be explained in the
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1941
following way: we are pruning away the possible matches that are not POSIX.
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1942
Since there could be exponentially many 
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1943
non-POSIX matchings and only 1 POSIX matching, it
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1944
is understandable that our $r''$ can be a lot smaller.  we can still provide
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1945
the same POSIX value if there is one.  This is not as straightforward as the
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1946
previous proposition, as the two regular expressions $r'$ and $r''$ might have
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1947
become very different.  The crucial point is to find the
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1948
$\textit{POSIX}$  information of a regular expression and how it is modified,
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1949
augmented and propagated 
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1950
during simplification in parallel with the regular expression that
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1951
has not been simplified in the subsequent derivative operations.  To aid this,
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1952
we use the helper function retrieve described by Sulzmann and Lu:
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1953
\begin{center}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1954
\begin{tabular}{@{}l@{\hspace{2mm}}c@{\hspace{2mm}}l@{}}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1955
  $\textit{retrieve}\,(\textit{ONE}\,bs)\,\Empty$ & $\dn$ & $bs$\\
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1956
  $\textit{retrieve}\,(\textit{CHAR}\,bs\,c)\,(\Char\,d)$ & $\dn$ & $bs$\\
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1957
  $\textit{retrieve}\,(\textit{ALTS}\,bs\,a::as)\,(\Left\,v)$ & $\dn$ &
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1958
     $bs \,@\, \textit{retrieve}\,a\,v$\\
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1959
  $\textit{retrieve}\,(\textit{ALTS}\,bs\,a::as)\,(\Right\,v)$ & $\dn$ &
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1960
  $bs \,@\, \textit{retrieve}\,(\textit{ALTS}\,bs\,as)\,v$\\
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1961
  $\textit{retrieve}\,(\textit{SEQ}\,bs\,a_1\,a_2)\,(\Seq\,v_1\,v_2)$ & $\dn$ &
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1962
     $bs \,@\,\textit{retrieve}\,a_1\,v_1\,@\, \textit{retrieve}\,a_2\,v_2$\\
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1963
  $\textit{retrieve}\,(\textit{STAR}\,bs\,a)\,(\Stars\,[])$ & $\dn$ &
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1964
     $bs \,@\, [\S]$\\
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1965
  $\textit{retrieve}\,(\textit{STAR}\,bs\,a)\,(\Stars\,(v\!::\!vs))$ & $\dn$ &\\
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1966
  \multicolumn{3}{l}{
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1967
     \hspace{3cm}$bs \,@\, [\Z] \,@\, \textit{retrieve}\,a\,v\,@\,
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1968
                    \textit{retrieve}\,(\textit{STAR}\,[]\,a)\,(\Stars\,vs)$}\\
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1969
\end{tabular}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1970
\end{center}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1971
%\comment{Did not read further}\\
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1972
This function assembles the bitcode 
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1973
%that corresponds to a lexical value for how
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1974
%the current derivative matches the suffix of the string(the characters that
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1975
%have not yet appeared, but will appear as the successive derivatives go on.
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1976
%How do we get this "future" information? By the value $v$, which is
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1977
%computed by a pass of the algorithm that uses
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1978
%$inj$ as described in the previous section).  
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1979
using information from both the derivative regular expression and the
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1980
value. Sulzmann and Lu poroposed this function, but did not prove
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1981
anything about it. Ausaf and Urban used it to connect the bitcoded
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1982
algorithm to the older algorithm by the following equation:
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1983
 
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1984
 \begin{center} $inj \;a\; c \; v = \textit{decode} \; (\textit{retrieve}\;
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1985
	 (r^\uparrow)\backslash_{simp} \,c)\,v)$ 
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1986
 \end{center} 
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1987
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1988
\noindent
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1989
whereby $r^\uparrow$ stands for the internalised version of $r$. Ausaf
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1990
and Urban also used this fact to prove  the correctness of bitcoded
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1991
algorithm without simplification.  Our purpose of using this, however,
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1992
is to establish 
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1993
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1994
\begin{center}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1995
$ \textit{retrieve} \;
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1996
a \; v \;=\; \textit{retrieve}  \; (\textit{simp}\,a) \; v'.$
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1997
\end{center}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1998
The idea is that using $v'$, a simplified version of $v$ that had gone
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  1999
through the same simplification step as $\textit{simp}(a)$, we are able
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  2000
to extract the bitcode that gives the same parsing information as the
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  2001
unsimplified one. However, we noticed that constructing such a  $v'$
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  2002
from $v$ is not so straightforward. The point of this is that  we might
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  2003
be able to finally bridge the gap by proving
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  2004
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  2005
\begin{center}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  2006
$\textit{retrieve} \; (r^\uparrow   \backslash  s) \; v = \;\textit{retrieve} \;
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  2007
(\textit{simp}(r^\uparrow)  \backslash  s) \; v'$
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  2008
\end{center}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  2009
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  2010
\noindent
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  2011
and subsequently
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  2012
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  2013
\begin{center}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  2014
$\textit{retrieve} \; (r^\uparrow \backslash  s) \; v\; = \; \textit{retrieve} \;
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  2015
(r^\uparrow  \backslash_{simp}  \, s) \; v'$.
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  2016
\end{center}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  2017
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  2018
\noindent
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  2019
The $\textit{LHS}$ of the above equation is the bitcode we want. This
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  2020
would prove that our simplified version of regular expression still
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  2021
contains all the bitcodes needed. The task here is to find a way to
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  2022
compute the correct $v'$.
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  2023
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  2024
The second task is to speed up the more aggressive simplification.  Currently
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  2025
it is slower than the original naive simplification by Ausaf and Urban (the
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  2026
naive version as implemented by Ausaf   and Urban of course can ``explode'' in
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  2027
some cases).  It is therefore not surprising that the speed is also much slower
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  2028
than regular expression engines in popular programming languages such as Java
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  2029
and Python on most inputs that are linear. For example, just by rewriting the
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  2030
example regular expression in the beginning of this report  $(a^*)^*\,b$ into
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  2031
$a^*\,b$ would eliminate the ambiguity in the matching and make the time
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  2032
for matching linear with respect to the input string size. This allows the 
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  2033
DFA approach to become blindingly fast, and dwarf the speed of our current
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  2034
implementation. For example, here is a comparison of Java regex engine 
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  2035
and our implementation on this example.
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  2036
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  2037
\begin{center}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  2038
\begin{tabular}{@{}c@{\hspace{0mm}}c@{\hspace{0mm}}c@{}}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  2039
\begin{tikzpicture}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  2040
\begin{axis}[
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  2041
    xlabel={$n*1000$},
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  2042
    x label style={at={(1.05,-0.05)}},
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  2043
    ylabel={time in secs},
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  2044
    enlargelimits=false,
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  2045
    xtick={0,5,...,30},
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  2046
    xmax=33,
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  2047
    ymax=9,
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  2048
    scaled ticks=true,
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  2049
    axis lines=left,
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  2050
    width=5cm,
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  2051
    height=4cm, 
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  2052
    legend entries={Bitcoded Algorithm},  
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  2053
    legend pos=north west,
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  2054
    legend cell align=left]
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  2055
\addplot[red,mark=*, mark options={fill=white}] table {bad-scala.data};
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  2056
\end{axis}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  2057
\end{tikzpicture}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  2058
  &
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  2059
\begin{tikzpicture}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  2060
\begin{axis}[
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  2061
    xlabel={$n*1000$},
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  2062
    x label style={at={(1.05,-0.05)}},
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  2063
    %ylabel={time in secs},
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  2064
    enlargelimits=false,
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  2065
    xtick={0,5,...,30},
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  2066
    xmax=33,
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  2067
    ymax=9,
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  2068
    scaled ticks=false,
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  2069
    axis lines=left,
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  2070
    width=5cm,
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  2071
    height=4cm, 
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  2072
    legend entries={Java},  
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  2073
    legend pos=north west,
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  2074
    legend cell align=left]
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  2075
\addplot[cyan,mark=*, mark options={fill=white}] table {good-java.data};
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  2076
\end{axis}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  2077
\end{tikzpicture}\\
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  2078
\multicolumn{3}{c}{Graphs: Runtime for matching $a^*\,b$ with strings 
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  2079
           of the form $\underbrace{aa..a}_{n}$.}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  2080
\end{tabular}    
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  2081
\end{center}  
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  2082
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  2083
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  2084
Java regex engine can match string of thousands of characters in a few milliseconds,
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  2085
whereas our current algorithm gets excruciatingly slow on input of this size.
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  2086
The running time in theory is linear, however it does not appear to be the 
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  2087
case in an actual implementation. So it needs to be explored how to
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  2088
make our algorithm faster on all inputs.  It could be the recursive calls that are
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  2089
needed to manipulate bits that are causing the slow down. A possible solution
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  2090
is to write recursive functions into tail-recusive form.
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  2091
Another possibility would be to explore
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  2092
again the connection to DFAs to speed up the algorithm on 
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  2093
subcalls that are small enough. This is very much work in progress.
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  2094
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  2095
\section{Conclusion}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  2096
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  2097
In this PhD-project we are interested in fast algorithms for regular
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  2098
expression matching. While this seems to be a ``settled'' area, in
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  2099
fact interesting research questions are popping up as soon as one steps
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  2100
outside the classic automata theory (for example in terms of what kind
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  2101
of regular expressions are supported). The reason why it is
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  2102
interesting for us to look at the derivative approach introduced by
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  2103
Brzozowski for regular expression matching, and then much further
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  2104
developed by Sulzmann and Lu, is that derivatives can elegantly deal
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  2105
with some of the regular expressions that are of interest in ``real
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  2106
life''. This includes the not-regular expression, written $\neg\,r$
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  2107
(that is all strings that are not recognised by $r$), but also bounded
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  2108
regular expressions such as $r^{\{n\}}$ and $r^{\{n..m\}}$). There is
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  2109
also hope that the derivatives can provide another angle for how to
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  2110
deal more efficiently with back-references, which are one of the
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  2111
reasons why regular expression engines in JavaScript, Python and Java
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  2112
choose to not implement the classic automata approach of transforming
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  2113
regular expressions into NFAs and then DFAs---because we simply do not
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  2114
know how such back-references can be represented by DFAs.
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  2115
We also plan to implement the bitcoded algorithm
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  2116
in some imperative language like C to see if the inefficiency of the 
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  2117
Scala implementation
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  2118
is language specific. To make this research more comprehensive we also plan
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  2119
to contrast our (faster) version of bitcoded algorithm with the
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  2120
Symbolic Regex Matcher, the RE2, the Rust Regex Engine, and the static
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  2121
analysis approach by implementing them in the same language and then compare
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  2122
their performance.
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  2123
443
c6351a96bf80 writeupforclosedforms
Chengsong
parents: 441
diff changeset
  2124
c6351a96bf80 writeupforclosedforms
Chengsong
parents: 441
diff changeset
  2125
\section{discarded}
c6351a96bf80 writeupforclosedforms
Chengsong
parents: 441
diff changeset
  2126
haha
438
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  2127
\bibliographystyle{plain}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  2128
\bibliography{root,regex_time_complexity}
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  2129
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  2130
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  2131
a73b2e553804 templateforPhd
Chengsong
parents:
diff changeset
  2132
\end{document}