On a term rewriting system controlled by sequences of integers (Q2702044)

The main result of this paper is a convergent, i.e., a terminating and confluent, term rewriting system \(R\) for the equational theory axiomatized by the single identity \(x\cdot(y\cdot z)= (x\triangleright y)\cdot(x\cdot z)\), where \(\cdot\) and \(\triangleright\) are binary operation symbols. Each rule in \(R\) corresponds to a finite sequence of integers of a certain kind, and a systematic analysis of the intricate properties of such sequences takes up most of the paper. Since \(R\) is infinite, it does not yet solve the word problem of the equational theory in question, but a possible way out is proposed. The author also shows how the above identity is related to conjugacy closed loops, braid groups and left distributive groupoids indicating then some potential applications of the results of the paper to such structures.NEWLINENEWLINENEWLINERemark: The fact that the quasi-orders defined in Section 3 are very similar to the lexicographic path orders used in term rewriting theory could have been noted and utilized.NEWLINENEWLINEFor the entire collection see [Zbl 0940.00028].