Is the word problem decidable for free finitely generated self-square groups?

Question

A self-square group is a group with extra structure, which encodes the fact that the group is isomorphic to its own direct square. To be exact, the group $G$ has a special element $1$, a unary operation of inverse $\operatorname{In}(x)$ or $x^{-1}$, and a binary operation, product, taking the pair $(x,y)$ to $x\cdot y$, all satisfying the usual identities of groups, and in addition two unary operations $L(x)$ and $R(x)$, and a binary operation $*$ taking the pair $(x,y)$ into $x*y$. These satisfy the identities

$L(x) * R(x) = x$ for all $x$,

$L(x * y) = x$ for all $x$, $y$,

$R(x*y) = y$ for all $x$, $y$.

So the function $*$ which maps $G \times G$ to $G$ can be inverted by the function $z$ goes to $(L(z), R(z))$, so we have a bijection between $G \times G$ and $G$. In order to make sure that this mapping and its inverse are isomorphisms, we must require that

$L(x \cdot y) = L(x) \cdot L(y)$,

$R(x \cdot y) = R(x) \cdot R(y)$, and

$(x * y) \cdot (u * v) = (x \cdot u)*(y \cdot v)$.

These identities insure that $L,R$ and $*$ are homomorphisms, so we have an isomorphism between $G \times G$ and $G$.

Since all these equations hold for all elements, we have an equational class or a variety in the sense of universal algebra. Standard theorems now guarantee the existence of free self-square groups, from here on SSG's for short.

Now the question: is the word problem decidable for free finitely generated self-square groups, in particular for the $1$-generator SSG? That is, given two well-formed expressions in $\cdot$, $*$, $\operatorname{In}$, $L$, $R$, $1$, and the variable $x$, can we determine if they represent the same element in the free SSG generated by $x$?

Some comments:

1) Notrivial SSG's exist, eg take the countable direct power of your favorite group. Less trivially, by the work of J.M. Tyrer-Jones, D. Meier, and Baumslag there are finitely generated self-square groups, and some can be found inside fairly easy finitely presented groups. It seems it is an open question whether there are finitely presented groups isomorphic to their direct squares.

2) The idea of encoding a bijection between a set and its direct square using operations and identities was explored by Jónsson and Tarski, and by Higman, who used this idea to study the Thompson group.

3) A self-square group may be finitely generated as a self-square group but not finitely generated as a group. In fact this is usually the case, and in particular it is the case for the free self-square group on one generator.

Answer 1

You can use the identities to move the $*$s up to the top of the syntactic tree.

To see this I have to check that if I have $(a * b)$ and I apply any operation that's not $*$ to it then I can replace it with one in which the star is gone or is higher than it was.

$(a*b)^{-1} = (a^{-1} * b^{-1})$

$(a* b) \cdot c= (a \cdot L(c)) * ( b\cdot R(c))$

$L(a * b) = a$

$R(a * b) = b$

So I can put the expressions in a form where they have a tree of $*$s at the top and the other operations down below. Using $L(x) * R(x)=x$, I can expand both trees of $*$s so that they are the same. Because $*$ is injective (being an isomorphism), it is sufficient to check equality of all the branches coming out of the tree of $*$s.

But this is just checking identity in the free group with two additional operations $L$ and $R$ that are both homomorphisms, which is the same as the free group on the elements that are a sequences of $L$s and $R$s followed by one of the variables.

In fact possibly this shows that you can put elements in canonical form.