Term rewriting; Compute critical pairs

Question

I have tried to solve the following exercise but I got stuck while trying to find all the critical pairs.

I have the following questions:

1. How do I know which critical pair produced a new rule?
2. How do I know I found all the critical pairs?

Let $\Sigma= \left \{ \circ, i, e \right \}$ where $\circ$ is binary, $i$ is unary, and $e$ is a constant. $$ E=\left \{ \begin{gather} ( x \circ y ) \circ z \approx x \circ\left ( y \circ z \right ) \\ x \circ e \approx x \\ x \circ i(x) \approx e \end{gather} \right\} $$

My work so far:

1. $x\circ e >_{\textsf{lpo}} x$   (LPO 1)   $x$ is a variable
   
   $x\circ i(x)>_{\textsf{lpo}} e$   (LPO 2b)   there are no terms in the right hand side
   
   $(x\circ y)\circ z\approx x\circ(y\circ z)$
   
   $s=\circ(\underset{\large s_1}{\circ(x,y)},\underset{\large s_2}{\strut z})\qquad t=\circ (\underset{\large t_1}{x\strut}, \underset{\large t_2}{\circ(y,z)})$     (LPO 2c)
   
   

   • check that $s>t_j$, $j=\overline{1,m}$
     
     $s>_{\textsf{lpo}}t_1$     (LPO 1)
     
     to prove that $s>_{\textsf{lpo}}t_2$ (LPO 2c) we prove that $$s>_{\textsf{lpo}} y \;\;\text{(LPO 1)};\qquad s>_{\textsf{lpo}}z \;\;\text{(LPO 1)};\qquad \circ(x,y)>y\;\;\text{(LPO 1)}$$
   • find $i$ such that $s_i>_{\textsf{lpo}}t_i$     $i=1$ $$\circ(x,y)>_{\textsf{lpo}}x\;\;\text{(LPO 1)}$$

   $(x\circ y)\circ z>_{\textsf{lpo}} x\circ (y\circ z)$
   
   

2. a. $(x\circ y)\circ z\;\rightarrow\; x\circ (y\circ z)$
   
   $x_1\circ e\;\rightarrow\; x_1$
   
   $x\circ y \mathrel{\,=?\,} x_1\circ e$
   
   $\theta\{x \;\leftarrow \;x_1;\; y\;\leftarrow \;e\}$ $$\require{AMScd} \require{cancel} \begin{CD} (x_1\circ e)\circ z @>>> \cancel{x_1}\circ z\\ @VVV @VVV\\ \cancel{x_1}\circ(e\circ z) @>>> e\circ z\approx z \end{CD}\qquad\text{left identity?}$$
   b. $(x\circ y)\circ z\;\rightarrow\; x\circ (y\circ z)$
   
   $e\circ x_1\;\rightarrow\; x_1$
   
   $x\circ y \mathrel{\,=?\,} e\circ x_1$
   
   $\theta\{x \;\leftarrow \;e;\; y\;\leftarrow \;x_1\}$ $$\begin{CD} (e\circ x_1)\circ z @>>> x_1\circ z\\ @VVV @VVV\\ e\circ(x_1\circ z) @>>> ? \end{CD}$$
   c. $(x\circ y)\circ z\;\rightarrow\; x\circ (y\circ z)$
   
   $x_1\circ i(x_1)\;\rightarrow\; e$
   
   $x\circ y \mathrel{\,=?\,} x_1\circ i(x_1)$
   
   $\theta\{x \;\leftarrow \;x_1;\; y\;\leftarrow \;i(x_1)\}$ $$\begin{CD} (x_1\circ i(x_1))\circ z @>>> e\circ z\\ @VVV @VVV\\ x_1\circ(i(x_1)\circ z) @>>> ? \end{CD}$$
   

As a support document I have "Term Rewriting and All That" by Franz Baader and Tobias Nipkow.

(original image here)

EDIT1

After searching for the critical pairs I have the following set of rules(assuming 2.a is corect):

$$ E=\left \{ \begin{gather} ( x \circ y ) \circ z \approx x \circ\left ( y \circ z \right ) \\ x \circ e \approx x \\ x \circ i(x) \approx e \\ x \circ (i(x) \circ y) \approx y \\ x \circ ( y \circ i(x \circ y) ) \approx e \\ e \circ x \approx x \\ e \circ (x \circ y) \approx x \circ y \end{gather} \right\} $$

Answer 1

Before adressing the actual questions, one remark on your work so far: the left cancellation in 2.a. is not correct in general, the critical pair would just be $x\circ(e\circ z) \approx x\circ z$. Consequently, you don't get the critical pair 2.b. The problem with this cancellation is that the equation you get does in general not follow from the axioms you started from; for example, if you are working in the language of rings, you might at some point derive the critical pair $0*x \approx 0*y$, but it would be incorrect to deduce $x\approx y$ (which would mean that you only have a trivial model). No sound rewriting procedure, including Huet's, should allow this reduction.

On the other hand, you are missing the critical pairs you get by unifying (variable-renamed versions of) $x\circ e$ or $x\circ i(x)$ with all of $(x\circ y)\circ z$ (i.e. using the second $\circ$). The resulting critical pairs are

• $x\circ(y\circ e)\leftarrow (x\circ y)\circ e\to x\circ y$, which after reduction becomes the trivial equation $x\circ y\approx x\circ y$, and
• $x\circ(y\circ i(x\circ y))\leftarrow(x\circ y)\circ i(x\circ y)\to e$, which cannot be reduced further and gives the rule $x\circ(y\circ i(x\circ y))\to e$ (assuming that $\circ\triangleright e$ in the precedence $\triangleright$ used to define the LPO, just as you did when orienting $x\circ i(x)\approx e$).

For the basic completion procedure:

1. Whenever you create a critical pair, you reduce both sides as far as possible using the current set of rules. If the resulting normal forms are not equal, you create a new rule. For example, your 2.c. gives a new rule $x\circ(i(x)\circ z)\to e\circ z$. On the other hand, unifying $(x\circ y)\circ z$ with $x_1\circ y_1$ gives the critical pair $(x\circ y)\circ(z\circ z_1)\leftarrow((x\circ y)\circ z)\circ z_1\to(x\circ(y\circ z))\circ z_1$, which can be reduced to the trivial $x\circ(y\circ(z\circ z_1))\approx x\circ(y\circ(z\circ z_1))$ and discarded.
2. Whenever you create a new rule $l\to r$, you must consider all critical pairs between it and the existing rules $l_1\to r_1,\dots,l_n\to r_n$, checking for unifiability of $l$ with each non-variable subterm of $l_i$ and vice versa. Also remember to check for self-overlaps, i.e. unifiability of $l$ with its own subterms, as we did above for associativity. You only stop when all critical pairs of the existing rules have been examined and either produced new rules, or been discarded.

This procedure can be improved quite a bit. In particular, you can use new rules to simplify old ones (and possibly discarding them if they become trivial, meaning they are subsumed by the new rule), and a good heuristic for picking the next critical pair to examine can drastically cut down on the amount of rules.