\documentclass[12pt]{article}
\usepackage{../style}
\usepackage{../langs}
\usepackage{graphicx}

\newtheorem{thm}{Theorem}
\newtheorem{lem}[thm]{Lemma}
\newtheorem{cor}[thm]{Corollary}
\newenvironment{proof}{\paragraph{Proof:}\it}{\hfill$\square$}


\begin{document}


\section*{Antimirov's Proof about Pders}

These are some rough notes about the result by Antimirov establishing
a bound on the number of regular expressions in a partial
derivative. From this bound on the number of partial derivatives one
can easily construct an NFA for a regular expression, but one can also
derive a bound on the size of the partial derivatives. This is what we
do first.  We start with the following definitions:

\begin{itemize}
\item $pder\,c\,r$ --- partial derivative according to a character; this can be defined
  inductively as follows:

  \begin{center}
    \begin{tabular}{l@ {\hspace{2mm}}c@ {\hspace{2mm}}l}
  $\textit{pder}\, c\, (\ZERO)$      & $\dn$ & $\emptyset$\\
  $\textit{pder}\, c\, (\ONE)$         & $\dn$ & $\emptyset$ \\
  $\textit{pder}\, c\, (d)$                & $\dn$ & if $c = d$ then $\{\ONE\}$ else $\emptyset$\\
  $\textit{pder}\, c\, (r_1 + r_2)$        & $\dn$ & $\textit{pder}\, c\, r_1 \;\cup\; \textit{pder}\, c\, r_2$\\
  $\textit{pder}\, c\, (r_1 \cdot r_2)$  & $\dn$  & if $\textit{nullable} (r_1)$\\
  & & then $\Pi\,(\textit{pder}\,c\,r_1)\,r_2 \;\cup\; \textit{pder}\, c\, r_2$\\ 
  & & else $\Pi\,(\textit{pder}\, c\, r_1)\,r_2$\\
  $\textit{pder}\, c\, (r^*)$          & $\dn$ & $\Pi\,(\textit{pder}\,c\,r)\, (r^*)$
  \end{tabular}
\end{center}
  
\item $pder^+\,c\,\,rs$ --- partial derivatives for a set regular exprssions $rs$
\item $pders\,s\,r$ --- partial derivative of a regular expression
  according to a string

\item $Pders\,A\,r \dn \bigcup_{s\in A}. pders\,s\,r$ --- partial
  derivatives according to a language (a set of strings)
\item $|rs|$ is the size of a set of regular expressions $rs$, or
  the number of elements in the
  set (also known as the cardinality of this set)
\item $\prod\,rs\;r \dn \{r_1 \cdot r \;|\; r_1 \in rs\}$ --- this is
  some convenience when writing a set of sequence regular
  expressions. It essentially ``appends'' the regular expression $r$ to all
  regular expressions in the set $rs$. As a result one can write
  the sequence case for partial derivatives (see above) more conveniently 
  as
  \[
    pder\,c\,(r_1\cdot r_2) \dn
    \begin{cases}
      \prod\,(pder\,c\,r_1)\,r_2\;\cup\;pder\,c\,r_2 &
        \!\!\textit{provided}\,r_1\, \textit{is nullable}\\
      \prod\,(pder\,c\,r_1)\,r_2 & \!\!\textit{otherwise}\\
    \end{cases}  
  \]
\item $\textit{Psuf}\,s$ is the set of all non-empty suffixes of $s$ defined as
  \[
  \textit{PSuf}\, s \dn \{v.\;v \not= [] \wedge \exists u. u \,@\, v = s \}  
\]

So for the string $abc$ the non-empty suffixes are $c$, $bc$ and
$abc$.  Also we have that
$\textit{Psuf}\,(s\,@\,[c]) = ((\textit{Psuf}\,s)\,@@\,[c]) \cup
\{[c]\}$. Here $@@$ means to concatenate $[c]$ to the end of
all strings in $\textit{Psuf}\,s$; in this equation  we also
need to add $\{[c]\}$ in order to make the equation to hold.
\end{itemize}  

\noindent
To state Antimirov's result we need the following definition of an
\emph{alphabetic width} of a regular expression defined as follows:

\begin{center}
\begin{tabular}{lcl}  
  $awidth(\ZERO)$ & $\dn$ & $0$\\
  $awidth(\ONE)$ & $\dn$ & $0$\\
  $awidth(c)$ & $\dn$ & $1$\\
  $awidth(r_1 + r_2)$     & $\dn$ & $awidth(r_1) + awidth(r_2)$\\
  $awidth(r_1 \cdot r_2)$ & $\dn$ & $awidth(r_1) + awidth(r_2)$\\
  $awidth(r^*)$ & $\dn$ & $awidth(r)$\\
\end{tabular}
\end{center}

\noindent
This function counts how many characters are in a regular expression.
Antimirov's result states

\begin{thm}\label{one}
$\forall\,A\,r\,.\;\;|Pders\;A\;r| \leq awidth(r) + 1$
\end{thm}

\noindent
Note this theorem holds for any set of strings $A$, for example
for the set of all strings, which I will write as $\textit{UNIV}$, and also
for the set $\{s\}$ containing only a single string $s$. Therefore a
simple corollary is 

\begin{cor}
$\forall\,s\,r\,.\;\;|pders\;s\;r| \leq awidth(r) + 1$
\end{cor}

\noindent
This property says that for every string $s$, the number of regular
expressions in the derivative can never be bigger than
$awidth(r) + 1$.  Interestingly we do not show Thm~\ref{one} for all
sets of strings $A$ directly, but rather only for one particular set of
strings which I call $UNIV_1$. It includes all strings except the empty string
(remember $UNIV$ contains all strings).\bigskip

\noindent
Let's try to give below a comprehensible account of Antimirov's proof
of Thm.~\ref{one}---I distictly remember that Antimirov's paper is
great, but pretty incomprehensible for the first 20+ times one reads
that paper.  The proof starts with the following much weaker property
about the size being finite:

\begin{lem}
$\forall\,A\,r\,.\;\;(Pders\;A\;r)$ is a finite set.
\end{lem}

\noindent This lemma is needed because some reasoning steps in
Thm~\ref{one} only work for finite sets, not infinite sets. But let us
skip over the proof of this property at first and let us assume we
know already that the partial derivatives are always finite sets (this for
example does not hold for unsimplified Brzozowski derivatives which
can be infinite for some sets of strings).

There are some central lemmas about partial derivatives for $\cdot$ and $\_^*$.
One is the following

\begin{lem}\label{central}\mbox{}\\
  \[Pders\,UNIV_1\,(r_1\cdot r_2) \subseteq (\prod (Pders\,UNIV_1\, r_1)\,r_2) \;
  \cup \; Pders\,UNIV_1\,r_2\]
\end{lem}  

\begin{proof}
  \noindent The proof is done via an induction for the following property
  \[
  pders\,s\,(r_1\cdot r_2) \subseteq (\prod (pders\,s\, r_1)\,r_2) \;
  \cup \; Pders\,(\textit{PSuf}\,s)\,r_2
  \]

  \noindent
  Note that this property uses $pders$ and $Pders$ together. The proof is done
  by ``reverse'' induction on $s$, meaning the cases to analyse are the
  empty string $[]$ and the case where a character is put at the end of the
  string $s$, namely $s \,@\, [c]$. The case $[]$ is trivial. In the other
  case we know by IH that

   \[
  pders\,s\,(r_1\cdot r_2) \subseteq (\prod (pders\,s\, r_1)\,r_2) \;
  \cup \; Pders\,(\textit{PSuf}\,s)\,r_2
  \]

  \noindent
  holds for $s$. Then we have to show it holds for $s\,@\,[c]$

  \begin{center}
  \begin{tabular}{r@{\hspace{2mm}}ll}
        & $pders\,(s\,@\,[c])\,(r_1\cdot r_2)$\\
    $=$ & $pder^+\,c\,(pders\,s\,(r_1\cdot r_2))$\\
    $\subseteq$ & $pder^+\,c\,(\prod (pders\,s\, r_1)\,r_2 \;
                  \cup \; Pders\,(\textit{PSuf}\,s)\,r_2)$\\
    & \hfill{}by IH\\
    $=$ & $(pder^+\,c\,(\prod (pders\,s\, r_1)\,r_2))\;\cup\;
          (pder^+\,c\,(Pders\,(\textit{PSuf}\,s)\,r_2))$\\
    $=$ & $(pder^+\,c\,(\prod (pders\,s\, r_1)\,r_2))\;\cup\;
          (Pders\,(\textit{PSuf}\,(s\,@\,[c]))\,r_2)$\\
    $\subseteq$ &
                  $(pder^+\,c\,(\prod (pders\,s\, r_1)\,r_2))\;\cup\;
                  (pder\,c\,r_2)\;\cup\;
                  (Pders\,(\textit{PSuf}\,s\,@@\,[c])\,r_2)$\\
    $\subseteq$ & $\prod (pder^+\,c\,(pders\,s\, r_1))\,r_2\;\cup\;
                  (pder\,c\,r_2)\;\cup\;
                  (Pders\,(\textit{PSuf}\,s\,@@\,[c])\,r_2)$\\
    $=$ & $(\prod (pders\,(s\,@\,[c])\, r_1)\,r_2)\;\cup\;
                  (pder\,c\,r_2)\;\cup\;
    (Pders\,(\textit{PSuf}\,s\,@@\,[c])\,r_2)$\\
    $\subseteq$ & $(\prod (pders\,(s\,@\,[c])\, r_1)\,r_2)\;\cup\;
    (Pders\,(\textit{PSuf}\,(s\,@\,[c]))\,r_2)$\\
  \end{tabular}    
  \end{center}

  \noindent The lemma now follows because for an $s \in UNIV_1$ it holds that

  \[
    \prod\,(pders\,s\,r_1)\,r_2 \subseteq \prod (Pders\,UNIV_1\, r_1)\,r_2
  \]

  \noindent and

  \[
    Pders\,(\textit{PSuf}\,s)\,r_2 \subseteq Pders\,UNIV_1\,r_2
  \]

  \noindent The left-hand sides of the inclusions above are
  euqal to $pders\,s\,(r_1\cdot r_2)$ for a string $s\in UNIV_1$.
\end{proof}\medskip

\noindent There is a similar lemma for the $^*$-regular expression, namely:

\begin{lem}\label{centraltwo}
$Pders\,UNIV_1\,(r^*) \subseteq \prod\, (Pders\,UNIV_1\,r)\,(r^*)$
\end{lem}  

\noindent 
We omit the proof for the moment (similar to Lem~\ref{central}). We
also need the following property about the cardinality of $\prod$:

\begin{lem}\label{centralthree}
  $|\prod\,(Pders\,A\,r_1)\,r_2| \le |Pders\,A\,r_1|$
\end{lem}  

\noindent
We only need the $\le$ version, which essentially says there
are as many sequences $r\cdot r_2$ as are elements in $r$. Now
for the proof of Thm~\ref{one}: The main induction in
Antimirov's proof establishes that:\footnote{Remember that it is
  always the hardest part in an induction proof to find the right
  property that is strong enough and of the right shape for the
  induction to go through.}

