ChengsongTanPhdThesis/Chapters/Cubic.tex
changeset 596 b306628a0eab
parent 594 62f8fa03863e
child 612 8c234a1bc7e0
--- a/ChengsongTanPhdThesis/Chapters/Cubic.tex	Fri Sep 02 19:35:55 2022 +0100
+++ b/ChengsongTanPhdThesis/Chapters/Cubic.tex	Sat Sep 03 00:14:20 2022 +0100
@@ -572,5 +572,32 @@
 %----------------------------------------------------------------------------------------
 
 \section{Bounded Repetitions}
+We define for the $r^{n}$ constructor something similar to $\starupdate$
+and $\starupdates$:
+\begin{center}
+	\begin{tabular}{lcl}
+		$\starupdate \; c \; r \; [] $ & $\dn$ & $[]$\\
+		$\starupdate \; c \; r \; (s :: Ss)$ & $\dn$ & \\
+						     & & $\textit{if} \; 
+						     (\rnullable \; (\rders \; r \; s))$ \\
+						     & & $\textit{then} \;\; (s @ [c]) :: [c] :: (
+						     \starupdate \; c \; r \; Ss)$ \\
+						     & & $\textit{else} \;\; (s @ [c]) :: (
+						     \starupdate \; c \; r \; Ss)$
+	\end{tabular}
+\end{center}
+\noindent
+As a generalisation from characters to strings,
+$\starupdates$ takes a string instead of a character
+as the first input argument, and is otherwise the same
+as $\starupdate$.
+\begin{center}
+	\begin{tabular}{lcl}
+		$\starupdates \; [] \; r \; Ss$ & $=$ & $Ss$\\
+		$\starupdates \; (c :: cs) \; r \; Ss$ &  $=$ &  $\starupdates \; cs \; r \; (
+		\starupdate \; c \; r \; Ss)$
+	\end{tabular}
+\end{center}
+\noindent