A computational problem

There have been a good few interesting talks at GAIA2013 dealing with computation. Peter Jipsen's talk was, as usual, both fun and stimulating; today's talk by David Clark was also well worth listening to.

Talking to Peter today in one of the coffee breaks, I asked him what computational tool is currently unimplemented for universal algebraists that he would like to see. His answer: finite presentations.

To wit: if you are a group theorist, you can use GAP to investigate the following problem: consider the group $$\langle X \| \mathcal{R} \rangle$$ given by a finite presentation. Now, it is a famous theorem that there does not exist an algorithm to determine whether two words in the generators evaluate to the same element; however, GAP tries to get "close" to this, whatever that might precisely mean.

This undecidability comes from the fact that a finitely presented group can still be infinite. But what if we're universal algebraists and we want to look at presentations with respect to a background theory strong enough to guarantee that finitely generated things are finite? Wait! We are universal algebraists, and such theories (called locally finite) are a stock in trade! In particular, presentations are the right tool for theories, like the theory of groups, which are axiomatized by equations.

Problem 1: Given a locally finite variety $\mathcal{V}$ in a finite language, to produce an algorithm which efficiently solves the word problem with respect to finite presentations.

INPUT: 

• a finite set $X = \{x_1, \ldots, x_n \}$ of generators
• a finite set $\mathcal{R} = \{ u_1 = v_1, \ldots, u_\ell = v_\ell \}$ of relators. (Each $u_i$ and $v_i$ is a term built from the variables in $X$.)
• two more terms $a,b$ built from $X$.

OUTPUT:

• "True" if, whenever $\mathbf{A}$ is an algebra in $\mathcal{V}$ generated by elements $x_1, \ldots, x_n$ such that the terms $u_i = v_i$ in $\mathbf{A}$, the elements $a(X)$ and $b(X)$ are equal also,
• "False" otherwise.

However, as stated, I don't know of even a brute-force algorithm that solves Problem 1.

I left something out of the description of this problem, however: how we even told the computer enough about $\mathcal{V}$ to make sense of the problem. I'm not going to remedy that: I don't know what you'd want to give the computer, or what would be reasonable to expect for an arbitrary locally finite variety.

Exercise for the reader 2: Give an algorithm solving problem 1 in the case where we have an algorithm which, given an input $n$, computes the word problem for the free algebra in $\mathcal{V}$ on $n$ generators.

The situation really isn't so bad, however, because we are very seldom actually interested in a completely arbitrary locally finite variety; instead, we're usually interested in varieties of the form $$\mathcal{V} = \mathrm{HSP}(\mathbf{A})$$ that is, algebras $\mathbf{B}$ which can be obtained by starting from some fixed finite algebra $\mathbf{A}$, taking some direct power, then taking a subalgebra, then taking a homomorphic image. (Such varieties are called finitely generated.)

Theorem 3: The free algebra on $n$ generators in $\mathrm{HSP}(\mathbf{A})$ can be found as a subalgebra of $\mathbf{A}^{(A^n)}$ in an algorithmic way.

Sketch of proof: Elements of $\mathbf{A}^{(A^n)}$ should be thought of as functions $f: A^n \rightarrow \mathbf{A}$. The generators we want to use are the functions $$\pi_i: \begin{bmatrix} a_1 \\ \vdots \\ a_n \end{bmatrix} \mapsto a_i \qquad (1 \leq i \leq n)$$ . Now we just have to prove that this works.

Together, Exercise 2 and Theorem 3 give a brute-force algorithm solving Problem 1 if $\mathcal{V}$ is finitely generated. However, it's not a good algorithm.

Problem 1': Give a better algorithm.

Problem 4: Find conditions under which the word problem for $\mathcal{V}$-presentations is polynomial-time. Then find the actual algorithm that works.

Problem 4': Find conditions under which the word problem for $\mathcal{V}$-presentations is in NP.

Problem 5: Implement these algorithms in Python, in UACalc, or in other systems.