| author | Chengsong |
| Wed, 23 Aug 2023 03:02:31 +0100 | |
| changeset 668 | 3831621d7b14 |
| parent 667 | 660cf698eb26 |
| permissions | -rwxr-xr-x |
| 532 | 1 |
% Chapter Template |
2 |
||
3 |
% Main chapter title |
|
| 538 | 4 |
\chapter{Bit-coded Algorithm of Sulzmann and Lu}
|
| 532 | 5 |
|
6 |
\label{Bitcoded1} % Change X to a consecutive number; for referencing this chapter elsewhere, use \ref{ChapterX}
|
|
7 |
%Then we illustrate how the algorithm without bitcodes falls short for such aggressive |
|
8 |
%simplifications and therefore introduce our version of the bitcoded algorithm and |
|
9 |
%its correctness proof in |
|
10 |
%Chapter 3\ref{Chapter3}.
|
|
| 564 | 11 |
In this chapter, we are going to describe the bit-coded algorithm |
|
653
bc5571c38d1f
more updates in section 4.2 and incorporating Christian comments
Chengsong
parents:
649
diff
changeset
|
12 |
introduced by Sulzmann and Lu \parencite{Sulzmann2014} and their correctness proof.
|
| 667 | 13 |
Just like in chapter \ref{Inj}, the algorithms and proofs have been included
|
14 |
for self-containedness reasons, |
|
15 |
even though they have been originally found and described by |
|
16 |
Sulzmann and Lu (\cite{Sulzmann2014}) and
|
|
17 |
Ausaf et al. (\cite{AusafDyckhoffUrban2016} and \cite{Ausaf}).
|
|
18 |
%In addition to this, the |
|
19 |
The details of the proofs in this thesis |
|
20 |
also follow more closely the actual Isabelle formalisation. |
|
21 |
For example, lemma \ref{flexStepwise} and \ref{retrieveStepwise}
|
|
22 |
are not included in the publications by Ausaf et al., despite them being |
|
23 |
some of the key lemmas leading to the correctness result. |
|
24 |
||
25 |
We will first motivate the bit-coded algorithm in section \ref{bitMotivate},
|
|
26 |
and then introduce their formal definitions in section \ref{bitDef},
|
|
27 |
followed by a description of the correctness proof of $\blexer$ in section \ref{blexerProof}.
|
|
28 |
||
|
653
bc5571c38d1f
more updates in section 4.2 and incorporating Christian comments
Chengsong
parents:
649
diff
changeset
|
29 |
%to address the growth problem of |
|
bc5571c38d1f
more updates in section 4.2 and incorporating Christian comments
Chengsong
parents:
649
diff
changeset
|
30 |
%derivatives of |
|
bc5571c38d1f
more updates in section 4.2 and incorporating Christian comments
Chengsong
parents:
649
diff
changeset
|
31 |
%regular expressions. |
| 667 | 32 |
%We have implemented their algorithm in Scala and Isabelle, |
33 |
%and found problems |
|
34 |
%in their algorithm, such as de-duplication not working properly and redundant |
|
35 |
%fixpoint construction. |
|
36 |
\section{The Motivation Behind Using Bitcodes}\label{bitMotivate}
|
|
| 624 | 37 |
Let us give again the definition of $\lexer$ from Chapter \ref{Inj}:
|
| 579 | 38 |
\begin{center}
|
39 |
\begin{tabular}{lcl}
|
|
40 |
$\lexer \; r \; [] $ & $=$ & $\textit{if} \; (\nullable \; r)\; \textit{then}\; \Some(\mkeps \; r) \; \textit{else} \; \None$\\
|
|
41 |
$\lexer \; r \;c::s$ & $=$ & $\textit{case}\; (\lexer \; (r\backslash c) \; s) \;\textit{of}\; $\\
|
|
42 |
& & $\quad \phantom{\mid}\; \None \implies \None$\\
|
|
43 |
& & $\quad \mid \Some(v) \implies \Some(\inj \; r\; c\; v)$ |
|
44 |
\end{tabular}
|
|
45 |
\end{center}
|
|
46 |
\noindent |
|
|
668
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
47 |
This algorithm works nicely as a functional program that utilizes Brzozowski derivatives: |
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
48 |
each derivative character is remembered and stacked up, and |
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
49 |
injected back in reverse order as they have been taken derivative of. |
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
50 |
The derivative operation $\backslash$ and its reverse operation |
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
51 |
$\inj$ is of similar shape and compexity, and work in lockstep with each other. |
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
52 |
However if we take a closer look into the example run |
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
53 |
of $\lexer$ we have shown in chapter \ref{Inj},
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
54 |
many inefficiencies exist: |
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
55 |
\begin{center}
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
56 |
\begin{tabular}{lcl}
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
57 |
$(a+\textcolor{magenta}{a}\textcolor{blue}{a})^* \cdot \textcolor{red}{c}$ & $\stackrel{\backslash \textcolor{magenta}{a}}{\rightarrow}$ & $((\ONE + \textcolor{magenta}{\ONE} \textcolor{blue}{a})\cdot (a+aa)^*)\cdot \textcolor{red}{c}+\ZERO$\\
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
58 |
%& $\stackrel{\rightarrow}{\backslash a}$ & $((\ONE + \ONE a)\cdot (a+aa)^*)\cdot c + \ZERO$\\
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
59 |
& $\stackrel{\backslash \textcolor{blue}{a}}{\rightarrow}$ &
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
60 |
$(((\ZERO+(\ZERO a+ \textcolor{blue}{\ONE}))\cdot (a+aa)^* + (\ONE+\ONE a)\cdot (a+aa)^* )\cdot \textcolor{red}{\mathbf{c}} + \ZERO)+\ZERO$\\
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
61 |
& $\stackrel{\backslash \textcolor{red}{c}}{\rightarrow}$ &
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
62 |
$((r_{=0}\cdot c + \textcolor{red}{\ONE})+\ZERO)+\ZERO$\\
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
63 |
& $\stackrel{\mkeps}{\rightarrow}$ & $\Left (\Left \; (\Right \; \textcolor{red}{\Empty}))$ \\
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
64 |
& $\stackrel{\inj \;\textcolor{red}{c} }{\rightarrow}$ &
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
65 |
$\Left \; (\Left \; (\Seq \;(\Left \; (\Seq \; (\Right \; (\Right\; \textcolor{blue}{\Empty})) \; \Stars \, [])) \; \textcolor{red}{c}))$\\
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
66 |
& $\stackrel{\inj \;\textcolor{blue}{a}}{\rightarrow}$ &
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
67 |
$\Left\; (\Seq \; (\Seq\; (\Right \; (\Seq \; \textcolor{magenta}{\Empty }\; \textcolor{blue}{ \mathbf{a}}) )
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
68 |
\;\Stars \,[]) \; \textcolor{red}{c})$\\
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
69 |
& $\stackrel{\inj \;\textcolor{magenta}{a}}{\rightarrow}$ & $\Seq \; (\Stars \; [\Right \; (\Seq \; \mathbf{\textcolor{magenta}{a}} \; \textcolor{blue}{a})]) \; \textcolor{red}{ c}$
|
| 579 | 70 |
|
|
668
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
71 |
%$\inj \; r \; c\A$ |
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
72 |
%$\inj \; (a\cdot b)\cdot c \; \Seq \; \ONE \; b$ & $=$ & $(a+e)$\\ |
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
73 |
\end{tabular}
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
74 |
\end{center}
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
75 |
\noindent |
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
76 |
For the un |
| 579 | 77 |
|
|
668
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
78 |
\begin{center}
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
79 |
\begin{tabular}{lcl}
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
80 |
$\inj$ & $\quad ((\ONE + {\ONE}
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
81 |
\textcolor{blue}{a})\cdot (a+aa)^*)\cdot
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
82 |
+ \ZERO \; \quad \textcolor{blue}{a} \; $ & \\
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
83 |
$\quad \Left \; |
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
84 |
(\Left \; (\Seq \;(\Left \; (\Seq \; (\Right \; (\Right\; |
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
85 |
\textcolor{blue}{\Empty})) \; \Stars \, [])) \; c))$ & \\$=$\\
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
86 |
$\Left \; (\inj \; ((\ONE + \ONE |
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
87 |
\textcolor{blue}{a})\cdot (a+aa)^*)\cdot
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
88 |
c \quad \textcolor{blue}{a} \quad (\Left \; (\Seq\; ( \Left \; (\Seq \; (\Right \; (\Right\;
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
89 |
\textcolor{blue}{\Empty})) \; \Stars \, []) ) \; c ) )\;\;)$ &\\ $=$\\
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
90 |
$\Left \; (\Seq \; (\inj \; (\ONE + \ONE \textcolor{blue}{a})\cdot(a+aa)^* \quad \textcolor{blue}{a} \quad
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
91 |
(\Left \; (\Seq \; (\Right \; (\Right\;\textcolor{blue}{\Empty})))) ) \; c ) $ & \\$=$\\
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
92 |
$\Left \; (\Seq \; (\Seq \; (\inj \quad (\ONE + \ONE \textcolor{blue}{a}) \quad \textcolor{blue}{a}\quad \Right \;(\Right \; \textcolor{blue}{\Empty}) ) \; \Stars \,[])\; c)$ &\\ $=$ \\
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
93 |
$\Left \; (\Seq \; (\Seq \; (\Right \; (\inj \; \ONE \textcolor{blue}{a} \quad \textcolor{blue}{a}\quad (\Right \;\textcolor{blue}{\Empty})))) \; \Stars \, [])$
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
94 |
& \\ $=$\\ |
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
95 |
$\Left \; (\Seq \; (\Seq \; (\Right \; (\Seq \; (\mkeps \; \ONE)\;(\inj \;\textcolor{blue}{a} \; \textcolor{blue}{a} \; \textcolor{blue}{\Empty})) ) ) \; \Stars \, [] )$
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
96 |
& \\ $=$\\ |
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
97 |
$\Left \; (\Seq \; (\Seq \; (\Right \; (\Seq \; \Empty \; \textcolor{blue}{a}) ) ) \; \Stars \, [] )$
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
98 |
\end{tabular}
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
99 |
\end{center}
|
| 579 | 100 |
|
101 |
||
102 |
||
103 |
||
104 |
||
105 |
||
106 |
||
107 |
||
|
668
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
108 |
% The first problem with this algorithm is that |
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
109 |
% for the function $\inj$ to work properly |
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
110 |
% we cannot destroy the structure of a regular expression, |
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
111 |
% and therefore cannot simplify along the way without mechanisms |
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
112 |
% that restores the values during the simplification process. |
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
113 |
% %too aggressively. |
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
114 |
% For example, |
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
115 |
% \[ |
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
116 |
% r + (r + a) \rightarrow r + a |
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
117 |
% \] |
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
118 |
% cannot be applied because that would require |
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
119 |
% breaking up the inner alternative. |
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
120 |
% The $\lexer$ plus $\textit{simp}$ therefore only enables
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
121 |
% same-level de-duplications like |
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
122 |
% \[ |
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
123 |
% r + r \rightarrow r. |
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
124 |
% \] |
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
125 |
% Secondly, the algorithm recursively calls $\lexer$ on |
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
126 |
% each new character input, |
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
127 |
% and before starting a child call |
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
128 |
% it stores information of previous lexing steps |
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
129 |
% on a stack, in the form of regular expressions |
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
130 |
% and characters: $r_0$, $c_0$, $r_1$, $c_1$, etc. |
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
131 |
% Each descent into deeper recursive calls in $\lexer$ |
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
132 |
% causes a new pair of $r_i, c_i$ to be pushed to the call stack. |
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
133 |
% \begin{figure}[H]
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
134 |
% \begin{tikzpicture}[->,>=stealth',shorten >=1pt,auto,thick]
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
135 |
% %\draw (-6,-6) grid (6,6); |
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
136 |
% \node [ circle ] (r) at (-6, 5) {$r$};
|
| 579 | 137 |
|
|
668
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
138 |
% %\node (-4, 6) (c1) circle [radius = 0.3] {$c_1$};
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
139 |
% \node [circle, minimum size = 0.1, draw] (c1) at (-4, 5.4) {$c_1$};
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
140 |
% % |
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
141 |
% %\node (-2, 5) (r1) circle [radius = 0.5] {$r_1$};
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
142 |
% \node [minimum size = 0.5, circle, draw] (r1) at (-2, 5) {$r_1$};
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
143 |
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
144 |
% \node [minimum width = 2cm, rectangle, draw] (stack) at (0, 3) {Stack};
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
145 |
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
146 |
% \path |
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
147 |
% (r) |
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
148 |
% edge [->, >=stealth',shorten >=1pt] node[left] {} (r1);
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
149 |
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
150 |
% \path (r1) |
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
151 |
% edge [bend right, dashed] node {saved} (stack);
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
152 |
% \path (c1) |
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
153 |
% edge [bend right, dashed] node {} (stack);
|
| 579 | 154 |
|
|
668
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
155 |
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
156 |
% \end{tikzpicture}
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
157 |
% \caption{First derivative taken}
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
158 |
% \end{figure}
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
159 |
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
160 |
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
161 |
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
162 |
% \begin{figure}[H]
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
163 |
% \begin{tikzpicture}[->,>=stealth',shorten >=1pt,auto,thick]
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
164 |
% %\draw (-6,-6) grid (6,6); |
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
165 |
% \node [ circle ] (r) at (-6, 5) {$r$};
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
166 |
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
167 |
% %\node (-4, 6) (c1) circle [radius = 0.3] {$c_1$};
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
168 |
% \node [circle, minimum size = 0.1, ] (c1) at (-4, 5.4) {$c_1$};
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
169 |
% % |
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
170 |
% %\node (-2, 5) (r1) circle [radius = 0.5] {$r_1$};
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
171 |
% \node [minimum size = 0.5, circle, ] (r1) at (-2, 5) {$r_1$};
|
| 580 | 172 |
|
173 |
||
|
668
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
174 |
% \node [circle, minimum size = 0.1, draw] (c2) at (0, 5.4) {$c_2$};
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
175 |
% % |
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
176 |
% %\node (2, 5) (r2) circle [radius = 0.5] {$r_2$};
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
177 |
% \node [circle, draw] (r2) at (2, 5) {$r_2$};
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
178 |
% \node [minimum width = 3cm, minimum height = 1cm, rectangle, draw] (stack) at (0, 2) {\large Stack};
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
179 |
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
180 |
% \path |
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
181 |
% (r) |
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
182 |
% edge [->, >=stealth',shorten >=1pt] node[left] {} (r1);
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
183 |
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
184 |
% \path (r2) |
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
185 |
% edge [bend right, dashed] node {} (stack);
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
186 |
% \path (c2) |
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
187 |
% edge [bend right, dashed] node {} (stack);
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
188 |
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
189 |
% \path (r1) |
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
190 |
% edge [] node {} (r2);
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
191 |
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
192 |
% \end{tikzpicture}
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
193 |
% \caption{Second derivative taken}
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
194 |
% \end{figure}
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
195 |
% \noindent |
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
196 |
% As the number of derivative steps increases, |
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
197 |
% the stack would increase: |
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
198 |
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
199 |
% \begin{figure}[H]
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
200 |
% \begin{tikzpicture}[->,>=stealth',shorten >=1pt,auto,thick]
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
201 |
% %\draw (-6,-6) grid (6,6); |
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
202 |
% \node [ circle ] (r) at (-6, 5) {$r$};
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
203 |
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
204 |
% %\node (-4, 6) (c1) circle [radius = 0.3] {$c_1$};
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
205 |
% \node [circle, minimum size = 0.1, ] (c1) at (-4, 5.4) {$c_1$};
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
206 |
% % |
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
207 |
% %\node (-2, 5) (r1) circle [radius = 0.5] {$r_1$};
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
208 |
% \node [minimum size = 0.5, circle, ] (r1) at (-2, 5) {$r_1$};
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
209 |
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
210 |
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
211 |
% \node [circle, minimum size = 0.1, ] (c2) at (0, 5.4) {$c_2$};
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
212 |
% % |
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
213 |
% %\node (2, 5) (r2) circle [radius = 0.5] {$r_2$};
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
214 |
% \node [circle, ] (r2) at (2, 5) {$r_2$};
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
215 |
% \node [minimum width = 4cm, minimum height = 2.5cm, rectangle, draw] (stack) at (0, 1) { \large Stack};
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
216 |
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
217 |
% \node [] (ldots) at (3.5, 5) {};
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
218 |
% %\node (6, 5) (rn) circle [radius = 0.5] {$r_n$};
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
219 |
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
220 |
% \node [minimum size = 0.5, circle, ] (rn) at (6, 5) {};
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
221 |
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
222 |
% \node (rldots) at ($(ldots)!.4!(rn)$) {\ldots};
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
223 |
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
224 |
% \path |
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
225 |
% (r) |
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
226 |
% edge [->, >=stealth',shorten >=1pt] node[left] {} (r1);
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
227 |
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
228 |
% \path (rldots) |
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
229 |
% edge [bend left, dashed] node {} (stack);
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
230 |
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
231 |
% \path (r1) |
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
232 |
% edge [] node {} (r2);
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
233 |
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
234 |
% \path (r2) |
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
235 |
% edge [] node {} (ldots);
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
236 |
% \path (ldots) |
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
237 |
% edge [bend left, dashed] node {} (stack);
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
238 |
% \path (5.03, 4.9) |
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
239 |
% edge [bend left, dashed] node {} (stack);
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
240 |
% \end{tikzpicture}
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
241 |
% \caption{More derivatives taken}
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
242 |
% \end{figure}
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
243 |
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
244 |
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
245 |
% \begin{figure}[H]
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
246 |
% \begin{tikzpicture}[->,>=stealth',shorten >=1pt,auto,thick]
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
247 |
% %\draw (-6,-6) grid (6,6); |
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
248 |
% \node [radius = 0.5, circle, draw] (r) at (-6, 5) {$r$};
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
249 |
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
250 |
% %\node (-4, 6) (c1) circle [radius = 0.3] {$c_1$};
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
251 |
% \node [circle, minimum size = 0.1, draw] (c1) at (-4, 5.4) {$c_1$};
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
252 |
% % |
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
253 |
% %\node (-2, 5) (r1) circle [radius = 0.5] {$r_1$};
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
254 |
% \node [minimum size = 0.5, circle, draw] (r1) at (-2, 5) {$r_1$};
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
255 |
% % |
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
256 |
% %\node (0, 6) (c2) circle [radius = 0.3] {$c_2$};
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
257 |
% \node [circle, minimum size = 0.1, draw] (c2) at (0, 5.4) {$c_2$};
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
258 |
% % |
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
259 |
% %\node (2, 5) (r2) circle [radius = 0.5] {$r_2$};
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
260 |
% \node [circle, draw] (r2) at (2, 5) {$r_2$};
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
261 |
% % |
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
262 |
% % |
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
263 |
% \node [] (ldots) at (4.5, 5) {};
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
264 |
% %\node (6, 5) (rn) circle [radius = 0.5] {$r_n$};
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
265 |
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
266 |
% \node [minimum size = 0.5, circle, draw] (rn) at (6, 5) {$r_n$};
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
267 |
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
268 |
% \node at ($(ldots)!.4!(rn)$) {\ldots};
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
269 |
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
270 |
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
271 |
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
272 |
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
273 |
% \node [minimum size = 6cm, rectangle, draw] (stack) at (0, 0) {\Huge Stack};
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
274 |
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
275 |
% \path |
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
276 |
% (r) |
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
277 |
% edge [->, >=stealth',shorten >=1pt] node[left] {} (r1);
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
278 |
% \path |
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
279 |
% (r1) |
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
280 |
% edge [] node {} (r2);
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
281 |
% \path (r2) |
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
282 |
% edge [] node {} (ldots);
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
283 |
% \path (r) |
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
284 |
% edge [dashed, bend right] node {} (stack);
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
285 |
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
286 |
% \path (r1) |
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
287 |
% edge [dashed, ] node {} (stack);
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
288 |
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
289 |
% \path (c1) |
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
290 |
% edge [dashed, bend right] node {} (stack);
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
291 |
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
292 |
% \path (c2) |
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
293 |
% edge [dashed] node {} (stack);
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
294 |
% \path (4.5, 5) |
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
295 |
% edge [dashed, bend left] node {} (stack);
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
296 |
% \path (4.9, 5) |
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
297 |
% edge [dashed, bend left] node {} (stack);
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
298 |
% \path (5.3, 5) |
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
299 |
% edge [dashed, bend left] node {} (stack);
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
300 |
% \path (r2) |
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
301 |
% edge [dashed, ] node {} (stack);
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
302 |
% \path (rn) |
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
303 |
% edge [dashed, bend left] node {} (stack);
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
304 |
% \end{tikzpicture}
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
305 |
% \caption{Before injection phase starts}
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
306 |
% \end{figure}
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
307 |
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
308 |
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
309 |
% \noindent |
| 580 | 310 |
After all derivatives have been taken, the stack grows to a maximum size |
311 |
and the pair of regular expressions and characters $r_i, c_{i+1}$
|
|
312 |
are then popped out and used in the injection phase. |
|
313 |
||
314 |
||
315 |
||
|
668
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
316 |
% \begin{figure}[H]
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
317 |
% \begin{tikzpicture}[->,>=stealth',shorten >=1pt,auto,thick]
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
318 |
% %\draw (-6,-6) grid (6,6); |
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
319 |
% \node [radius = 0.5, circle, ] (r) at (-6, 5) {$r$};
|
| 580 | 320 |
|
|
668
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
321 |
% %\node (-4, 6) (c1) circle [radius = 0.3] {$c_1$};
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
322 |
% \node [circle, minimum size = 0.1, ] (c1) at (-4, 5.4) {$c_1$};
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
323 |
% % |
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
324 |
% %\node (-2, 5) (r1) circle [radius = 0.5] {$r_1$};
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
325 |
% \node [minimum size = 0.5, circle, ] (r1) at (-2, 5) {$r_1$};
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
326 |
% % |
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
327 |
% %\node (0, 6) (c2) circle [radius = 0.3] {$c_2$};
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
328 |
% \node [circle, minimum size = 0.1, ] (c2) at (0, 5.4) {$c_2$};
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
329 |
% % |
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
330 |
% %\node (2, 5) (r2) circle [radius = 0.5] {$r_2$};
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
331 |
% \node [circle, ] (r2) at (2, 5) {$r_2$};
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
332 |
% % |
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
333 |
% % |
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
334 |
% \node [] (ldots) at (4.5, 5) {};
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
335 |
% %\node (6, 5) (rn) circle [radius = 0.5] {$r_n$};
|
| 580 | 336 |
|
|
668
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
337 |
% \node [minimum size = 0.5, circle, ] (rn) at (6, 5) {$r_n$};
|
| 580 | 338 |
|
|
668
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
339 |
% \node at ($(ldots)!.4!(rn)$) {\ldots};
|
| 580 | 340 |
|
|
668
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
341 |
% \node [minimum size = 0.5, circle, ] (vn) at (6, -5) {$v_n$};
|
| 580 | 342 |
|
|
668
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
343 |
% \node [] (ldots2) at (3.5, -5) {};
|
| 580 | 344 |
|
|
668
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
345 |
% \node [minimum size = 0.5, circle, ] (v2) at (2, -5) {$v_2$};
|
| 580 | 346 |
|
|
668
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
347 |
% \node at ($(ldots2)!.4!(v2)$) {\ldots};
|
| 580 | 348 |
|
349 |
||
|
668
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
350 |
% \node [circle, ] (v1) at (-2, -5) {$v_1$};
|
| 580 | 351 |
|
|
668
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
352 |
% \node [radius = 0.5, circle, ] (v) at (-6, -5) {$v$};
|
| 580 | 353 |
|
|
668
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
354 |
% \node [minimum size = 6cm, rectangle, draw] (stack) at (0, 0) {\Huge Stack};
|
| 580 | 355 |
|
|
668
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
356 |
% \path |
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
357 |
% (r) |
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
358 |
% edge [->, >=stealth',shorten >=1pt] node[left] {} (r1);
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
359 |
% \path |
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
360 |
% (r1) |
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
361 |
% edge [] node {} (r2);
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
362 |
% \path (r2) |
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
363 |
% edge [] node {} (ldots);
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
364 |
% \path (rn) |
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
365 |
% edge [] node {$\mkeps$} (vn);
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
366 |
% \path (vn) |
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
367 |
% edge [] node {} (ldots2);
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
368 |
% \path (v2) |
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
369 |
% edge [] node {$\inj \; r_1 \; c_2\;v_2$} (v1);
|
| 580 | 370 |
|
|
668
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
371 |
% \path (v1) |
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
372 |
% edge [] node {$\inj \; r \; c_1 \; v_1$} (v);
|
| 580 | 373 |
|
|
668
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
374 |
% \path (stack) |
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
375 |
% edge [dashed] node {} (-4.2, -5.2);
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
376 |
% \path (stack) |
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
377 |
% edge [dashed] node {} (-4, -5.2);
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
378 |
% \path (stack) |
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
379 |
% edge [dashed] node {} (-0.1, -5.2);
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
380 |
% \path (stack) |
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
381 |
% edge [dashed] node {} (0.2, -5.26);
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
382 |
% \path (stack) |
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
383 |
% edge [dashed] node {} (3.2, -5);
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
384 |
% \path (stack) |
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
385 |
% edge [dashed] node {} (2.7, -5);
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
386 |
% \path (stack) |
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
387 |
% edge [dashed] node {} (3.7, -5);
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
388 |
% \end{tikzpicture}
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
389 |
% \caption{Stored $r_i, c_{i+1}$ Used by $\inj$}
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
390 |
% \end{figure}
|
|
3831621d7b14
added technical Overview section, almost done introduction
Chengsong
parents:
667
diff
changeset
|
391 |
% \noindent |
| 580 | 392 |
Storing all $r_i, c_{i+1}$ pairs recursively
|
393 |
allows the algorithm to work in an elegant way, at the expense of |
|
| 624 | 394 |
storing quite a bit of verbose information on the stack. |
395 |
The stack seems to grow at least quadratically with respect |
|
| 580 | 396 |
to the input (not taking into account the size bloat of $r_i$), |
| 624 | 397 |
which can be inefficient and prone to stack overflows. |
| 667 | 398 |
\section{Bitcoded Algorithm}\label{bitDef}
|
| 580 | 399 |
To address this, |
| 624 | 400 |
Sulzmann and Lu defined a new datatype |
| 580 | 401 |
called \emph{annotated regular expression},
|
402 |
which condenses all the partial lexing information |
|
403 |
(that was originally stored in $r_i, c_{i+1}$ pairs)
|
|
404 |
into bitcodes. |
|
| 581 | 405 |
The bitcodes are then carried with the regular |
406 |
expression, and augmented or moved around |
|
| 638 | 407 |
as the lexing proceeds. |
| 581 | 408 |
It becomes unnecessary |
409 |
to remember all the |
|
|
640
bd1354127574
more proofreading done, last version before submission
Chengsong
parents:
639
diff
changeset
|
410 |
intermediate expressions, but only the most recent one |
| 581 | 411 |
with this bit-carrying regular expression. |
| 580 | 412 |
Annotated regular expressions |
413 |
are defined as the following |
|
| 638 | 414 |
Isabelle datatype:\footnote{ We use subscript notation to indicate
|
|
640
bd1354127574
more proofreading done, last version before submission
Chengsong
parents:
639
diff
changeset
|
415 |
that the bitcodes are auxiliary information that does not |
| 638 | 416 |
interfere with the structure of the regular expressions } |
| 580 | 417 |
\begin{center}
|
418 |
\begin{tabular}{lcl}
|
|
419 |
$\textit{a}$ & $::=$ & $\ZERO$\\
|
|
420 |
& $\mid$ & $_{bs}\ONE$\\
|
|
421 |
& $\mid$ & $_{bs}{\bf c}$\\
|
|
422 |
& $\mid$ & $_{bs}\sum\,as$\\
|
|
423 |
& $\mid$ & $_{bs}a_1\cdot a_2$\\
|
|
424 |
& $\mid$ & $_{bs}a^*$
|
|
425 |
\end{tabular}
|
|
426 |
\end{center}
|
|
427 |
\noindent |
|
428 |
where $bs$ stands for bit-codes, $a$ for $\mathbf{a}$nnotated regular
|
|
429 |
expressions and $as$ for lists of annotated regular expressions. |
|
| 638 | 430 |
The alternative constructor, written $\sum$, has been generalised to |
| 624 | 431 |
take a list of annotated regular expressions rather than just two. |
432 |
Why is it generalised? This is because when we analyse nested |
|
433 |
alternatives, there can be more than two elements at the same level |
|
| 580 | 434 |
after de-duplication, which can no longer be stored in a binary |
435 |
constructor. |
|
436 |
Bits and bitcodes (lists of bits) are defined as: |
|
437 |
\begin{center}
|
|
438 |
$b ::= S \mid Z \qquad |
|
439 |
bs ::= [] \mid b::bs |
|
440 |
$ |
|
441 |
\end{center}
|
|
442 |
\noindent |
|
443 |
We use $S$ and $Z$ rather than $1$ and $0$ is to avoid |
|
444 |
confusion with the regular expressions $\ZERO$ and $\ONE$. |
|
| 624 | 445 |
The idea is to use the bitcodes |
| 580 | 446 |
to indicate which choice was made at a certain point |
447 |
during lexing. |
|
448 |
For example, |
|
449 |
$(_{Z}a+_{S}b) \backslash a$ gives us
|
|
| 624 | 450 |
$_{Z}\ONE + \ZERO$, where the $Z$ bitcode will
|
| 580 | 451 |
later be used to decode that a left branch was |
| 638 | 452 |
selected at the time when the part $a+b$ was analysed by |
| 624 | 453 |
derivative. |
| 580 | 454 |
\subsection{A Bird's Eye View of the Bit-coded Lexer}
|
| 624 | 455 |
Before we give the details of the functions and definitions |
| 580 | 456 |
related to our |
457 |
$\blexer$ (\emph{b}-itcoded lexer), we first provide a high-level
|
|
| 624 | 458 |
view of the algorithm. |
| 580 | 459 |
\begin{figure}[H]
|
460 |
\begin{tikzpicture}[->,>=stealth',shorten >=1pt,auto,thick]
|
|
461 |
%\draw (-6,-6) grid (6,6); |
|
462 |
||
463 |
\node [circle, draw] (r0) at (-6, 2) {$r$};
|
|
464 |
||
465 |
\node [radius = 0.5, circle, draw] (r) at (-6, 5) {$_{bs}a$};
|
|
466 |
\path (r0) |
|
467 |
edge [] node {$\internalise$} (r);
|
|
468 |
%\node (-4, 6) (c1) circle [radius = 0.3] {$c_1$};
|
|
469 |
\node [circle, minimum size = 0.1, draw] (c1) at (-4, 5.4) {$c_1$};
|
|
| 579 | 470 |
% |
| 580 | 471 |
%\node (-2, 5) (r1) circle [radius = 0.5] {$r_1$};
|
472 |
\node [minimum size = 1.0cm, circle, draw] (r1) at (-2, 5) {$_{bs_1}a_1$};
|
|
473 |
% |
|
474 |
%\node (0, 6) (c2) circle [radius = 0.3] {$c_2$};
|
|
475 |
\node [circle, minimum size = 0.1, draw] (c2) at (0, 5.4) {$c_2$};
|
|
476 |
% |
|
477 |
%\node (2, 5) (r2) circle [radius = 0.5] {$r_2$};
|
|
478 |
\node [circle, draw, minimum size = 1.4cm] (r2) at (2, 5) {$_{bs_2}a_2$};
|
|
479 |
% |
|
480 |
% |
|
481 |
\node [] (ldots) at (4.5, 5) {};
|
|
482 |
%\node (6, 5) (rn) circle [radius = 0.5] {$r_n$};
|
|
483 |
||
484 |
\node [minimum size = 2.2cm, circle, draw] (rn) at (6, 5) {$_{bs_n}a_n$};
|
|
485 |
||
486 |
\node at ($(ldots)!.1!(rn)$) {\ldots};
|
|
487 |
||
488 |
\node [minimum size = 0.5, circle, ] (v) at (6, 2) {$v$};
|
|
489 |
||
490 |
%\node [] (v2) at (4, -5) {};
|
|
491 |
% |
|
492 |
%\node [draw, cross out] (ldots2) at (5, -5) {};
|
|
| 579 | 493 |
% |
| 580 | 494 |
%\node at ($(ldots2)!.4!(v2)$) {\ldots};
|
495 |
||
496 |
||
497 |
\node [align = center] (decode) at (6.6, 3.2) {$\bmkeps$\\$\decode$};
|
|
498 |
||
499 |
\path (c1) |
|
500 |
edge [dashed, bend left] node {} (r0);
|
|
501 |
||
502 |
\path (c2) |
|
503 |
edge [dashed, bend left] node {} (r0);
|
|
504 |
||
505 |
\path (r1) |
|
506 |
edge [dashed, bend right] node {} (r2);
|
|
507 |
||
508 |
||
509 |
\path |
|
510 |
(r) |
|
511 |
edge [dashed, bend right] node[left] {} (r1);
|
|
512 |
||
513 |
\path |
|
514 |
(r) |
|
515 |
edge [->, >=stealth',shorten >=1pt] node[left] {} (r1);
|
|
516 |
||
517 |
\path |
|
518 |
(r1) |
|
519 |
edge [] node {} (r2);
|
|
520 |
\path (r2) |
|
521 |
edge [] node {} (ldots);
|
|
522 |
\path (rn) |
|
523 |
edge [] node {} (v);
|
|
524 |
||
525 |
\path (r0) |
|
526 |
edge [dashed, bend right] node {} (decode);
|
|
527 |
%\path (v) |
|
528 |
%edge [] node {} (ldots2);
|
|
| 579 | 529 |
|
530 |
||
531 |
||
| 580 | 532 |
\end{tikzpicture}
|
| 624 | 533 |
\caption{A bird's eye view of $\blexer$. The $_{bsi}a_{i}$s stand
|
534 |
for the annotated regular expressions in each derivative step. |
|
|
640
bd1354127574
more proofreading done, last version before submission
Chengsong
parents:
639
diff
changeset
|
535 |
The characters used in each derivative are written as $c_i$. |
|
bd1354127574
more proofreading done, last version before submission
Chengsong
parents:
639
diff
changeset
|
536 |
The size of the derivatives typically increases during each derivative step. |
| 638 | 537 |
The process starts with an internalise phase and concludes with a decoding phase.} |
| 580 | 538 |
\end{figure}
|
539 |
\noindent |
|
540 |
The plain regular expressions |
|
541 |
are first ``lifted'' to an annotated regular expression, |
|
| 624 | 542 |
with the function called \emph{internalise} ($r \rightarrow _{bs}a$).
|
| 580 | 543 |
Then the annotated regular expression $_{bs}a$ will
|
| 624 | 544 |
be transformed by successive derivatives with respect |
| 580 | 545 |
to the input stream of characters $c_1, c_2$ etc. |
546 |
Each time a derivative is taken, the bitcodes |
|
547 |
are moved around, discarded or augmented together |
|
548 |
with the regular expression they are attached to. |
|
549 |
After all input has been consumed, the |
|
550 |
bitcodes are collected by $\bmkeps$, |
|
551 |
which traverses the nullable part of the regular expression |
|
| 624 | 552 |
and collects the bitcodes along the way. |
| 580 | 553 |
The collected bitcodes are then $\decode$d with the guidance |
| 624 | 554 |
of the input regular expression $r$ ( $_{bs}a \rightarrow r$).
|
| 580 | 555 |
The most notable improvements of $\blexer$ |
556 |
over $\lexer$ are |
|
557 |
\begin{itemize}
|
|
558 |
\item |
|
559 |
||
| 638 | 560 |
the absence of the second injection phase. |
| 580 | 561 |
\item |
| 638 | 562 |
one does not need to store each pair of the |
| 580 | 563 |
intermediate regular expressions $_{bs_i}a_i$ and $c_{i+1}$.
|
564 |
The previous annotated regular expression $_{bs_i}a_i$'s information is passed
|
|
565 |
on without loss to its successor $_{bs_{i+1}}a_{i+1}$,
|
|
| 624 | 566 |
and $c_{i+1}$'s information is stored in $L\;r$.\footnote{
|
567 |
which will be used during the decode phase, where we use $r$ as |
|
568 |
a source of information.} |
|
| 580 | 569 |
\item |
| 638 | 570 |
simplification works much smoother--one can maintain correctness |
| 624 | 571 |
while applying quite aggressive simplifications. |
| 580 | 572 |
\end{itemize}
|
| 624 | 573 |
%In the next section we will |
574 |
%give the operations needed in $\blexer$, |
|
575 |
%with some remarks on the idea behind their definitions. |
|
| 580 | 576 |
\subsection{Operations in $\textit{Blexer}$}
|
577 |
The first operation we define related to bit-coded regular expressions |
|
578 |
is how we move bits to the inside of regular expressions. |
|
| 624 | 579 |
This operation is called $\fuse$: |
| 580 | 580 |
\begin{center}
|
581 |
\begin{tabular}{lcl}
|
|
| 624 | 582 |
$\textit{fuse}\;bs \; (\ZERO)$ & $\dn$ & $\ZERO$\\
|
583 |
$\textit{fuse}\;bs\; (_{bs'})\ONE$ & $\dn$ &
|
|
| 580 | 584 |
$_{bs @ bs'}\ONE$\\
|
| 624 | 585 |
$\textit{fuse}\;bs\;(_{bs'}{\bf c})$ & $\dn$ &
|
| 580 | 586 |
$_{bs@bs'}{\bf c}$\\
|
| 624 | 587 |
$\textit{fuse}\;bs\;(_{bs'}\sum\textit{as})$ & $\dn$ &
|
| 580 | 588 |
$_{bs@bs'}\sum\textit{as}$\\
|
| 624 | 589 |
$\textit{fuse}\;bs\; (_{bs'}a_1\cdot a_2)$ & $\dn$ &
|
| 580 | 590 |
$_{bs@bs'}a_1 \cdot a_2$\\
|
| 624 | 591 |
$\textit{fuse}\;bs\;(_{bs'}a^*)$ & $\dn$ &
|
| 580 | 592 |
$_{bs @ bs'}a^*$
|
593 |
\end{tabular}
|
|
594 |
\end{center}
|
|
595 |
||
596 |
\noindent |
|
| 624 | 597 |
With \emph{fuse} we are able to define the $\internalise$ function,
|
598 |
written $(\_)^\uparrow$, |
|
| 580 | 599 |
that translates a ``standard'' regular expression into an |
600 |
annotated regular expression. |
|
601 |
This function will be applied before we start |
|
602 |
with the derivative phase of the algorithm. |
|
603 |
||
604 |
\begin{center}
|
|
605 |
\begin{tabular}{lcl}
|
|
606 |
$(\ZERO)^\uparrow$ & $\dn$ & $\ZERO$\\ |
|
607 |
$(\ONE)^\uparrow$ & $\dn$ & $_{[]}\ONE$\\
|
|
608 |
$(c)^\uparrow$ & $\dn$ & $_{[]}{\bf c}$\\
|
|
609 |
$(r_1 + r_2)^\uparrow$ & $\dn$ & |
|
610 |
$_{[]}\sum[\textit{fuse}\,[Z]\,r_1^\uparrow,\,
|
|
611 |
\textit{fuse}\,[S]\,r_2^\uparrow]$\\
|
|
612 |
$(r_1\cdot r_2)^\uparrow$ & $\dn$ & |
|
613 |
$_{[]}r_1^\uparrow \cdot r_2^\uparrow$\\
|
|
614 |
$(r^*)^\uparrow$ & $\dn$ & |
|
615 |
$_{[]}(r^\uparrow)^*$\\
|
|
616 |
\end{tabular}
|
|
617 |
\end{center}
|
|
618 |
\noindent |
|
619 |
The opposite of $\textit{internalise}$ is
|
|
| 624 | 620 |
$\erase$, where all bit-codes are removed, |
| 580 | 621 |
and the alternative operator $\sum$ for annotated |
|
640
bd1354127574
more proofreading done, last version before submission
Chengsong
parents:
639
diff
changeset
|
622 |
regular expressions is transformed into the binary version |
| 624 | 623 |
in (plain) regular expressions. This can be defined as follows: |
624 |
\begin{center}\label{eraseDef}
|
|
| 580 | 625 |
\begin{tabular}{lcl}
|
626 |
$\ZERO_\downarrow$ & $\dn$ & $\ZERO$\\ |
|
627 |
$( _{bs}\ONE )_\downarrow$ & $\dn$ & $\ONE$\\
|
|
628 |
$( _{bs}\mathbf{c} )_\downarrow$ & $\dn$ & $\mathbf{c}$\\
|
|
629 |
$( _{bs} a_1 \cdot a_2 )_\downarrow$ & $\dn$ &
|
|
630 |
$ (a_1) _\downarrow \cdot (a_2) _\downarrow$\\ |
|
631 |
$( _{bs} [])_\downarrow $ & $\dn$ & $\ZERO $\\
|
|
632 |
$( _{bs} [a] )_\downarrow$ & $\dn$ & $a_\downarrow$\\
|
|
| 624 | 633 |
$(_{bs} \sum [a_1, \; a_2])_\downarrow$ & $\dn$ & $ (a_1) _\downarrow + ( a_2 ) _\downarrow $\\
|
| 580 | 634 |
$(_{bs} \sum (a :: as))_\downarrow$ & $\dn$ & $ a_\downarrow + \; (_{[]} \sum as)_\downarrow$\\
|
635 |
$( _{bs} a^* )_\downarrow$ & $\dn$ & $(a_\downarrow)^*$
|
|
636 |
\end{tabular}
|
|
637 |
\end{center}
|
|
638 |
\noindent |
|
| 638 | 639 |
Where we abbreviate the $\erase\; a$ operation |
640 |
as $(a)_\downarrow$, for conciseness. |
|
| 580 | 641 |
|
| 624 | 642 |
Determining whether an annotated regular expression |
| 638 | 643 |
contains the empty string in its language requires |
| 580 | 644 |
a dedicated function $\bnullable$. |
| 624 | 645 |
In our formalisation this function is defined by simply calling $\erase$ |
646 |
before $\nullable$. |
|
| 580 | 647 |
\begin{definition}
|
648 |
$\bnullable \; a \dn \nullable \; (a_\downarrow)$ |
|
649 |
\end{definition}
|
|
650 |
The function for collecting |
|
651 |
bitcodes from a |
|
652 |
(b)nullable regular expression is called $\bmkeps$. |
|
| 624 | 653 |
This function is a lifted version of the $\textit{mkeps}$ function,
|
| 580 | 654 |
which follows the path $\mkeps$ takes to traverse the |
655 |
$\nullable$ branches when visiting a regular expression, |
|
| 624 | 656 |
but collects bitcodes instead of generating a value. |
| 580 | 657 |
\begin{center}
|
658 |
\begin{tabular}{lcl}
|
|
659 |
$\textit{bmkeps}\,(_{bs}\ONE)$ & $\dn$ & $bs$\\
|
|
660 |
$\textit{bmkeps}\,(_{bs}\sum a::\textit{as})$ & $\dn$ &
|
|
661 |
$\textit{if}\;\textit{bnullable}\,a$\\
|
|
662 |
& &$\textit{then}\;bs\,@\,\textit{bmkeps}\,a$\\
|
|
663 |
& &$\textit{else}\;bs\,@\,\textit{bmkeps}\,(_{[]}\sum \textit{as})$\\
|
|
664 |
$\textit{bmkeps}\,(_{bs} a_1 \cdot a_2)$ & $\dn$ &
|
|
665 |
$bs \,@\,\textit{bmkeps}\,a_1\,@\, \textit{bmkeps}\,a_2$\\
|
|
666 |
$\textit{bmkeps}\,(_{bs}a^*)$ & $\dn$ &
|
|
| 585 | 667 |
$bs \,@\, [S]$ |
| 580 | 668 |
\end{tabular}
|
669 |
\end{center}
|
|
670 |
\noindent |
|
| 624 | 671 |
This function, just like $\mkeps$, |
| 581 | 672 |
visits a regular expression tree respecting |
| 624 | 673 |
the POSIX rules. |
| 581 | 674 |
It traverses each child of the sequence regular expression |
675 |
from left to right and creates a bitcode by stitching |
|
676 |
together bitcodes obtained from the children expressions. |
|
677 |
In the case of alternative regular expressions, |
|
678 |
it looks for the leftmost |
|
679 |
$\nullable$ branch |
|
| 638 | 680 |
to visit and ignores the other siblings. |
| 581 | 681 |
%Whenever there is some bitcodes attached to a |
682 |
%node, it returns the bitcodes concatenated with whatever |
|
683 |
%child recursive calls return. |
|
684 |
The only time when $\bmkeps$ creates new bitcodes |
|
685 |
is when it completes a star's iterations by attaching a $S$ to the end of the bitcode |
|
| 624 | 686 |
list it returns. |
687 |
||
| 580 | 688 |
The bitcodes extracted by $\bmkeps$ need to be |
| 638 | 689 |
$\decode$d (with the guidance of a ``plain'' regular expression): |
| 580 | 690 |
%\begin{definition}[Bitdecoding of Values]\mbox{}
|
691 |
\begin{center}
|
|
692 |
\begin{tabular}{@{}l@{\hspace{1mm}}c@{\hspace{1mm}}l@{}}
|
|
693 |
$\textit{decode}'\,bs\,(\ONE)$ & $\dn$ & $(\Empty, bs)$\\
|
|
694 |
$\textit{decode}'\,bs\,(c)$ & $\dn$ & $(\Char\,c, bs)$\\
|
|
695 |
$\textit{decode}'\,(Z\!::\!bs)\;(r_1 + r_2)$ & $\dn$ &
|
|
696 |
$\textit{let}\,(v, bs_1) = \textit{decode}'\,bs\,r_1\;\textit{in}\;
|
|
697 |
(\Left\,v, bs_1)$\\ |
|
698 |
$\textit{decode}'\,(S\!::\!bs)\;(r_1 + r_2)$ & $\dn$ &
|
|
699 |
$\textit{let}\,(v, bs_1) = \textit{decode}'\,bs\,r_2\;\textit{in}\;
|
|
700 |
(\Right\,v, bs_1)$\\ |
|
701 |
$\textit{decode}'\,bs\;(r_1\cdot r_2)$ & $\dn$ &
|
|
702 |
$\textit{let}\,(v_1, bs_1) = \textit{decode}'\,bs\,r_1\;\textit{in}$\\
|
|
703 |
& & $\textit{let}\,(v_2, bs_2) = \textit{decode}'\,bs_1\,r_2$\\
|
|
704 |
& & \hspace{35mm}$\textit{in}\;(\Seq\,v_1\,v_2, bs_2)$\\
|
|
| 585 | 705 |
$\textit{decode}'\,(S\!::\!bs)\,(r^*)$ & $\dn$ & $(\Stars\,[], bs)$\\
|
706 |
$\textit{decode}'\,(Z\!::\!bs)\,(r^*)$ & $\dn$ &
|
|
| 580 | 707 |
$\textit{let}\,(v, bs_1) = \textit{decode}'\,bs\,r\;\textit{in}$\\
|
708 |
& & $\textit{let}\,(\Stars\,vs, bs_2) = \textit{decode}'\,bs_1\,r^*$\\
|
|
709 |
& & \hspace{35mm}$\textit{in}\;(\Stars\,v\!::\!vs, bs_2)$\bigskip\\
|
|
710 |
||
711 |
$\textit{decode}\,bs\,r$ & $\dn$ &
|
|
712 |
$\textit{let}\,(v, bs') = \textit{decode}'\,bs\,r\;\textit{in}$\\
|
|
713 |
& & $\textit{if}\;bs' = []\;\textit{then}\;\textit{Some}\,v\;
|
|
714 |
\textit{else}\;\textit{None}$
|
|
715 |
\end{tabular}
|
|
716 |
\end{center}
|
|
| 537 | 717 |
\noindent |
| 580 | 718 |
The function $\decode'$ returns a pair consisting of |
| 624 | 719 |
a partially decoded value and some leftover bit-list. |
| 580 | 720 |
The function $\decode'$ succeeds if the left-over |
721 |
bit-sequence is empty. |
|
| 624 | 722 |
|
723 |
%$\decode$ is terminating as $\decode'$ is terminating. |
|
724 |
%$\decode'$ is terminating |
|
725 |
%because at least one of $\decode'$'s parameters will go down in terms |
|
726 |
%of size.\\ |
|
| 580 | 727 |
The reverse operation of $\decode$ is $\code$. |
| 624 | 728 |
This function encodes a value into a bitcode by converting |
| 580 | 729 |
$\Left$ into $Z$, $\Right$ into $S$, and marks the start of any non-empty |
|
640
bd1354127574
more proofreading done, last version before submission
Chengsong
parents:
639
diff
changeset
|
730 |
star iteration by $S$. $ Z$ marks the border where a star iteration |
|
bd1354127574
more proofreading done, last version before submission
Chengsong
parents:
639
diff
changeset
|
731 |
terminates. |
| 580 | 732 |
This coding is lossy, as it throws away the information about |
733 |
characters, and does not encode the ``boundary'' between two |
|
734 |
sequence values. Moreover, with only the bitcode we cannot even tell |
|
| 624 | 735 |
whether the $S$s and $Z$s are for $\Left/\Right$ or $\Stars$, |
|
640
bd1354127574
more proofreading done, last version before submission
Chengsong
parents:
639
diff
changeset
|
736 |
but this will not be necessary for our correctness proof. |
| 580 | 737 |
\begin{center}
|
738 |
\begin{tabular}{lcl}
|
|
739 |
$\textit{code}(\Empty)$ & $\dn$ & $[]$\\
|
|
740 |
$\textit{code}(\Char\,c)$ & $\dn$ & $[]$\\
|
|
741 |
$\textit{code}(\Left\,v)$ & $\dn$ & $Z :: code(v)$\\
|
|
742 |
$\textit{code}(\Right\,v)$ & $\dn$ & $S :: code(v)$\\
|
|
743 |
$\textit{code}(\Seq\,v_1\,v_2)$ & $\dn$ & $code(v_1) \,@\, code(v_2)$\\
|
|
744 |
$\textit{code}(\Stars\,[])$ & $\dn$ & $[Z]$\\
|
|
745 |
$\textit{code}(\Stars\,(v\!::\!vs))$ & $\dn$ & $S :: code(v) \;@\;
|
|
746 |
code(\Stars\,vs)$ |
|
747 |
\end{tabular}
|
|
748 |
\end{center}
|
|
749 |
\noindent |
|
| 624 | 750 |
We can prove that given a value $v$ and regular expression $r$ |
| 580 | 751 |
with $\vdash v:r$, |
752 |
then we have the property that $\decode$ and $\code$ are |
|
753 |
reverse operations of one another: |
|
754 |
\begin{lemma}
|
|
755 |
\[If \vdash v : r \; then \;\decode \; (\code \; v) \; r = \textit{Some}(v) \]
|
|
756 |
\end{lemma}
|
|
757 |
\begin{proof}
|
|
758 |
By proving a more general version of the lemma, on $\decode'$: |
|
759 |
\[\vdash v : r \implies \decode' \; ((\code \; v) @ ds) \; r = (v, ds) \] |
|
|
640
bd1354127574
more proofreading done, last version before submission
Chengsong
parents:
639
diff
changeset
|
760 |
Then we obtain the property by setting $ds$ to be $[]$ and unfolding the $\decode$ definition. |
| 580 | 761 |
\end{proof}
|
762 |
\noindent |
|
| 638 | 763 |
Now we define the central part of Sulzmann and Lu's second lexing algorithm, |
| 624 | 764 |
the $\bder$ function (which stands for \emph{b}itcoded-derivative):
|
| 580 | 765 |
\begin{center}
|
766 |
\begin{tabular}{@{}lcl@{}}
|
|
767 |
$(\ZERO)\,\backslash c$ & $\dn$ & $\ZERO$\\ |
|
768 |
$(_{bs}\ONE)\,\backslash c$ & $\dn$ & $\ZERO$\\
|
|
769 |
$(_{bs}{\bf d})\,\backslash c$ & $\dn$ &
|
|
770 |
$\textit{if}\;c=d\; \;\textit{then}\;
|
|
771 |
_{bs}\ONE\;\textit{else}\;\ZERO$\\
|
|
772 |
$(_{bs}\sum \;\textit{as})\,\backslash c$ & $\dn$ &
|
|
773 |
$_{bs}\sum\;(\textit{map} \; (\_\backslash c) \; as )$\\
|
|
774 |
$(_{bs}\;a_1\cdot a_2)\,\backslash c$ & $\dn$ &
|
|
775 |
$\textit{if}\;\textit{bnullable}\,a_1$\\
|
|
776 |
& &$\textit{then}\;_{bs}\sum\,[(_{[]}\,(a_1\,\backslash c)\cdot\,a_2),$\\
|
|
777 |
& &$\phantom{\textit{then},\;_{bs}\sum\,}(\textit{fuse}\,(\textit{bmkeps}\,a_1)\,(a_2\,\backslash c))]$\\
|
|
778 |
& &$\textit{else}\;_{bs}\,(a_1\,\backslash c)\cdot a_2$\\
|
|
779 |
$(_{bs}a^*)\,\backslash c$ & $\dn$ &
|
|
780 |
$_{bs}(\textit{fuse}\, [Z] \; r\,\backslash c)\cdot
|
|
781 |
(_{[]}r^*))$
|
|
782 |
\end{tabular}
|
|
783 |
\end{center}
|
|
784 |
\noindent |
|
| 639 | 785 |
For $\bder \; c\; a$, we use the infix notation $a\backslash c$ for readability. |
| 624 | 786 |
The $\bder$ function tells us how regular expressions can be recursively traversed, |
| 580 | 787 |
where the bitcodes are augmented and carried around |
788 |
when a derivative is taken. |
|
789 |
We give the intuition behind some of the more involved cases in |
|
| 638 | 790 |
$\bder$. |
791 |
||
| 580 | 792 |
For example, |
793 |
in the \emph{star} case,
|
|
| 624 | 794 |
a derivative of $_{bs}a^*$ means
|
795 |
that one more star iteration needs to be taken. |
|
796 |
We therefore need to unfold it into a sequence, |
|
797 |
and attach an additional bit $Z$ to the front of $a \backslash c$ |
|
| 580 | 798 |
as a record to indicate one new star iteration is unfolded. |
799 |
||
800 |
\noindent |
|
801 |
\begin{center}
|
|
802 |
\begin{tabular}{@{}lcl@{}}
|
|
803 |
$(_{bs}a^*)\,\backslash c$ & $\dn$ &
|
|
804 |
$_{bs}(\underbrace{\textit{fuse}\, [Z] \; a\,\backslash c}_{\text{One more iteration}})\cdot
|
|
805 |
(_{[]}a^*))$
|
|
806 |
\end{tabular}
|
|
807 |
\end{center}
|
|
808 |
||
809 |
\noindent |
|
810 |
This information will be recovered later by the $\decode$ function. |
|
| 624 | 811 |
%The intuition is that the bit $Z$ will be decoded at the right location, |
812 |
%because we accumulate bits from left to right (a rigorous proof will be given |
|
813 |
%later). |
|
| 580 | 814 |
|
815 |
%\begin{tikzpicture}[ > = stealth, % arrow head style
|
|
816 |
% shorten > = 1pt, % don't touch arrow head to node |
|
817 |
% semithick % line style |
|
818 |
% ] |
|
819 |
% |
|
820 |
% \tikzstyle{every state}=[
|
|
821 |
% draw = black, |
|
822 |
% thin, |
|
823 |
% fill = cyan!29, |
|
824 |
% minimum size = 7mm |
|
825 |
% ] |
|
826 |
% \begin{scope}[node distance=1cm and 0cm, every node/.style=state]
|
|
827 |
% \node (k) [rectangle split, rectangle split horizontal, rectangle split parts=2, rectangle split part fill={red!30,blue!20},]
|
|
828 |
% {$bs$
|
|
829 |
% \nodepart{two} $a^*$ };
|
|
830 |
% \node (l) [below =of k, rectangle split, rectangle split horizontal, rectangle split parts=2, rectangle split part fill={red!30,blue!20},]
|
|
831 |
% { $bs$ + [Z]
|
|
832 |
% \nodepart{two} $(a\backslash c )\cdot a^*$ };
|
|
833 |
% \end{scope}
|
|
834 |
% \path[->] |
|
835 |
% (k) edge (l); |
|
836 |
%\end{tikzpicture}
|
|
837 |
% |
|
838 |
%Pictorially the process looks like below. |
|
839 |
%Like before, the red region denotes |
|
840 |
%previous lexing information (stored as bitcodes in $bs$). |
|
841 |
||
842 |
%\begin{tikzpicture}[every node/.append style={draw, rounded corners, inner sep=10pt}]
|
|
843 |
% \begin{scope}[node distance=1cm]
|
|
844 |
% \node (a) [rectangle split, rectangle split horizontal, rectangle split parts=2, rectangle split part fill={red!30,blue!20},]
|
|
845 |
% {$bs$
|
|
846 |
% \nodepart{two} $a^*$ };
|
|
847 |
% \node (b) [rectangle split, rectangle split horizontal, rectangle split parts=2, rectangle split part fill={red!30,blue!20},]
|
|
848 |
% { $bs$ + [Z]
|
|
849 |
% \nodepart{two} $(a\backslash c )\cdot a^*$ };
|
|
850 |
%%\caption{term 1 \ref{term:1}'s matching configuration}
|
|
851 |
% \end{scope}
|
|
852 |
%\end{tikzpicture}
|
|
853 |
||
854 |
\noindent |
|
855 |
Another place the $\bder$ function differs |
|
| 624 | 856 |
from derivatives on regular expressions |
| 580 | 857 |
is the sequence case: |
858 |
\begin{center}
|
|
859 |
\begin{tabular}{@{}lcl@{}}
|
|
860 |
||
861 |
$(_{bs}\;a_1\cdot a_2)\,\backslash c$ & $\dn$ &
|
|
862 |
$\textit{if}\;\textit{bnullable}\,a_1$\\
|
|
863 |
& &$\textit{then}\;_{bs}\sum\,[(_{[]}\,(a_1\,\backslash c)\cdot\,a_2),$\\
|
|
864 |
& &$\phantom{\textit{then},\;_{bs}\sum\,}(\textit{fuse}\,(\textit{bmkeps}\,a_1)\,(a_2\,\backslash c))]$\\
|
|
865 |
& &$\textit{else}\;_{bs}\,(a_1\,\backslash c)\cdot a_2$
|
|
866 |
\end{tabular}
|
|
867 |
\end{center}
|
|
868 |
\noindent |
|
| 624 | 869 |
%We assume that $\bmkeps$ |
870 |
%correctly extracts the bitcode for how $a_1$ |
|
871 |
%matches the string prior to $c$ (more on this later). |
|
872 |
%The bitsequence $\textit{bs}$ which was initially
|
|
873 |
%attached to the first element of the sequence |
|
874 |
%$a_1 \cdot a_2$, has now been |
|
875 |
%elevated to the top level of the $\sum$ constructor. |
|
876 |
%This is because this piece of information will be needed |
|
877 |
%whichever way the sequence is matched, |
|
878 |
%regardless of whether $c$ belongs to $a_1$ or $a_2$. |
|
879 |
The difference mainly lies in the $\textit{if}$ branch (when $a_1$ is $\bnullable$):
|
|
| 580 | 880 |
we use $\bmkeps$ to store the lexing information |
881 |
in $a_1$ before collapsing |
|
882 |
it (as it has been fully matched by string prior to $c$), |
|
883 |
and attach the collected bit-codes to the front of $a_2$ |
|
| 624 | 884 |
before throwing away $a_1$. |
| 580 | 885 |
In the injection-based lexer, $r_1$ is immediately thrown away in |
| 638 | 886 |
the $\textit{if}$ branch,
|
| 624 | 887 |
the information $r_1$ stores is therefore lost: |
| 580 | 888 |
\begin{center}
|
| 624 | 889 |
\begin{tabular}{lcl}
|
890 |
$(r_1 \cdot r_2)\backslash c$ & $\dn$ & $\mathit{if} \, [] \in L(r_1)$\\
|
|
891 |
& & $\mathit{then}\;(r_1\backslash c) \cdot r_2 \,+\, r_2\backslash c$\\
|
|
892 |
& & $\mathit{else}\; \ldots$\\
|
|
893 |
\end{tabular}
|
|
| 580 | 894 |
\end{center}
|
895 |
\noindent |
|
| 624 | 896 |
|
897 |
%\noindent |
|
898 |
%this loss of information makes it necessary |
|
899 |
%to store on stack all the regular expressions' |
|
900 |
%``snapshots'' before they were |
|
901 |
%taken derivative of. |
|
902 |
%So that the related information will be available |
|
903 |
%once the child recursive |
|
904 |
%call finishes.\\ |
|
| 580 | 905 |
The rest of the clauses of $\bder$ is rather similar to |
906 |
$\der$. \\ |
|
907 |
Generalising the derivative operation with bitcodes to strings, we have |
|
908 |
\begin{center}
|
|
909 |
\begin{tabular}{@{}lcl@{}}
|
|
910 |
$a\backslash_s [] $ & $\dn$ & $a$\\ |
|
911 |
$a\backslash (c :: s) $ & $\dn$ & $(a \backslash c) \backslash_s s$ |
|
912 |
\end{tabular}
|
|
913 |
\end{center}
|
|
914 |
\noindent |
|
915 |
As we did earlier, we omit the $s$ subscript at $\backslash_s$ when there is no danger |
|
916 |
of confusion. |
|
917 |
\subsection{Putting Things Together}
|
|
918 |
Putting these operations altogether, we obtain a lexer with bit-coded regular expressions |
|
919 |
as its internal data structures, which we call $\blexer$: |
|
920 |
||
921 |
\begin{center}
|
|
922 |
\begin{tabular}{lcl}
|
|
923 |
$\textit{blexer}\;r\,s$ & $\dn$ &
|
|
924 |
$\textit{let}\;a = (r^\uparrow)\backslash s\;\textit{in}$\\
|
|
925 |
& & $\;\;\textit{if}\; \textit{bnullable}(a)$\\
|
|
926 |
& & $\;\;\textit{then}\;\textit{decode}\,(\textit{bmkeps}\,a)\,r$\\
|
|
927 |
& & $\;\;\textit{else}\;\textit{None}$
|
|
928 |
\end{tabular}
|
|
929 |
\end{center}
|
|
930 |
\noindent |
|
| 624 | 931 |
This function first attaches bitcodes to a |
932 |
plain regular expression $r$, and then builds successive derivatives |
|
| 581 | 933 |
with respect to the input string $s$, and |
| 624 | 934 |
then test whether the result is (b)nullable. |
935 |
If yes, then extract the bitcodes from the nullable expression, |
|
| 581 | 936 |
and decodes the bitcodes into a lexical value. |
|
640
bd1354127574
more proofreading done, last version before submission
Chengsong
parents:
639
diff
changeset
|
937 |
If there does not exist a match between $r$ and $s$, the lexer |
| 638 | 938 |
outputs $\None$ indicating a mismatch. |
| 580 | 939 |
Ausaf and Urban formally proved the correctness of the $\blexer$, namely |
940 |
\begin{property}
|
|
941 |
$\blexer \;r \; s = \lexer \; r \; s$. |
|
942 |
\end{property}
|
|
| 581 | 943 |
\noindent |
| 580 | 944 |
This was claimed but not formalised in Sulzmann and Lu's work. |
945 |
We introduce the proof later, after we give all |
|
946 |
the needed auxiliary functions and definitions. |
|
| 581 | 947 |
\subsection{An Example $\blexer$ Run}
|
| 624 | 948 |
Before introducing the proof we shall first walk |
| 580 | 949 |
through a concrete example of our $\blexer$ calculating the right |
| 638 | 950 |
lexical information through bit-coded regular expressions. |
951 |
||
| 581 | 952 |
Consider the regular expression $(aa)^* \cdot (b+c)$ matching the string $aab$. |
953 |
We give again the bird's eye view of this particular example |
|
954 |
in each stage of the algorithm: |
|
955 |
||
956 |
\tikzset{three sided/.style={
|
|
957 |
draw=none, |
|
958 |
append after command={
|
|
959 |
[-,shorten <= -0.5\pgflinewidth] |
|
960 |
([shift={(-1.5\pgflinewidth,-0.5\pgflinewidth)}]\tikzlastnode.north east)
|
|
961 |
edge([shift={( 0.5\pgflinewidth,-0.5\pgflinewidth)}]\tikzlastnode.north west)
|
|
962 |
([shift={( 0.5\pgflinewidth,-0.5\pgflinewidth)}]\tikzlastnode.north west)
|
|
963 |
edge([shift={( 0.5\pgflinewidth,+0.5\pgflinewidth)}]\tikzlastnode.south west)
|
|
964 |
([shift={( 0.5\pgflinewidth,+0.5\pgflinewidth)}]\tikzlastnode.south west)
|
|
965 |
edge([shift={(-1.0\pgflinewidth,+0.5\pgflinewidth)}]\tikzlastnode.south east)
|
|
966 |
} |
|
967 |
} |
|
968 |
} |
|
969 |
||
970 |
\tikzset{three sided1/.style={
|
|
971 |
draw=none, |
|
972 |
append after command={
|
|
973 |
[-,shorten <= -0.5\pgflinewidth] |
|
974 |
([shift={(1.5\pgflinewidth,-0.5\pgflinewidth)}]\tikzlastnode.north west)
|
|
975 |
edge([shift={(-0.5\pgflinewidth,-0.5\pgflinewidth)}]\tikzlastnode.north east)
|
|
976 |
([shift={(-0.5\pgflinewidth,-0.5\pgflinewidth)}]\tikzlastnode.north east)
|
|
977 |
edge([shift={(-0.5\pgflinewidth,+0.5\pgflinewidth)}]\tikzlastnode.south east)
|
|
978 |
([shift={(-0.5\pgflinewidth,+0.5\pgflinewidth)}]\tikzlastnode.south east)
|
|
979 |
edge([shift={(1.0\pgflinewidth,+0.5\pgflinewidth)}]\tikzlastnode.south west)
|
|
980 |
} |
|
981 |
} |
|
982 |
} |
|
983 |
||
984 |
\begin{figure}[H]
|
|
985 |
\begin{tikzpicture}[->, >=stealth', shorten >= 1pt, auto, thick]
|
|
986 |
\node [rectangle, draw] (r) at (-6, -1) {$(aa)^*(b+c)$};
|
|
987 |
\node [rectangle, draw] (a) at (-6, 4) {$(aa)^*(_{Z}b + _{S}c)$};
|
|
988 |
\path (r) |
|
989 |
edge [] node {$\internalise$} (a);
|
|
990 |
\node [rectangle, draw] (a1) at (-3, 1) {$(_{Z}(\ONE \cdot a) \cdot (aa)^*) (_{Z}b + _Sc)$};
|
|
991 |
\path (a) |
|
992 |
edge [] node {$\backslash a$} (a1);
|
|
993 |
||
994 |
\node [rectangle, draw, three sided] (a21) at (-2.5, 4) {$(_{Z}\ONE \cdot (aa)^*)$};
|
|
995 |
\node [rectangle, draw, three sided1] (a22) at (-0.8, 4) {$(_{Z}b + _{S}c)$};
|
|
996 |
\path (a1) |
|
997 |
edge [] node {$\backslash a$} (a21);
|
|
998 |
\node [rectangle, draw] (a3) at (0.5, 2) {$_{ZS}(_{Z}\ONE + \ZERO)$};
|
|
999 |
\path (a22) |
|
1000 |
edge [] node {$\backslash b$} (a3);
|
|
1001 |
\path (a21) |
|
1002 |
edge [dashed, bend right] node {} (a3);
|
|
1003 |
\node [rectangle, draw] (bs) at (2, 4) {$ZSZ$};
|
|
1004 |
\path (a3) |
|
1005 |
edge [below] node {$\bmkeps$} (bs);
|
|
1006 |
\node [rectangle, draw] (v) at (3, 0) {$\Seq \; (\Stars\; [\Seq \; a \; a]) \; (\Left \; b)$};
|
|
1007 |
\path (bs) |
|
1008 |
edge [] node {$\decode$} (v);
|
|
1009 |
||
1010 |
||
1011 |
\end{tikzpicture}
|
|
| 638 | 1012 |
\caption{$\blexer$ with the regular expression $(aa)^*(b+c)$ and $aab$}
|
| 581 | 1013 |
\end{figure}
|
| 537 | 1014 |
\noindent |
| 581 | 1015 |
The one dashed arrow indicates that $_Z(\ONE \cdot (aa)^*)$ |
1016 |
turned into $ZS$ after derivative w.r.t $b$ |
|
| 638 | 1017 |
is taken, which calls $\bmkeps$ on the nullable $_Z\ONE\cdot (aa)^*$ |
1018 |
before processing $_Zb+_Sc$. |
|
1019 |
||
| 581 | 1020 |
The annotated regular expressions |
| 624 | 1021 |
would look overwhelming if we explicitly indicate all the |
| 581 | 1022 |
locations where bitcodes are attached. |
1023 |
For example, |
|
1024 |
$(aa)^*\cdot (b+c)$ would |
|
1025 |
look like $_{[]}(_{[]}(_{[]}a \cdot _{[]}a)^*\cdot _{[]}(_{[]}b+_{[]}c))$
|
|
1026 |
after |
|
1027 |
internalise. |
|
1028 |
Therefore for readability we omit bitcodes if they are empty. |
|
| 624 | 1029 |
This applies to all annotated |
| 638 | 1030 |
regular expressions in this thesis. |
1031 |
||
| 581 | 1032 |
%and assume we have just read the first character $a$: |
1033 |
%\begin{center}
|
|
1034 |
%\begin{tikzpicture}[every node/.append style={draw, rounded corners, inner sep=10pt}]
|
|
1035 |
% \node [rectangle split, rectangle split horizontal, rectangle split parts=2, rectangle split part fill={red!30,blue!20},]
|
|
1036 |
% {$(_{[Z]}(\ONE \cdot a) \cdot (aa)^* )\cdot bc$
|
|
1037 |
% \nodepart{two} $[Z] \iff \Seq \; (\Stars \; [\Seq\; a \; ??, \;??]) \; ??$};
|
|
1038 |
%\end{tikzpicture}
|
|
1039 |
%\end{center}
|
|
1040 |
%\noindent |
|
1041 |
%We use the red area for (annotated) regular expressions and the blue |
|
1042 |
%area the (partially calculated) bitcodes |
|
1043 |
%and its corresponding (partial) values. |
|
1044 |
%The first derivative |
|
1045 |
%generates a $Z$ bitcode to indicate |
|
1046 |
%a new iteration has been started. |
|
1047 |
%This bitcode is attached to the front of |
|
1048 |
%the unrolled star iteration $\ONE\cdot a$ |
|
1049 |
%for later decoding. |
|
1050 |
%\begin{center}
|
|
1051 |
%\begin{tikzpicture}[]
|
|
1052 |
% \node [rectangle split, rectangle split horizontal, |
|
1053 |
% rectangle split parts=2, rectangle split part fill={red!30,blue!20}, draw, rounded corners, inner sep=10pt]
|
|
1054 |
% (der2) at (0,0) |
|
1055 |
% {$(_{[Z]}(\ONE \cdot \ONE) \cdot (aa)^*) \cdot bc $
|
|
1056 |
% \nodepart{two} $[Z] \iff \Seq \; (\Stars \; [\Seq \; a\;a, ??]) \; ??$};
|
|
1057 |
% |
|
1058 |
%\node [draw=none, minimum size = 0.1, ] (r) at (-7, 0) {$a_1$};
|
|
1059 |
%\path |
|
1060 |
% (r) |
|
1061 |
% edge [->, >=stealth',shorten >=1pt, above] node {$\backslash a$} (der2);
|
|
1062 |
%%\caption{term 1 \ref{term:1}'s matching configuration}
|
|
1063 |
%\end{tikzpicture}
|
|
1064 |
%\end{center}
|
|
1065 |
%\noindent |
|
1066 |
%After we take derivative with respect to |
|
1067 |
%second input character $a$, the annotated |
|
1068 |
%regular expression has the second $a$ chopped off. |
|
1069 |
%The second derivative does not involve any |
|
1070 |
%new bitcodes being generated, because |
|
1071 |
%there are no new iterations or bifurcations |
|
1072 |
%in the regular expression requiring any $S$ or $Z$ marker |
|
1073 |
%to indicate choices. |
|
1074 |
%\begin{center}
|
|
1075 |
%\begin{tikzpicture}[every node/.append style={draw, rounded corners, inner sep=10pt}]
|
|
1076 |
% \node [rectangle split, rectangle split horizontal, rectangle split parts=2, rectangle split part fill={red!30,blue!20},]
|
|
1077 |
% {$(_{[Z]}(\ONE \cdot \ONE) \cdot (aa)^*) \cdot (\ONE \cdot c) $
|
|
1078 |
% \nodepart{two} $[Z] \iff \Seq \; (\Stars \; [\Seq \; a\;a, ??]) \; ??$};
|
|
1079 |
%%\caption{term 1 \ref{term:1}'s matching configuration}
|
|
1080 |
%\end{tikzpicture}
|
|
1081 |
%\end{center}
|
|
1082 |
%\noindent |
|
1083 |
% |
|
1084 |
% |
|
1085 |
%\begin{center}
|
|
1086 |
%\begin{tikzpicture}[every node/.append style={draw, rounded corners, inner sep=10pt}]
|
|
1087 |
% \node [rectangle split, rectangle split horizontal, rectangle split parts=2, rectangle split part fill={red!30,blue!20},]
|
|
1088 |
% {$\stackrel{Bitcoded}{\longrightarrow} \Seq(\Stars[\Char(a), \Char(a)], ???)$
|
|
1089 |
% \nodepart{two} $\Seq(\ldots, \Seq(\Char(b), \Char(c)))$ $\stackrel{Inj}{\longleftarrow}$};
|
|
1090 |
%%\caption{term 1 \ref{term:1}'s matching configuration}
|
|
1091 |
%\end{tikzpicture}
|
|
1092 |
%\end{center}
|
|
1093 |
%\noindent |
|
1094 |
%If we do this kind of "attachment" |
|
1095 |
%and each time augment the attached partially |
|
1096 |
%constructed value when taking off a |
|
1097 |
%character: |
|
1098 |
%\begin{center}
|
|
1099 |
%\begin{tikzpicture}[every node/.append style={draw, rounded corners, inner sep=10pt}]
|
|
1100 |
% \node [rectangle split, rectangle split horizontal, rectangle split parts=2, rectangle split part fill={red!30,blue!20},] (spPoint)
|
|
1101 |
% {$\Seq(\Stars[\Char(a), \Char(a)], \ldots)$
|
|
1102 |
% \nodepart{two} Remaining: $b c$};
|
|
1103 |
%\end{tikzpicture}\\
|
|
1104 |
%$\downarrow$\\ |
|
1105 |
%\begin{tikzpicture}[every node/.append style={draw, rounded corners, inner sep=10pt}]
|
|
1106 |
% \node [rectangle split, rectangle split horizontal, rectangle split parts=2, rectangle split part fill={red!30,blue!20},]
|
|
1107 |
% {$\Seq(\Stars[\Char(a), \Char(a)], \Seq(\Char(b), \ldots))$
|
|
1108 |
% \nodepart{two} Remaining: $c$};
|
|
1109 |
%\end{tikzpicture}\\
|
|
1110 |
%$\downarrow$\\ |
|
1111 |
%\begin{tikzpicture}[every node/.append style={draw, rounded corners, inner sep=10pt}]
|
|
1112 |
% \node [rectangle split, rectangle split horizontal, rectangle split parts=2, rectangle split part fill={red!30,blue!20},]
|
|
1113 |
% {$\Seq(\Stars[\Char(a), \Char(a)], \Seq(\Char(b), \Char(c)))$
|
|
1114 |
% \nodepart{two} EOF};
|
|
1115 |
%\end{tikzpicture}
|
|
1116 |
%\end{center}
|
|
| 638 | 1117 |
|
| 581 | 1118 |
In the next section we introduce the correctness proof |
1119 |
found by Ausaf and Urban |
|
1120 |
of the bitcoded lexer. |
|
| 532 | 1121 |
%----------------------------------- |
1122 |
% SUBSECTION 1 |
|
1123 |
%----------------------------------- |
|
| 667 | 1124 |
\section{Correctness Proof of $\textit{Blexer}$}\label{blexerProof}
|
| 581 | 1125 |
Why is $\blexer$ correct? |
1126 |
In other words, why is it the case that |
|
1127 |
$\blexer$ outputs the same value as $\lexer$? |
|
1128 |
Intuitively, |
|
1129 |
that is because |
|
1130 |
\begin{itemize}
|
|
1131 |
\item |
|
1132 |
$\blexer$ follows an almost identical |
|
1133 |
path as that of $\lexer$, |
|
1134 |
for example $r_1, r_2, \ldots$ and $a_1, a_2, \ldots$ being produced, |
|
1135 |
which are the same up to the application of $\erase$. |
|
1136 |
\item |
|
1137 |
The bit-encodings work properly, |
|
1138 |
allowing the possibility of |
|
1139 |
pulling out the right lexical value from an |
|
1140 |
annotated regular expression at |
|
| 624 | 1141 |
any stage, using $\bmkeps$ or $\retrieve$ (details in |
1142 |
lemmas \ref{bmkepsRetrieve} and \ref{blexer_retrieve}).
|
|
| 581 | 1143 |
\end{itemize}
|
1144 |
We will elaborate on this, with the help of |
|
1145 |
some helper functions such as $\retrieve$ and |
|
1146 |
$\flex$. |
|
1147 |
\subsection{Specifications of Some Helper Functions}
|
|
| 622 | 1148 |
The functions we introduce will give a more detailed view into |
|
640
bd1354127574
more proofreading done, last version before submission
Chengsong
parents:
639
diff
changeset
|
1149 |
the lexing process, which is not possible |
| 581 | 1150 |
using $\lexer$ or $\blexer$ alone. |
1151 |
\subsubsection{$\textit{Retrieve}$}
|
|
1152 |
The first function we shall introduce is $\retrieve$. |
|
1153 |
Sulzmann and Lu gave its definition, and |
|
| 638 | 1154 |
Ausaf and Urban found it |
| 624 | 1155 |
useful in their mechanised proofs. |
| 581 | 1156 |
Our bit-coded lexer ``retrieve''s the bitcodes using $\bmkeps$, |
| 624 | 1157 |
after all the derivatives have been taken: |
| 532 | 1158 |
\begin{center}
|
| 542 | 1159 |
\begin{tabular}{lcl}
|
1160 |
& & $\ldots$\\ |
|
1161 |
& & $\;\;\textit{if}\; \textit{bnullable}(a)$\\
|
|
1162 |
& & $\;\;\textit{then}\;\textit{decode}\,(\textit{bmkeps}\,a)\,r$\\
|
|
1163 |
& & $\ldots$ |
|
| 532 | 1164 |
\end{tabular}
|
1165 |
\end{center}
|
|
| 542 | 1166 |
\noindent |
| 624 | 1167 |
The function $\bmkeps$ retrieves the value $v$'s |
| 581 | 1168 |
information in the format |
1169 |
of bitcodes, by travelling along the |
|
1170 |
path of the regular expression that corresponds to a POSIX match, |
|
1171 |
collecting all the bitcodes. |
|
| 542 | 1172 |
We know that this "retrieved" bitcode leads to the correct value after decoding, |
| 624 | 1173 |
which is $v_0$ in the injection-based lexing diagram: |
| 542 | 1174 |
\vspace{20mm}
|
| 581 | 1175 |
\begin{figure}[H]%\label{graph:injLexer}
|
1176 |
\begin{center}
|
|
| 542 | 1177 |
\begin{tikzcd}[
|
1178 |
every matrix/.append style = {name=p},
|
|
1179 |
remember picture, overlay, |
|
1180 |
] |
|
1181 |
a_0 \arrow[r, "\backslash c_0"] \arrow[d] & a_1 \arrow[r, "\backslash c_1"] \arrow[d] & a_2 \arrow[r, dashed] \arrow[d] & a_n \arrow[d] \\ |
|
1182 |
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]
|
|
1183 |
\end{tikzcd}
|
|
| 581 | 1184 |
\end{center}
|
| 542 | 1185 |
\begin{tikzpicture}[
|
1186 |
remember picture, overlay, |
|
1187 |
E/.style = {ellipse, draw=blue, dashed,
|
|
1188 |
inner xsep=4mm,inner ysep=-4mm, rotate=90, fit=#1} |
|
1189 |
] |
|
1190 |
\node[E = (p-1-1) (p-2-1)] {};
|
|
1191 |
\node[E = (p-1-4) (p-2-4)] {};
|
|
| 581 | 1192 |
\node[E = (p-1-2) (p-2-2)] {};
|
1193 |
\node[E = (p-1-3) (p-2-3)] {};
|
|
| 542 | 1194 |
\end{tikzpicture}
|
| 624 | 1195 |
\caption{Injection-based lexing diagram,
|
1196 |
with matching value and regular expression pairs |
|
1197 |
encircled}\label{Inj2}
|
|
| 581 | 1198 |
\end{figure}
|
| 542 | 1199 |
\vspace{20mm}
|
1200 |
\noindent |
|
| 624 | 1201 |
We have that $\vdash v_i:(a_i)_\downarrow$, |
1202 |
where $v_i$ are the intermediate values generated step by step in $\lexer$. |
|
1203 |
These values are not explicitly created in $\blexer$. |
|
1204 |
||
1205 |
We encircled in the diagram all the pairs $v_i, a_i$ to show that these values |
|
| 582 | 1206 |
and regular expressions share the same structure. |
1207 |
These pairs all contain adequate information to |
|
1208 |
obtain the final lexing result. |
|
1209 |
For example, in the leftmost pair the |
|
| 581 | 1210 |
lexical information is condensed in |
| 582 | 1211 |
$v_0$, whereas for the rightmost pair, |
| 638 | 1212 |
the lexing result hides is in the bitcodes of $a_n$. |
1213 |
||
| 624 | 1214 |
The function $\bmkeps$ is able to extract from $a_n$ the result |
| 582 | 1215 |
by looking for nullable parts of the regular expression. |
1216 |
However for regular expressions $a_i$ in general, |
|
1217 |
they might not necessarily be nullable. |
|
1218 |
For those regular expressions that are not nullable, |
|
1219 |
$\bmkeps$ will not work. |
|
1220 |
Therefore they need some additional ``help'' |
|
1221 |
finding the POSIX bit-encoding. |
|
| 581 | 1222 |
The most straightforward ``help'' comes from $a_i$'s corresponding |
1223 |
value $v_i$, and this suggests a function $f$ satisfying the |
|
1224 |
following properties: |
|
| 542 | 1225 |
\begin{itemize}
|
1226 |
\item |
|
| 581 | 1227 |
$f \; a_i\;v_i = f \; a_n \; v_n = \bmkeps \; a_n$%\decode \; (\bmkeps \; a_n) \; (\erase \; a_0)$ |
| 542 | 1228 |
\item |
| 582 | 1229 |
$f \; a_i\;v_i = f \; a_0 \; v_0 = \code \; v_0$ %\decode \;(\code \; v_0) \; (\erase \; a_0)$ |
| 542 | 1230 |
\end{itemize}
|
1231 |
\noindent |
|
| 624 | 1232 |
Sulzmann and Lu came up with the following definition for $f$ satisfying |
| 582 | 1233 |
the above |
| 624 | 1234 |
requirements, and named it \emph{retrieve}:
|
1235 |
\vspace{-7mm}
|
|
| 542 | 1236 |
\begin{center}
|
| 582 | 1237 |
\begin{tabular}{llcl}
|
1238 |
$\retrieve \; \, _{bs} \ONE$ & $ \Empty$ & $\dn$ & $\textit{bs}$\\
|
|
1239 |
||
1240 |
$\retrieve \; \, _{bs} \mathbf{c}$ & $ (\Char \; c) $ & $\dn$ & $ \textit{bs}$\\
|
|
1241 |
||
1242 |
$\retrieve \; \, _{bs} a_1 \cdot a_2$ & $ (\Seq \; v_1 \; v_2) $ &
|
|
1243 |
$\dn$ & $\textit{bs} \; @\; (\retrieve \; a_1\; v_1)\; @ \;(\retrieve \; a_2 \; v_2)$\\
|
|
1244 |
||
1245 |
$\retrieve \; \, _{bs} \Sigma (a :: \textit{as})$ & $ (\Left \; v) $ &
|
|
1246 |
$\dn$ & $\textit{bs}\; @\; (\retrieve \; a \; v)$\\
|
|
1247 |
||
1248 |
$\retrieve \; \, _{bs} \Sigma (a :: \textit{as})$ & $ (\Right \; v) $ &
|
|
1249 |
$\dn$ & $\textit{bs}\; @\; (\retrieve \; (_{[]}\Sigma \textit{as}) \; v)$\\
|
|
1250 |
||
1251 |
$\retrieve \; \, _{bs} a^* $ & $ (\Stars \; (v :: vs)) $ & $\dn$ &
|
|
| 585 | 1252 |
$\textit{bs}\; @\; [Z] \; @ \; (\retrieve \; a \; v)\; @ \;
|
| 582 | 1253 |
(\retrieve \; (_{[]} a^*) \; (\Stars \; vs) )$\\
|
1254 |
||
| 585 | 1255 |
$\retrieve \; \, _{bs} a^* $ & $ (\Stars \; []) $ & $\dn$ & $\textit{bs} \; @ \; [S]$
|
| 542 | 1256 |
\end{tabular}
|
1257 |
\end{center}
|
|
1258 |
\noindent |
|
| 624 | 1259 |
As stated, $\retrieve$ collects the right bit-codes from the |
1260 |
final derivative $a_n$, guided by $v_n$. This can be proved |
|
1261 |
as follows: |
|
| 582 | 1262 |
\begin{lemma}\label{bmkepsRetrieve}
|
|
657
00171b627b8d
Fixed some annotated/unannotated a/r notation inconsistencies.
Chengsong
parents:
653
diff
changeset
|
1263 |
\mbox{}
|
|
00171b627b8d
Fixed some annotated/unannotated a/r notation inconsistencies.
Chengsong
parents:
653
diff
changeset
|
1264 |
\begin{itemize}
|
|
00171b627b8d
Fixed some annotated/unannotated a/r notation inconsistencies.
Chengsong
parents:
653
diff
changeset
|
1265 |
\item |
|
00171b627b8d
Fixed some annotated/unannotated a/r notation inconsistencies.
Chengsong
parents:
653
diff
changeset
|
1266 |
If $\forall v \in vs. \vdash v : r$, and $\code \; v = \retrieve \; (\internalise\; r) \; v$\\ |
|
00171b627b8d
Fixed some annotated/unannotated a/r notation inconsistencies.
Chengsong
parents:
653
diff
changeset
|
1267 |
then $\code \; (\Stars \; vs) = \retrieve \; _{[]}((\internalise \; r)^*) \; (\Stars \; vs)$
|
|
00171b627b8d
Fixed some annotated/unannotated a/r notation inconsistencies.
Chengsong
parents:
653
diff
changeset
|
1268 |
\item |
|
00171b627b8d
Fixed some annotated/unannotated a/r notation inconsistencies.
Chengsong
parents:
653
diff
changeset
|
1269 |
$\vdash v : r \implies \retrieve \; (r)^\uparrow \; v = \code \; v$ |
|
00171b627b8d
Fixed some annotated/unannotated a/r notation inconsistencies.
Chengsong
parents:
653
diff
changeset
|
1270 |
\item |
|
00171b627b8d
Fixed some annotated/unannotated a/r notation inconsistencies.
Chengsong
parents:
653
diff
changeset
|
1271 |
$\bnullable \; a \implies \bmkeps \; a = \retrieve \; a \; (\mkeps \; (a_\downarrow))$ |
|
00171b627b8d
Fixed some annotated/unannotated a/r notation inconsistencies.
Chengsong
parents:
653
diff
changeset
|
1272 |
\end{itemize}
|
|
00171b627b8d
Fixed some annotated/unannotated a/r notation inconsistencies.
Chengsong
parents:
653
diff
changeset
|
1273 |
\begin{proof}
|
|
00171b627b8d
Fixed some annotated/unannotated a/r notation inconsistencies.
Chengsong
parents:
653
diff
changeset
|
1274 |
The first part is by induction on the value list $vs$. |
|
00171b627b8d
Fixed some annotated/unannotated a/r notation inconsistencies.
Chengsong
parents:
653
diff
changeset
|
1275 |
The second part is by induction on $r$, |
|
00171b627b8d
Fixed some annotated/unannotated a/r notation inconsistencies.
Chengsong
parents:
653
diff
changeset
|
1276 |
and the star case uses the first part. |
|
00171b627b8d
Fixed some annotated/unannotated a/r notation inconsistencies.
Chengsong
parents:
653
diff
changeset
|
1277 |
The last part is by a routine induction on $a$. |
|
00171b627b8d
Fixed some annotated/unannotated a/r notation inconsistencies.
Chengsong
parents:
653
diff
changeset
|
1278 |
\end{proof}
|
|
00171b627b8d
Fixed some annotated/unannotated a/r notation inconsistencies.
Chengsong
parents:
653
diff
changeset
|
1279 |
\noindent |
| 542 | 1280 |
\end{lemma}
|
1281 |
\begin{proof}
|
|
1282 |
By a routine induction on $a$. |
|
1283 |
\end{proof}
|
|
| 582 | 1284 |
\noindent |
| 624 | 1285 |
%The design of $\retrieve$ enables us to extract bitcodes |
1286 |
%from both annotated regular expressions and values. |
|
1287 |
%$\retrieve$ always ``sucks up'' all the information. |
|
|
657
00171b627b8d
Fixed some annotated/unannotated a/r notation inconsistencies.
Chengsong
parents:
653
diff
changeset
|
1288 |
%When more information is stored in the value, we would be able to |
|
00171b627b8d
Fixed some annotated/unannotated a/r notation inconsistencies.
Chengsong
parents:
653
diff
changeset
|
1289 |
%extract more from the value, and vice versa. |
|
00171b627b8d
Fixed some annotated/unannotated a/r notation inconsistencies.
Chengsong
parents:
653
diff
changeset
|
1290 |
%For example in star iterations, $\retrieve$ will be able to extract from $\Stars \; vs$ |
|
00171b627b8d
Fixed some annotated/unannotated a/r notation inconsistencies.
Chengsong
parents:
653
diff
changeset
|
1291 |
%exactly the same bitcodes as $\code \; (\Stars \; vs)$: |
|
00171b627b8d
Fixed some annotated/unannotated a/r notation inconsistencies.
Chengsong
parents:
653
diff
changeset
|
1292 |
%\begin{lemma}\label{retrieveEncodeSTARS}
|
|
00171b627b8d
Fixed some annotated/unannotated a/r notation inconsistencies.
Chengsong
parents:
653
diff
changeset
|
1293 |
% If $\forall v \in vs. \vdash v : r$, and $\code \; v = \retrieve \; (\internalise\; r) \; v$\\ |
|
00171b627b8d
Fixed some annotated/unannotated a/r notation inconsistencies.
Chengsong
parents:
653
diff
changeset
|
1294 |
% then $\code \; (\Stars \; vs) = \retrieve \; _{[]}((\internalise \; r)^*) \; (\Stars \; vs)$
|
|
00171b627b8d
Fixed some annotated/unannotated a/r notation inconsistencies.
Chengsong
parents:
653
diff
changeset
|
1295 |
%\end{lemma}
|
|
00171b627b8d
Fixed some annotated/unannotated a/r notation inconsistencies.
Chengsong
parents:
653
diff
changeset
|
1296 |
%\begin{proof}
|
|
00171b627b8d
Fixed some annotated/unannotated a/r notation inconsistencies.
Chengsong
parents:
653
diff
changeset
|
1297 |
% By induction on the value list $vs$. |
|
00171b627b8d
Fixed some annotated/unannotated a/r notation inconsistencies.
Chengsong
parents:
653
diff
changeset
|
1298 |
%\end{proof}
|
|
00171b627b8d
Fixed some annotated/unannotated a/r notation inconsistencies.
Chengsong
parents:
653
diff
changeset
|
1299 |
%\noindent |
|
00171b627b8d
Fixed some annotated/unannotated a/r notation inconsistencies.
Chengsong
parents:
653
diff
changeset
|
1300 |
%Similarly, when the value list does not hold information, |
|
00171b627b8d
Fixed some annotated/unannotated a/r notation inconsistencies.
Chengsong
parents:
653
diff
changeset
|
1301 |
%only the bitcodes plus some delimiter will be recorded: |
|
00171b627b8d
Fixed some annotated/unannotated a/r notation inconsistencies.
Chengsong
parents:
653
diff
changeset
|
1302 |
%\begin{center}
|
|
00171b627b8d
Fixed some annotated/unannotated a/r notation inconsistencies.
Chengsong
parents:
653
diff
changeset
|
1303 |
% $\retrieve \; _{bs}((\internalise \; r)^*) \; (\Stars \; [] ) = bs @ [S]$.
|
|
00171b627b8d
Fixed some annotated/unannotated a/r notation inconsistencies.
Chengsong
parents:
653
diff
changeset
|
1304 |
%\end{center}
|
|
00171b627b8d
Fixed some annotated/unannotated a/r notation inconsistencies.
Chengsong
parents:
653
diff
changeset
|
1305 |
%In general, if we have a regular expression that is just internalised |
|
00171b627b8d
Fixed some annotated/unannotated a/r notation inconsistencies.
Chengsong
parents:
653
diff
changeset
|
1306 |
%and the final lexing result value, we can $\retrieve$ the bitcodes |
|
00171b627b8d
Fixed some annotated/unannotated a/r notation inconsistencies.
Chengsong
parents:
653
diff
changeset
|
1307 |
%that look as if we have en$\code$-ed the value as bitcodes: |
|
00171b627b8d
Fixed some annotated/unannotated a/r notation inconsistencies.
Chengsong
parents:
653
diff
changeset
|
1308 |
%\begin{lemma}
|
|
00171b627b8d
Fixed some annotated/unannotated a/r notation inconsistencies.
Chengsong
parents:
653
diff
changeset
|
1309 |
% $\vdash v : r \implies \retrieve \; (r)^\uparrow \; v = \code \; v$ |
|
00171b627b8d
Fixed some annotated/unannotated a/r notation inconsistencies.
Chengsong
parents:
653
diff
changeset
|
1310 |
%\end{lemma}
|
|
00171b627b8d
Fixed some annotated/unannotated a/r notation inconsistencies.
Chengsong
parents:
653
diff
changeset
|
1311 |
%\begin{proof}
|
|
00171b627b8d
Fixed some annotated/unannotated a/r notation inconsistencies.
Chengsong
parents:
653
diff
changeset
|
1312 |
% By induction on $r$. |
|
00171b627b8d
Fixed some annotated/unannotated a/r notation inconsistencies.
Chengsong
parents:
653
diff
changeset
|
1313 |
% The star case uses lemma \ref{retrieveEncodeSTARS}.
|
|
00171b627b8d
Fixed some annotated/unannotated a/r notation inconsistencies.
Chengsong
parents:
653
diff
changeset
|
1314 |
%\end{proof}
|
|
00171b627b8d
Fixed some annotated/unannotated a/r notation inconsistencies.
Chengsong
parents:
653
diff
changeset
|
1315 |
%\noindent |
| 624 | 1316 |
The following property of $\retrieve$ is crucial, as |
| 582 | 1317 |
it provides a "bridge" between $a_0$ and $a_n $ in the |
1318 |
lexing diagram by linking adjacent regular expressions $a_i$ and |
|
1319 |
$a_{i+1}$.
|
|
1320 |
The property says that one |
|
1321 |
can retrieve the same bits from a derivative |
|
1322 |
regular expression as those from |
|
1323 |
before the derivative took place, |
|
| 624 | 1324 |
provided that the corresponding values are used respectively: |
| 542 | 1325 |
\begin{lemma}\label{retrieveStepwise}
|
|
657
00171b627b8d
Fixed some annotated/unannotated a/r notation inconsistencies.
Chengsong
parents:
653
diff
changeset
|
1326 |
$\vdash v : (a\backslash c)_\downarrow \implies \retrieve \; (a \backslash c) \; v= |
|
00171b627b8d
Fixed some annotated/unannotated a/r notation inconsistencies.
Chengsong
parents:
653
diff
changeset
|
1327 |
\retrieve \; a \; (\inj \; a_\downarrow\; c\; v)$ |
| 542 | 1328 |
\end{lemma}
|
1329 |
\begin{proof}
|
|
|
640
bd1354127574
more proofreading done, last version before submission
Chengsong
parents:
639
diff
changeset
|
1330 |
We do an induction on $r$, generalising over $v$. |
| 624 | 1331 |
The induction principle in our formalisation |
1332 |
is function $\erase$'s cases. |
|
| 542 | 1333 |
\end{proof}
|
1334 |
\noindent |
|
| 649 | 1335 |
Intuitively the lemma can be understood as all lexical value |
1336 |
information being preserved and recoverable throughout each lexing step. |
|
1337 |
We shall see in the next chapter that this no longer |
|
1338 |
holds with simplifications which takes away certain sub-expressions |
|
1339 |
corresponding to non-POSIX lexical values. |
|
1340 |
||
|
657
00171b627b8d
Fixed some annotated/unannotated a/r notation inconsistencies.
Chengsong
parents:
653
diff
changeset
|
1341 |
%Before we move on to the next |
|
00171b627b8d
Fixed some annotated/unannotated a/r notation inconsistencies.
Chengsong
parents:
653
diff
changeset
|
1342 |
%helper function, we rewrite $\blexer$ in |
|
00171b627b8d
Fixed some annotated/unannotated a/r notation inconsistencies.
Chengsong
parents:
653
diff
changeset
|
1343 |
%the following way which makes later proofs more convenient: |
|
00171b627b8d
Fixed some annotated/unannotated a/r notation inconsistencies.
Chengsong
parents:
653
diff
changeset
|
1344 |
%\begin{lemma}\label{blexer_retrieve}
|
|
00171b627b8d
Fixed some annotated/unannotated a/r notation inconsistencies.
Chengsong
parents:
653
diff
changeset
|
1345 |
%$\blexer \; r \; s = \decode \; (\retrieve \; (\internalise \; r) \; (\mkeps \; (r \backslash s) )) \; r$ |
|
00171b627b8d
Fixed some annotated/unannotated a/r notation inconsistencies.
Chengsong
parents:
653
diff
changeset
|
1346 |
%\end{lemma}
|
|
00171b627b8d
Fixed some annotated/unannotated a/r notation inconsistencies.
Chengsong
parents:
653
diff
changeset
|
1347 |
%\begin{proof}
|
|
00171b627b8d
Fixed some annotated/unannotated a/r notation inconsistencies.
Chengsong
parents:
653
diff
changeset
|
1348 |
% Using lemma \ref{bmkepsRetrieve}.
|
|
00171b627b8d
Fixed some annotated/unannotated a/r notation inconsistencies.
Chengsong
parents:
653
diff
changeset
|
1349 |
%\end{proof}
|
|
00171b627b8d
Fixed some annotated/unannotated a/r notation inconsistencies.
Chengsong
parents:
653
diff
changeset
|
1350 |
%\noindent |
| 624 | 1351 |
The function $\retrieve$ allows connecting |
| 582 | 1352 |
between the intermediate |
1353 |
results $a_i$ and $a_{i+1}$ in $\blexer$.
|
|
1354 |
For plain regular expressions something similar is required. |
|
| 542 | 1355 |
|
| 638 | 1356 |
\subsection{The Function $\flex$}
|
| 624 | 1357 |
Ausaf and Urban defined an auxiliary function called $\flex$ for $\lexer$, |
| 532 | 1358 |
defined as |
| 536 | 1359 |
\begin{center}
|
| 582 | 1360 |
\begin{tabular}{lcl}
|
| 536 | 1361 |
$\flex \; r \; f \; [] \; v$ & $=$ & $f\; v$\\ |
| 582 | 1362 |
$\flex \; r \; f \; (c :: s) \; v$ & $=$ & $\flex \; r \; (\lambda v. \, f (\inj \; r\; c\; v)) \;\; s \; v$ |
| 536 | 1363 |
\end{tabular}
|
1364 |
\end{center}
|
|
| 582 | 1365 |
which accumulates the characters that need to be injected back, |
|
640
bd1354127574
more proofreading done, last version before submission
Chengsong
parents:
639
diff
changeset
|
1366 |
and does the injection in a stack-like manner (the last character being chopped off in the derivatives phase is first injected). |
| 624 | 1367 |
The function |
| 582 | 1368 |
$\flex$ can calculate what $\lexer$ calculates, given the input regular expression |
1369 |
$r$, the identity function $id$, the input string $s$ and the value |
|
1370 |
$v_n= \mkeps \; (r\backslash s)$: |
|
| 532 | 1371 |
\begin{lemma}
|
| 582 | 1372 |
$\flex \;\; r \;\; \textit{id}\;\; s \;\; (\mkeps \;(r\backslash s)) = \lexer \; r \; s$
|
| 532 | 1373 |
\end{lemma}
|
| 542 | 1374 |
\begin{proof}
|
1375 |
By reverse induction on $s$. |
|
1376 |
\end{proof}
|
|
| 582 | 1377 |
\noindent |
1378 |
The main advantage of using $\flex$ |
|
| 624 | 1379 |
in $\lexer$ is that |
| 582 | 1380 |
$\flex$ makes the value $v$ and function $f$ |
1381 |
that manipulates the value explicit parameters, |
|
1382 |
which ``exposes'' $\lexer$'s recursive call |
|
1383 |
arguments and allows us to ``set breakpoints'' and ``resume'' |
|
| 624 | 1384 |
at any point during $\lexer$'s recursive calls. Therefore |
1385 |
the following stepwise property holds. |
|
| 532 | 1386 |
\begin{lemma}\label{flexStepwise}
|
| 582 | 1387 |
$\textit{flex} \;\; r \;\; f \;\; (s@[c]) \;\; v = \flex \;\; r \;\; f \;\; s \;\; (\inj \; (r\backslash s) \; c \; v) $
|
| 532 | 1388 |
\end{lemma}
|
1389 |
\begin{proof}
|
|
| 582 | 1390 |
By induction on the shape of $r\backslash s$. |
| 532 | 1391 |
\end{proof}
|
| 582 | 1392 |
\noindent |
1393 |
With $\flex$ and $\retrieve$, |
|
1394 |
we are ready to connect $\lexer$ and $\blexer$, |
|
| 624 | 1395 |
giving the correctness proof for $\blexer$. |
| 532 | 1396 |
|
| 542 | 1397 |
%---------------------------------------------------------------------------------------- |
1398 |
% SECTION correctness proof |
|
1399 |
%---------------------------------------------------------------------------------------- |
|
| 624 | 1400 |
\section{Correctness of the Bit-coded Algorithm (Without Simplification)}
|
1401 |
We can first show that |
|
| 638 | 1402 |
$\flex$ and $\blexer$ calculates the same value. |
| 582 | 1403 |
\begin{lemma}\label{flex_retrieve}
|
1404 |
If $\vdash v: (r\backslash s)$, then\\ |
|
1405 |
$\flex \; r \; \textit{id}\; s\; v = \decode \; (\retrieve \; (r\backslash s )\; v) \; r$
|
|
| 532 | 1406 |
\end{lemma}
|
1407 |
\begin{proof}
|
|
| 582 | 1408 |
By induction on $s$. |
1409 |
We prove the interesting case where |
|
1410 |
both $\flex$ and $\decode$ successfully terminates |
|
1411 |
with some value. |
|
1412 |
We take advantage of the stepwise properties |
|
1413 |
both sides. |
|
1414 |
The induction tactic is reverse induction on string $s$. |
|
1415 |
The inductive hypothesis says that $\flex \; r \; id \;s \; v = |
|
1416 |
\decode \; (\retrieve \; (r\backslash s) \; v) \; r$ holds, |
|
1417 |
where $v$ can be any value satisfying |
|
1418 |
the assumption $\vdash v: (r\backslash s)$. |
|
1419 |
The crucial point is to rewrite |
|
1420 |
\[ |
|
1421 |
\retrieve \;\; (r \backslash (s@[c])) \;\; (\mkeps\; (r \backslash (s@[c]) )) |
|
1422 |
\] |
|
1423 |
as |
|
1424 |
\[ |
|
1425 |
\retrieve \;\; (r \backslash s) |
|
1426 |
\;\; (\inj \; (r \backslash s) \; c\; \mkeps (r \backslash (s@[c]))) |
|
1427 |
\] |
|
1428 |
using lemma \ref{retrieveStepwise}.
|
|
1429 |
This enables us to equate |
|
1430 |
\[ |
|
1431 |
\retrieve \; (r \backslash (s@[c])) \; (\mkeps \; (r \backslash (s@[c]) )) |
|
1432 |
\] |
|
1433 |
with |
|
1434 |
\[ |
|
1435 |
\flex \; r \; \textit{id} \; s \; (\inj \; (r\backslash s) \; c\; (\mkeps (r\backslash s@[c])))
|
|
1436 |
\] |
|
1437 |
using IH, |
|
1438 |
which in turn can be rewritten as |
|
1439 |
\[ |
|
1440 |
\flex \; r \; \textit{id} \; (s@[c]) \; (\mkeps \; (r \backslash (s@[c])))
|
|
1441 |
\]. |
|
| 532 | 1442 |
\end{proof}
|
| 582 | 1443 |
\noindent |
1444 |
With this pivotal lemma we can now link $\flex$ and $\blexer$ |
|
1445 |
and finally give the correctness of $\blexer$--it outputs the same result as $\lexer$: |
|
| 649 | 1446 |
\begin{theorem}\label{blexerCorrect}
|
| 542 | 1447 |
$\blexer\; r \; s = \lexer \; r \; s$ |
1448 |
\end{theorem}
|
|
1449 |
\begin{proof}
|
|
|
657
00171b627b8d
Fixed some annotated/unannotated a/r notation inconsistencies.
Chengsong
parents:
653
diff
changeset
|
1450 |
We can rewrite the expression $\blexer \; r \; s$ by using lemma \ref{bmkepsRetrieve}:
|
|
00171b627b8d
Fixed some annotated/unannotated a/r notation inconsistencies.
Chengsong
parents:
653
diff
changeset
|
1451 |
\[ |
|
00171b627b8d
Fixed some annotated/unannotated a/r notation inconsistencies.
Chengsong
parents:
653
diff
changeset
|
1452 |
\blexer \; r \; s = \decode \; (\retrieve \; (\; r^\uparrow) \; (\mkeps \; (r \backslash s) )) \; r |
|
00171b627b8d
Fixed some annotated/unannotated a/r notation inconsistencies.
Chengsong
parents:
653
diff
changeset
|
1453 |
\] |
|
00171b627b8d
Fixed some annotated/unannotated a/r notation inconsistencies.
Chengsong
parents:
653
diff
changeset
|
1454 |
From \ref{flex_retrieve} we have that the left-hand-side is equal to
|
|
00171b627b8d
Fixed some annotated/unannotated a/r notation inconsistencies.
Chengsong
parents:
653
diff
changeset
|
1455 |
\[ |
|
00171b627b8d
Fixed some annotated/unannotated a/r notation inconsistencies.
Chengsong
parents:
653
diff
changeset
|
1456 |
\textit{flex} \; r \; \textit{id} \; s \; \mkeps \; (r \backslash s),
|
|
00171b627b8d
Fixed some annotated/unannotated a/r notation inconsistencies.
Chengsong
parents:
653
diff
changeset
|
1457 |
\] |
|
00171b627b8d
Fixed some annotated/unannotated a/r notation inconsistencies.
Chengsong
parents:
653
diff
changeset
|
1458 |
which in turn equals |
|
00171b627b8d
Fixed some annotated/unannotated a/r notation inconsistencies.
Chengsong
parents:
653
diff
changeset
|
1459 |
\[ |
|
00171b627b8d
Fixed some annotated/unannotated a/r notation inconsistencies.
Chengsong
parents:
653
diff
changeset
|
1460 |
\lexer \; r \; s. |
|
00171b627b8d
Fixed some annotated/unannotated a/r notation inconsistencies.
Chengsong
parents:
653
diff
changeset
|
1461 |
\] |
|
00171b627b8d
Fixed some annotated/unannotated a/r notation inconsistencies.
Chengsong
parents:
653
diff
changeset
|
1462 |
%which immediately implies this theorem. |
| 542 | 1463 |
\end{proof}
|
1464 |
\noindent |
|
|
657
00171b627b8d
Fixed some annotated/unannotated a/r notation inconsistencies.
Chengsong
parents:
653
diff
changeset
|
1465 |
To piece things together |
|
00171b627b8d
Fixed some annotated/unannotated a/r notation inconsistencies.
Chengsong
parents:
653
diff
changeset
|
1466 |
%and spell out the correctness |
|
00171b627b8d
Fixed some annotated/unannotated a/r notation inconsistencies.
Chengsong
parents:
653
diff
changeset
|
1467 |
%result of the bitcoded lexer more explicitly, |
|
00171b627b8d
Fixed some annotated/unannotated a/r notation inconsistencies.
Chengsong
parents:
653
diff
changeset
|
1468 |
and give the correctness result explicitly, |
| 576 | 1469 |
we use the fact from the previous chapter that |
1470 |
\[ |
|
| 624 | 1471 |
(r, s) \rightarrow v \;\; \textit{iff} \;\; \lexer \; r \; s =\Some \; v
|
1472 |
\quad \quad |
|
1473 |
\nexists v. (r, s) \rightarrow v\;\; \textit{iff} \;\; \lexer \;r\;s = None
|
|
| 576 | 1474 |
\] |
1475 |
to obtain this corollary: |
|
1476 |
\begin{corollary}\label{blexerPOSIX}
|
|
|
657
00171b627b8d
Fixed some annotated/unannotated a/r notation inconsistencies.
Chengsong
parents:
653
diff
changeset
|
1477 |
The $\blexer$ function correctly implements a POSIX lexer, namely |
|
00171b627b8d
Fixed some annotated/unannotated a/r notation inconsistencies.
Chengsong
parents:
653
diff
changeset
|
1478 |
\begin{itemize}
|
|
00171b627b8d
Fixed some annotated/unannotated a/r notation inconsistencies.
Chengsong
parents:
653
diff
changeset
|
1479 |
\item |
|
00171b627b8d
Fixed some annotated/unannotated a/r notation inconsistencies.
Chengsong
parents:
653
diff
changeset
|
1480 |
$(r, s) \rightarrow v \;\; \textit{iff} \;\; \blexer \; r \; s = \Some \; v$
|
|
00171b627b8d
Fixed some annotated/unannotated a/r notation inconsistencies.
Chengsong
parents:
653
diff
changeset
|
1481 |
\item |
| 624 | 1482 |
$\nexists v. (r, s) \rightarrow v\;\; \textit{iff} \;\; \blexer \;r\;s = None$
|
|
657
00171b627b8d
Fixed some annotated/unannotated a/r notation inconsistencies.
Chengsong
parents:
653
diff
changeset
|
1483 |
\end{itemize}
|
| 576 | 1484 |
\end{corollary}
|
| 624 | 1485 |
Our main reason for analysing the bit-coded algorithm over |
1486 |
the injection-based one is that it allows us to define |
|
| 542 | 1487 |
more aggressive simplifications. |
1488 |
We will elaborate on this in the next chapter. |
|
| 532 | 1489 |
|
1490 |