diff -r b797c9a709d9 -r 1c8525061545 ChengsongTanPhdThesis/Chapters/Inj.tex --- a/ChengsongTanPhdThesis/Chapters/Inj.tex Thu Nov 17 23:13:57 2022 +0000 +++ b/ChengsongTanPhdThesis/Chapters/Inj.tex Mon Nov 21 23:56:15 2022 +0000 @@ -387,7 +387,8 @@ returns a new regular expression representing the original regular expression's language $L \; r$ being taken the language derivative with respect to $c$. -\begin{center} +\begin{table} + \begin{center} \begin{tabular}{lcl} $\ZERO \backslash c$ & $\dn$ & $\ZERO$\\ $\ONE \backslash c$ & $\dn$ & $\ZERO$\\ @@ -399,7 +400,10 @@ & & $\mathit{else}\;(r_1\backslash c) \cdot r_2$\\ $(r^*)\backslash c$ & $\dn$ & $(r\backslash c) \cdot r^*$\\ \end{tabular} -\end{center} + \end{center} +\caption{Derivative on Regular Expressions} +\label{table:der} +\end{table} \noindent The most involved cases are the sequence case and the star case. @@ -694,6 +698,7 @@ to indicate that a value $v$ could be generated from a lexing algorithm with input $r$. They call it the value inhabitation relation, defined by the rules. +\begin{figure}[H]\label{fig:inhab} \begin{mathpar} \inferrule{\mbox{}}{\vdash \Char \; c : \mathbf{c}} \hspace{2em} @@ -707,6 +712,8 @@ \inferrule{\forall v \in vs. \vdash v:r \land |v| \neq []}{\vdash \Stars \; vs : r^*} \end{mathpar} +\caption{The inhabitation relation for values and regular expressions} +\end{figure} \noindent The condition $|v| \neq []$ in the premise of star's rule is to make sure that for a given pair of regular