% Chapter Template

% Main chapter title

\chapter{Correctness of Bit-coded Algorithm with Simplification}

\label{Bitcoded2} % Change X to a consecutive number; for referencing this chapter elsewhere, use \ref{ChapterX}

%Then we illustrate how the algorithm without bitcodes falls short for such aggressive 

%simplifications and therefore introduce our version of the bitcoded algorithm and 

%its correctness proof in 

%Chapter 3\ref{Chapter3}. 

Now we introduce the simplifications, which is why we introduce the 

bitcodes in the first place.

\subsection*{Simplification Rules}

This section introduces aggressive (in terms of size) simplification rules

on annotated regular expressions

to keep derivatives small. Such simplifications are promising

as we have

generated test data that show

that a good tight bound can be achieved. We could only

partially cover the search space as there are infinitely many regular

expressions and strings. 

One modification we introduced is to allow a list of annotated regular

expressions in the $\sum$ constructor. This allows us to not just

delete unnecessary $\ZERO$s and $\ONE$s from regular expressions, but

also unnecessary ``copies'' of regular expressions (very similar to

simplifying $r + r$ to just $r$, but in a more general setting). Another

modification is that we use simplification rules inspired by Antimirov's

work on partial derivatives. They maintain the idea that only the first

``copy'' of a regular expression in an alternative contributes to the

calculation of a POSIX value. All subsequent copies can be pruned away from

the regular expression. A recursive definition of our  simplification function 

that looks somewhat similar to our Scala code is given below:

%\comment{Use $\ZERO$, $\ONE$ and so on. 

%Is it $ALTS$ or $ALTS$?}\\

\begin{center}

  \begin{tabular}{@{}lcl@{}}

  $\textit{simp} \; (_{bs}a_1\cdot a_2)$ & $\dn$ & $ (\textit{simp} \; a_1, \textit{simp}  \; a_2) \; \textit{match} $ \\

   &&$\quad\textit{case} \; (\ZERO, \_) \Rightarrow  \ZERO$ \\

   &&$\quad\textit{case} \; (\_, \ZERO) \Rightarrow  \ZERO$ \\

   &&$\quad\textit{case} \;  (\ONE, a_2') \Rightarrow  \textit{fuse} \; bs \;  a_2'$ \\

   &&$\quad\textit{case} \; (a_1', \ONE) \Rightarrow  \textit{fuse} \; bs \;  a_1'$ \\

   &&$\quad\textit{case} \; (a_1', a_2') \Rightarrow   _{bs}a_1' \cdot a_2'$ \\

  $\textit{simp} \; (_{bs}\sum \textit{as})$ & $\dn$ & $\textit{distinct}( \textit{flatten} ( \textit{map} \; simp \; as)) \; \textit{match} $ \\

  &&$\quad\textit{case} \; [] \Rightarrow  \ZERO$ \\

   &&$\quad\textit{case} \; a :: [] \Rightarrow  \textit{fuse bs a}$ \\

   &&$\quad\textit{case} \;  as' \Rightarrow _{bs}\sum \textit{as'}$\\ 

   $\textit{simp} \; a$ & $\dn$ & $\textit{a} \qquad \textit{otherwise}$   

\end{tabular}    

\end{center}    

\noindent

The simplification does a pattern matching on the regular expression.

When it detected that the regular expression is an alternative or

sequence, it will try to simplify its child regular expressions

recursively and then see if one of the children turns into $\ZERO$ or

$\ONE$, which might trigger further simplification at the current level.

The most involved part is the $\sum$ clause, where we use two

auxiliary functions $\textit{flatten}$ and $\textit{distinct}$ to open up nested

alternatives and reduce as many duplicates as possible. Function

$\textit{distinct}$  keeps the first occurring copy only and removes all later ones

when detected duplicates. Function $\textit{flatten}$ opens up nested $\sum$s.

Its recursive definition is given below:

 \begin{center}

  \begin{tabular}{@{}lcl@{}}

  $\textit{flatten} \; (_{bs}\sum \textit{as}) :: \textit{as'}$ & $\dn$ & $(\textit{map} \;

     (\textit{fuse}\;bs)\; \textit{as}) \; @ \; \textit{flatten} \; as' $ \\

  $\textit{flatten} \; \ZERO :: as'$ & $\dn$ & $ \textit{flatten} \;  \textit{as'} $ \\

    $\textit{flatten} \; a :: as'$ & $\dn$ & $a :: \textit{flatten} \; \textit{as'}$ \quad(otherwise) 

