سؤال

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

لا يوجد حل صحيح

مرخصة بموجب: CC-BY-SA مع الإسناد
لا تنتمي إلى cs.stackexchange
scroll top