I have the following TRS $R$: $$ l_1 = f(g(x)) \to f(x) = r_1 \\ l_2 = g(f(y)) \to g(y) = r_2 $$

I want to know if $R$ is confluent, and whether $g(f(f(x))) \leftrightarrow_R^* g(g(g(x)))$. I have already proven termination.

  1. I use the fact that $t = f(y)$ is a subterm of $l_2$ and can find a substitution $\sigma$ that unifies $t$ with $l_1$, namely $\sigma(y) = g(x)$. This yields critical pair $\langle g(g(x)), g(f(x)) \rangle$.

    I can use similar reasoning to unify $t = g(x)$ with $l_2$ and find critical pair $\langle f(f(y)), f(g(y)) \rangle$.

    Now I wonder whether these critical pairs converge (i.e. whether they are joinable). For example, I consider the former critical pair. If I understand correctly, I need to find whether there exist a $v$ such that $g(g(x)) \to_R^* v \leftarrow_R^ * g(f(x))$.

    However, I do not understand whether I can conclude that they are not joinable since $g(g(x))$ is in normal form and $g(f(x)) \to g(x)$, $g(x) \ne g(g(x))$, or, whether I can rename the second to $g(z)$ and unify. Say, $g(z)\tau = g(g(x))$ for $\tau(z) = g(x)$ and conclude that the critical pair is joinable.

  2. If they are joinable, then $R$ is locally confluent. By Newman's theorem, I have that $R$ is confluent, since $R$ is also terminating. But then $g(f(f(x))) \leftrightarrow_R^* g(g(g(x)))$ iff the normal forms of both side are equal.

    Here I have the same problem, $g(g(g(x)))$ is already in normal form, and $g(f(f(x))) \to g(f(x) \to g(x)$. Strictly speaking these are not equal, or can I rename the latter (to $g(z)$) and conclude they are equal for a substitution $\tau(z) = g(g(x))$?


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.