\end{tabular}    

\end{center}  

\noindent

Here $\textit{flatten}$ behaves like the traditional functional programming flatten

function, except that it also removes $\ZERO$s. Or in terms of regular expressions, it

removes parentheses, for example changing $a+(b+c)$ into $a+b+c$.

Having defined the $\simp$ function,

we can use the previous notation of  natural

extension from derivative w.r.t.~character to derivative

w.r.t.~string:%\comment{simp in  the [] case?}

\begin{center}

\begin{tabular}{lcl}

$r \backslash_{simp} (c\!::\!s) $ & $\dn$ & $(r \backslash_{simp}\, c) \backslash_{simp}\, s$ \\

$r \backslash_{simp} [\,] $ & $\dn$ & $r$

\end{tabular}

\end{center}

\noindent

to obtain an optimised version of the algorithm:

 \begin{center}

\begin{tabular}{lcl}

  $\textit{blexer\_simp}\;r\,s$ & $\dn$ &

      $\textit{let}\;a = (r^\uparrow)\backslash_{simp}\, s\;\textit{in}$\\                

  & & $\;\;\textit{if}\; \textit{bnullable}(a)$\\

  & & $\;\;\textit{then}\;\textit{decode}\,(\textit{bmkeps}\,a)\,r$\\

  & & $\;\;\textit{else}\;\textit{None}$

\end{tabular}

\end{center}

\noindent

This algorithm keeps the regular expression size small, for example,

with this simplification our previous $(a + aa)^*$ example's 8000 nodes

will be reduced to just 17 and stays constant, no matter how long the

input string is.

%----------------------------------------------------------------------------------------

%	SECTION common identities

%----------------------------------------------------------------------------------------

\section{Common Identities In Simplification-Related Functions} 

Need to prove these before starting on the big correctness proof.

%-----------------------------------

%	SUBSECTION 

%-----------------------------------

\subsection{Idempotency of $\simp$}

\begin{equation}

	\simp \;r = \simp\; \simp \; r 

\end{equation}

This property means we do not have to repeatedly

apply simplification in each step, which justifies

our definition of $\blexersimp$.

It will also be useful in future proofs where properties such as 

closed forms are needed.

The proof is by structural induction on $r$.

%-----------------------------------

%	SUBSECTION 

%-----------------------------------

\subsection{Syntactic Equivalence Under $\simp$}

We prove that minor differences can be annhilated

by $\simp$.

For example,

\begin{center}

$\simp \;(\simpALTs\; (\map \;(\_\backslash \; x)\; (\distinct \; \mathit{rs}\; \phi))) = 

 \simp \;(\simpALTs \;(\distinct \;(\map \;(\_ \backslash\; x) \; \mathit{rs}) \; \phi))$

\end{center}

%----------------------------------------------------------------------------------------

%	SECTION corretness proof

%----------------------------------------------------------------------------------------

\section{Proof Technique of Correctness of Bit-coded Algorithm with Simplification}

The non-trivial part of proving the correctness of the algorithm with simplification

compared with not having simplification is that we can no longer use the argument 

in \cref{flex_retrieve}.

The function \retrieve needs the structure of the annotated regular expression to 

agree with the structure of the value, but simplification will always mess with the 

structure:

%TODO: after simp does not agree with each other: (a + 0) --> a v.s. Left(Char(a))