% 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}. +
−
+
−
+
−
+
−
+
−
%----------------------------------------------------------------------------------------+
−
%	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))+
−