Un conjunto completo y terminante de reglas para la reescritura de términos en ecuaciones lineales

Question

Recientemente he investigado sobre la reescritura de términos.
Todavía no tengo mucha experiencia y por lo tanto podría haber una respuesta fácil a estas preguntas, pero tenía curiosidad por saber si existe un conjunto de reglas para un sistema de reescritura de términos para ecuaciones lineales que proporcione conmutatividad , asociatividad y distributividad así como integridad y terminación .

He encontrado algunos 'trucos' que utilizan el sistema 'modulo' de conmutación, por ejemplo, pero dado que las 'ecuaciones lineales' son una especificación de este tipo, me parece que tiene que haber un conjunto de reglas finito para cubrir esto.
Por otro lado he encontrado conjuntos de reglas para Grupos (por lo tanto con un solo operador), pero eso no es suficiente en mi caso.
En el papel TeReSe Encontré que

Un término puede representarse como un árbol etiquetado finito, no conmutativo, según la siguiente definición inductiva:

1. Una variable o una constante está representada por el árbol que consta de un solo nodo, etiquetado por la propia variable o constante.
2. El término $F(t_1,\dots,t_n)$ está representado por el árbol cuyo nodo raíz tiene como etiqueta el símbolo $F$ y que tiene como subárboles inmediatos, en orden de izquierda a derecha, los árboles que representan $t_1,\dots,t_n$ . '

Así que usando esta representación de árbol se me ocurrió la idea de evaluar los subárboles como conjuntos. Con esto me refiero a reglas como

1. Si $symb(t) = A:$
   1.1 si $\exists x \in graph(t): symb(x)=A$ entonces $graph(t) \rightarrow graph(t) \backslash \{x \in graph(t)|symb(x)=A\} \cup \{y \in graph(x)| x \in graph(t) \wedge symb(x)=A\}$
   1.2 si $\forall x \in graph(t)~ \exists (-x) \in graph(t)$ entonces $ graph(t) \rightarrow 0$
   1.3 si $\exists x \in graph(t): \exists (-x) \in graph(t)$ entonces $graph(t) \rightarrow t\backslash \{x|(-x) \in graph(t)\}$
   1.4 si $\exists 0 \in graph(t)$ entonces $graph(t) \rightarrow graph(t) \backslash \{0\}$

2. Si $symb(t) = M:$
   2.1 si $\exists x \in graph(t): symb(x)=M$ entonces $graph(t) \rightarrow graph(t) \backslash \{x \in graph(t)|symb(x)=M\} \cup \{y \in graph(x)| x \in graph(t) \wedge symb(x)=M\}$
   2.2 si $\forall x \in graph(t)~ \exists x^{-1} \in graph(t)$ entonces $graph(t) \rightarrow 1$
   2.3 si $\exists x \in graph(t): \exists x^{-1} \in graph(t)$ entonces $t \rightarrow graph(t)\backslash \{x|x^{-1} \in graph(t)\}$
   2.4 si $\exists 1 \in graph(t)$ entonces $graph(t) \rightarrow graph(t) \backslash \{1\}$
   2,5 si $\exists 0 \in graph(t)$ entonces $graph(t) \rightarrow 0$

3. si $\exists !x \in graph(t)$ entonces $t \rightarrow \{x | x \in graph(t) \}$

4. Si $symb(t) = A $ entonces si $\exists x : symb(x) = M \wedge t \in graph(x) $ entonces $graph(t) \rightarrow \{y \rightarrow y~ \cup x\backslash t ~(symb(y) \rightarrow M)|y \in t \}; x \rightarrow t$

