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} |
|