Word problem for an algebra

Remarks

Solvability does not depend on the choice of the finite presentation of $A$. Suppose that $\mathcal{V}$ is finitely based. Then the set of pairs $(s, t)$ with $s = t$ in $A$ is computably enumerable, by listing all derivations from $R$ and the identities of $\mathcal{V}$. The difficulty is to certify that $s \neq t$. The problem is unsolvable in general. Markov and Post independently gave finitely presented semigroups with unsolvable word problem in 1947. Novikov and Boone gave finitely presented groups with unsolvable word problem for groups. It is solvable in many classes, for example for finitely presented abelian groups and for one-relator groups, the latter by a theorem of Magnus. When the relations together with the identities of $\mathcal{V}$ can be oriented into a finite convergent rewriting system, normal forms solve it.