\begin{lem}\label{two}
$\forall r.\;\;|Pders\;UNIV_1\;r| \leq awidth(r)$
\end{lem}

\begin{proof} This is proved by induction on
  $r$. The interesting cases are $r_1 + r_2$, $r_1\cdot r_2$ and
  $r^*$. Let us start with the relatively simple case:\medskip

\noindent  
\textbf{Case $r_1 + r_2$:} By induction hypothesis we know

\begin{center}
\begin{tabular}{l}
  $|Pders\;UNIV_1\;r_1| \leq awidth(r_1)$\\
  $|Pders\;UNIV_1\;r_2| \leq awidth(r_2)$
\end{tabular}    
\end{center}  

\noindent
In this case we can reason as follows

\begin{center}
\begin{tabular}{r@{\hspace{2mm}}ll}
  & $|Pders\;UNIV_1\;(r_1+r_2)|$\\
  $=$ & $|(Pders\;UNIV_1\;r_1) \;\cup\; (Pders\;UNIV_1\;r_2)|$\\
  $\leq$ & $|(Pders\;UNIV_1\;r_1)| \;+\; |(Pders\;UNIV_1\;r_2)|$ & (*)\\
  $\leq$ & $awidth(r_1) + awidth(r_2)$\\
  $\dn$ & $awidth(r_1 + r_2)$
