530 \end{figure} |
530 \end{figure} |
531 \noindent |
531 \noindent |
532 Given the size difference, it is not |
532 Given the size difference, it is not |
533 surprising that our $\blexersimp$ significantly outperforms |
533 surprising that our $\blexersimp$ significantly outperforms |
534 $\textit{blexer\_SLSimp}$ by Sulzmann and Lu. |
534 $\textit{blexer\_SLSimp}$ by Sulzmann and Lu. |
|
535 Indeed $\blexersimp$ seems to be a correct algorithm that effectively |
|
536 bounds the size of intermediate representations. |
|
537 \marginpar{\em more connecting material to make narration more coherent.} |
|
538 As promised we will use formal proofs to show that our speculation |
|
539 based on these experimental results indeed hold. |
|
540 %intuitions indeed hold. |
535 In the next section we are going to establish that our |
541 In the next section we are going to establish that our |
536 simplification preserves the correctness of the algorithm. |
542 simplification preserves the correctness of the algorithm. |
537 |
543 |
538 |
544 |
539 |
545 \section{Correctness of $\blexersimp$} |
540 |
546 A natural thought would be to directly re-use the formal |
541 \section{Why $\textit{Blexer}$'s Proof Does Not Work} |
547 proof of $\blexer$'s correctness, with some minor modifications |
542 The fundamental reason is we cannot extend the correctness proof of theorem 4 |
548 but keeping the way the induction is done. |
543 because lemma 13 does not hold anymore when simplifications are involved. |
549 However we were not able to find a simple way to re-factor |
|
550 proof of \ref{blexerCorrect} in chapter \ref{Bitcoded1}. |
|
551 |
|
552 \subsection{Why $\textit{Blexer}$'s Proof Does Not Work} |
|
553 The fundamental reason is %we cannot extend the correctness proof of theorem 4 |
|
554 because lemma \ref{retrieveStepwise} does not hold |
|
555 anymore when simplifications are involved. |
544 \marginpar{\em rephrased things \\so why new \\proof makes sense.} |
556 \marginpar{\em rephrased things \\so why new \\proof makes sense.} |
545 %The proof details are necessary materials for this thesis |
557 %The proof details are necessary materials for this thesis |
546 %because it provides necessary context to explain why we need a |
558 %because it provides necessary context to explain why we need a |
547 %new framework for the proof of $\blexersimp$, which involves |
559 %new framework for the proof of $\blexersimp$, which involves |
548 %simplifications that cause structural changes to the regular expression. |
560 %simplifications that cause structural changes to the regular expression. |
567 of the un-optimised bit-coded lexer $\blexer$ in |
579 of the un-optimised bit-coded lexer $\blexer$ in |
568 chapter \ref{Bitcoded1} formalised by Ausaf et al. |
580 chapter \ref{Bitcoded1} formalised by Ausaf et al. |
569 relies crucially on lemma \ref{retrieveStepwise} that says |
581 relies crucially on lemma \ref{retrieveStepwise} that says |
570 any value can be retrieved in a stepwise manner, namely: |
582 any value can be retrieved in a stepwise manner, namely: |
571 \begin{equation}\label{eq:stepwise}%eqref: this proposition needs to be referred |
583 \begin{equation}\label{eq:stepwise}%eqref: this proposition needs to be referred |
572 \vdash v : (r\backslash c) \implies \retrieve \; (r \backslash c) \; v= \retrieve \; r \; (\inj \; r\; c\; v) |
584 \vdash v : ((a_\downarrow) \backslash c) \implies \retrieve \; (a \backslash c) \; v= \retrieve \; a \; (\inj \; (a_\downarrow) \; c\; v) |
573 \end{equation} |
585 \end{equation} |
574 %This no longer holds once we introduce simplifications. |
586 %This no longer holds once we introduce simplifications. |
575 Simplifications are necessary to control the size of derivatives, |
587 The regular expressions $a$ and $a\backslash c$ correspond to the intermediate |
576 but they also destroy the structures of the regular expressions |
588 result before and after the derivative with respect to $c$, and similarly |
577 such that \ref{eq:stepwise} does not hold. |
589 $\inj\; a_\downarrow \; c \; v$ and $v$ correspond to the value before and after the derivative. |
578 |
590 They go in lockstep pairs |
579 |
591 \[ |
580 We want to prove the correctness of $\blexersimp$ which integrates |
592 (a, \; \inj\; a_\downarrow \; c \; v)\; \text{and} \; (a\backslash c,\; v) |
581 $\textit{bsimp}$ by applying it after each call to the derivative: |
593 \] |
|
594 and the structure of annotated regular expression and |
|
595 value within a pair always align with each other. |
|
596 |
|
597 As $\blexersimp$ integrates |
|
598 $\textit{bsimp}$ by applying it after each call to the derivatives function, |
|
599 %Simplifications are necessary to control the size of derivatives, |
|
600 %but they also destroy the structures of the regular expressions |
|
601 %such that \ref{eq:stepwise} does not hold. |
582 \begin{center} |
602 \begin{center} |
583 \begin{tabular}{lcl} |
603 \begin{tabular}{lcl} |
584 $r \backslash_{bsimps} (c\!::\!s) $ & $\dn$ & $(\textit{bsimp} \; (r \backslash\, c)) \backslash_{bsimps}\, s$ \\ |
604 $a \backslash_{bsimps} (c\!::\!s) $ & $\dn$ & $(\textit{bsimp} \; (a \backslash\, c)) \backslash_{bsimps}\, s$ \\ |
585 $r \backslash_{bsimps} [\,] $ & $\dn$ & $r$ |
605 %$r \backslash_{bsimps} [\,] $ & $\dn$ & $r$ |
586 \end{tabular} |
606 \end{tabular} |
587 \begin{tabular}{lcl} |
607 %\begin{tabular}{lcl} |
588 $\textit{blexer\_simp}\;r\,s$ & $\dn$ & |
608 % $\textit{blexer\_simp}\;r\,s$ & $\dn$ & |
589 $\textit{let}\;a = (r^\uparrow)\backslash_{bsimp}\, s\;\textit{in}$\\ |
609 % $\textit{let}\;a = (r^\uparrow)\backslash_{bsimp}\, s\;\textit{in}$\\ |
590 & & $\;\;\textit{if}\; \textit{bnullable}(a)$\\ |
610 % & & $\;\;\textit{if}\; \textit{bnullable}(a)$\\ |
591 & & $\;\;\textit{then}\;\textit{decode}\,(\textit{bmkeps}\,a)\,r$\\ |
611 % & & $\;\;\textit{then}\;\textit{decode}\,(\textit{bmkeps}\,a)\,r$\\ |
592 & & $\;\;\textit{else}\;\textit{None}$ |
612 % & & $\;\;\textit{else}\;\textit{None}$ |
593 \end{tabular} |
613 %\end{tabular} |
594 \end{center} |
614 \end{center} |
595 \noindent |
615 \noindent |
|
616 it becomes a problem to maintain a similar property as \ref{retrieveStepwise}. |
596 Previously without $\textit{bsimp}$ the exact structure of each intermediate |
617 Previously without $\textit{bsimp}$ the exact structure of each intermediate |
597 regular expression is preserved, allowing pairs of inhabitation relations |
618 regular expression is preserved, |
598 in the form $\vdash v : r \backslash c $ and |
619 %allowing pairs of inhabitation relations |
599 $\vdash \inj \; r\; c \; v : r $ to hold in \ref{eq:stepwise}. |
620 %in the form $\vdash v : r \backslash c $ and |
|
621 %$\vdash \inj \; r\; c \; v : r $ to hold in \ref{eq:stepwise}. |
|
622 We can illustrate this using the diagram \ref{fig:inj} in chapter \ref{Inj}, |
|
623 by zooming in to the middle bit involving $r_i$, $r_{i+1}$, $v_i$ and $v_{i+1}$, |
|
624 and adding the bottom row to show how bitcodes encoding the lexing information |
|
625 can be extracted from every pair $(r_i, \; v_i)$: |
|
626 \begin{center} |
|
627 \begin{tikzpicture}[->, >=stealth', shorten >= 1pt, auto, thick] |
|
628 %\node [rectangle ] (1) at (-7, 2) {$\ldots$}; |
|
629 %\node [rectangle, draw] (2) at (-4, 2) {$r_i = _{bs'}(_Za+_Saa)^*$}; |
|
630 %\node [rectangle, draw] (3) at (4, 2) {$r_{i+1} = _{bs'}(_Z(_Z\ONE + _S(\ONE \cdot a)))\cdot(_Za+_Saa)^*$}; |
|
631 %\node [rectangle] (4) at (9, 2) {$\ldots$}; |
|
632 %\node [rectangle] (5) at (-7, -2) {$\ldots$}; |
|
633 %\node [rectangle, draw] (6) at (-4, -2) {$v_i = \Stars \; [\Left (a)]$}; |
|
634 %\node [rectangle, draw] (7) at ( 4, -2) {$v_{i+1} = \Seq (\Alt (\Left \; \Empty)) \; \Stars \, []$}; |
|
635 %\node [rectangle] (8) at ( 9, -2) {$\ldots$}; |
|
636 %\node [rectangle] (9) at (-7, -6) {$\ldots$}; |
|
637 %\node [rectangle, draw] (10) at (-4, -6) {$\textit{bits}_{i} = bs' @ ZZS$}; |
|
638 %\node [rectangle, draw] (11) at (4, -6) {$\textit{bits}_{i+1} = bs'@ ZZS$}; |
|
639 %\node [rectangle] (12) at (9, -6) {$\ldots$}; |
|
640 |
|
641 \node [rectangle ] (1) at (-8, 2) {$\ldots$}; |
|
642 \node [rectangle, draw] (2) at (-5, 2) {$r_i = a_\downarrow$}; |
|
643 \node [rectangle, draw] (3) at (3, 2) {$r_{i+1} = (a\backslash c)_\downarrow$}; |
|
644 \node [rectangle] (4) at (8, 2) {$\ldots$}; |
|
645 \node [rectangle] (5) at (-8, -2) {$\ldots$}; |
|
646 \node [rectangle, draw] (6) at (-5, -2) {$v_i = \inj\; r \; c \; v$}; |
|
647 \node [rectangle, draw] (7) at ( 3, -2) {$v_{i+1} = v$}; |
|
648 \node [rectangle] (8) at ( 8, -2) {$\ldots$}; |
|
649 \node [rectangle] (9) at (-8, -6) {$\ldots$}; |
|
650 \node [rectangle, draw] (10) at (-5, -6) {$\textit{bits}_{i} = bs' @ ZZS$}; |
|
651 \node [rectangle, draw] (11) at (3, -6) {$\textit{bits}_{i+1} = bs'@ ZZS$}; |
|
652 \node [rectangle] (12) at (8, -6) {$\ldots$}; |
|
653 |
|
654 |
|
655 |
|
656 \path (1) edge [] node {} (2); |
|
657 \path (6) edge [] node {} (5); |
|
658 \path (9) edge [] node {} (10); |
|
659 |
|
660 \path (11) edge [] node {} (12); |
|
661 \path (8) edge [] node {} (7); |
|
662 \path (3) edge [] node {} (4); |
|
663 |
|
664 |
|
665 \path (6) edge [dashed,bend right = 30] node {$\retrieve \; a_i \; v_i$} (10); |
|
666 \path (2) edge [dashed,bend left = 48] node {} (10); |
|
667 |
|
668 \path (7) edge [dashed,bend right = 30] node {$\retrieve \; a_{i+1} \; v_{i+1}$} (11); |
|
669 \path (3) edge [dashed,bend left = 45] node {} (11); |
|
670 |
|
671 \path (2) edge [] node {$\backslash c$} (3); |
|
672 \path (2) edge [dashed, <->] node {$\vdash v_i : r_i$} (6); |
|
673 \path (3) edge [dashed, <->] node {$\vdash v_{i+1} : r_{i+1}$} (7); |
|
674 %\path (6) edge [] node {$\vdash v_i : r_i$} (10); |
|
675 %\path (7) edge [dashed, <->] node {$\vdash v_i : r_i$} (11); |
|
676 |
|
677 \path (10) edge [dashed, <->] node {$=$} (11); |
|
678 |
|
679 \path (7) edge [] node {$\inj \; r_{i+1} \; a \; v_i$} (6); |
|
680 |
|
681 % \node [rectangle, draw] (r) at (-6, -1) {$(aa)^*(b+c)$}; |
|
682 % \node [rectangle, draw] (a) at (-6, 4) {$(aa)^*(_{Z}b + _{S}c)$}; |
|
683 % \path (r) |
|
684 % edge [] node {$\internalise$} (a); |
|
685 % \node [rectangle, draw] (a1) at (-3, 1) {$(_{Z}(\ONE \cdot a) \cdot (aa)^*) (_{Z}b + _Sc)$}; |
|
686 % \path (a) |
|
687 % edge [] node {$\backslash a$} (a1); |
|
688 % |
|
689 % \node [rectangle, draw, three sided] (a21) at (-2.5, 4) {$(_{Z}\ONE \cdot (aa)^*)$}; |
|
690 % \node [rectangle, draw, three sided1] (a22) at (-0.8, 4) {$(_{Z}b + _{S}c)$}; |
|
691 % \path (a1) |
|
692 % edge [] node {$\backslash a$} (a21); |
|
693 % \node [rectangle, draw] (a3) at (0.5, 2) {$_{ZS}(_{Z}\ONE + \ZERO)$}; |
|
694 % \path (a22) |
|
695 % edge [] node {$\backslash b$} (a3); |
|
696 % \path (a21) |
|
697 % edge [dashed, bend right] node {} (a3); |
|
698 % \node [rectangle, draw] (bs) at (2, 4) {$ZSZ$}; |
|
699 % \path (a3) |
|
700 % edge [below] node {$\bmkeps$} (bs); |
|
701 % \node [rectangle, draw] (v) at (3, 0) {$\Seq \; (\Stars\; [\Seq \; a \; a]) \; (\Left \; b)$}; |
|
702 % \path (bs) |
|
703 % edge [] node {$\decode$} (v); |
|
704 |
|
705 |
|
706 \end{tikzpicture} |
|
707 %\caption{$\blexer$ with the regular expression $(aa)^*(b+c)$ and $aab$} |
|
708 \end{center} |
|
709 |
600 But $\blexersimp$ introduces simplification after the derivative, |
710 But $\blexersimp$ introduces simplification after the derivative, |
601 making it difficult to align the structures of values and regular expressions. |
711 making it difficult to align the structures of values and regular expressions. |
602 If we change the form of property \ref{eq:stepwise} to |
712 If we change the form of property \ref{eq:stepwise} to |
603 adapt to the needs of $\blexersimp$ the precondition of becomes |
713 adapt to the needs of $\blexersimp$ the precondition of becomes |
604 \[ |
714 \[ |