
diff -r 83b021fc7d29 -r 569280c1f56c corr_pr_sketch.tex
--- a/corr_pr_sketch.tex	Wed Jul 10 23:16:14 2019 +0100
+++ b/corr_pr_sketch.tex	Sat Jul 13 22:56:31 2019 +0100
@@ -12,238 +12,139 @@
 
 \theoremstyle{lemma}
 \newtheorem{lemma}{Lemma}
-
+\usepackage{amsmath}
 \newcommand{\lemmaautorefname}{Lemma}
 
 \theoremstyle{definition}
  \newtheorem{definition}{Definition}
 \begin{document}
-This is an outline of the structure of the paper with a little bit of flesh in it.
-\section{The Flow of thought process}
-
-
-\begin{definition}{Regular Expressions and values}
-\begin{verbatim}
-TODO
-\end{verbatim}
-\end{definition}
-
-Value is.a parse tree for the regular expression matching the string.
-
-
-
-\begin{definition}{nullable}
-\begin{verbatim}
-TODO
-\end{verbatim}
-\end{definition}
-The idea behind nullable: whether it contains the empty string.
-
-\begin{definition}{derivatives}
-TODO
-
-\end{definition}
-
-This definition can be used for matching algorithm.
-
-\begin{definition}{matcher}
-TODO
-\end{definition}
-
-\begin{definition}{POSIX values}
-TODO
-\end{definition}
-
-\begin{definition}{POSIX lexer algorithm}
-TODO
-\end{definition}
-
-\begin{definition}{POSIX lexer algorithm with simplification}
-TODO
-\end{definition}
-This simplification algorithm is rather complicated as it entangles derivative, simplification and value reconstruction. We need to split the regular expression structure of the information for lexing so that simplifcation only changes the regex but does not destroy the information for reconstructing the resulting value.\\
-
-Introduce regex with auxiliary information:
-
-\begin{definition}{annotated regular expression}
-TODO
-\end{definition}
-
-\begin{definition}{encoding}
-TODO
-\end{definition}
-Encoding translates values into bit codes with some information loss.
-
-\begin{definition}{decoding}
-TODO
-\end{definition}
-Decoding translates bitcodes back into values with the help of regex to recover the structure.\\
-
-During different phases of lexing, we sometimes already know what the value would look like if we match the branch of regex with the string(e.g. a STAR with 1 more iteration, a left/right value), so we can partially encode the value at diffferent phases of the algorithm for later decoding.
-\\
-Examples of such partial encoding:
-
-\begin{definition}{internalise}
-TODO
-\end{definition}
-When doing internalise on ALT:\\
-Whichever branch is chosen, we know exactly the shape of the value, and therefore can get the bit code for such a value: Left corresponds to Z and Right to S
-
-\begin{definition}{bmkeps}
-TODO
-\end{definition}
-bmkeps on the STAR case:\\
-We know there could be no more iteration for a star if we want to get a POSIX value for an empty string, so the value must be Stars [], corresponding to an S in the bit code.
-
-\begin{definition}{bder}
-TODO
-\end{definition}
-SEQ case with the first regex nullable:\\
-bmkeps will extract the value for how a1 mathces the empty string and encode it into a bit sequence.
-
-\begin{definition}{blexer}
-\begin{verbatim}
-TODO
-\end{verbatim}
-\end{definition}
-
-adding simplifcation.\\
-
-size of simplified regex: smaller than Antimirov's pder.\\
-
-
-
-The rest of the document is the residual from a previous doc and may be deleted.\\
-\begin{definition}{bsimp}
-\begin{verbatim}
-  def bsimp(r: ARexp): ARexp = r match {
-    case ASEQ(bs1, r1, r2) => (bsimp(r1), bsimp(r2)) match {
-        case (AZERO, _) => AZERO
-        case (_, AZERO) => AZERO
-        case (AONE(bs2), r2s) => fuse(bs1 ++ bs2, r2s)
-        case (r1s, r2s) => ASEQ(bs1, r1s, r2s)
-    }
-    case AALTS(bs1, rs) => {
-      val rs_simp = rs.map(bsimp)
-      val flat_res = flats(rs_simp)
-      val dist_res = distinctBy(flat_res, erase)
-      dist_res match {
-        case Nil => AZERO
-        case s :: Nil => fuse(bs1, s)
-        case rs => AALTS(bs1, rs)  
-      }
-    }
-    //case ASTAR(bs, r) => ASTAR(bs, bsimp(r))
-    case r => r
-  }
-\end{verbatim}
-\end{definition}
-
-\begin{definition}{sub-parts of bsimp}
-\begin{itemize}
-\item{flats}\\
-flattens the list.
-\item{dB}\\
-means distinctBy
-\item{Co}\\
-The last matching clause of the function bsimp, with a slight modification to suit later reasoning.
-\begin{verbatim}
-def Co(bs1, rs): ARexp = {
-      rs match {
-        case Nil => AZERO
-        case s :: Nil => fuse(bs1, s)
-        case rs => AALTS(bs1, rs)  
-      }
-\end{verbatim}
-\end{itemize}
-\end{definition}
-
-\begin{definition}{fuse}
-\begin{verbatim}
-  def fuse(bs: Bits, r: ARexp) : ARexp = r match {
-    case AZERO => AZERO
-    case AONE(cs) => AONE(bs ++ cs)
-    case ACHAR(cs, f) => ACHAR(bs ++ cs, f)
-    case AALTS(cs, rs) => AALTS(bs ++ cs, rs)
-    case ASEQ(cs, r1, r2) => ASEQ(bs ++ cs, r1, r2)
-    case ASTAR(cs, r) => ASTAR(bs ++ cs, r)
-  }
-\end{verbatim}
-\end{definition}
-
-
-\begin{definition}{mkepsBC}
-\begin{verbatim}
-  def mkepsBC(r: ARexp) : Bits = r match {
-    case AONE(bs) => bs
-    case AALTS(bs, rs) => {
-      val n = rs.indexWhere(bnullable)
-      bs ++ mkepsBC(rs(n))
-    }
-    case ASEQ(bs, r1, r2) => bs ++ mkepsBC(r1) ++ mkepsBC(r2)
-    case ASTAR(bs, r) => bs ++ List(Z)
-  }
-\end{verbatim}
-\end{definition}
-
-\begin{definition}{mkepsBC equicalence}
-\\
-Given 2 nullable annotated regular expressions r1, r2, if mkepsBC(r1) == mkepsBC(r2)
-then r1 and r2 are mkepsBC equivalent, denoted as r1 $\sim_{m\epsilon}$ r2
-\end{definition}
-
-\begin{definition}{shorthand notation for ders}
-\\For the sake of reducing verbosity, we sometimes use the shorthand notation
-$d_{c}(r)$ for the function application bder(c, r) and $s(r)$(s here stands for simplification) for the function application bsimp(r) .
-\\We omit the subscript when it is clear from context what that character is and write $d(r)$ instead of $d_{c}(r)$. 
-\\And we omit the parentheses when no confusion can be caused. For example ders\_simp(c, r) can be written as $s(d_{c}(r))$ or even $s d r$ as we know the derivative operation is w.r.t the character c. Here the s and d are more like operators that take an annotated regular expression as an input and return an annotated regular expression as an output
-
-\end{definition}
-
-
-
-\begin{definition}{distinctBy operation expressed in a different way--how it transforms the list}\\
-Given two lists rs1 and rs2, we define the operation $--$:\\
-$rs1 -- rs2 := [r \in rs1 |  r \notin rs2]$
-Note that the order each term appears in $rs_1 -- rs_2$ is preserved as in the original list.
-\end{definition}
 
 
 \section{Main Result}
 
-\begin{lemma}{simplification function does not simplify an already simplified regex}\label{lma1}\\
-bsimp(r) == bsimp(bsimp(r)) holds for any annotated regular expression r.
+Want to prove 
+\begin{equation}\label{cen}
+\textit{bsimp}(\textit{bder}(c,a)) = \textit{bsimp}(\textit{bder}(c,\textit{bsimp}(a))).
+\end{equation}
+For simplicity, we use $s$ to denote $\textit{bsimp}$ and use $a \backslash c$ or $d \; c \; a $ to denote $\textit{bder}(c,a)$, then we can write the equation we want to prove in the following manner:
+\begin{center}
+$s \; d \; c \; a= s \; d \; c \; s \; a$
+\end{center}
+Specifically, we are interested in the case where $a = a_1+a_2$. The inductive hypothesis is that
+
+\begin{center}
+$s \; d \; c \; a_1= s \; d \; c \; s \; a_1 \;  \textbf{and}  \; s \; d \; c \; a_2= s \; d \; c \; s \; a_2.$
+\end{center}
+\noindent
+We want to prove that the $\textit{LHS}$ of \eqref{cen} is equal to the $\textit{RHS}$ of \eqref{cen}.
+For better readability the bits are ommitted as they don't inhibit the proof process but just adds to the
+nuisance of writing.
+$\textit{LHS}$ can be manipulated successively as follows:
+\begin{center}
+		\begin{tabular}{@{}rrl@{}}
+			%\multicolumn{3}{@{}l}{}\medskip\\
+			$\textit{LHS}$ & $=$  & $s \; (a_1+a_2) \backslash c$\\
+			& $=$ & $s \; (a_1 \backslash c + a_2 \backslash c)$   \\
+			& $\overset{\autoref{lma1}}{=}$ & $s(s(a_1 \backslash c) + s(a_2 \backslash c))$         \\
+			& $\overset{\autoref{lma2}}{=}$ & $s(s(a_1) \backslash c + s(a_2) \backslash c).$\\
+		\end{tabular}
+\end{center}
+$\textit{RHS}$ can be manipulated this way:
+\begin{center}
+		\begin{tabular}{@{}rrl@{}}
+			%\multicolumn{3}{@{}l}{}\medskip\\
+			$\textit{RHS}$ & $=$  & $s \; [(s(a_1+a_2)] \backslash c$\\
+		\end{tabular}
+\end{center}
+If we refer to $s(a_1+a_2)$ as $core$, then we have
+\begin{center}
+		\begin{tabular}{@{}rrl@{}}
+			%\multicolumn{3}{@{}l}{}\medskip\\
+			$\textit{RHS}$ & $=$  & $s \; (core \backslash c)$\\
+		\end{tabular}
+\end{center}
+and then
+\begin{center}
+		\begin{tabular}{@{}rrl@{}}
+			%\multicolumn{3}{@{}l}{}\medskip\\
+			$\textit{core}$ & $=$  & $s \; \textit{ALTS}(bs, a_1+a_2)$\\
+			& $\overset{\mathit{bsimp \; def}}{=}$ & $Li(ALTS(bs, dB(flats(s(a_1)+s(a_2))))$\\	
+		\end{tabular}
+\end{center}
+Here we use $Li$ to refer to the operation that opens up the $\textit{ALTS}$ when it has 1
+element, returns 0 when it has 0 elements or does nothing when 
+there are 2 or more elements in the list $rs$ in $\textit{ALTS}(bs, rs)$(in scala code corresponds to the case clauses).
+
+Now in order to establish that $LHS = RHS$, we need to
+ prove the transformed results we got above
+for $LHS$ and $RHS$ are equal to each other.
+That is,
+\begin{center}
+		\begin{tabular}{@{}rrl@{}}
+			%\multicolumn{3}{@{}l}{}\medskip\\
+			$s(s(a_1) \backslash c + s(a_2) \backslash c)$ & $=$  &  $Li(ALTS(bs, dB(flats(s(a_1)+s(a_2))))$\\	
+		\end{tabular}
+\end{center}
+We shall call the two sides of the above equation $LHS'$ and $RHS'$.
+To prove this equality we just need to consider what $s(a_1)$ and $s(a_2)$ look like.
+There are three interesting possibility for each, namely 
+$s(a_i)$ is an alt, a star or a sequence. Combined that is
+9 possibilities. We just need to investigate each of these 9 possibilities.
+Here we only one of the 9 cases. The others are handled in a similar 
+fashion.
+
+When $s(a_1) = ALTS(bs_1, as_1)$ and $s(a_2) = ALTS(bs_2, as_2)$,
+\begin{center}
+			$\textit{LHS'}$ \\
+			 $=$   \\
+			  $s(ALTS(bs, ALTS(bs_1, as_1) \backslash c
+			+ ALTS(bs_2, as_2) \backslash c))$\\
+			$=$ \\
+			 $s(ALTS(bs, ALTS(bs_1, as_1.map \backslash c )+ ALTS(bs_2,as_2.map \backslash c) )  )$\\
+			 			$\overset{\autoref{lma3}}{=}$ \\
+			 $s(ALTS(bs,  (as_1.map \backslash c ).map(fuse(bs_1))+ (as_2.map \backslash c).map(fuse(bs_2)) )  )$\\
+\end{center} 
+
+And then we deal with $RHS'$:
+$RHS'$\\
+			 			$\overset{\autoref{lma4}}{=}$ \\
+			 $s(ALTS(bs,  (as_1.map \backslash c ).map(fuse(bs_1))++ (as_2.map \backslash c).map(fuse(bs_2)) )  )$\\
+and this completes the proof.
+
+\begin{lemma}{doing simplification in advance to subparts}\label{lma1}\\
+We have that for any annotated regular expressions $a_1 \; a_2$ and bitcode $bs$,\\
+$\textit{bsimp}(\textit{ALTS}(bs, a_1, a_2)) =
+ \textit{bsimp}(\textit{ALTS}(bs, \textit{bsimp}(a_1), \textit{bsimp}(a_2))) $
 \end{lemma}
 
-\begin{lemma}{simp and mkeps}\label{lma2}\\
-When r is nullable, we have that
-mkeps(bsimp(r)) == mkeps(r)
+\begin{lemma}{combination of lemma 1 and inductive hypothesis(from now on use simple notation)}\label{lma2}\\
+We have that for any annotated regular expressions $a_1 \; a_2$ and bitcode $bs$,
+$s(s(a_1 \backslash c) + s(a_2 \backslash c)) = 
+s(s(a_1) \backslash c + s(a_2) \backslash c)$
 \end{lemma}
 
 
 %\begin{theorem}See~\cref{lma1}.\end{theorem}
 %\begin{lemma}\label{lma1}\lipsum[2]\end{lemma}
 
-\begin{lemma}{mkeps equivalence  w.r.t some syntactically different regular expressions(1 ALTS)}\label{lma3}\\
-When one of the 2 regular expressions $s(r_1)$ and $s(r_2)$ is of the form ALTS(bs1, rs1), we have that $ds(ALTS(bs, r1, r2)) \sim_{m\epsilon} d(ALTS(bs, sr_1, sr_2))$
+\begin{lemma}{Spilling out ALTS does not affect simplification result}\label{lma3}\\
+$s(ALTS(bs, ALTS(bs_1, as_1.map \backslash c )+ ALTS(bs_2,as_2.map \backslash c) )  )$\\
+			 			$\overset{\autoref{lma3}}{=}$ \\
+			 $s(ALTS(bs,  (as_1.map \backslash c ).map(fuse(bs_1))+ (as_2.map \backslash c).map(fuse(bs_2)) )  )$\\
 \end{lemma}
-\begin{proof}
-By opening up one of the alts and show no additional changes are made.\\
-Details: $ds(ALTS(bs, r1, r2)) = d Co( bs, dB(flats(sr1, sr2)) )$
-\end{proof}
 
+\begin{lemma}{deleting duplicates does not affect simplification result}\label{lma4}\\
+$s(ALTS(bs,  (as_1.map \backslash c ).map(fuse(bs_1))+ (as_2.map \backslash c).map(fuse(bs_2)) )  )$\\
+$=$\\
+$s(ALTS(bs,  dB((as_1.map \backslash c ).map(fuse(bs_1))+ (as_2.map \backslash c).map(fuse(bs_2)) )  ))$
+\end{lemma}
 
 \begin{lemma}{mkepsBC invariant manipulation of bits and notation}\label{lma7}\\
 ALTS(bs, ALTS(bs1, rs1), ALTS(bs2, rs2)) $\sim_{m\epsilon}$ ALTS(bs, rs1.map(fuse(bs1, \_)) ++ rs2.map(fuse(bs2, \_)) ). \\
 We also use $bs2>>rs2 $ as a shorthand notation for rs2.map(fuse(bs2,\_)).
 \end{lemma}
 
-\begin{lemma}{mkepsBC equivalence w.r.t syntactically different regular expressions(2 ALTS)}\label{lma4}\\
-$sr_1 = ALTS(bs1, rs1)$ and $sr_2 = ALTS(bs2, rs2)$ we have  $  d(sr_1 +sr_2 ) \sim_{m\epsilon} d(ALTS(bs, bs1>>rs1 ++ bs2>>rs2))$ 
-\end{lemma}
-\begin{proof}
-We are just fusing bits inside here, there is no other structural change.
-\end{proof}
+
 
 \begin{lemma}{What does dB do to two already simplified ALTS}\label{lma5}\\
 $d Co(ALTS(bs, dB(bs1>>rs1 ++ bs2>>rs2))) = d Co(ALTS(bs, bs1>>rs1 ++ ((bs2>>rs2)--rs1)        )) $ 




