|
369
|
1 |
\relax
|
|
|
2 |
\providecommand\hyper@newdestlabel[2]{}
|
|
|
3 |
\providecommand\HyperFirstAtBeginDocument{\AtBeginDocument}
|
|
|
4 |
\HyperFirstAtBeginDocument{\ifx\hyper@anchor\@undefined
|
|
|
5 |
\global\let\oldcontentsline\contentsline
|
|
|
6 |
\gdef\contentsline#1#2#3#4{\oldcontentsline{#1}{#2}{#3}}
|
|
|
7 |
\global\let\oldnewlabel\newlabel
|
|
|
8 |
\gdef\newlabel#1#2{\newlabelxx{#1}#2}
|
|
|
9 |
\gdef\newlabelxx#1#2#3#4#5#6{\oldnewlabel{#1}{{#2}{#3}}}
|
|
|
10 |
\AtEndDocument{\ifx\hyper@anchor\@undefined
|
|
|
11 |
\let\contentsline\oldcontentsline
|
|
|
12 |
\let\newlabel\oldnewlabel
|
|
|
13 |
\fi}
|
|
|
14 |
\fi}
|
|
|
15 |
\global\let\hyper@last\relax
|
|
|
16 |
\gdef\HyperFirstAtBeginDocument#1{#1}
|
|
|
17 |
\providecommand\HyField@AuxAddToFields[1]{}
|
|
|
18 |
\providecommand\HyField@AuxAddToCoFields[2]{}
|
|
|
19 |
\citation{AusafDyckhoffUrban2016}
|
|
|
20 |
\citation{OkuiSuzuki2010,OkuiSuzukiTech}
|
|
|
21 |
\citation{Sulzmann2014}
|
|
|
22 |
\@writefile{toc}{\contentsline {section}{\numberline {1}Bit-Encodings}{2}{section.1.1}}
|
|
|
23 |
\@writefile{toc}{\contentsline {section}{\numberline {2}Annotated Regular Expressions}{3}{section.1.2}}
|
|
|
24 |
\citation{Brzozowski1964}
|
|
|
25 |
\citation{Owens2008}
|
|
|
26 |
\citation{Krauss2011}
|
|
|
27 |
\citation{Coquand2012}
|
|
|
28 |
\@writefile{toc}{\contentsline {section}{\numberline {3}Introduction}{41}{section.1.3}}
|
|
|
29 |
\citation{Frisch2004}
|
|
|
30 |
\citation{POSIX,Kuklewicz,OkuiSuzuki2010,Sulzmann2014,Vansummeren2006}
|
|
|
31 |
\citation{POSIX}
|
|
|
32 |
\citation{Sulzmann2014}
|
|
|
33 |
\citation{HosoyaVouillonPierce2005}
|
|
|
34 |
\citation{Sulzmann2014}
|
|
|
35 |
\citation{Frisch2004}
|
|
|
36 |
\citation{Sulzmann2014}
|
|
|
37 |
\citation{Kuklewicz}
|
|
|
38 |
\citation{Sulzmann2014}
|
|
|
39 |
\citation{CrashCourse2014}
|
|
|
40 |
\citation{Sulzmann2014}
|
|
|
41 |
\citation{Vansummeren2006}
|
|
|
42 |
\citation{Sulzmann2014}
|
|
|
43 |
\citation{Sulzmann2014}
|
|
|
44 |
\citation{OkuiSuzuki2010}
|
|
|
45 |
\@writefile{toc}{\contentsline {section}{\numberline {4}Preliminaries}{44}{section.1.4}}
|
|
|
46 |
\citation{Krauss2011}
|
|
|
47 |
\citation{Brzozowski1964}
|
|
|
48 |
\newlabel{SemDer}{{1}{45}{Preliminaries}{equation.1.4.1}{}}
|
|
|
49 |
\citation{Sulzmann2014}
|
|
|
50 |
\citation{Sulzmann2014}
|
|
|
51 |
\citation{Frisch2004}
|
|
|
52 |
\citation{Sulzmann2014}
|
|
|
53 |
\citation{AusafDyckhoffUrban2016}
|
|
|
54 |
\newlabel{derprop}{{1}{46}{Preliminaries}{proposition.1.1}{}}
|
|
|
55 |
\newlabel{posixsec}{{5}{46}{POSIX Regular Expression Matching}{section.1.5}{}}
|
|
|
56 |
\@writefile{toc}{\contentsline {section}{\numberline {5}POSIX Regular Expression Matching}{46}{section.1.5}}
|
|
|
57 |
\citation{OkuiSuzuki2010}
|
|
|
58 |
\citation{Frisch2004}
|
|
|
59 |
\citation{Sulzmann2014}
|
|
|
60 |
\citation{Sulzmann2014}
|
|
|
61 |
\newlabel{prfintros}{{5}{47}{POSIX Regular Expression Matching}{section.1.5}{}}
|
|
|
62 |
\newlabel{inhabs}{{2}{47}{POSIX Regular Expression Matching}{proposition.1.2}{}}
|
|
|
63 |
\citation{Sulzmann2014}
|
|
|
64 |
\@writefile{lof}{\contentsline {figure}{\numberline {1}{\ignorespaces The two phases of the algorithm by Sulzmann \& Lu \cite {Sulzmann2014}, matching the string \emph {\sfcode 42 1000 \sfcode 63 1000 \sfcode 33 1000 \sfcode 58 1000 \sfcode 59 1000 \sfcode 44 1000 \it {\emph {$[$}}{\kern 0pt}a{\emph {$\mathord ,$}}{\kern 0pt}\ b{\emph {$\mathord ,$}}{\kern 0pt}\ c{\emph {$]$}}{\kern 0pt}}. The first phase (the arrows from left to right) is Brzozowski's matcher building successive derivatives. If the last regular expression is \emph {\sfcode 42 1000 \sfcode 63 1000 \sfcode 33 1000 \sfcode 58 1000 \sfcode 59 1000 \sfcode 44 1000 \it nullable}, then the functions of the second phase are called (the top-down and right-to-left arrows): first \emph {\sfcode 42 1000 \sfcode 63 1000 \sfcode 33 1000 \sfcode 58 1000 \sfcode 59 1000 \sfcode 44 1000 \it mkeps} calculates a value \emph {\sfcode 42 1000 \sfcode 63 1000 \sfcode 33 1000 \sfcode 58 1000 \sfcode 59 1000 \sfcode 44 1000 \it v\emph {\isascriptstyle ${}\sb {4}$}} witnessing how the empty string has been recognised by \emph {\sfcode 42 1000 \sfcode 63 1000 \sfcode 33 1000 \sfcode 58 1000 \sfcode 59 1000 \sfcode 44 1000 \it r\emph {\isascriptstyle ${}\sb {4}$}}. After that the function \emph {\sfcode 42 1000 \sfcode 63 1000 \sfcode 33 1000 \sfcode 58 1000 \sfcode 59 1000 \sfcode 44 1000 \it inj} ``injects back'' the characters of the string into the values. }}{48}{figure.1.1}}
|
|
|
65 |
\newlabel{Sulz}{{1}{48}{The two phases of the algorithm by Sulzmann \& Lu \cite {Sulzmann2014}, matching the string \isa {{\isacharbrackleft }{\kern 0pt}a{\isacharcomma }{\kern 0pt}\ b{\isacharcomma }{\kern 0pt}\ c{\isacharbrackright }{\kern 0pt}}. The first phase (the arrows from left to right) is \Brz 's matcher building successive derivatives. If the last regular expression is \isa {nullable}, then the functions of the second phase are called (the top-down and right-to-left arrows): first \isa {mkeps} calculates a value \isa {v\isactrlsub {\isadigit {4}}} witnessing how the empty string has been recognised by \isa {r\isactrlsub {\isadigit {4}}}. After that the function \isa {inj} ``injects back'' the characters of the string into the values}{figure.1.1}{}}
|
|
|
66 |
\newlabel{Prf_injval_flat}{{2}{49}{POSIX Regular Expression Matching}{lemma.1.2}{}}
|
|
|
67 |
\citation{Sulzmann2014}
|
|
|
68 |
\citation{Vansummeren2006}
|
|
|
69 |
\newlabel{posixdeterm}{{1}{50}{POSIX Regular Expression Matching}{theorem.1.5.1}{}}
|
|
|
70 |
\@writefile{lof}{\contentsline {figure}{\numberline {2}{\ignorespaces Our inductive definition of POSIX values.}}{51}{figure.1.2}}
|
|
|
71 |
\newlabel{POSIXrules}{{2}{51}{Our inductive definition of POSIX values}{figure.1.2}{}}
|
|
|
72 |
\newlabel{LVposix}{{3}{51}{POSIX Regular Expression Matching}{lemma.1.3}{}}
|
|
|
73 |
\newlabel{lemmkeps}{{4}{51}{POSIX Regular Expression Matching}{lemma.1.4}{}}
|
|
|
74 |
\newlabel{Posix2}{{5}{52}{POSIX Regular Expression Matching}{lemma.1.5}{}}
|
|
|
75 |
\newlabel{lexercorrect}{{2}{52}{POSIX Regular Expression Matching}{theorem.1.5.2}{}}
|
|
|
76 |
\citation{Sulzmann2014}
|
|
|
77 |
\citation{Sulzmann2014}
|
|
|
78 |
\citation{OkuiSuzuki2010,OkuiSuzukiTech}
|
|
|
79 |
\newlabel{lexercorrectcor}{{1}{53}{POSIX Regular Expression Matching}{corollary.1.1}{}}
|
|
|
80 |
\@writefile{toc}{\contentsline {section}{\numberline {6}Ordering of Values according to Okui and Suzuki}{53}{section.1.6}}
|
|
|
81 |
\citation{OkuiSuzuki2010}
|
|
|
82 |
\citation{OkuiSuzuki2010}
|
|
|
83 |
\citation{OkuiSuzuki2010}
|
|
|
84 |
\newlabel{transitivity}{{6}{55}{Ordering of Values according to Okui and Suzuki}{lemma.1.6}{}}
|
|
|
85 |
\newlabel{ordlen}{{4}{56}{Ordering of Values according to Okui and Suzuki}{proposition.1.4}{}}
|
|
|
86 |
\newlabel{ordintros}{{5}{56}{Ordering of Values according to Okui and Suzuki}{proposition.1.5}{}}
|
|
|
87 |
\newlabel{orderone}{{3}{56}{Ordering of Values according to Okui and Suzuki}{theorem.1.6.3}{}}
|
|
|
88 |
\citation{Sulzmann2014}
|
|
|
89 |
\citation{Sulzmann2014}
|
|
|
90 |
\@writefile{toc}{\contentsline {section}{\numberline {7}Bitcoded Lexing}{58}{section.1.7}}
|
|
|
91 |
\@writefile{toc}{\contentsline {section}{\numberline {8}Optimisations}{58}{section.1.8}}
|
|
|
92 |
\newlabel{Simpl}{{2}{58}{Optimisations}{equation.1.8.2}{}}
|
|
|
93 |
\newlabel{slexeraux}{{7}{63}{Optimisations}{lemma.1.7}{}}
|
|
|
94 |
\@writefile{toc}{\contentsline {section}{\numberline {9}HERE}{64}{section.1.9}}
|
|
|
95 |
\bibstyle{plain}
|
|
|
96 |
\bibdata{root}
|