Does there exist a polynomial time algorithm to determine whether an equation is a consequence of (x+y)*(y+z)=(x*y)+(y*z)?

Question

Consider the identity $C$ $$(x+y)\times(y+z)=(x\times y)+(y\times z).$$

Is the problem of determining whether an identity is a consequence of $C$ in universal algebra a polynomial time problem? This problem is in PSPACE since if $p=q$ is a consequence of $C$, then the terms $p$ and $q$ must have the same length and $q$ can be obtained from $p$ by just repeatedly replacing the operation $+$ with $\times$ and vice versa.

Algebras that satisfy identity $C$ are precisely the algebraic structures that can be used to produce commuting one-dimensional cellular automata (these cellular automata have two dimensions of time).

Note: We do not assume that the operations $+,\times$ are associative, commutative, or distributive in any way.

1. Moore, Cristopher; Boykett, Timothy. Commuting cellular automata. Complex Systems 11 (1997), no. 1, 55–64.

Answer 1

Yes, this problem is decidable in polynomial time.

Let $R$ denote the term-rewriting system given by reductions of the form $$(r+s)\times(s+u)\longrightarrow(r\times s)+(s\times u).$$ Clearly, $R$ is strongly normalizing: indeed, each reduction step decreases the number of occurrences of $+$ in the term, hence any reduction sequence terminates after at most $n$ steps.

I claim that $R$ is confluent. By Newman's lemma, it sufices to show it is weakly confluent. Thus, consider a pair of single-step reductions $t\to t_0$ and $t\to t_1$; we need to find $t'$ such that $t_0\stackrel{*}{\to}t'$ and $t_1\stackrel*\to t'$. This is easy to do by case analysis of possible redexes. The trivial cases are when the redexes are disjoint (as then we can perform the two reductions in arbitrary order) and when they coincide (as then $t_0=t_1$).

The remaining case is when one redex is strictly contained in the other. Now, this means that one redex is of the form $(r+s)\times(s+u)$, and the other one is a subterm of $r$, $u$, or of one of the two occurrences of $s$. In the first two cases, the two reduction again commute, and we are done. This also works in the third case after we duplicate the second reduction to apply to both occurrences of $s$.

So, each term has a unique $R$-normal form, which can be computed in polynomial time just by applying reductions in arbitrary order until the term becomes reduced. Finally, $t=s$ is a consequence of $C$ if and only if the normal forms of $t$ and $s$ coincide.