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)


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\} $$

  • $\begingroup$ @MartinSleziak I meant that the document that I am using to solve the problem is Term Rewriting and All That" by Franz Baader and Tobias Nipkow. And that the notions and notation style is from there. $\endgroup$ Sep 10, 2015 at 4:25
  • 1
    $\begingroup$ I am not sure whether this will help you in any way, but searching for "critical pairs" "term rewriting" "group axioms" leads to some slides which talk about the critical points of your system. (Or at least very similar system). See here or here. $\endgroup$
    – Martin
    Sep 10, 2015 at 9:38
  • $\begingroup$ @MartinSleziak, I had a look over the slides, they might be useful at this point, I was king of struggling with the book. I am currently trying some ideas. Thank you for your help. $\endgroup$ Sep 10, 2015 at 10:35

1 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.

  • $\begingroup$ Can we make simplifications like 2.a when talking about Huet's completion procedure? $\endgroup$ Sep 17, 2015 at 4:31
  • $\begingroup$ How do you unify x∘e or x∘i(x) with all of (x∘y)∘z (i.e. using the second ∘) ? $\endgroup$ Sep 17, 2015 at 5:46
  • $\begingroup$ Regarding that simplification, at 2.a, it was done at the class, so it must have some logic behind it. $\endgroup$ Sep 17, 2015 at 11:34
  • $\begingroup$ Were you perhaps treating conditional equation systems, and your axioms included left cancellability ($x*y=x*z\Rightarrow y=z$)? That is the step you do in 2.a, and if justified by an axiom, then you can. Even that would be a shortcut, though - strictly speaking you would first derive the unreduced equation, then get the reduced one via the conditional equation, and then get rid of the unreduced one (because it is subsumed). $\endgroup$ Sep 17, 2015 at 11:39
  • $\begingroup$ I don't know. I thought it had to do with the advanced completion procedure (with which I am not familiar with). Let's assume 2.a is correct, I edited my question to post the new rules I obtained. $\endgroup$ Sep 17, 2015 at 11:44

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.