5 "../Simplifying" |
5 "../Simplifying" |
6 "../Positions" |
6 "../Positions" |
7 "../SizeBound4" |
7 "../SizeBound4" |
8 "HOL-Library.LaTeXsugar" |
8 "HOL-Library.LaTeXsugar" |
9 begin |
9 begin |
|
10 |
|
11 declare [[show_question_marks = false]] |
|
12 |
|
13 notation (latex output) |
|
14 If ("(\<^latex>\<open>\\textrm{\<close>if\<^latex>\<open>}\<close> (_)/ \<^latex>\<open>\\textrm{\<close>then\<^latex>\<open>}\<close> (_)/ \<^latex>\<open>\\textrm{\<close>else\<^latex>\<open>}\<close> (_))" 10) and |
|
15 Cons ("_\<^latex>\<open>\\mbox{$\\,$}\<close>::\<^latex>\<open>\\mbox{$\\,$}\<close>_" [75,73] 73) |
|
16 |
|
17 |
|
18 abbreviation |
|
19 "der_syn r c \<equiv> der c r" |
|
20 |
|
21 notation (latex output) |
|
22 der_syn ("_\\_" [79, 1000] 76) and |
|
23 |
|
24 ZERO ("\<^bold>0" 81) and |
|
25 ONE ("\<^bold>1" 81) and |
|
26 CH ("_" [1000] 80) and |
|
27 ALT ("_ + _" [77,77] 78) and |
|
28 SEQ ("_ \<cdot> _" [77,77] 78) and |
|
29 STAR ("_\<^sup>\<star>" [79] 78) and |
|
30 |
|
31 val.Void ("Empty" 78) and |
|
32 val.Char ("Char _" [1000] 78) and |
|
33 val.Left ("Left _" [79] 78) and |
|
34 val.Right ("Right _" [1000] 78) and |
|
35 val.Seq ("Seq _ _" [79,79] 78) and |
|
36 val.Stars ("Stars _" [79] 78) and |
|
37 |
|
38 Posix ("'(_, _') \<rightarrow> _" [63,75,75] 75) and |
|
39 |
|
40 flat ("|_|" [75] 74) and |
|
41 flats ("|_|" [72] 74) and |
|
42 injval ("inj _ _ _" [79,77,79] 76) and |
|
43 mkeps ("mkeps _" [79] 76) and |
|
44 length ("len _" [73] 73) and |
|
45 set ("_" [73] 73) and |
|
46 |
|
47 AZERO ("ZERO" 81) and |
|
48 AONE ("ONE _" [79] 81) and |
|
49 ACHAR ("CHAR _ _" [79, 79] 80) and |
|
50 AALTs ("ALTs _ _" [77,77] 78) and |
|
51 ASEQ ("SEQ _ _ _" [79, 77,77] 78) and |
|
52 ASTAR ("STAR _ _" [79, 79] 78) and |
|
53 |
|
54 code ("code _" [79] 74) and |
|
55 intern ("_\<^latex>\<open>\\mbox{$^\\uparrow$}\<close>" [900] 80) and |
|
56 erase ("_\<^latex>\<open>\\mbox{$^\\downarrow$}\<close>" [1000] 74) and |
|
57 bnullable ("nullable\<^latex>\<open>\\mbox{$_b$}\<close> _" [1000] 80) and |
|
58 bmkeps ("mkeps\<^latex>\<open>\\mbox{$_b$}\<close> _" [1000] 80) |
|
59 |
|
60 |
|
61 lemma better_retrieve: |
|
62 shows "rs \<noteq> Nil ==> retrieve (AALTs bs (r#rs)) (Left v) = bs @ retrieve r v" |
|
63 and "rs \<noteq> Nil ==> retrieve (AALTs bs (r#rs)) (Right v) = bs @ retrieve (AALTs [] rs) v" |
|
64 apply (metis list.exhaust retrieve.simps(4)) |
|
65 by (metis list.exhaust retrieve.simps(5)) |
|
66 |
10 (*>*) |
67 (*>*) |
|
68 |
|
69 section {* Introduction *} |
|
70 |
|
71 text {* |
|
72 |
|
73 In the last fifteen or so years, Brzozowski's derivatives of regular |
|
74 expressions have sparked quite a bit of interest in the functional |
|
75 programming and theorem prover communities. The beauty of |
|
76 Brzozowski's derivatives \cite{Brzozowski1964} is that they are neatly |
|
77 expressible in any functional language, and easily definable and |
|
78 reasoned about in theorem provers---the definitions just consist of |
|
79 inductive datatypes and simple recursive functions. A mechanised |
|
80 correctness proof of Brzozowski's matcher in for example HOL4 has been |
|
81 mentioned by Owens and Slind~\cite{Owens2008}. Another one in |
|
82 Isabelle/HOL is part of the work by Krauss and Nipkow |
|
83 \cite{Krauss2011}. And another one in Coq is given by Coquand and |
|
84 Siles \cite{Coquand2012}. |
|
85 |
|
86 |
|
87 The notion of derivatives |
|
88 \cite{Brzozowski1964}, written @{term "der c r"}, of a regular |
|
89 expression give a simple solution to the problem of matching a string |
|
90 @{term s} with a regular expression @{term r}: if the derivative of |
|
91 @{term r} w.r.t.\ (in succession) all the characters of the string |
|
92 matches the empty string, then @{term r} matches @{term s} (and {\em |
|
93 vice versa}). The derivative has the property (which may almost be |
|
94 regarded as its specification) that, for every string @{term s} and |
|
95 regular expression @{term r} and character @{term c}, one has @{term |
|
96 "cs \<in> L(r)"} if and only if \mbox{@{term "s \<in> L(der c r)"}}. |
|
97 |
|
98 |
|
99 If a regular expression matches a string, then in general there is more |
|
100 than one way of how the string is matched. There are two commonly used |
|
101 disambiguation strategies to generate a unique answer: one is called |
|
102 GREEDY matching \cite{Frisch2004} and the other is POSIX |
|
103 matching~\cite{POSIX,Kuklewicz,OkuiSuzuki2010,Sulzmann2014,Vansummeren2006}. |
|
104 For example consider the string @{term xy} and the regular expression |
|
105 \mbox{@{term "STAR (ALT (ALT x y) xy)"}}. Either the string can be |
|
106 matched in two `iterations' by the single letter-regular expressions |
|
107 @{term x} and @{term y}, or directly in one iteration by @{term xy}. The |
|
108 first case corresponds to GREEDY matching, which first matches with the |
|
109 left-most symbol and only matches the next symbol in case of a mismatch |
|
110 (this is greedy in the sense of preferring instant gratification to |
|
111 delayed repletion). The second case is POSIX matching, which prefers the |
|
112 longest match. |
|
113 |
|
114 |
|
115 \begin{center} |
|
116 \begin{tabular}{cc} |
|
117 \begin{tabular}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l} |
|
118 @{thm (lhs) der.simps(1)} & $\dn$ & @{thm (rhs) der.simps(1)}\\ |
|
119 @{thm (lhs) der.simps(2)} & $\dn$ & @{thm (rhs) der.simps(2)}\\ |
|
120 @{thm (lhs) der.simps(3)} & $\dn$ & @{thm (rhs) der.simps(3)}\\ |
|
121 @{thm (lhs) der.simps(4)[of c "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) der.simps(4)[of c "r\<^sub>1" "r\<^sub>2"]}\\ |
|
122 @{thm (lhs) der.simps(5)[of c "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{text "if"} @{term "nullable(r\<^sub>1)"}\\ |
|
123 & & @{text "then"} @{term "ALT (SEQ (der c r\<^sub>1) r\<^sub>2) (der c r\<^sub>2)"}\\ |
|
124 & & @{text "else"} @{term "SEQ (der c r\<^sub>1) r\<^sub>2"}\\ |
|
125 % & & @{thm (rhs) der.simps(5)[of c "r\<^sub>1" "r\<^sub>2"]}\\ |
|
126 @{thm (lhs) der.simps(6)} & $\dn$ & @{thm (rhs) der.simps(6)} |
|
127 \end{tabular} |
|
128 & |
|
129 \begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l} |
|
130 @{thm (lhs) nullable.simps(1)} & $\dn$ & @{thm (rhs) nullable.simps(1)}\\ |
|
131 @{thm (lhs) nullable.simps(2)} & $\dn$ & @{thm (rhs) nullable.simps(2)}\\ |
|
132 @{thm (lhs) nullable.simps(3)} & $\dn$ & @{thm (rhs) nullable.simps(3)}\\ |
|
133 @{thm (lhs) nullable.simps(4)[of "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) nullable.simps(4)[of "r\<^sub>1" "r\<^sub>2"]}\\ |
|
134 @{thm (lhs) nullable.simps(5)[of "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) nullable.simps(5)[of "r\<^sub>1" "r\<^sub>2"]}\\ |
|
135 @{thm (lhs) nullable.simps(6)} & $\dn$ & @{thm (rhs) nullable.simps(6)}\medskip\\ |
|
136 \end{tabular} |
|
137 \end{tabular} |
|
138 \end{center} |
|
139 |
|
140 |
|
141 \begin{figure}[t] |
|
142 \begin{center} |
|
143 \begin{tikzpicture}[scale=2,node distance=1.3cm, |
|
144 every node/.style={minimum size=6mm}] |
|
145 \node (r1) {@{term "r\<^sub>1"}}; |
|
146 \node (r2) [right=of r1]{@{term "r\<^sub>2"}}; |
|
147 \draw[->,line width=1mm](r1)--(r2) node[above,midway] {@{term "der a DUMMY"}}; |
|
148 \node (r3) [right=of r2]{@{term "r\<^sub>3"}}; |
|
149 \draw[->,line width=1mm](r2)--(r3) node[above,midway] {@{term "der b DUMMY"}}; |
|
150 \node (r4) [right=of r3]{@{term "r\<^sub>4"}}; |
|
151 \draw[->,line width=1mm](r3)--(r4) node[above,midway] {@{term "der c DUMMY"}}; |
|
152 \draw (r4) node[anchor=west] {\;\raisebox{3mm}{@{term nullable}}}; |
|
153 \node (v4) [below=of r4]{@{term "v\<^sub>4"}}; |
|
154 \draw[->,line width=1mm](r4) -- (v4); |
|
155 \node (v3) [left=of v4] {@{term "v\<^sub>3"}}; |
|
156 \draw[->,line width=1mm](v4)--(v3) node[below,midway] {\<open>inj r\<^sub>3 c\<close>}; |
|
157 \node (v2) [left=of v3]{@{term "v\<^sub>2"}}; |
|
158 \draw[->,line width=1mm](v3)--(v2) node[below,midway] {\<open>inj r\<^sub>2 b\<close>}; |
|
159 \node (v1) [left=of v2] {@{term "v\<^sub>1"}}; |
|
160 \draw[->,line width=1mm](v2)--(v1) node[below,midway] {\<open>inj r\<^sub>1 a\<close>}; |
|
161 \draw (r4) node[anchor=north west] {\;\raisebox{-8mm}{@{term "mkeps"}}}; |
|
162 \end{tikzpicture} |
|
163 \end{center} |
|
164 \mbox{}\\[-13mm] |
|
165 |
|
166 \caption{The two phases of the algorithm by Sulzmann \& Lu \cite{Sulzmann2014}, |
|
167 matching the string @{term "[a,b,c]"}. The first phase (the arrows from |
|
168 left to right) is \Brz's matcher building successive derivatives. If the |
|
169 last regular expression is @{term nullable}, then the functions of the |
|
170 second phase are called (the top-down and right-to-left arrows): first |
|
171 @{term mkeps} calculates a value @{term "v\<^sub>4"} witnessing |
|
172 how the empty string has been recognised by @{term "r\<^sub>4"}. After |
|
173 that the function @{term inj} ``injects back'' the characters of the string into |
|
174 the values. |
|
175 \label{Sulz}} |
|
176 \end{figure} |
|
177 |
|
178 |
|
179 *} |
|
180 |
|
181 section {* Background *} |
|
182 |
|
183 text {* |
|
184 Sulzmann-Lu algorithm with inj. State that POSIX rules. |
|
185 metion slg is correct. |
|
186 |
|
187 |
|
188 \begin{figure}[t] |
|
189 \begin{center} |
|
190 \begin{tabular}{c} |
|
191 @{thm[mode=Axiom] Posix.intros(1)}\<open>P\<close>@{term "ONE"} \qquad |
|
192 @{thm[mode=Axiom] Posix.intros(2)}\<open>P\<close>@{term "c"}\medskip\\ |
|
193 @{thm[mode=Rule] Posix.intros(3)[of "s" "r\<^sub>1" "v" "r\<^sub>2"]}\<open>P+L\<close>\qquad |
|
194 @{thm[mode=Rule] Posix.intros(4)[of "s" "r\<^sub>2" "v" "r\<^sub>1"]}\<open>P+R\<close>\medskip\\ |
|
195 $\mprset{flushleft} |
|
196 \inferrule |
|
197 {@{thm (prem 1) Posix.intros(5)[of "s\<^sub>1" "r\<^sub>1" "v\<^sub>1" "s\<^sub>2" "r\<^sub>2" "v\<^sub>2"]} \qquad |
|
198 @{thm (prem 2) Posix.intros(5)[of "s\<^sub>1" "r\<^sub>1" "v\<^sub>1" "s\<^sub>2" "r\<^sub>2" "v\<^sub>2"]} \\\\ |
|
199 @{thm (prem 3) Posix.intros(5)[of "s\<^sub>1" "r\<^sub>1" "v\<^sub>1" "s\<^sub>2" "r\<^sub>2" "v\<^sub>2"]}} |
|
200 {@{thm (concl) Posix.intros(5)[of "s\<^sub>1" "r\<^sub>1" "v\<^sub>1" "s\<^sub>2" "r\<^sub>2" "v\<^sub>2"]}}$\<open>PS\<close>\\ |
|
201 @{thm[mode=Axiom] Posix.intros(7)}\<open>P[]\<close>\medskip\\ |
|
202 $\mprset{flushleft} |
|
203 \inferrule |
|
204 {@{thm (prem 1) Posix.intros(6)[of "s\<^sub>1" "r" "v" "s\<^sub>2" "vs"]} \qquad |
|
205 @{thm (prem 2) Posix.intros(6)[of "s\<^sub>1" "r" "v" "s\<^sub>2" "vs"]} \qquad |
|
206 @{thm (prem 3) Posix.intros(6)[of "s\<^sub>1" "r" "v" "s\<^sub>2" "vs"]} \\\\ |
|
207 @{thm (prem 4) Posix.intros(6)[of "s\<^sub>1" "r" "v" "s\<^sub>2" "vs"]}} |
|
208 {@{thm (concl) Posix.intros(6)[of "s\<^sub>1" "r" "v" "s\<^sub>2" "vs"]}}$\<open>P\<star>\<close> |
|
209 \end{tabular} |
|
210 \end{center} |
|
211 \caption{Our inductive definition of POSIX values.}\label{POSIXrules} |
|
212 \end{figure} |
|
213 |
|
214 |
|
215 \begin{center} |
|
216 \begin{tabular}{lcl} |
|
217 @{thm (lhs) mkeps.simps(1)} & $\dn$ & @{thm (rhs) mkeps.simps(1)}\\ |
|
218 @{thm (lhs) mkeps.simps(2)[of "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) mkeps.simps(2)[of "r\<^sub>1" "r\<^sub>2"]}\\ |
|
219 @{thm (lhs) mkeps.simps(3)[of "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) mkeps.simps(3)[of "r\<^sub>1" "r\<^sub>2"]}\\ |
|
220 @{thm (lhs) mkeps.simps(4)} & $\dn$ & @{thm (rhs) mkeps.simps(4)}\\ |
|
221 \end{tabular} |
|
222 \end{center} |
|
223 |
|
224 \begin{center} |
|
225 \begin{tabular}{l@ {\hspace{5mm}}lcl} |
|
226 \textit{(1)} & @{thm (lhs) injval.simps(1)} & $\dn$ & @{thm (rhs) injval.simps(1)}\\ |
|
227 \textit{(2)} & @{thm (lhs) injval.simps(2)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1"]} & $\dn$ & |
|
228 @{thm (rhs) injval.simps(2)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1"]}\\ |
|
229 \textit{(3)} & @{thm (lhs) injval.simps(3)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>2"]} & $\dn$ & |
|
230 @{thm (rhs) injval.simps(3)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>2"]}\\ |
|
231 \textit{(4)} & @{thm (lhs) injval.simps(4)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1" "v\<^sub>2"]} & $\dn$ |
|
232 & @{thm (rhs) injval.simps(4)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1" "v\<^sub>2"]}\\ |
|
233 \textit{(5)} & @{thm (lhs) injval.simps(5)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1" "v\<^sub>2"]} & $\dn$ |
|
234 & @{thm (rhs) injval.simps(5)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1" "v\<^sub>2"]}\\ |
|
235 \textit{(6)} & @{thm (lhs) injval.simps(6)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>2"]} & $\dn$ |
|
236 & @{thm (rhs) injval.simps(6)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>2"]}\\ |
|
237 \textit{(7)} & @{thm (lhs) injval.simps(7)[of "r" "c" "v" "vs"]} & $\dn$ |
|
238 & @{thm (rhs) injval.simps(7)[of "r" "c" "v" "vs"]}\\ |
|
239 \end{tabular} |
|
240 \end{center} |
|
241 |
|
242 *} |
|
243 |
|
244 section {* Bitcoded Regular Expressions and Derivatives *} |
|
245 |
|
246 text {* |
|
247 bitcoded regexes / decoding / bmkeps |
|
248 gets rid of the second phase (only single phase) |
|
249 correctness |
|
250 |
|
251 |
|
252 \begin{center} |
|
253 \begin{tabular}{lcl} |
|
254 @{thm (lhs) code.simps(1)} & $\dn$ & @{thm (rhs) code.simps(1)}\\ |
|
255 @{thm (lhs) code.simps(2)} & $\dn$ & @{thm (rhs) code.simps(2)}\\ |
|
256 @{thm (lhs) code.simps(3)} & $\dn$ & @{thm (rhs) code.simps(3)}\\ |
|
257 @{thm (lhs) code.simps(4)} & $\dn$ & @{thm (rhs) code.simps(4)}\\ |
|
258 @{thm (lhs) code.simps(5)[of "v\<^sub>1" "v\<^sub>2"]} & $\dn$ & @{thm (rhs) code.simps(5)[of "v\<^sub>1" "v\<^sub>2"]}\\ |
|
259 @{thm (lhs) code.simps(6)} & $\dn$ & @{thm (rhs) code.simps(6)}\\ |
|
260 @{thm (lhs) code.simps(7)} & $\dn$ & @{thm (rhs) code.simps(7)} |
|
261 \end{tabular} |
|
262 \end{center} |
|
263 |
|
264 |
|
265 The idea of the bitcodes is to annotate them to regular expressions and generate values |
|
266 incrementally. The bitcodes can be read off from the @{text breg} and then decoded into a value. |
|
267 |
|
268 \begin{center} |
|
269 \begin{tabular}{lcl} |
|
270 @{term breg} & $::=$ & @{term "AZERO"}\\ |
|
271 & $\mid$ & @{term "AONE bs"}\\ |
|
272 & $\mid$ & @{term "ACHAR bs c"}\\ |
|
273 & $\mid$ & @{term "AALTs bs rs"}\\ |
|
274 & $\mid$ & @{term "ASEQ bs r\<^sub>1 r\<^sub>2"}\\ |
|
275 & $\mid$ & @{term "ASTAR bs r"} |
|
276 \end{tabular} |
|
277 \end{center} |
|
278 |
|
279 |
|
280 |
|
281 \begin{center} |
|
282 \begin{tabular}{lcl} |
|
283 @{thm (lhs) retrieve.simps(1)} & $\dn$ & @{thm (rhs) retrieve.simps(1)}\\ |
|
284 @{thm (lhs) retrieve.simps(2)} & $\dn$ & @{thm (rhs) retrieve.simps(2)}\\ |
|
285 @{thm (lhs) retrieve.simps(3)} & $\dn$ & @{thm (rhs) retrieve.simps(3)}\\ |
|
286 @{thm (lhs) better_retrieve(1)} & $\dn$ & @{thm (rhs) better_retrieve(1)}\\ |
|
287 @{thm (lhs) better_retrieve(2)} & $\dn$ & @{thm (rhs) better_retrieve(2)}\\ |
|
288 @{thm (lhs) retrieve.simps(6)[of _ "r\<^sub>1" "r\<^sub>2" "v\<^sub>1" "v\<^sub>2"]} |
|
289 & $\dn$ & @{thm (rhs) retrieve.simps(6)[of _ "r\<^sub>1" "r\<^sub>2" "v\<^sub>1" "v\<^sub>2"]}\\ |
|
290 @{thm (lhs) retrieve.simps(7)} & $\dn$ & @{thm (rhs) retrieve.simps(7)}\\ |
|
291 @{thm (lhs) retrieve.simps(8)} & $\dn$ & @{thm (rhs) retrieve.simps(8)} |
|
292 \end{tabular} |
|
293 \end{center} |
|
294 |
|
295 |
|
296 \begin{theorem} |
|
297 @{thm blexer_correctness} |
|
298 \end{theorem} |
|
299 *} |
|
300 |
|
301 |
|
302 section {* Simplification *} |
|
303 |
|
304 text {* |
|
305 Sulzmann \& Lu apply simplification via a fixpoint operation; also does not use erase to filter out duplicates. |
|
306 |
|
307 not direct correspondence with PDERs, because of example |
|
308 problem with retrieve |
|
309 |
|
310 correctness |
|
311 |
|
312 |
|
313 |
|
314 |
|
315 |
|
316 |
|
317 \begin{figure}[t] |
|
318 \begin{center} |
|
319 \begin{tabular}{c} |
|
320 @{thm[mode=Axiom] bs1[of _ "r\<^sub>2"]}\qquad |
|
321 @{thm[mode=Axiom] bs2[of _ "r\<^sub>1"]}\qquad |
|
322 @{thm[mode=Axiom] bs3[of "bs\<^sub>1" "bs\<^sub>2"]}\\ |
|
323 @{thm[mode=Rule] bs4[of "r\<^sub>1" "r\<^sub>2" _ "r\<^sub>3"]}\qquad |
|
324 @{thm[mode=Rule] bs5[of "r\<^sub>3" "r\<^sub>4" _ "r\<^sub>1"]}\\ |
|
325 @{thm[mode=Axiom] bs6}\qquad |
|
326 @{thm[mode=Axiom] bs7}\\ |
|
327 @{thm[mode=Rule] bs8[of "rs\<^sub>1" "rs\<^sub>2"]}\\ |
|
328 @{thm[mode=Axiom] ss1}\qquad |
|
329 @{thm[mode=Rule] ss2[of "rs\<^sub>1" "rs\<^sub>2"]}\qquad |
|
330 @{thm[mode=Rule] ss3[of "r\<^sub>1" "r\<^sub>2"]}\\ |
|
331 @{thm[mode=Axiom] ss4}\qquad |
|
332 @{thm[mode=Axiom] ss5[of "bs" "rs\<^sub>1" "rs\<^sub>2"]}\\ |
|
333 @{thm[mode=Rule] ss6[of "r\<^sub>1" "r\<^sub>2" "rs\<^sub>1" "rs\<^sub>2" "rs\<^sub>3"]}\\ |
|
334 \end{tabular} |
|
335 \end{center} |
|
336 \caption{???}\label{SimpRewrites} |
|
337 \end{figure} |
|
338 *} |
|
339 |
|
340 section {* Bound - NO *} |
|
341 |
|
342 section {* Bounded Regex / Not *} |
|
343 |
|
344 section {* Conclusion *} |
|
345 |
11 text {* |
346 text {* |
12 |
347 |
13 \cite{AusafDyckhoffUrban2016} |
348 \cite{AusafDyckhoffUrban2016} |
14 |
349 |
15 %%\bibliographystyle{plain} |
350 %%\bibliographystyle{plain} |