\end{tabular}    
\end{center}  

\noindent Note that (*) is a step that only works if one knows that
$|(Pders\;UNIV_1\;r_1)|$ and so on are finite. The next case is
a bit more interesting:\medskip

\noindent  
\textbf{Case $r_1 \cdot r_2$:} We have the same induction
hypothesis as in the case before. 

\begin{center}
\begin{tabular}{r@{\hspace{2mm}}ll}
  & $|Pders\;UNIV_1\;(r_1\cdot r_2)|$\\
  $\leq$ & $|\prod\,(Pders\;UNIV_1\;r_1)\,r_2\;\cup\; (Pders\;UNIV_1\;r_2)|$
  & by Lem~\ref{central}\\
  $\leq$ & $|\prod\,(Pders\;UNIV_1\;r_1)\,r_2| \;+\; |(Pders\;UNIV_1\;r_2)|$\\
  $\leq$ & $|Pders\;UNIV_1\;r_1| \;+\; |Pders\;UNIV_1\;r_2|$
  & by Lem~\ref{centralthree} \\
  $\leq$ & $awidth(r_1) + awidth(r_2)$\\
  $\dn$ & $awidth(r_1 \cdot r_2)$
\end{tabular}    
\end{center} \medskip

\noindent  
\textbf{Case $r^*$:} Again we have the same induction
hypothesis as in the cases before.

