19 \draw (0,0) node[inner sep=2mm,fill=cream,ultra thick,draw=red,rounded corners=2mm]% |
19 \draw (0,0) node[inner sep=2mm,fill=cream,ultra thick,draw=red,rounded corners=2mm]% |
20 \bgroup\begin{minipage}{#1}\raggedright{}} |
20 \bgroup\begin{minipage}{#1}\raggedright{}} |
21 {\end{minipage}\egroup;% |
21 {\end{minipage}\egroup;% |
22 \end{tikzpicture}\bigskip} |
22 \end{tikzpicture}\bigskip} |
23 |
23 |
24 \newcommand\grid[1]{% |
24 \title{\bf POSIX Lexing with\\ |
25 \begin{tikzpicture}[baseline=(char.base)] |
|
26 \path[use as bounding box] |
|
27 (0,0) rectangle (1em,1em); |
|
28 \draw[red!50, fill=red!20] |
|
29 (0,0) rectangle (1em,1em); |
|
30 \node[inner sep=1pt,anchor=base west] |
|
31 (char) at (0em,\gridraiseamount) {#1}; |
|
32 \end{tikzpicture}} |
|
33 \newcommand\gridraiseamount{0.12em} |
|
34 |
|
35 \makeatletter |
|
36 \newcommand\Grid[1]{% |
|
37 \@tfor\z:=#1\do{\grid{\z}}} |
|
38 \makeatother |
|
39 |
|
40 \newcommand\Vspace[1][.3em]{% |
|
41 \mbox{\kern.06em\vrule height.3ex}% |
|
42 \vbox{\hrule width#1}% |
|
43 \hbox{\vrule height.3ex}} |
|
44 |
|
45 \def\VS{\Vspace[0.6em]} |
|
46 |
|
47 |
|
48 \title[POSIX Lexing with Derivatives of Regexes] |
|
49 {\bf POSIX Lexing with\\ |
|
50 \bf Derivatives of Regular Expressions\\ |
25 \bf Derivatives of Regular Expressions\\ |
51 \bf (Proof Pearl)} |
26 \bf (Proof Pearl)} |
52 \author{Fahad Ausaf, Roy Dyckhoff and Christian Urban} |
27 \author{Fahad Ausaf, Roy Dyckhoff and Christian Urban} |
53 \date{King's College London, University of St Andrews} |
28 \date{King's College London, University of St Andrews} |
54 |
29 |
175 |
162 |
176 There are several possible answers for |
163 There are several possible answers for |
177 \alert{\textbf{how}}: POSIX, GREEDY, \ldots |
164 \alert{\textbf{how}}: POSIX, GREEDY, \ldots |
178 |
165 |
179 \end{frame} |
166 \end{frame} |
180 |
|
181 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
182 |
|
183 \begin{frame}{Regular Expressions and Values} |
|
184 Regular expressions and their corresponding values (for how a |
|
185 regular expression matched a string):\bigskip |
|
186 |
|
187 \begin{columns}[c] % the "c" option specifies center vertical alignment |
|
188 \column{.4\textwidth} % column designated by a command |
|
189 \begin{tabular}{ l l l } |
|
190 \smath{r} & ::= & \smath{\Zero} \\ |
|
191 & $\mid$ & \smath{\One} \\ |
|
192 & $\mid$ & \smath{c} \\ |
|
193 & $\mid$ & \smath{r_1 \cdot r_2} \\ |
|
194 & $\mid$ & \smath{r_1 + r_2} \\ \\ |
|
195 & $\mid$ & \smath{r^*} \\ |
|
196 \end{tabular} |
|
197 \column{.4\textwidth} |
|
198 \begin{tabular}{ l l l } |
|
199 |
|
200 \smath{v} & ::= & \\ |
|
201 & $\mid$ & \smath{Empty} \\ |
|
202 & $\mid$ & \smath{Char(c)} \\ |
|
203 & $\mid$ & \smath{Seq(v_1\cdot v_2)} \\ |
|
204 & $\mid$ & \smath{Left(v)} \\ |
|
205 & $\mid$ & \smath{Right(v)} \\ |
|
206 & $\mid$ & \smath{[v_1,...,v_n]} |
|
207 \end{tabular} |
|
208 \end{columns} |
|
209 \end{frame} |
|
210 |
|
211 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
212 |
|
213 |
167 |
214 |
168 |
215 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
169 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
216 |
170 |
217 \begin{frame} |
171 \begin{frame} |
264 |
220 |
265 \end{frame} |
221 \end{frame} |
266 |
222 |
267 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
223 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
268 |
224 |
269 \begin{frame} |
225 % \begin{frame} |
270 \frametitle{``Correctness'' by Sulzmann and Lu} |
226 % \frametitle{Correctness} |
271 \begin{itemize} |
227 % \begin{itemize} |
272 \item Sulzmann \& Lu's idea is to order all possible |
228 % \item Sulzmann \& Lu came up with a beautiful idea for how |
273 answer such that they can prove the correct answer is |
229 % to extend the simple regular expression matcher to POSIX |
274 the maximum |
230 % matching/lexing (FLOPS 2014) |
275 \item The idea is taken from a GREEDY algorithm (and it |
231 % \item The idea: define an inverse operation to the derivatives |
276 works there)\bigskip\pause |
232 % \end{itemize} |
277 |
233 % \end{frame} |
278 \item {\bf But} we made no progress in formalising |
234 |
279 Sulzmann \& Lu's idea, because |
235 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
280 |
236 |
281 \begin{itemize} |
237 \begin{frame} |
282 \item transitivity, existence of maxima etc all fail to |
238 \frametitle{Regular Expressions and Values} |
283 turn into real proofs |
239 Regular expressions and their corresponding values (for how a |
284 \item the reason: the ordering works only if .... |
240 regular expression matched string): |
285 \item though we did find mistakes: |
241 \begin{columns}[c] % the "c" option specifies center vertical alignment |
286 \begin{center} |
242 \column{.5\textwidth} % column designated by a command |
287 \small |
243 \begin{tabular}{ l l l } |
288 ``How could I miss this? Well, I was rather careless when |
244 $r$ & ::= & $\varnothing$ \\ |
289 stating this Lemma :)\smallskip |
245 & $\mid$ & $\epsilon$ \\ |
290 |
246 & $\mid$ & $c$ \\ |
291 Great example how formal machine checked proofs (and |
247 & $\mid$ & $r_1 \cdot r_2$ \\ |
292 proof assistants) can help to spot flawed reasoning steps.'' |
248 & $\mid$ & $r_1 + r_2$ \\ |
293 |
249 & $\mid$ & $r^*$ \\ |
294 \end{center}\pause |
250 \end{tabular} |
295 |
251 \column{.5\textwidth} |
296 \begin{center} |
252 \begin{tabular}{ l l l } |
297 \small |
253 $v$ & ::= & $\varnothing$ \\ |
298 ``Well, I don't think there's any flaw. The issue is how to |
254 & $\mid$ & $Empty$ \\ |
299 come up with a mechanical proof. In my world mathematical |
255 & $\mid$ & $Char$($c$) \\ |
300 proof $=$ mechanical proof doesn't necessarily hold.'' |
256 & $\mid$ & $Seq$($v_1.v_2$) \\ |
301 |
257 & $\mid$ & $Left$($v$) \\ |
302 \end{center}\pause |
258 & $\mid$ & $Right$($v$) \\ |
303 \end{itemize} |
259 & $\mid$ & [] \\ |
304 |
260 & $\mid$ & [$v_1,...,v_n$] |
305 \end{itemize} |
261 \end{tabular} |
306 \end{frame} |
262 \end{columns} |
307 |
263 There is also a notion of a string behind a value $\mid v \mid$ |
308 |
264 \end{frame} |
|
265 |
309 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
266 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
310 |
267 |
311 \begin{frame} |
268 \begin{frame} |
312 \frametitle{Sulzmann and Lu Matcher} |
269 \frametitle{Sulzmann and Lu Matcher} |
313 |
270 |
322 \draw[->,line width=1mm] (r2) -- (r3) node[above,midway] {$der\,b$};\pause |
279 \draw[->,line width=1mm] (r2) -- (r3) node[above,midway] {$der\,b$};\pause |
323 \node (r4) [right=of r3] {$r_4$}; |
280 \node (r4) [right=of r3] {$r_4$}; |
324 \draw[->,line width=1mm] (r3) -- (r4) node[above,midway] {$der\,c$};\pause |
281 \draw[->,line width=1mm] (r3) -- (r4) node[above,midway] {$der\,c$};\pause |
325 \draw (r4) node[anchor=west] {\;\raisebox{3mm}{$\;\;nullable?$}};\pause |
282 \draw (r4) node[anchor=west] {\;\raisebox{3mm}{$\;\;nullable?$}};\pause |
326 \node (v4) [below=of r4] {$v_4$}; |
283 \node (v4) [below=of r4] {$v_4$}; |
327 \draw[->,line width=1mm] (r4) -- (v4);\pause |
284 \draw[->,line width=1mm] (r4) -- (v4); |
|
285 \draw (r4) node[anchor=north west] {\;\raisebox{-8mm}{$mkeps$}};\pause |
328 \node (v3) [left=of v4] {$v_3$}; |
286 \node (v3) [left=of v4] {$v_3$}; |
329 \draw[->,line width=1mm] (v4) -- (v3) node[below,midway] {$inj\,c$};\pause |
287 \draw[->,line width=1mm] (v4) -- (v3) node[below,midway] {$inj\,c$};\pause |
330 \node (v2) [left=of v3] {$v_2$}; |
288 \node (v2) [left=of v3] {$v_2$}; |
331 \draw[->,line width=1mm] (v3) -- (v2) node[below,midway] {$inj\,b$};\pause |
289 \draw[->,line width=1mm] (v3) -- (v2) node[below,midway] {$inj\,b$};\pause |
332 \node (v1) [left=of v2] {$v_1$}; |
290 \node (v1) [left=of v2] {$v_1$}; |
333 \draw[->,line width=1mm] (v2) -- (v1) node[below,midway] {$inj\,a$};\pause |
291 \draw[->,line width=1mm] (v2) -- (v1) node[below,midway] {$inj\,a$};\pause |
334 \draw[->,line width=0.5mm] (r3) -- (v3); |
292 \draw[->,line width=0.5mm] (r3) -- (v3); |
335 \draw[->,line width=0.5mm] (r2) -- (v2); |
293 \draw[->,line width=0.5mm] (r2) -- (v2); |
336 \draw[->,line width=0.5mm] (r1) -- (v1); |
294 \draw[->,line width=0.5mm] (r1) -- (v1); |
337 \draw (r4) node[anchor=north west] {\;\raisebox{-8mm}{$mkeps$}}; |
|
338 \end{tikzpicture} |
295 \end{tikzpicture} |
339 \end{center} |
296 \end{center} |
340 |
297 |
341 \end{frame} |
298 \end{frame} |
342 |
299 |
343 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
300 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
344 |
301 |
|
302 \begin{frame} |
|
303 \frametitle{Nullable, Mkeps and Injection Functions} |
|
304 |
|
305 \textbf{Nullable Function} |
|
306 \begin{tabular}{ l l l } |
|
307 \textit{nullable} (\textbf{0}) & $\dn$ & \textit{False}\\ |
|
308 \textit{nullable} (\textbf{1}) & $\dn$ & \textit{True}\\ |
|
309 \textit{nullable} (c) & $\dn$ & \textit{False}\\ |
|
310 \textit{nullable} ($r_1 + r_2$) & $\dn$ & \textit{nullable} $r_1$ $\lor$ \textit{nullable} $r_2$\\ |
|
311 \textit{nullable} ($r_1 \cdot r_2$) & $\dn$ & \textit{nullable} $r_1$ $\land$ \textit{nullable} $r_2$\\ |
|
312 \textit{nullable} ($r^*$) & $\dn$ & \textit{True}\\ |
|
313 \end{tabular}\\ |
|
314 \vspace{3 mm} |
|
315 \textbf{Mkeps Function} |
|
316 \begin{tabular}{ l l l } |
|
317 \textit{mkeps} (\textbf{1}) & $\dn$ & () \\ |
|
318 \textit{mkeps} ($r_1 \cdot r_2$) & $\dn$ & \textit{Seq} (\textit{mkeps} $r_1$) (\textit{mkeps} $r_2$)\\ |
|
319 \textit{mkeps} ($r_1 + r_2$) & $\dn$ & \textit{if nullable $r_1$ then Left} (\textit{mkeps $r_1$})\\ |
|
320 & & \textit{else Right} (\textit{mkeps $r_2$})\\ |
|
321 \textit{mkeps} ($r^*$) & $\dn$ & \textit{Stars} [] \\ |
|
322 \end{tabular}\\ |
|
323 |
|
324 \end{frame} |
|
325 |
|
326 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
327 |
|
328 \begin{frame} |
|
329 \frametitle{Nullable, Mkeps and Injection Functions} |
|
330 |
|
331 \textbf{Injection Function} |
|
332 \begin{tabular}{ l l l } |
|
333 \textit{inj d c} () & $\dn$ & \textit{Char d}\\ |
|
334 \textit{inj} ($r_1 + r_2$) \textit{c} (\textit{Left $v_1$}) & $\dn$ & \textit{Left} (\textit{inj $r_1$ c $v_1$})\\ |
|
335 \textit{inj} ($r_1 + r_2$) \textit{c} (\textit{Right $v_2$}) & $\dn$ & \textit{Right} (\textit{inj $r_2$ c $v_2$})\\ |
|
336 \textit{inj} ($r_1 \cdot r_2$) \textit{c} (\textit{Seq $v_1$ $v_2$}) & $\dn$ & \textit{Seq} (\textit{inj $r_1$ c $v_1$}) $v_2$\\ |
|
337 \textit{inj} ($r_1 \cdot r_2$) \textit{c} (\textit{Left} (\textit{Seq $v_1$ $v_2$})) & $\dn$ & \textit{Seq} (\textit{inj $r_1$ c $v_1$}) $v_2$\\ |
|
338 \textit{inj} ($r_1 \cdot r_2$) \textit{c} (\textit{Right $v_2$}) & $\dn$ & \textit{Seq} (\textit{mkeps $r_1$}) (\textit{inj $r_2$ c $v_2$})\\ |
|
339 \textit{inj} ($r^*$) \textit{c} (\textit{Seq v} (\textit{Stars vs})) & $\dn$ & \textit{Stars} (\textit{inj r c v}::\textit{vs}) |
|
340 \end{tabular} |
|
341 |
|
342 \end{frame} |
|
343 |
|
344 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
345 |
|
346 \begin{frame} |
|
347 \frametitle{POSIX Ordering Relation by Sulzmann \& Lu} |
|
348 |
|
349 \begin{itemize} |
|
350 \item Introduce an inductive defined ordering relation |
|
351 $v \succ_r v'$ which captures the idea of POSIX matching. |
|
352 |
|
353 \item The algorithm returns the maximum of all possible values |
|
354 that are possible for a regular expression. |
|
355 |
|
356 \item The idea is from a paper by Frisch \& Cardelli about |
|
357 GREEDY matching (GREEDY = preferring instant gratification |
|
358 to delayed repletion): |
|
359 |
|
360 \item e.g. given $(a + (b + ab))^{*}$ and string $ab$\\ |
|
361 \begin{center} |
|
362 \begin{tabular}{ll} |
|
363 GREEDY: & $[Left(a), Right(Left(b))]$\\ |
|
364 POSIX: & $[Right(Right(Seq(a, b)))]$ |
|
365 \end{tabular} |
|
366 \end{center} |
|
367 |
|
368 \end{itemize} |
|
369 \end{frame} |
|
370 |
|
371 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
372 |
|
373 \begin{frame} |
|
374 \frametitle{POSIX Ordering Relation by Sulzmann \& Lu} |
|
375 |
|
376 \begin{center} |
|
377 $\infer{\vdash Empty : \epsilon}{}$\hspace{15mm} |
|
378 $\infer{\vdash Char(c): c}{}$\bigskip |
|
379 |
|
380 $\infer{\vdash Seq(v_1, v_2) : r_1\cdot r_2}{\vdash v_1 : r_1 \quad \vdash v_2 : r_2}$ |
|
381 \bigskip |
|
382 |
|
383 $\infer{\vdash Left(v) : r_1 + r_2}{\vdash v : r_1}$\hspace{15mm} |
|
384 $\infer{\vdash Right(v): r_1 + r_2}{\vdash v : r_2}$\bigskip |
|
385 |
|
386 $\infer{\vdash [] : r^*}{}$\hspace{15mm} |
|
387 $\infer{\vdash [v_1,\ldots, v_n] : r^*} |
|
388 {\vdash v_1 : r \quad\ldots\quad \vdash v_n : r}$ |
|
389 \end{center} |
|
390 |
|
391 \end{frame} |
345 |
392 |
346 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
393 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
347 |
394 |
348 \begin{frame} |
395 \begin{frame} |
349 \frametitle{Problems} |
396 \frametitle{Problems} |
350 \begin{itemize} |
397 \begin{itemize} |
351 |
398 |
352 \item Sulzmann: \ldots Let's assume $v$ is not a $POSIX$ value, |
399 \item Sulzmann: \ldots Let's assume $v$ is not a $POSIX$ value, |
353 then there must be another one \ldots contradiction.\pause |
400 then there must be another one \ldots contradiction. |
354 |
401 |
355 \item Exists ? |
402 \item Exists ? |
356 \begin{center} |
403 \begin{center} |
357 $L(r) \not= \varnothing \;\Rightarrow\; \exists v.\;POSIX(v, r)$ |
404 $L(r) \not= \varnothing \;\Rightarrow\; \exists v.\;POSIX(v, r)$ |
358 \end{center}\pause |
405 \end{center} |
359 |
406 |
360 \item In the sequence case |
407 \item In the sequence case |
361 $Seq(v_1,v_2)\succ_{r_1\cdot r_2} Seq(v_1', v_2')$, |
408 $Seq(v_1,v_2)\succ_{r_1\cdot r_2} Seq(v_1', v_2')$, |
362 the induction hypotheses require |
409 the induction hypotheses require |
363 $|v_1| = |v_1'|$ and $|v_2| = |v_2'|$, but you only know |
410 $|v_1| = |v_1'|$ and $|v_2| = |v_2'|$, but you only know |
364 |
411 |
365 \begin{center} |
412 \begin{center} |
366 $|v_1| @ |v_2| = |v_1'| @ |v_2'|$ |
413 $|v_1| @ |v_2| = |v_1'| @ |v_2'|$ |
367 \end{center}\pause |
414 \end{center} |
368 |
415 |
369 \item Although one begins with the assumption that the two |
416 \item Although one begins with the assumption that the two |
370 values have the same flattening, this cannot be maintained |
417 values have the same flattening, this cannot be maintained |
371 as one descends into the induction (alternative, sequence) |
418 as one descends into the induction (alternative, sequence) |
372 |
419 |
374 \end{frame} |
421 \end{frame} |
375 |
422 |
376 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
423 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
377 |
424 |
378 \begin{frame} |
425 \begin{frame} |
|
426 \frametitle{Problems} |
|
427 |
|
428 \begin{itemize} |
|
429 \item I have no doubt the algorithm is correct --- |
|
430 the problem is I do not believe their proof. |
|
431 |
|
432 \begin{center} |
|
433 \small |
|
434 ``How could I miss this? Well, I was rather careless when |
|
435 stating this Lemma :)\smallskip |
|
436 |
|
437 Great example how formal machine checked proofs (and |
|
438 proof assistants) can help to spot flawed reasoning steps.'' |
|
439 |
|
440 \end{center} |
|
441 |
|
442 \begin{center} |
|
443 \small |
|
444 ``Well, I don't think there's any flaw. The issue is how to |
|
445 come up with a mechanical proof. In my world mathematical |
|
446 proof $=$ mechanical proof doesn't necessarily hold.'' |
|
447 |
|
448 \end{center} |
|
449 |
|
450 \end{itemize} |
|
451 |
|
452 \end{frame} |
|
453 |
|
454 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
455 |
|
456 \begin{frame} |
379 \frametitle{Our Solution} |
457 \frametitle{Our Solution} |
380 |
458 |
381 \begin{itemize} |
459 \begin{itemize} |
382 \item A direct definition of what a POSIX value is, using the |
460 \item A direct definition of what a POSIX value is, using the |
383 relation \smath{s \in r \to v} (our specification)\bigskip |
461 relation $s \in r \to v$ (specification) |
384 |
462 |
385 \begin{center} |
463 \begin{center} |
386 \smath{\infer{[] \in \epsilon \to Empty}{}}\hspace{15mm} |
464 $\infer{[] \in \epsilon \to Empty}{}$\hspace{15mm} |
387 \smath{\infer{[c] \in c \to Char(c)}{}}\bigskip\medskip |
465 $\infer{c \in c \to Char(c)}{}$\bigskip\medskip |
388 |
466 |
389 \smath{\infer{s \in r_1 + r_2 \to Left(v)} |
467 $\infer{s \in r_1 + r_2 \to Left(v)} |
390 {s \in r_1 \to v}}\hspace{10mm} |
468 {s \in r_1 \to v}$\hspace{10mm} |
391 \smath{\infer{s \in r_1 + r_2 \to Right(v)} |
469 $\infer{s \in r_1 + r_2 \to Right(v)} |
392 {s \in r_2 \to v & s \not\in L(r_1)}}\bigskip\medskip |
470 {s \in r_2 \to v & s \not\in L(r_1)}$\bigskip\medskip |
393 |
471 |
394 \smath{\infer{s_1 @ s_2 \in r_1 \cdot r_2 \to Seq(v_1, v_2)} |
472 $\infer{s_1 @ s_2 \in r_1 \cdot r_2 \to Seq(v_1, v_2)} |
395 {\small\begin{array}{l} |
473 {\small\begin{array}{l} |
396 s_1 \in r_1 \to v_1 \\ |
474 s_1 \in r_1 \to v_1 \\ |
397 s_2 \in r_2 \to v_2 \\ |
475 s_2 \in r_2 \to v_2 \\ |
398 \neg(\exists s_3\,s_4.\; s_3 \not= [] |
476 \neg(\exists s_3\,s_4.\; s_3 \not= [] |
399 \wedge s_3 @ s_4 = s_2 \wedge |
477 \wedge s_3 @ s_4 = s_2 \wedge |
400 s_1 @ s_3 \in L(r_1) \wedge |
478 s_1 @ s_3 \in L(r_1) \wedge |
401 s_4 \in L(r_2)) |
479 s_4 \in L(r_2)) |
402 \end{array}}} |
480 \end{array}}$ |
403 |
481 \\ |
404 {\ldots} |
482 \bigskip |
|
483 ... |
405 \end{center} |
484 \end{center} |
406 |
485 |
407 \end{itemize} |
486 \end{itemize} |
408 \end{frame} |
487 \end{frame} |
409 |
488 |