donde $symb(t)$ es el símbolo de $t$ , $A$ es la adición, $M$ es la multiplicidad y con $\in$ que significa es un subárbol de .
Tenga en cuenta que las reglas deben procesarse en orden, ya que 1.3 y 2.3 necesitan una comprobación de la regla anterior para no ser eliminadas por completo.
Junto con la ley distributiva, en mi opinión, esto debería resolver mi problema. Mi conjunto de reglas aún no está completo, pero estoy trabajando en él.
En realidad, la ley distributiva parece convertirse en mi mayor problema aquí.
Intenté una aproximación para una regla, pero la notación se vuelve muy poco clara aquí.

Mi pregunta resultante es la siguiente: ¿Existe un conjunto de reglas para ecuaciones lineales (o incluso más complejas) que satisfaga mis requisitos? Si no es así, ¿qué más necesito para completar el conjunto de reglas que me han proporcionado? Como estoy empezando a confundirme con mi propia notación, también me gustaría recibir consejos para mejorarla.

Nota 1: En el papel TeReSe He encontrado

"[...] el pliego de condiciones $E$ que consiste en un único operador binario conmutativo $+$ y una constante $0$ y una única ecuación $x + y = y + x$ . [...] no hay un TRS completo $R$ se puede encontrar para $E$ .'

¿Significa eso que nunca puede haber un TRS completo cuando se cumple la conmutatividad?

Nota 2: El teorema 10.5 del artículo no publicado libremente (G.E. Peterson y M.E. Stickel, Complete sets of reductions for some equational theories, Journal of the ACM, 28, 2, p.233-264, 1981.) podría tener la respuesta para mí, pero no la entiendo. Para completarlo, lo citaré aquí, aunque puede que no sea muy útil para ti debido a que faltan varias definiciones:

Teorema 10.5. Sea $T$ ser un $A,C$ (que significa asociativo y conmutativo) y $R$ un conjunto de reducciones. Entonces $R^e_T$ es $T$ -compatible.

Si lo desea, puedo proporcionar algunas de las definiciones anteriores.

Answer 1

Creo que ahora puedo dar una respuesta a la mayor parte de mi pregunta: ¿Existe un conjunto de reglas para un TRS con los requisitos especificados?

Para ello citaré un artículo que tampoco se ha publicado abiertamente (Siekmann, J., y P. Szabó. "The Undecidability of the DA-Unification Problem". The Journal of Symbolic Logic, vol. 54, no. 2, 1989, pp. 402-414. JSTOR, JSTOR, www.jstor.org/stable/2274856.):

Demostramos que el problema de unificación de DA es indecidible. Es decir, dados dos símbolos de funciones binarias $+$ y $*$ , variables y constantes, es indecidible si dos términos construidos a partir de estos símbolos se pueden unificar siempre que se cumplan los siguientes axiomas DA: $ (x + y) * z = (x * z) + (y * z),\\ x * (y + z) = (x * y) + (x * z),\\ x + (y + z) = (x + y) + z \\ $
Dos términos son unificables en DA (es decir, una ecuación es resoluble en DA) si existen términos que pueden ser sustituidos por sus variables de tal manera que los términos resultantes son iguales en la teoría ecuacional de la teoría DA.
Este es el subconjunto axiomático más pequeño conocido actualmente del décimo problema de Hilbert para el que se ha obtenido un resultado de indecidibilidad.
[...] El décimo problema de Hilbert presentado en el Congreso Internacional de Matemáticos en su discurso de 1900 en París plantea la pregunta de si es decidible si una ecuación polinómica dada es resoluble en enteros positivos; un problema que finalmente se demostró indecidible.

A mi entender, esto demuestra directamente que no puede haber reducciones definidas que garanticen que los términos matemáticamente iguales y representados de forma arbitraria se reduzcan exactamente al mismo término, por lo que no toda ocurrencia ("lógica") de $x + (-x)$ puede ser encontrado y eliminado.

En el futuro es probable que vuelva a trabajar en mi conjunto de reglas mencionado anteriormente, ya que me di cuenta de que no cumple con los requisitos de las reglas de reescritura de términos de todos modos, pero podría ser interesante investigar de todos modos.