Przepisywanie terminów; Oblicz pary krytyczne

Próbowałem rozwiązać następujące ćwiczenie, ale utknąłem podczas próby znalezienia wszystkich krytycznych par .

Mam następujące pytania:

1. Skąd mam wiedzieć, która para krytyczna stworzyła nową regułę?
2. Skąd mam wiedzieć, że znalazłem wszystkie krytyczne pary?

Niech gdzie jest binarny, jest jednoargumentowy, a jest stałą. $\Sigma= \left \{ \circ, i, e \right \}$$\circ$$i$$e$

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

Moja dotychczasowa praca:

1. $x\circ e >_{\textsf{lpo}} x$   (LPO 1)   jest zmienną   (LPO 2b) po prawej stronie nie ma żadnych terminów strona strony     (LPO 2c)$x$
   
   $x\circ i(x)>_{\textsf{lpo}} e$
   
   $(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)})$
   
   

   • sprawdź, czy ,     (LPO 1), aby udowodnić, że (LPO 2c) that j = ¯ 1 , m s > lpo t 1 s > lpo t 2 s > lpo$s>t_j$$j=\overline{1,m}$
     
     $s>_{\textsf{lpo}}t_1$
     
     $s>_{\textsf{lpo}}t_2$ $$s>_{\textsf{lpo}} y \;\;\text{(LPO 1)};\qquad s>_{\textsf{lpo}}z \;\;\text{(LPO 1)};\qquad \circ(x,y)>y\;\;\text{(LPO 1)}$$
   • znajdź taki, żes i > lpo t i i = 1 ∘ ( x , y ) > lpo$i$$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. za. B. c. x 1 ∘ $(x\circ y)\circ z\;\rightarrow\; x\circ (y\circ z)$
   
   x ∘ $x_1\circ e\;\rightarrow\; x_1$
   
   θ { $x\circ y \mathrel{\,=?\,} x_1\circ e$
   
   ( x 1 ∘ e ) ∘ $\theta\{x \;\leftarrow \;x_1;\; y\;\leftarrow \;e\}$ ( x ∘ y ) ∘

   $$\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?}$$
   e ∘ x $(x\circ y)\circ z\;\rightarrow\; x\circ (y\circ z)$
   
   x ∘ $e\circ x_1\;\rightarrow\; x_1$
   
   θ { $x\circ y \mathrel{\,=?\,} e\circ x_1$
   
   ( e ∘ 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}$$
   x $(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}$$
   

Jako dokument pomocniczy mam „Przepisywanie terminów i wszystko inne” autorstwa Franza Baadera i Tobiasa Nipkowa.

( oryginalny obraz tutaj )

EDYCJA 1

Po wyszukaniu par krytycznych mam następujący zestaw reguł (przy założeniu, że 2.a jest corect):

Zanim odniosę się do rzeczywistych pytań, jedna uwaga na temat dotychczasowej pracy: lewe anulowanie w 2.a. ogólnie nie jest poprawny, krytyczna para to po prostu . W związku z tym nie dostajesz pary krytycznej 2.b. Problem z tym anulowaniem polega na tym, że otrzymane równanie zasadniczo nie wynika z aksjomatów, od których zacząłeś; na przykład, jeśli pracujesz w języku pierścieni, możesz w pewnym momencie wyprowadzić parę krytyczną , ale błędne byłoby wydedukowanie (co oznaczałoby, że masz tylko model trywialny). Żadna procedura przepisywania dźwięku, w tym Hueta, nie powinna pozwolić na tę redukcję.0 ∗ x ≈ 0 ∗ y x ≈ $x\circ(e\circ z) \approx x\circ z$$0*x \approx 0*y$$x\approx y$

Z drugiej strony brakuje kluczowych par, które uzyskuje się przez ujednolicenie (wersje o zmienionych nazwach) lub ze wszystkimi (tj. Za pomocą second ). Wynikowe pary krytyczne tox ∘ i ( x ) ( x ∘ y ) ∘ z $x\circ e$$x\circ i(x)$$(x\circ y)\circ z$$\circ$

• $x\circ(y\circ e)\leftarrow (x\circ y)\circ e\to x\circ y$ , który po zmniejszeniu staje się trywialnym równaniem , i$x\circ y\approx x\circ y$
• $x\circ(y\circ i(x\circ y))\leftarrow(x\circ y)\circ i(x\circ y)\to e$ , którego nie można dalej zmniejszyć i daje regułę (przy założeniu, że w priorytecie służyło do definiowania LPO, tak jak to robiłeś podczas orientacji ).$x\circ(y\circ i(x\circ y))\to e$$\circ\triangleright e$$\triangleright$$x\circ i(x)\approx e$

W przypadku podstawowej procedury wypełniania:

1. Za każdym razem, gdy tworzysz parę krytyczną, redukujesz obie strony tak daleko, jak to możliwe, korzystając z obecnego zestawu reguł. Jeśli wynikowe normalne formularze nie są równe, tworzysz nową regułę. Na przykład twój 2.c. daje nową regułę . Z drugiej strony unifikacja pomocą daje parę krytyczną , które można sprowadzić do trywialnego i odrzucone.( x ∘ y ) $x\circ(i(x)\circ z)\to e\circ z$$(x\circ y)\circ z$$x_1\circ y_1$$(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$$x\circ(y\circ(z\circ z_1))\approx x\circ(y\circ(z\circ z_1))$
2. Za każdym razem, gdy tworzysz nową regułę , musisz wziąć pod uwagę wszystkie krytyczne pary między nią a istniejącymi regułami , sprawdzając unifikowalność z każdym niezmiennym podtermem i nawzajem. Pamiętaj również, aby sprawdzić, czy nakładają się na siebie, tj. Unifikowalność z własnymi subtermami, tak jak zrobiliśmy powyżej dla asocjatywności. Zatrzymujesz się tylko wtedy, gdy wszystkie krytyczne pary istniejących reguł zostały zbadane i albo stworzyły nowe reguły lub zostały odrzucone.$l\to r$$l_1\to r_1,\dots,l_n\to r_n$$l$$l_i$$l$

Procedurę tę można nieco poprawić. W szczególności możesz użyć nowych reguł, aby uprościć stare (i być może odrzucić je, jeśli staną się trywialne, co oznacza, że ​​nowa zasada je obejmuje), a dobra heurystyka wyboru następnej pary krytycznej do zbadania może drastycznie ograniczyć ilość zasad.