\begin{center}
\begin{tabular}{r@{\hspace{2mm}}ll}
  & $|Pders\;UNIV_1\;(r^*)|$\\
  $\leq$ & $|\prod\,(Pders\;UNIV_1\;r)\,(r^*)|$
  & by Lem~\ref{centraltwo}\\
  $\leq$ & $|Pders\;UNIV_1\;r|$
  & by Lem~\ref{centralthree} \\
  $\leq$ & $awidth(r)$\\
\end{tabular}    
\end{center}  
\end{proof}\bigskip  

\noindent
From this lemma we can derive the next corrollary which extends
the property to $UNIV$ ($= UNIV_1 \cup \{[]\}$):

\begin{cor}
$\forall r.\;\;|Pders\;UNIV\;r| \leq awidth(r) + 1$
\end{cor}

\begin{proof} This can be proved as follows
\begin{center}
\begin{tabular}{r@{\hspace{2mm}}ll}
  & $|Pders\;UNIV\;r|$\\
  $=$ & $|Pders\;(UNIV_1 \cup \{[]\})\;r|$\\
  $=$ & $|(Pders\;UNIV_1\,r) \;\cup\;\{r\}|$\\
  $\leq$ & $|Pders\;UNIV_1\,r| + 1$ & by Lem~\ref{two}\\
  $\leq$ & $awidth(r) + 1$\\
\end{tabular}    
\end{center}  
\end{proof}

\noindent
From the last corollary, it is easy to infer Antimirov's
Thm~\ref{one}, because

\[ Pders\,A\,r \subseteq Pders\,UNIV\,r \]


\noindent
for all sets $A$.\bigskip

\noindent
While I was earlier a bit dismissive above about the intelligibility
of Antimirov's paper, you have to admit this proof is a work of
beauty. It only gives a bound (\textit{awidth}) for the number of
regular expressions in the de\-rivatives---this is important for
constructing NFAs.  Maybe it has not been important before, but I have
never seen a result about the \emph{size} of the partial
derivatives.\footnote{Update: I have now seen a paper which proves
  this result as well.}  However, a very crude bound, namely
$(size(r)^2 + 1) \times (awidth(r) + 1)$, can be easily derived by
using Antimirov's result. The definition we need for this is a
function that collects subexpressions from which partial derivatives
are built:


\begin{center}
\begin{tabular}{lcl}  
  $subs(\ZERO)$ & $\dn$ & $\{\ZERO\}$\\
  $subs(\ONE)$ & $\dn$ & $\{\ONE\}$\\
  $subs(c)$ & $\dn$ & $\{c, \ONE\}$\\
  $subs(r_1 + r_2)$     & $\dn$ & $\{r_1 + r_2\}\,\cup\,subs(r_1) \,\cup\, subs(r_2)$\\
  $subs(r_1 \cdot r_2)$ & $\dn$ & $\{r_1 \cdot r_2\}\,\cup (\prod\,subs(r_1)\;r_2)\,\cup \,
                                  subs(r_1) \,\cup\, subs(r_2)$\\
  $subs(r^*)$ & $\dn$ & $\{r^*\}\,\cup\,(\prod\,subs(r)\;r^*) \,\cup\, subs(r)$\\
