37 $\llbracket \ACHAR{bs}{c} \rrbracket $ & $\dn$ & $1$\\

    48 	$\llbracket _{bs}\ONE \rrbracket$ & $\dn$ & $1$\\

    38 \end{tabular}

    49 	$\llbracket \ZERO \rrbracket$ & $\dn$ & $1$ \\

    39 \end{center}

    50 	$\llbracket _{bs} r_1 \cdot r_2 \rrbracket$ & $\dn$ & $\llbracket r_1 \rrbracket + \llbracket r_2 \rrbracket + 1$\\

    40 (TODO: COMPLETE this defn and for $rs$)

    51 $\llbracket _{bs}\mathbf{c} \rrbracket $ & $\dn$ & $1$\\

    41 

    52 $\llbracket _{bs}\sum as \rrbracket $ & $\dn$ & $\map \; (\llbracket \_ \rrbracket)\; as   + 1$\\

    42 The size is based on a recursive function on the structure of the regex,

    53 $\llbracket _{bs} a^* \rrbracket $ & $\dn$ & $\llbracket a \rrbracket + 1$

    43 not the bitcodes.

    54 \end{tabular}

    44 Therefore we may as well talk about size of an annotated regular expression 

    55 \end{center}

    45 in their un-annotated form:

    56 

    46 \begin{center}

    57 \noindent

    47 $\asize(a) = \size(\erase(a))$. 

    58 Similarly there is a size function for plain regular expressions:

    48 \end{center}

    49 (TODO: turn equals to roughly equals)

    50 

    51 But there is a minor nuisance here:

    52 the erase function actually messes with the structure of the regular expression:

    55 $\erase(\AALTS{bs}{[]} )$ & $\dn$ & $\ZERO$\\

    61 	$\llbracket \ONE \rrbracket_p$ & $\dn$ & $1$\\

    56 \end{tabular}

    62 	$\llbracket \ZERO \rrbracket_p$ & $\dn$ & $1$ \\

    57 \end{center}

    63 	$\llbracket r_1 \cdot r_2 \rrbracket_p$ & $\dn$ & $\llbracket r_1 \rrbracket_p + \llbracket r_2 \rrbracket_p + 1$\\

    58 (TODO: complete this definition with singleton r in alts)

    64 $\llbracket \mathbf{c} \rrbracket_p $ & $\dn$ & $1$\\

    59 

    65 $\llbracket r_1 \cdot r_2 \rrbracket_p $ & $\dn$ & $\llbracket r_1 \rrbracket_p \; + \llbracket r_2 \rrbracket_p + 1$\\

    66 $\llbracket a^* \rrbracket_p $ & $\dn$ & $\llbracket a \rrbracket_p + 1$

    67 \end{tabular}

    68 \end{center}

    69 

    70 \noindent

    71 The idea of obatining a bound for $\llbracket \bderssimp{a}{s} \rrbracket$

    72 is to get an equivalent form

    73 of something like $\llbracket \bderssimp{a}{s}\rrbracket = f(a, s)$, where $f(a, s)$ 

    74 is easier to estimate than $\llbracket \bderssimp{a}{s}\rrbracket$.

    75 We notice that while it is not so clear how to obtain

    76 a metamorphic representation of $\bderssimp{a}{s}$ (as we argued in chapter \ref{Bitcoded2},

    77 not interleaving the application of the functions $\backslash$ and $\bsimp{\_}$ 

    78 in the order as our lexer will result in the bit-codes dispensed differently),

    79 it is possible to get an slightly different representation of the unlifted versions:

    80 $ (\bderssimp{a}{s})_\downarrow = (\erase \; \bsimp{a \backslash s})_\downarrow$.

    81 This suggest setting the bounding function $f(a, s)$ as 

    82 $\llbracket  (a \backslash s)_\downarrow \rrbracket_p$, the plain size

    83 of the erased annotated regular expression.

    84 This requires the the regular expression accompanied by bitcodes

    85 to have the same size as its plain counterpart after erasure:

    86 \begin{center}

    87 	$\asize{a} \stackrel{?}{=} \llbracket \erase(a)\rrbracket_p$. 

    88 \end{center}

    89 \noindent

    90 But there is a minor nuisance: 

    91 the erase function unavoidbly messes with the structure of the regular expression,

    92 due to the discrepancy between annotated regular expression's $\sum$ constructor

    93 and plain regular expression's $+$ constructor having different arity.

    94 \begin{center}

    95 \begin{tabular}{ccc}

    96 $\erase \; _{bs}\sum [] $ & $\dn$ & $\ZERO$\\

    97 $\erase \; _{bs}\sum [a]$ & $\dn$ & $a$\\

    98 $\erase \; _{bs}\sum a :: as$ & $\dn$ & $a + (\erase \; _{[]} \sum as)\quad \text{if $as$ length over 1}$

    99 \end{tabular}

   100 \end{center}

   101 \noindent

    61  is turned into an $\ZERO$ during the

   103  is turned into a $\ZERO$ during the

    84 $\rerase{\AZERO}$ & $=$ & $\RZERO$\\

   125 $\rerase{\ZERO}$ & $\dn$ & $\RZERO$\\

    85 $\rerase{\ASEQ{bs}{r_1}{r_2}}$ & $=$ & $\RSEQ{\rerase{r_1}}{\rerase{r_2}}$\\

   126 $\rerase{_{bs}\ONE}$ & $\dn$ & $\RONE$\\

    86 $\rerase{\AALTS{bs}{rs}}$ & $ =$ & $ \RALTS{rs}$

   127 	$\rerase{_{bs}\mathbf{c}}$ & $\dn$ & $\RCHAR{c}$\\

    87 \end{tabular}

   128 $\rerase{_{bs}r_1\cdot r_2}$ & $\dn$ & $\RSEQ{\rerase{r_1}}{\rerase{r_2}}$\\

    88 \end{center}

   129 $\rerase{_{bs}\sum as}$ & $\dn$ & $\RALTS{\map \; \rerase{\_} \; as}$\\

    89 %TODO: FINISH definition of rerase

   130 $\rerase{_{bs} a ^*}$ & $\dn$ & $\rerase{a}^*$

   131 \end{tabular}

   132 \end{center}

   133 \noindent

   134 $\rrexp$ give the exact correspondence between an annotated regular expression

   135 and its (r-)erased version:

   136 \begin{lemma}

   137 $\rsize{\rerase a} = \asize a$

   138 \end{lemma}

   139 This does not hold for plain $\rexp$s. 

   140 

    96 $\RALTS{rs} \backslash c$ & $=$ &  $\RALTS{map\; (\_ \backslash c) \;rs}$\\

   147 	$(\RALTS{rs})\; \backslash c$ & $\dn$ &  $\RALTS{\map\; (\_ \backslash c) \;rs}$\\

    98 \end{tabular}

   149 With the new $\rrexp$ datatype in place, one can define its size function,

    99 \end{center}

   150 which precisely mirrors that of the annotated regular expressions:

   100 

   151 \end{tabular}

   101 Now that $\rrexp$s do not have bitcodes on them, we can do the 

   152 \end{center}

   102 duplicate removal without  an equivalence relation:

   153 \noindent

   154 \begin{center}

   155 \begin{tabular}{ccc}

   156 	$\llbracket _{bs}\ONE \rrbracket_r$ & $\dn$ & $1$\\

   157 	$\llbracket \ZERO \rrbracket_r$ & $\dn$ & $1$ \\

   158 	$\llbracket _{bs} r_1 \cdot r_2 \rrbracket_r$ & $\dn$ & $\llbracket r_1 \rrbracket_r + \llbracket r_2 \rrbracket_r + 1$\\

   159 $\llbracket _{bs}\mathbf{c} \rrbracket_r $ & $\dn$ & $1$\\

   160 $\llbracket _{bs}\sum as \rrbracket_r $ & $\dn$ & $\map \; (\llbracket \_ \rrbracket_r)\; as   + 1$\\

   161 $\llbracket _{bs} a^* \rrbracket_r $ & $\dn$ & $\llbracket a \rrbracket_r + 1$

   162 \end{tabular}

   163 \end{center}

   164 \noindent

   165 

   166 \subsection{Lexing Related Functions for $\rrexp$}

   167 Everything else for $\rrexp$ will be precisely the same for annotated expressions,

   168 except that they do not involve rectifying and augmenting bit-encoded tokenization information.

   169 As expected, most functions are simpler, such as the derivative:

   170 \begin{center}

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

   172   $(\ZERO)\,\backslash_r c$ & $\dn$ & $\ZERO$\\  

   173   $(\ONE)\,\backslash_r c$ & $\dn$ &

   174         $\textit{if}\;c=d\; \;\textit{then}\;

   175          \ONE\;\textit{else}\;\ZERO$\\  

   176   $(\sum \;\textit{rs})\,\backslash_r c$ & $\dn$ &

   177   $\sum\;(\textit{map} \; (\_\backslash_r c) \; rs )$\\

   178   $(r_1\cdot r_2)\,\backslash_r c$ & $\dn$ &

   179      $\textit{if}\;\textit{rnullable}\,r_1$\\

   180 					       & &$\textit{then}\;\sum\,[(r_1\,\backslash_r c)\cdot\,r_2,$\\

   181 					       & &$\phantom{\textit{then},\;\sum\,}((r_2\,\backslash_r c))]$\\

   182   & &$\textit{else}\;\,(r_1\,\backslash_r c)\cdot r_2$\\

   183   $(r^*)\,\backslash_r c$ & $\dn$ &

   184       $( r\,\backslash_r c)\cdot

   185        (_{[]}r^*))$

   186 \end{tabular}    

   187 \end{center}  

   188 \noindent

   189 The simplification function is simplified without annotation causing superficial differences.

   190 Duplicate removal without  an equivalence relation:

   105 $\rdistinct{r :: rs}{rset}$ & $=$ & $\textit{if}(r \in \textit{rset}) \; \textit{then} \; \rdistinct{rs}{rset}$\\

   193 	$\rdistinct{[]}{rset} $ & $\dn$ & $[]$\\

   194 $\rdistinct{r :: rs}{rset}$ & $\dn$ & $\textit{if}(r \in \textit{rset}) \; \textit{then} \; \rdistinct{rs}{rset}$\\

   110 

   199 \noindent

   111 

   200 With $\textit{rdistinct}$ one can chain together all the other modules

   112 The reason why these definitions  mirror precisely the corresponding operations

   201 of $\bsimp{\_}$ (removing the functionalities related to bit-sequences)

   113 on annotated regualar expressions is that we can calculate sizes more easily:

   202 and get $\textit{rsimp}$ and $\rderssimp{\_}{\_}$.

   114 

   203 We omit these functions, as they are routine. Please refer to the formalisation

   115 \begin{lemma}

   204 (in file BasicIdentities.thy) for the exact definition.

   116 $\rsize{\rerase a} = \asize a$

   205 With $\rrexp$ the size caclulation of annotated regular expressions'

   117 \end{lemma}

   206 simplification and derivatives can be done by the size of their unlifted 

   118 This lemma says that the size of an r-erased regex is the same as the annotated regex.

   207 counterpart with the unlifted version of simplification and derivatives applied.

   119 this does not hold for plain $\rexp$s due to their ways of how alternatives are represented.

   208 \begin{lemma}

   120 \begin{lemma}

   209 	\begin{itemize}

   210 		\item

   122 \end{lemma}

   212 \item

   123 Putting these two together we get a property that allows us to estimate the 

   124 size of an annotated regular expression derivative using its un-annotated counterpart:

   125 \begin{lemma}

   127 \end{lemma}

   214 \end{itemize}

   215 \end{lemma}

   216 \noindent

   217 In the following content, we will focus on $\rrexp$'s size bound.

   218 We will piece together this bound and show the same bound for annotated regular 

   219 expressions in the end.

   139 \section{preparatory properties for getting a finiteness bound}

   231  \section{Roadmap to a Finiteness Proof}

   232  Now that we have defined the $\rrexp$ datatype, and proven that its size changes

   233  w.r.t derivatives and simplifications mirrors precisely those of annotated regular expressions,

   234  we aim to bound the size of $r \backslash s$ for any $\rrexp$  $r$.

   235 The way we do it is by two steps:

   236 \begin{itemize}

   237 	\item

   238 		First, we rewrite $r\backslash s$ into something else that is easier

   239 		to bound. This step is especially important for the inductive case 

   240 		$r_1 \cdot r_2$ and $r^*$, where the derivative can grow and bloat in a wild way,

   241 		but after simplification they will always be equal or smaller to a form consisting of an alternative

   242 		list of regular expressions $f \; (g\; (\sum rs))$ with some functions applied to it, where each element will be distinct after the function application.

   243 		The functions $f$ and $g$ are usually from $\flts$ $\distinctBy$ and other appearing in $\bsimp{_}$.

   244 		This way we get a different but equivalent way of expressing : $r\backslash s = f \; (g\; (\sum rs))$, we call the

   245 		right hand side the "closed form" of $r\backslash s$.

   246 	\item

   247 		Then, for such a sum  list of regular expressions $f\; (g\; (\sum rs))$, we can control its size

   248 		by estimation, since $\distinctBy$ and $\flts$ are well-behaved and working together would only 

   249 		reduce the size of a regular expression, not adding to it. The closed form $f\; (g\; (\sum rs)) $ is controlled

   250 		by the size of $rs'$, where every element in $rs'$ is distinct, and each element can be described by som e inductive sub-structures (for example when $r = r_1 \cdot r_2$ then $rs'$ will be solely comprised of $r_1 \backslash s'$ and $r_2 \backslash s''$, $s'$ and $s''$ being sub-strings of $s$), which will have a numeric uppder bound according to inductive hypothesis, which controls $r \backslash s$.

   251 \end{itemize}

   252 

   253 \section{Closed Forms}

   254 

   255 \subsection{Basic Properties needed for Closed Forms}

   256 

   257 \subsubsection{$\textit{rdistinct}$'s Deduplicates Successfully}

   258 The $\textit{rdistinct}$ function, as its name suggests, will

   259 remove duplicates according to the accumulator

   260 and leave only one of each different element in a list:

   261 \begin{lemma}

   262 	The function $\textit{rdistinct}$ satisfies the following

   263 	properties:

   264 	\begin{itemize}

   265 		\item

   266 			If $a \in acc$ then $a \notin (\rdistinct{rs}{acc})$.

   267 		\item

   268 			If list $rs'$ is the result of $\rdistinct{rs}{acc}$,

   269 			All the elements in $rs'$ are unique.

   270 	\end{itemize}

   271 \end{lemma}

   272 \begin{proof}

   273 	The first part is by an induction on $rs$.

   274 	The second part can be proven by using the 

   275 	induction rules of $\rdistinct{\_}{\_}$.

   276 	

   277 \end{proof}

   278 

   279 \noindent

   280 $\rdistinct{\_}{\_}$ will cancel out all regular expression terms

   281 that are in the accumulator, therefore prepending a list $rs_a$ with an arbitrary

   282 list $rs$ whose elements are all from the accumulator, and then call $\rdistinct{\_}{\_}$

   283 on the resulting list, the output will be as if we had called $\rdistinct{\_}{\_}$

   284 without the prepending of $rs$:

   285 \begin{lemma}

   286 	If $rs \subseteq rset$, then 

   287 	$\rdistinct{rs@rsa }{acc} = \rdistinct{rsa }{acc}$.

   288 \end{lemma}

   289 \begin{proof}

   290 	By induction on $rs$.

   291 \end{proof}

   292 \noindent

   293 On the other hand, if an element $r$ does not appear in the input list waiting to be deduplicated,

   294 then expanding the accumulator to include that element will not cause the output list to change:

   295 \begin{lemma}

   296 	The accumulator can be augmented to include elements not appearing in the input list,

   297 	and the output will not change.	

   298 	\begin{itemize}

   299 		\item

   300 		If $r \notin rs$, then $\rdistinct{rs}{acc} = \rdistinct{rs}{\{r\} \cup acc}$.

   301 		\item

   302 			Particularly, when $acc = \varnothing$ and $rs$ de-duplicated, we have\\

   303 			\[ \rdistinct{rs}{\varnothing} = rs \]

   304 	\end{itemize}

   305 \end{lemma}

   306 \begin{proof}

   307 	The first half is by induction on $rs$. The second half is a corollary of the first.

   308 \end{proof}

   309 \noindent

   310 The next property gives the condition for

   311 when $\rdistinct{\_}{\_}$ becomes an identical mapping

   312 for any prefix of an input list, in other words, when can 

   313 we ``push out" the arguments of $\rdistinct{\_}{\_}$:

   314 \begin{lemma}

   315 	If $rs_1$'s elements are all unique, and not appearing in the accumulator $acc$, 

   316 	then it can be taken out and left untouched in the output:

   317 	\[\textit{rdistinct}\;  rs_1 @ rsa\;\, acc

   318 	= rs_1@(\textit{rdistinct} rsa \; (acc \cup rs_1)\]

   319 \end{lemma}

   320 

   321 \begin{proof}

   322 By an induction on $rs_1$, where $rsa$ and $acc$ are allowed to be arbitrary.

   323 \end{proof}

   324 \subsubsection{The properties of $\backslash_r$, $\backslash_{rsimp}$, $\textit{Rflts}$ and $\textit{Rsimp}_{ALTS}$} 

   325 We give in this subsection some properties of how $\backslash_r$, $\backslash_{rsimp}$, $\textit{Rflts}$ and $\textit{Rsimp}_{ALTS} $ interact with each other and  with $@$, the concatenation operator.

   326 These will be helpful in later closed form proofs, when

   327 we want to transform the ways in which multiple functions involving

   328 those are composed together

   329 in interleaving derivative and  simplification steps.

   330 

   331 When the function $\textit{Rflts}$ 

   332 is applied to the concatenation of two lists, the output can be calculated by first applying the

   333 functions on two lists separately, and then concatenating them together.

   334 \begin{lemma}

   335 	The function $\rflts$ has the below properties:\\

   336 	\begin{itemize}

   337 		\item

   338 	$\rflts \; (rs_1 @ rs_2) = \rflts \; rs_1 @ \rflts \; rs_2$

   339 \item

   340 	If $r \neq \RZERO$ and $\nexists rs_1. r = \RALTS{rs}_1$, then $\rflts \; (r::rs) = r :: \rflts \; rs$

   341 	\end{itemize}

   342 \end{lemma}

   343 \noindent

   344 \begin{proof}

   345 	By induction on $rs_1$.

   346 \end{proof}

   347 

   348 

   349 

   350 \subsection{A Closed Form for the Sequence Regular Expression}

   351 \begin{quote}\it

   352 	Claim: For regular expressions $r_1 \cdot r_2$, we claim that

   353 	\begin{center}

   354 		$ \rderssimp{r_1 \cdot r_2}{s} = 

   355 	\rsimp{(\sum (r_1 \backslash s \cdot r_2 ) \; :: \;(\map \; \rderssimp{r2}{\_} \;(\vsuf{s}{r_1})))}$

   356 	\end{center}

   357 \end{quote}

   358 \noindent

   359