<?xml version="1.0" encoding="UTF-8"?>

<record version="7" id="11825">
 <title>equivalent regular expressions</title>
 <name>EquivalenceOnRegularExpressions</name>
 <created>2009-06-22 22:27:17</created>
 <modified>2009-06-24 16:35:16</modified>
 <type>Definition</type>
<parent id="2583">regular expression</parent>
 <creator id="3771" name="CWoo"/>
 <author id="3771" name="CWoo"/>
 <classification>
	<category scheme="msc" code="68Q70"/>
	<category scheme="msc" code="20M35"/>
 </classification>
 <preamble>\usepackage{amssymb,amscd}
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{mathrsfs}
\usepackage{multicol}

% used for TeXing text within eps files
%\usepackage{psfrag}
% need this for including graphics (\includegraphics)
%\usepackage{graphicx}
% for neatly defining theorems and propositions
\usepackage{amsthm}
% making logically defined graphics
\usepackage{xypic}
\usepackage{pst-plot}

% define commands here
\newcommand*{\abs}[1]{\left\lvert #1\right\rvert}
\newtheorem{prop}{Proposition}
\newtheorem{thm}{Theorem}
\newtheorem{ex}{Example}
\newcommand{\real}{\mathbb{R}}
\newcommand{\pdiff}[2]{\frac{\partial #1}{\partial #2}}
\newcommand{\mpdiff}[3]{\frac{\partial^#1 #2}{\partial #3^#1}}</preamble>
 <content>Let $\Sigma$ be an alphabet, and $E(\Sigma)$ be the set of all regular expressions over $\Sigma$.  Two expressions $p,q$ are said to be \emph{equivalent}, written $p\equiv q$, if they describe the same language: $L(p)=L(q)$.  

This relation is clearly an equivalence relation on $E(\Sigma)$, and therefore partitions $E(\Sigma)$ into equivalence classes.  Furthermore, if $\cup,\cdot$, and $^*$ are interpreted as operations on $E(\Sigma)$, then it is clear that $\equiv$ respects each of these operations, and so is a congruence relation on $E(\Sigma)$.

Let $E=E(\Sigma)/\equiv$, the set of equivalence classes.  Members of $E$ are denoted $[p]$.  For simplicity, we drop the square brackets around $p$ from now on.

The following identities (in $E$) are easily established: for any $p,q,r\in E$:

\begin{enumerate}
\begin{multicols}{3}{
\item $p\cup q = q\cup p$\\ [-3ex]
\item $p\cup p=  p$\\[-3ex]
\item $p\cup \varnothing = p$ \\[-3ex]
\item $p\cup (q\cup r) = (p\cup q)\cup r$\\[-3ex]
\item $p(qr) = (pq)r$\\[-3ex]
\item $p(q\cup r) = pq \cup pr$\\[-3ex]
\item $(p\cup q)r = pr \cup qr$\\[-3ex]
\item $\varnothing p=\varnothing$\\[-3ex]
\item $p\varnothing=\varnothing$\\[-3ex]
\item $\varnothing^* p = p$\\[-3ex]
\item $p\varnothing^*  = p$\\[-3ex]
\item $pp^*=p^*p$\\[-3ex]
\item $p^*p \cup \varnothing^* = p^*$\\[-3ex]
\item $(p\cup \varnothing^*)^* = p^*$\\[-3ex]
}\end{multicols}
\end{enumerate}
Identities 1,3,4 establish that $E$ is a commutative monoid with $\cup$ as the ``addition'', and $\varnothing$ as the identity.  Likewise, identities 5,10,11 establish that $E$ is a monoid with $\cdot$ as the ``multiplication'', and $\varnothing^*$ as the identity element.  By identities 6 through 9, $E$ with the two operations form a semiring ($\cup$ being the addition and $\cdot$ the multiplication).  Lastly, identity 2 says that $E$ is an idempotent semiring.  

Now, as a idempotent semiring, the binary relation $\le$ such that $p\le q$ iff $p\cup q=q$ (or $L(p)\subseteq L(q)$).  It is not hard to see the following implication:
\begin{equation}
pq\cup r\le q \qquad \mbox{implies} \qquad p^*r \le q.
\end{equation}
Assume the left hand side of the implication.  In other words, $L(pq\cup r)\subseteq L(q)$.  Then $L(p)L(q)\cup L(r)\subseteq L(q)$, which implies that $L(r)\subseteq L(q)$, and $L(p)L(q)\subseteq L(q)$, which, by induction, implies that $L(p)^n L(q)\subseteq L(q)$, and hence $L(p)^+ L(q)\subseteq L(q)$.  Now, $L(p^*r)=L(p)^*L(r)=L(r)\cup L(p)^+L(r) \subseteq L(q)\cup L(p)^+L(q)\subseteq L(q)$.  Hence we arrive at the right hand side of the implication.

This implication, together with identities 12 and 13, show that $E$, with binary operations $\cup,\cdot$ and the unary operation $^*$, is a Kleene algebra.

\textbf{Remarks}.
\begin{enumerate}
\item
If we impose the condition $\varnothing^* \not\le p$, the above implication can be written as 
\begin{equation}
pq\cup r= q \qquad \mbox{implies} \qquad p^*r = q.
\end{equation}
Suppose $x\in L(q)=L(pq\cup r)=L(p)L(q)\cup L(r)$.  We use induction on the length of $x$.  If $|x|=0$, then $x\in L(r)\subseteq L(p)^*L(r)$, since $L(p)$ does not contain the empty word $\lambda$.  Suppose now that $|x|&gt;0$.  Then either $x=yz$ where $y\in L(p)$ and $z\in L(q)$, or $x\in L(r)$.  In the former case, since $y$ is not the empty word by the imposed condition, $z$ is a strictly shorter word than $x$, which, by induction, is in $L(p^*r)=L(p)^*L(r)$.  As a result, $x=yz\in L(p)L(p)^*L(r)\subseteq L(p)^*L(r)$.  In the latter case, we have $x\in L(p)^*L(r)$.  In either case, $x\in L(p^*r)$, and the implication is proved.
\item Regular expressions can be thought of as well-formed formulas in a formal system.  A sentence is of the form $p=q$ where $p,q$ are wffs.  An interpretation of the sentence $p=q$ may be defined as the equation $L(p)=L(q)$.  A sentence is valid if its interpretation is true.  The list of identities above are all valid sentences, and can in fact be thought of as axioms of the system.  There are two rules of inferences: 
\begin{enumerate}
\item formal variable substitution, and 
\item \emph{from $pq\cup r= q$ infer $p^*r = q$}, given that $p\cup \varnothing^*=p$ is not valid (implication 2 above).  
\end{enumerate}
The system is \emph{complete} if all valid sentences may be derived from the axioms by rules of inferences.  We have the following results:
\begin{itemize}
\item If the set of axioms is finite, and (a) as the sole rule of inference, then the system is not complete.
\item However, the system is complete if the (finite) set of axioms above, and both rules (a) and (b) are used.
\item In fact, with (a) and (b), all the axioms we need are 1, 4, 5, 6, 7, 8, 10, 13, 14, and none can be removed to keep the system complete.
\end{itemize}
\end{enumerate}

\begin{thebibliography}{9}
\bibitem{AS} A. Salomaa, {\em Formal Languages}, Academic Press, New York (1973).
\end{thebibliography}</content>
</record>
