|
1 \documentclass[dvipsnames,14pt,t]{beamer} |
|
2 \usepackage{slides} |
|
3 \usepackage{langs} |
|
4 \usepackage{graph} |
|
5 \usepackage{data} |
|
6 \usepackage{proof} |
|
7 |
|
8 % beamer stuff |
|
9 \renewcommand{\slidecaption}{ITP ????} |
|
10 \newcommand{\bl}[1]{\textcolor{blue}{#1}} |
|
11 |
|
12 |
|
13 \begin{document} |
|
14 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
15 \begin{frame}[t] |
|
16 \frametitle{% |
|
17 \begin{tabular}{@ {}c@ {}} |
|
18 \\ |
|
19 \Large POSIX Lexing with Derivatives\\[-1.5mm] |
|
20 \Large of Regular Expressions\\ |
|
21 \Large (Proof Pearl)\\[-1mm] |
|
22 \end{tabular}}\bigskip\bigskip\bigskip |
|
23 |
|
24 \normalsize |
|
25 \begin{center} |
|
26 \begin{tabular}{c} |
|
27 \small Fahad Ausaf\\ |
|
28 \small King's College London\\ |
|
29 \\ |
|
30 \small joint work with Roy Dyckhoff and Christian Urban |
|
31 \end{tabular} |
|
32 \end{center} |
|
33 |
|
34 \end{frame} |
|
35 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
36 |
|
37 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
38 \begin{frame}[c] |
|
39 \frametitle{Regular Expressions} |
|
40 |
|
41 |
|
42 \begin{textblock}{6}(2,5) |
|
43 \begin{tabular}{rrl@ {\hspace{13mm}}l} |
|
44 \bl{$r$} & \bl{$::=$} & \bl{$\varnothing$} & null\\ |
|
45 & \bl{$\mid$} & \bl{$\epsilon$} & empty string\\ |
|
46 & \bl{$\mid$} & \bl{$c$} & character\\ |
|
47 & \bl{$\mid$} & \bl{$r_1 \cdot r_2$} & sequence\\ |
|
48 & \bl{$\mid$} & \bl{$r_1 + r_2$} & alternative / choice\\ |
|
49 & \bl{$\mid$} & \bl{$r^*$} & star (zero or more)\\ |
|
50 \end{tabular} |
|
51 \end{textblock} |
|
52 |
|
53 \end{frame} |
|
54 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
55 |
|
56 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
57 \begin{frame}[c] |
|
58 \frametitle{The Derivative of a Rexp} |
|
59 |
|
60 \large |
|
61 If \bl{$r$} matches the string \bl{$c\!::\!s$}, what is a regular |
|
62 expression that matches just \bl{$s$}?\bigskip\bigskip\bigskip\bigskip |
|
63 |
|
64 \small |
|
65 \bl{$der\,c\,r$} gives the answer, Brzozowski (1964), Owens (2005) |
|
66 ``\ldots have been lost in the sands of time\ldots'' |
|
67 \end{frame} |
|
68 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
69 |
|
70 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
71 \begin{frame}[c] |
|
72 \frametitle{Correctness} |
|
73 |
|
74 It is a relative easy exercise in a theorem prover: |
|
75 |
|
76 \begin{center} |
|
77 \bl{$matches(r, s)$} if and only if \bl{$s \in L(r)$} |
|
78 \end{center}\bigskip |
|
79 |
|
80 \small |
|
81 where \bl{$matches(r, s) \dn nullable(ders(r, s))$} |
|
82 |
|
83 \end{frame} |
|
84 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
85 |
|
86 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
87 \begin{frame}[c] |
|
88 \frametitle{POSIX Regex Matching} |
|
89 |
|
90 Two rules: |
|
91 |
|
92 \begin{itemize} |
|
93 \item Longest match rule (``maximal munch rule''): The |
|
94 longest initial substring matched by any regular expression |
|
95 is taken as the next token. |
|
96 |
|
97 \begin{center} |
|
98 \bl{$\texttt{\Grid{iffoo\VS bla}}$} |
|
99 \end{center}\medskip |
|
100 |
|
101 \item Rule priority: |
|
102 For a particular longest initial substring, the first regular |
|
103 expression that can match determines the token. |
|
104 |
|
105 \begin{center} |
|
106 \bl{$\texttt{\Grid{if\VS bla}}$} |
|
107 \end{center} |
|
108 \end{itemize}\bigskip\pause |
|
109 |
|
110 \small |
|
111 \hfill Kuklewicz: most POSIX matchers are buggy\\ |
|
112 \footnotesize |
|
113 \hfill \url{http://www.haskell.org/haskellwiki/Regex_Posix} |
|
114 |
|
115 \end{frame} |
|
116 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
117 |
|
118 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
119 \begin{frame}[c] |
|
120 \frametitle{POSIX Regex Matching} |
|
121 |
|
122 \begin{itemize} |
|
123 |
|
124 \item Sulzmann \& Lu came up with a beautiful |
|
125 idea for how to extend the simple regular expression |
|
126 matcher to POSIX matching/lexing (FLOPS 2014)\bigskip\bigskip |
|
127 |
|
128 \begin{tabular}{@{\hspace{4cm}}c@{}} |
|
129 \includegraphics[scale=0.20]{pics/sulzmann.jpg}\\[-2mm] |
|
130 \hspace{0cm}\footnotesize Martin Sulzmann |
|
131 \end{tabular}\bigskip\bigskip |
|
132 |
|
133 \item the idea: define an inverse operation to the derivatives |
|
134 \end{itemize} |
|
135 |
|
136 |
|
137 |
|
138 \end{frame} |
|
139 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
140 |
|
141 |
|
142 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
143 \begin{frame}[c] |
|
144 \frametitle{Regexes and Values} |
|
145 |
|
146 Regular expressions and their corresponding values |
|
147 (for \emph{how} a regular expression matched a string): |
|
148 |
|
149 \begin{center} |
|
150 \begin{columns} |
|
151 \begin{column}{3cm} |
|
152 \begin{tabular}{@{}rrl@{}} |
|
153 \bl{$r$} & \bl{$::=$} & \bl{$\varnothing$}\\ |
|
154 & \bl{$\mid$} & \bl{$\epsilon$} \\ |
|
155 & \bl{$\mid$} & \bl{$c$} \\ |
|
156 & \bl{$\mid$} & \bl{$r_1 \cdot r_2$}\\ |
|
157 & \bl{$\mid$} & \bl{$r_1 + r_2$} \\ |
|
158 \\ |
|
159 & \bl{$\mid$} & \bl{$r^*$} \\ |
|
160 \\ |
|
161 \end{tabular} |
|
162 \end{column} |
|
163 \begin{column}{3cm} |
|
164 \begin{tabular}{@{\hspace{-7mm}}rrl@{}} |
|
165 \bl{$v$} & \bl{$::=$} & \\ |
|
166 & & \bl{$Empty$} \\ |
|
167 & \bl{$\mid$} & \bl{$Char(c)$} \\ |
|
168 & \bl{$\mid$} & \bl{$Seq(v_1,v_2)$}\\ |
|
169 & \bl{$\mid$} & \bl{$Left(v)$} \\ |
|
170 & \bl{$\mid$} & \bl{$Right(v)$} \\ |
|
171 & \bl{$\mid$} & \bl{$[]$} \\ |
|
172 & \bl{$\mid$} & \bl{$[v_1,\ldots\,v_n]$} \\ |
|
173 \end{tabular} |
|
174 \end{column} |
|
175 \end{columns} |
|
176 \end{center}\pause |
|
177 |
|
178 There is also a notion of a string behind a value: \bl{$|v|$} |
|
179 |
|
180 \end{frame} |
|
181 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
182 |
|
183 |
|
184 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
185 \begin{frame}[c] |
|
186 \frametitle{Sulzmann \& Lu Matcher} |
|
187 |
|
188 We want to match the string \bl{$abc$} using \bl{$r_1$}: |
|
189 |
|
190 \begin{center} |
|
191 \begin{tikzpicture}[scale=2,node distance=1.3cm,every node/.style={minimum size=8mm}] |
|
192 \node (r1) {\bl{$r_1$}}; |
|
193 \node (r2) [right=of r1] {\bl{$r_2$}}; |
|
194 \draw[->,line width=1mm] (r1) -- (r2) node[above,midway] {\bl{$der\,a$}};\pause |
|
195 \node (r3) [right=of r2] {\bl{$r_3$}}; |
|
196 \draw[->,line width=1mm] (r2) -- (r3) node[above,midway] {\bl{$der\,b$}};\pause |
|
197 \node (r4) [right=of r3] {\bl{$r_4$}}; |
|
198 \draw[->,line width=1mm] (r3) -- (r4) node[above,midway] {\bl{$der\,c$}};\pause |
|
199 \draw (r4) node[anchor=west] {\;\raisebox{3mm}{\bl{$\;\;nullable?$}}};\pause |
|
200 \node (v4) [below=of r4] {\bl{$v_4$}}; |
|
201 \draw[->,line width=1mm] (r4) -- (v4);\pause |
|
202 \node (v3) [left=of v4] {\bl{$v_3$}}; |
|
203 \draw[->,line width=1mm] (v4) -- (v3) node[below,midway] {\bl{$inj\,c$}};\pause |
|
204 \node (v2) [left=of v3] {\bl{$v_2$}}; |
|
205 \draw[->,line width=1mm] (v3) -- (v2) node[below,midway] {\bl{$inj\,b$}};\pause |
|
206 \node (v1) [left=of v2] {\bl{$v_1$}}; |
|
207 \draw[->,line width=1mm] (v2) -- (v1) node[below,midway] {\bl{$inj\,a$}};\pause |
|
208 \draw[->,line width=0.5mm] (r3) -- (v3); |
|
209 \draw[->,line width=0.5mm] (r2) -- (v2); |
|
210 \draw[->,line width=0.5mm] (r1) -- (v1); |
|
211 \draw (r4) node[anchor=north west] {\;\raisebox{-8mm}{\bl{$mkeps$}}}; |
|
212 \end{tikzpicture} |
|
213 \end{center} |
|
214 |
|
215 \only<10>{ |
|
216 The original ideas of Sulzmann and Lu are the \bl{\textit{mkeps}} |
|
217 and \bl{\textit{inj}} functions (ommitted here).} |
|
218 \end{frame} |
|
219 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
220 |
|
221 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
222 \begin{frame}[t,squeeze] |
|
223 \frametitle{Sulzmann \& Lu Paper} |
|
224 |
|
225 \begin{itemize} |
|
226 \item I have no doubt the algorithm is correct --- |
|
227 the problem is I do not believe their proof. |
|
228 |
|
229 \begin{center} |
|
230 \begin{bubble}[10cm]\small |
|
231 ``How could I miss this? Well, I was rather careless when |
|
232 stating this Lemma :)\smallskip |
|
233 |
|
234 Great example how formal machine checked proofs (and |
|
235 proof assistants) can help to spot flawed reasoning steps.'' |
|
236 \end{bubble} |
|
237 \end{center}\pause |
|
238 |
|
239 \begin{center} |
|
240 \begin{bubble}[10cm]\small |
|
241 ``Well, I don't think there's any flaw. The issue is how to |
|
242 come up with a mechanical proof. In my world mathematical |
|
243 proof $=$ mechanical proof doesn't necessarily hold.'' |
|
244 \end{bubble} |
|
245 \end{center}\pause |
|
246 |
|
247 \end{itemize} |
|
248 |
|
249 \only<3>{% |
|
250 \begin{textblock}{11}(1,4.4) |
|
251 \begin{center} |
|
252 \begin{bubble}[10.9cm]\small\centering |
|
253 \includegraphics[scale=0.37]{pics/msbug.png} |
|
254 \end{bubble} |
|
255 \end{center} |
|
256 \end{textblock}} |
|
257 |
|
258 |
|
259 \end{frame} |
|
260 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
261 |
|
262 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
263 \begin{frame}[c] |
|
264 \frametitle{\begin{tabular}{c}The Proof Idea\\[-1mm] by Sulzmann \& Lu |
|
265 \end{tabular}} |
|
266 |
|
267 \begin{itemize} |
|
268 \item introduce an inductively defined ordering relation |
|
269 \bl{$v \succ_r v'$} which captures the idea of POSIX matching |
|
270 |
|
271 \item the algorithm returns the maximum of all possible |
|
272 values that are possible for a regular expression.\pause |
|
273 \bigskip\small |
|
274 |
|
275 \item the idea is from a paper by Cardelli \& Frisch about |
|
276 GREEDY matching (GREEDY $=$ preferring instant gratification to delayed |
|
277 repletion): |
|
278 |
|
279 \item e.g.~given \bl{$(a + (b + ab))^*$} and string \bl{$ab$} |
|
280 |
|
281 \begin{center} |
|
282 \begin{tabular}{ll} |
|
283 GREEDY: & \bl{$[Left(a), Right(Left(b)]$}\\ |
|
284 POSIX: & \bl{$[Right(Right(Seq(a, b))))]$} |
|
285 \end{tabular} |
|
286 \end{center} |
|
287 \end{itemize} |
|
288 |
|
289 \end{frame} |
|
290 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
291 |
|
292 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
293 \begin{frame}[c] |
|
294 \frametitle{} |
|
295 \centering |
|
296 |
|
297 |
|
298 \bl{\infer{\vdash Empty : \epsilon}{}}\hspace{15mm} |
|
299 \bl{\infer{\vdash Char(c): c}{}}\bigskip |
|
300 |
|
301 \bl{\infer{\vdash Seq(v_1, v_2) : r_1\cdot r_2}{\vdash v_1 : r_1 \quad \vdash v_2 : r_2}} |
|
302 \bigskip |
|
303 |
|
304 \bl{\infer{\vdash Left(v) : r_1 + r_2}{\vdash v : r_1}}\hspace{15mm} |
|
305 \bl{\infer{\vdash Right(v): r_1 + r_2}{\vdash v : r_2}}\bigskip |
|
306 |
|
307 \bl{\infer{\vdash [] : r^*}{}}\hspace{15mm} |
|
308 \bl{\infer{\vdash [v_1,\ldots, v_n] : r^*} |
|
309 {\vdash v_1 : r \quad\ldots\quad \vdash v_n : r}} |
|
310 |
|
311 \end{frame} |
|
312 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
313 |
|
314 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
315 \begin{frame}<1>[c] |
|
316 \frametitle{} |
|
317 \small |
|
318 |
|
319 %\begin{tabular}{@{}lll@{}} |
|
320 %\bl{$POSIX(v, r)$} & \bl{$\dn$} & \bl{$\vdash v : r$}\\ |
|
321 % & & \bl{$\wedge \;\;(\forall v'.\;\; \vdash v' : r \,\wedge\, |v'| = |v| |
|
322 % \Rightarrow v \succ_{\alert<2>{r}} v')$} |
|
323 %\end{tabular}\bigskip\bigskip\bigskip |
|
324 |
|
325 |
|
326 \centering |
|
327 |
|
328 %\bl{\infer{Seq(v_1, v_2) \succ_{\alert<2>{r_1\cdot r_2}} Seq(v'_1, v'_2)} |
|
329 % {v_1 = v'_1 \quad v_2 \succ_{\alert<2>{r_2}} v'_2}}\hspace{3mm} |
|
330 %\bl{\infer{Seq(v_1, v_2) \succ_{\alert<2>{r_1\cdot r_2}} Seq(v'_1, v'_2)} |
|
331 % {v_1 \not= v'_1 \quad v_1 \succ_{\alert<2>{r_1}} v'_1}} |
|
332 %\bigskip |
|
333 |
|
334 %\bl{\infer{Left(v) \succ_{\alert<2>{r_1 + r_2}} Left(v')} |
|
335 % {v \succ_{\alert<2>{r_1}} v'}}\hspace{15mm} |
|
336 %\bl{\infer{Right(v) \succ_{\alert<2>{r_1 + r_2}} Right(v')} |
|
337 % {v \succ_{\alert<2>{r_2}} v'}}\bigskip\medskip |
|
338 |
|
339 %\bl{\infer{Left(v) \succ_{\alert<2>{r_1 + r_2}} Right(v')} |
|
340 % {length |v| \ge length |v'|}}\hspace{15mm} |
|
341 %\bl{\infer{Right(v) \succ_{\alert<2>{r_1 + r_2}} Left(v')} |
|
342 % {length |v| > length |v'|}}\bigskip |
|
343 |
|
344 %\bl{$\big\ldots$} |
|
345 |
|
346 \end{frame} |
|
347 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
348 |
|
349 |
|
350 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
351 \begin{frame}[c] |
|
352 \frametitle{Problems} |
|
353 |
|
354 \begin{itemize} |
|
355 \item Sulzmann: \ldots Let's assume \bl{$v$} is not |
|
356 a $POSIX$ value, then there must be another one |
|
357 \ldots contradiction.\bigskip\pause |
|
358 |
|
359 \item Exists? |
|
360 |
|
361 \begin{center} |
|
362 \bl{$L(r) \not= \varnothing \;\Rightarrow\; \exists v.\;POSIX(v, r)$} |
|
363 \end{center}\bigskip\bigskip\pause |
|
364 |
|
365 \item in the sequence case |
|
366 \bl{$Seq(v_1, v_2)\succ_{r_1\cdot r_2} Seq(v_1', v_2')$}, |
|
367 the induction hypotheses require |
|
368 \bl{$|v_1| = |v'_1|$} and \bl{$|v_2| = |v'_2|$}, |
|
369 but you only know |
|
370 |
|
371 \begin{center} |
|
372 \bl{$|v_1| \;@\; |v_2| = |v'_1| \;@\; |v'_2|$} |
|
373 \end{center}\pause\small |
|
374 |
|
375 \item although one begins with the assumption that the two |
|
376 values have the same flattening, this cannot be maintained |
|
377 as one descends into the induction (alternative, sequence) |
|
378 \end{itemize} |
|
379 |
|
380 \end{frame} |
|
381 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
382 |
|
383 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
384 \begin{frame}[c] |
|
385 \frametitle{Our Solution} |
|
386 |
|
387 \begin{itemize} |
|
388 \item a direct definition of what a POSIX value is, using |
|
389 the relation \bl{$s \in r \to v$} (specification):\medskip |
|
390 |
|
391 \begin{center} |
|
392 \bl{\infer{[] \in \epsilon \to Empty}{}}\hspace{15mm} |
|
393 \bl{\infer{c \in c \to Char(c)}{}}\bigskip\medskip |
|
394 |
|
395 \bl{\infer{s \in r_1 + r_2 \to Left(v)} |
|
396 {s \in r_1 \to v}}\hspace{10mm} |
|
397 \bl{\infer{s \in r_1 + r_2 \to Right(v)} |
|
398 {s \in r_2 \to v & s \not\in L(r_1)}}\bigskip\medskip |
|
399 |
|
400 \bl{\infer{s_1 @ s_2 \in r_1 \cdot r_2 \to Seq(v_1, v_2)} |
|
401 {\small\begin{array}{l} |
|
402 s_1 \in r_1 \to v_1 \\ |
|
403 s_2 \in r_2 \to v_2 \\ |
|
404 \neg(\exists s_3\,s_4.\; s_3 \not= [] |
|
405 \wedge s_3 @ s_4 = s_2 \wedge |
|
406 s_1 @ s_3 \in L(r_1) \wedge |
|
407 s_4 \in L(r_2)) |
|
408 \end{array}}} |
|
409 |
|
410 \bl{\ldots} |
|
411 \end{center} |
|
412 \end{itemize} |
|
413 |
|
414 \end{frame} |
|
415 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
416 |
|
417 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
418 \begin{frame}[c] |
|
419 \frametitle{Properties} |
|
420 |
|
421 It is almost trival to prove: |
|
422 |
|
423 \begin{itemize} |
|
424 \item Uniqueness |
|
425 \begin{center} |
|
426 If \bl{$s \in r \to v_1$} and \bl{$s \in r \to v_2$} then |
|
427 \bl{$v_1 = v_2$}. |
|
428 \end{center}\bigskip |
|
429 |
|
430 \item Correctness |
|
431 \begin{center} |
|
432 \bl{$lexer(r, s) = v$} if and only if \bl{$s \in r \to v$} |
|
433 \end{center} |
|
434 \end{itemize}\bigskip\bigskip\pause |
|
435 |
|
436 |
|
437 You can now start to implement optimisations and derive |
|
438 correctness proofs for them. But we still do not know whether |
|
439 |
|
440 \begin{center} |
|
441 \bl{$s \in r \to v$} |
|
442 \end{center} |
|
443 |
|
444 is a POSIX value according to Sulzmann \& Lu's definition |
|
445 (biggest value for \bl{$s$} and \bl{$r$}) |
|
446 \end{frame} |
|
447 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
448 |
|
449 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
450 \begin{frame}[c] |
|
451 \frametitle{Conclusion} |
|
452 |
|
453 \begin{itemize} |
|
454 |
|
455 \item we replaced the POSIX definition of Sulzmann \& Lu by a |
|
456 new definition (ours is inspired by work of Vansummeren, |
|
457 2006)\medskip |
|
458 |
|
459 \item their proof contained small gaps (acknowledged) but had |
|
460 also fundamental flaws\medskip |
|
461 |
|
462 \item now, its a nice exercise for theorem proving\medskip |
|
463 |
|
464 \item some optimisations need to be applied to the algorithm |
|
465 in order to become fast enough\medskip |
|
466 |
|
467 \item can be used for lexing, is a small beautiful functional |
|
468 program |
|
469 |
|
470 \end{itemize} |
|
471 |
|
472 \end{frame} |
|
473 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
474 |
|
475 |
|
476 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
477 \begin{frame}[b] |
|
478 \frametitle{ |
|
479 \begin{tabular}{c} |
|
480 \mbox{}\\[13mm] |
|
481 \alert{\LARGE Questions?} |
|
482 \end{tabular}} |
|
483 |
|
484 \end{frame} |
|
485 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
486 |
|
487 \end{document} |
|
488 |
|
489 |
|
490 %%% Local Variables: |
|
491 %%% mode: latex |
|
492 %%% TeX-master: t |
|
493 %%% End: |
|
494 |