\end{tabular}
\end{center}

\noindent
We can show that

\begin{lem}
$pders\,s\,r \subseteq subs(r)$
\end{lem}  

\noindent
This is a relatively simple induction on $r$. The point is that for every element
in $subs$, the maximum size is given by

\begin{lem}
  If $r' \in subs(r)$ then $size(r') \le 1 + size(r)^2$.
\end{lem}  

\noindent
Again the proof is a relatively simple induction on $r$. Stringing Antimirov's result
and the lemma above together gives

\begin{thm}
$\sum_{r' \in pders\,s\,r}.\;size(r') \le (size(r)^2 + 1) \times (awidth(r) + 1)$
\end{thm}  

\noindent
Since $awidth$ is always smaller than the $size$ of a regular expression,
one can also state the bound as follows:

\[
\sum_{r' \in pders\,s\,r}.\;size(r') \le (size(r) + 1)^3
\]  

\noindent
This, by the way, also holds for $Pders$, namely

\[
\sum_{r' \in Pders\,A\,r}.\;size(r') \le (size(r) + 1)^3
\]  

\noindent
for all $r$ and $A$. If one is interested in the height of the partial derivatives, one can derive:

\[
\forall\,r' \in pders\,s\,r.\;height(r') \le height(r) + 1
\]  


\noindent
meaning the height of the partial derivatives is never bigger than
the height of the original regular expression (+1).

\section*{NFA Construction via Antimirov's Partial Derivatives}

Let's finish these notes with the construction of an NFA for a regular
expression using partial derivatives.  As usual an automaton is a
quintuple $(Q, A, \delta, q_0, F)$ where $Q$ is the set of states of
the automaton, $A$ is the alphabet, $q_0$ is the starting state and
$F$ are the accepting states.  For DFAs the $\delta$ is a (partial)
function from state $\times$ character to state. For NFAs it is a
relation between state $\times$ character $\times$ state. The
non-determinism can be seen by the following: consider three
(distinct) states $q_1$, $q_2$ and $q_3$, then the relation can
include $(q_1, a, q_2)$ and $(q_1, a, q_3)$, which means there is a
transition between $q_1$ and both $q_2$ and $q_3$ for the character
$a$.

The Antimirov's NFA for a regular expression $r$ is then
given by the quintuple
\[(PD(r), A, \delta_{PD}, r, F)\]

\noindent
where $PD(r)$ are all the partial
derivatives according to all strings, that is
\[
PD(r) \;\dn\; \textit{Pders}\;\textit{UNIV}\;r
\]

\noindent
Because of the previous proof, we know that this set is finite. We
also see that the states in Antimirov's NFA are ``labelled'' by single
regular expressions.  The starting state is labelled with the original
regular expression $r$. The set of accepting states $F$ is all states
$r'\in F$ where $r'$ is nullable. The relation $\delta_{PD}$ is given by
\[
(r_1, c, r_2)
\]

\noindent
for every $r_1 \in PD(r)$ and $r_2 \in \textit{pder}\,c\,r$. This is
in general a ``non-deterministic'' relation because the set of partial
derivatives often contains more than one element. A nice example of
an NFA constructed via Antimirov's partial derivatives is given in
\cite{IlieYu2003} on Page 378.

The difficulty of course in this construction is to find the set of
partial derivatives according to \emph{all} strings. However, it seem
a procedure that enumerates strings according to size suffices until
no new derivative is found. There are various improvements that apply
clever tricks on how to more efficiently discover this set.


\begin{thebibliography}{999}

\bibitem{IlieYu2003}
  L.~Ilie and S.~Yu,
  \emph{Reducing NFAs by Invariant Equivalences}.
  In Theoretical Computer Science, Volume 306(1--3), Pages 373–-390, 2003.\\
  \url{https://core.ac.uk/download/pdf/82545723.pdf}

\end{thebibliography}






\end{document}


%%% Local Variables: 
%%% mode: latex
%%% TeX-master: t
%%% End: