Finite algebraic envelopes and the Boone–Higman conjecture

1 Introduction

The word problem for a group with a specified finite generating set asks whether a given word in the generators and their inverses represents the identity. It is decidable if an algorithm answers this question for every word. A group is simple here if it is nontrivial and its only normal subgroups are the identity subgroup and the whole group.

An embedding throughout means an injective group homomorphism. In the constructive implication, G is supplied with a finite generating set and a word-problem decider; it need not be finitely presented. Theorem 1.1 resolves the Boone–Higman conjecture positively.

Higman’s embedding theorem characterizes the finitely generated subgroups of finitely presented groups as those admitting a recursively enumerable set of defining relations [10]; see also [1, Theorem A]. Decidability of the word problem is stronger: it supplies an algorithm for both equality and inequality. Boone and Higman characterized this condition by the existence of embeddings

[6, Theorem I]. They asked whether the simple overgroup H could itself be chosen finitely presented [6, p. 43]. The two properties in their theorem belong to different groups, and finite presentation does not in general pass to subgroups. Thompson subsequently obtained a finitely generated simple overgroup with decidable word problem [18]; a later proof appears in [9, Theorem 7.1]. This strengthens the conclusion to finite generation of the simple overgroup, but does not supply its finite presentation.

Positive cases of the conjecture include hyperbolic and contracting self-similar groups [3, Theorem A and Corollary D], Baumslag–Solitar groups and finite-rank free-by-cyclic groups [8, Theorem A], and automorphism groups of finite-rank free groups and mapping class groups of orientable punctured surfaces of finite type [4, Theorem A and Corollary B]. The survey [2] describes further results and the development of the conjecture.

Our principal intermediate result concerns permutation actions. An action on a set X is faithful if only the identity acts trivially, and two-transitive if it is transitive on the ordered pairs of distinct points of X.

The action is designed for the twisted Brin–Thompson construction of Belk and Zaremsky, which embeds an acting group in a simple group [5, Section 3 and Theorem 3.4]. Their original finite-presentation theorem used finitely many orbits on finite subsets of each size and finitely presented finite-set stabilizers [5, Theorem D]. Zaremsky subsequently showed that finite presentation of the acting group, finite generation of point stabilizers, and finitely many orbits on unordered pairs suffice [20, Theorem A and Corollary B]. Two-transitivity supplies the last condition here. We state this criterion precisely in Theorem 2.3; the construction below provides its faithful action and the embedding of the prescribed group.

The proof

The action is affine. Translations move the first point of an ordered pair to zero, so two-transitivity reduces to transitivity of the linear part on nonzero vectors. A simple algebra A provides the required coefficient operations: if 0\ne m\in A, then its identity belongs to AmA, and hence is a finite sum of left and right multiples of m. Elementary row operations can use this identity to move vectors. Finite presentation, however, will come from a different algebra.

Over k=\F_2, we construct a finitely presented algebra B, a simple subalgebra A\subseteq B with its own identity, and an injective nonunital map \phi:B\to B with image in A. The additive direct limit M_\infty=\varinjlim(B,\phi) is the carrier for the action on X=M_\infty^6. Every finite collection of its coordinates lies in one copy of B; advancing once places them in A. Thus simplicity becomes available at a later stage without requiring the finitely presented algebra B itself to be simple.

The coefficient ring R=B\otimes_k B^{\op} acts on B by left and right multiplication. We give an explicit finite presentation of the affine Steinberg group

The Steinberg group maps onto the elementary matrix group \E_6(R), but its kernel is an obstruction to the desired faithful affine action. We remove that entire kernel by a single application of the coefficient map induced by \phi. The key algebraic input consists of two splitting pairs commuting with the coefficient image. Their corner identities give an exact calculation in the Steinberg presentation; no centrality hypothesis on the kernel is needed.

The resulting endomorphism of \Gamma_0 defines a finitely presented mapping torus \Gamma. In its direct-limit description the Steinberg kernel has disappeared, leaving elementary matrices acting on M_\infty^6, together with translations and a stage shift. Simplicity of A gives the nonzero-vector orbit required for two-transitivity. Faithfulness uses two further properties of the algebra construction: a separating vector detects every nonzero coefficient after one advance, and the proper support \phi(1_B)\ne1_B makes the stage shift detectable. The stabilizer of zero is the quotient by the translation subgroup, so it is finitely generated. To embed the original G, we first use an HNN extension to express its elements as controlled commutators; balanced elementary diagonals then place this copy of G in the linear part.

It remains to construct the algebras with these simultaneous properties. We do so through a finitely presented monoid and a decidable monoid that encode one another. A finite presentation is compiled syntactically from a program index, before any totality assertion is available. Its partial evaluator controls the length of every call to the encoded program. Long codes make the calls needed to normalize a word strictly shorter than that word. A fixed-point argument and induction on length then establish totality and compatibility with multiplication. Finite-tuple selectors isolate individual basis terms in a contracted monoid algebra, producing A; a separate separator distinguishes ordered pairs of basis terms, producing the faithful coefficient detector.

The finite-presentation construction follows the machine-encoding tradition of Post and Murskii [15, 17]. Here the bounded evaluator permits the two monoids to be constructed together. The selectors strengthen the contextual-collapse property in the semigroup counterpart of the Boone–Higman theorem [6, pp. 49–52]: isolating each term of a finite linear combination gives the simplicity needed for the affine action.

Section 2 states the algebraic data and gives the HNN reduction. Sections 3–5 construct the action and prove the two theorems from those data. Section 6 constructs the algebras from a precise monoid theorem, proved by bounded self-reference in Section 7. Appendix A gives the full finite compiler and its evaluator proof.

2 The group input and the algebraic data

We first enlarge the input group so that each of its elements is a commutator in the larger group. This will allow us to embed the input group in an elementary matrix group in Section 5. We then state the algebraic construction used in the next three sections. All rings and algebras have identities; a homomorphism explicitly called nonunital is not required to preserve them. Our commutator convention is [a,b]=aba^{-1}b^{-1}.

Here is the algebraic construction. A simple algebra means a nonzero algebra with no proper nonzero two-sided ideal. A subalgebra with identity e need not contain the identity of the ambient algebra; its units are taken relative to e. For an idempotent q\in B, the subalgebra qBq=\{qbq:b\in B\} is called a corner; its identity is q.

Theorem 2.2 is proved in Section 6, using the monoid construction of Section 7 and Appendix A. To see how these data produce an action, regard the elements of R as coefficients for row operations on B^6. Such a coefficient acts on a coordinate by a finite sum of left and right multiplications. Simplicity of A will let a nonzero coordinate produce any prescribed element of A; applying \phi places all coordinates in that subalgebra. Finite presentation of B supplies a finitely presented Steinberg group acting by row operations. The splitting pairs make its matrix kernel disappear under the induced coefficient map, while b_* detects every remaining nonidentity matrix after that map is applied. Finally, the support identity p\ne1_B makes successive vector stages strictly larger, so that shifting stages gives a nontrivial permutation. Sections 3–5 establish these claims and assemble the action.

In particular, p\phi(b)=\phi(b)p=\phi(b), so 1_B\notin\phi(B). The detection condition concerns the action after applying \psi; it does not require the original action of R on B to be faithful.

Apply the theorem with L=\widehat G from Lemma 2.1. For the remainder of Sections 3–5, fix these data. Tensor products are over k. Besides p, define

Tensoring injective linear maps over a field shows that \psi is injective, so P\ne0. Also P\ne1_R, since the nonzero tensor (1_B-p)\otimes1_B annihilates P on the left. The elements U_i,V_i lie in PRP, commute with \psi(R), and satisfy

These identities follow directly from the corresponding identities in B; the second tensor factor is always the idempotent p^{\op}.

The final passage from an action to a simple group uses the following established result, in the precise form needed here.

These are the hypotheses of a type-(A) action in [20, Theorem A and Corollary B]. Finite presentation follows from that theorem; the canonical embedding and simplicity are those of the twisted Brin–Thompson construction [5, Section 3 and Theorem 3.4]. Since X is nonempty, the constructed group contains Thompson’s group V on a coordinate and is nontrivial. Our construction will provide a countably infinite X with one orbit on pairs, and will prove each of the other hypotheses separately.

3 A finitely presented affine group

We now use the algebraic data in Theorem 2.2 to construct a finitely presented group of translations and elementary operations. The translations form the additive group of B^6. We first give their finite presentation relative to a Steinberg group, and then construct the endomorphism used in the next two sections.

3.1 The coefficient ring and the translation module

Put

Thus r=\sum_\nu a_\nu\otimes b_\nu^{\op} acts on B by the operation m\mapsto\sum_\nu a_\nu m b_\nu. The opposite multiplication in the second factor makes composition of these operations agree with multiplication in R, so B is a left R-module. The ring R is finitely presented as a unital associative ring: take a finite algebra presentation of B, a second copy with products reversed, the relations commuting every generator of the first copy with every generator of the second, and 2\cdot1=0. The universal property of the tensor product identifies the resulting ring with R. The module B is generated by 1_B; we next show that the relations on this module generator also have a finite description.

For a unital ring R and n\geq3, the Steinberg group \St_n(R) has generators x_{ab}(r), where 1\leq a\ne b\leq n and r\in R, with relations

Let e_{ab} denote the matrix unit. The map x_{ab}(r)\mapsto I+r e_{ab} gives a surjection

where \E_n(R) is the subgroup of \mathrm{GL}_n(R) generated by these elementary matrices. Krstić and McCool prove that \St_n(R) is finitely presented whenever R is a finitely presented unital associative ring and n\geq4 [13, Theorem 3]. Their theorem permits noncommutative rings, and applies to the ring constructed above.

3.2 A finite relative presentation

The next lemma supplies the additional relations needed for the translations. Finite presentation of the module and of the linear group alone would not establish its conclusion; we prove the semidirect-product presentation explicitly.

3.3 The transition endomorphism

Write \St=\St_6(R), \E=\E_6(R), and \pi=\pi_6:\St\to\E. Recall the injective algebra map \phi:B\to B from Theorem 2.2, and set \psi=\phi\otimes\phi^{\op}:R\to R. This map is injective because tensoring vector spaces over k preserves injections. Both maps may be nonunital.

We have obtained a finite presentation and compatible transition maps. The map \Theta need not be injective: the remaining obstruction lies in the kernel of \pi. The next section proves that \theta annihilates this entire kernel.

4 Annihilating the Steinberg kernel

The affine group of Section 3 uses a Steinberg group, whose matrix action can have a kernel. We now show that the coefficient endomorphism annihilates this entire kernel. The argument uses the splitting pairs from Theorem 2.2, whose elements commute with the coefficient image. It is convenient to state it for an arbitrary unital associative ring.

Recall that \operatorname{St}_6(R) has generators x_{ij}(a), where 1\leq i\ne j\leq6 and a\in R, with relations

Here [u,v]=uvu^{-1}v^{-1}. Let \pi:\operatorname{St}_6(R)\to\operatorname{E}_6(R) send x_{ij}(a) to I+ae_{ij}.

For the binary Leavitt algebra L=L_{\F_2}(1,2), Khanh proves that the natural map \St_r(L)\to\mathrm{GL}_r(L) is an isomorphism for r\ge3 [11, Theorem 5.4]. Theorem 4.1 concerns an arbitrary ring and annihilation of its matrix kernel under the specified coefficient map.

Additivity and multiplicativity make \theta a homomorphism by the defining relations. The map \psi need not preserve the identity. For any additive multiplicative map \lambda:R\to R, the corresponding image of a root word with matrix g has matrix

where \lambda^{(6)} acts entrywise. This follows on generators and then on products by expanding gh-I=(g-I)+(h-I)+(g-I)(h-I). In particular, coefficient maps preserve the condition of having identity matrix. We shall use this for maps whose images lie in smaller idempotent corners of R.

The proof has two parts. First, a word with identity matrix becomes central when all its coefficients are placed in a suitable corner. Second, two orthogonal copies of that corner can be interchanged and split. Four corners suffice to make the resulting central element equal to its square.

4.1 Conjugation with an unused index

The use of an index outside the support of a root word is the classical Steinberg centrality argument; see [19, proof of Theorem III.5.2.1]. We record its row-and-column form to justify the corner conjugations inside the Steinberg group. The kernel-annihilation theorem also uses the corner comparisons and four-corner splitting proved below.

4.2 Interchanging and splitting corners

For a unit a\in R^\times, define

Direct multiplication gives

both matrices are the identity on the other indices.

We can now finish the kernel calculation. The preceding lemmas allow us to compare corner images as group elements, and to split an image over an orthogonal sum without a residual central factor.

For R=B\otimes_k B^{\mathrm{op}} and \psi=\phi\otimes\phi^{\mathrm{op}}, the elements P,U_i,V_i constructed in Section 2 satisfy the support and commutation hypotheses and the pair identities (1). Theorem 4.1 therefore applies to the Steinberg transition of Section 3: it annihilates the matrix kernel in one step.

5 The two-transitive envelope

We now turn the algebraic construction into the required permutation representation. Proposition 3.3 and Lemma 3.4 give the finitely presented group

and its endomorphism \Theta=(\phi^{(6)},\theta). Theorem 4.1 says that \theta kills the kernel of the matrix map. A mapping torus will remove this kernel while retaining finite presentation. We then use the simple subalgebra A\subseteq B to obtain two-transitivity.

5.1 The mapping torus and its linear part

We first record explicitly why a mapping torus has the needed description even when its defining endomorphism is not injective.

Apply Lemma 5.1 to (\Gamma_0,\Theta) and denote the resulting finitely presented group by \Gamma. Put

The transition F is the injective homomorphism of Lemma 3.4; recall the matrix map \pi:\St_6(R)\to\E_6(R).

5.2 A faithful action and two-transitivity

Set X=M_\infty^6. The subgroup M_\infty^6 acts on X by translations, and E_\infty acts by matrices after passing to a common stage, as in (24). Let t act by the forward stage shift. This shift intertwines the matrix actions, so these formulas define an action of \Gamma on X.

5.3 Embedding the input group and finishing the proof

The last step is to put the original group into the elementary matrix part of \Gamma. Here the commutator property of Lemma 2.1 is essential.

6 The algebra construction

We now prove Theorem 2.2. The construction has two parts. A pair of monoids supplies a simple algebra and an embedding into a finitely presented algebra. Partial affine maps then give a corner with two equivalent orthogonal subcorners. A separator in the monoid construction will prove the tensor detection property.

6.1 The monoid input

We first define the auxiliary monoid used in the construction. Let \mathcal P be the monoid of partial maps of \mathbb Q generated by the full affine maps

their inverses, and the partial identities e_0,e_1 on [0,\infty)\cap\mathbb Q and [1,\infty)\cap\mathbb Q, respectively. Composition applies the right-hand factor first. The identity 1_{\mathcal P} is the full identity map.

For a monoid K with zero \Omega\ne1_K, write

The element 0_T is absorbing. Nonzero pairs multiply coordinatewise, except that a product whose K-coordinate is \Omega is replaced by 0_T. Its identity is (1_K,1_{\mathcal P}).

The proof of Theorem 6.2 occupies Section 7, using the finite compiler proved in Appendix A. In the construction, \zeta is the zero symbol and z is the class of a distinct separator letter \mathtt z.

6.2 A simple algebra inside a finitely presented algebra

Throughout this section k=\mathbb F_2. For any monoid D with zero 0_D\ne1_D, its contracted monoid algebra k_0[D] has k-basis D\setminus\{0_D\}. Basis elements multiply as in D, with a product equal to 0_D interpreted as the zero vector. It is a unital algebra, with identity the basis element 1_D.

To prove Theorem 2.2 for a given group L, apply Theorem 6.2 with \widehat G=L and set

Both algebras are nonzero. We distinguish the monoid elements \zeta,\Omega from algebra zero, and distinguish c_{\zeta} from all three: it is a nonzero basis element of B.

The monoid requirements now serve distinct purposes. The selectors in Theorem 6.2(iii) isolate one coefficient of a nonzero element of A_0, forcing simplicity. The maps in (ii) and (iv) provide algebra embeddings in opposite directions, but treat zero differently: \kappa preserves it, whereas the linear extension of c requires a correction by c_{\zeta}. Finally, the separator in (v) keeps the ordered pairs indexing a tensor basis distinct, which will supply the tensor detector.

Identify A=i(A_0)\subseteq B. It is a simple algebra with its own identity e, and Theorem 6.2(i) embeds L in A^\times: a unit of H and its inverse give inverse basis elements in A_0, which i sends to units relative to e. We next construct an injective nonunital endomorphism of B whose image lies in A.

6.3 Two equivalent subcorners

For a dyadic rational a, let e_a denote the partial identity on [a,\infty)\cap\mathbb Q. These maps belong to \mathcal P: u^{-1}v is translation by 1, its powers and conjugates by powers of u give all dyadic translations, and conjugating e_0 by translation by a gives e_a. In the monoid itself,

for every available full increasing affine map w. Thus these are equalities of basis elements in the abstract algebra k[\mathcal P].

We require a nonzero corner that decomposes into two orthogonal copies of itself. The identities in the next lemma have the rectangular-inverse form familiar from Leavitt’s module-type construction [14, Section 3], with the corner idempotent as identity. Here we realize them directly using the partial affine maps above.

Define

These maps are nonunital algebra homomorphisms. The map j is multiplicative because q^2=q, and it is injective because q\ne0 and tensor products are over the field k. Hence \phi is injective and \phi(B)\subseteq A. Let

The idempotent p belongs to A, so p\ne1_B. Applying the two algebra maps to Lemma 6.4 gives

These elements commute with \phi(B). Indeed,

and the identical calculation holds for t'_l; now apply i\rho. Thus the required self-embedding and binary pairs centralizing \phi(B) have been constructed. It remains to verify detection for the tensor action.

6.4 A separating tensor vector

As in Section 3, set R=B\otimes_k B^{\mathrm{op}}, acting on B by (a\otimes b^{\mathrm{op}})m=amb, and define

We need one vector on which \psi(r) acts nontrivially for every r\ne0. The separator gives this simultaneously for all r, by realizing distinct basis tensors as distinct monoid elements.

Let W=\rho(B\otimes_k k[\mathcal P])\subseteq A_0, with basis \{\kappa(\tau):\tau\in T\setminus\{0_T\}\}. Part (v) of Theorem 6.2 proves that the linear map

is injective: it sends distinct basis tensors to distinct nonzero basis elements of A_0. This includes tensors with an identity factor. Since j(B)\subseteq W, the composite

is a sequence of injective linear maps. For r=\sum_{\nu}a_{\nu}\otimes b_{\nu}^{\mathrm{op}}, its value is

Thus b_*=i(z) satisfies

The assertion concerns the action after \psi; its proof uses the explicit separator vector.

7 Coding with a decreasing dependency bound

We prove Theorem 6.2. The two monoids in that theorem must contain information about one another: the finitely presented monoid will multiply representatives of the decidable monoid, while the latter will contain a coded copy of the former. We arrange this using a program whose evaluations on words of length n depend only on its values at strictly smaller lengths. The other ingredient is a family of separated words that supplies the finite-tuple selectors.

7.1 The bounded compiler

Fix a finite alphabet \Sigma containing the disjoint triples

and the six further letters \mathtt z,\mathtt d,\mathtt l,\mathtt r,\mathtt h,\zeta. Fix a total order with \mathtt a_T<\mathtt c_T and \mathtt a_G<\mathtt c_G. Words are ordered by shortlex: first by length and then lexicographically. We use an acceptable programming system for partial functions \Sigma^*\to\Sigma^*, writing f_\eta for the function with index \eta. In particular, universal evaluation and effective substitution of parameters are available; integers and tuples are represented by fixed computable word encodings.

The following finite construction is proved in Appendix A. Its conditional statement is essential: the program index determines the presentation without running the program. The evaluator is also fixed independently of a length bound; its termination and compatibility with equations will be proved from the program’s behavior within that bound.

For clarity, (32) follows from the preceding derivation statement. Transplant the paths from u and v to their common output into x(-)y. Neither contextual path leaves the budget, so one-step invariance identifies their outputs. A general machine encoding without this bounded conclusion would not suffice below. The raw singleton rule has a different role: it will distinguish the elements used for the injection H\to K. Multiplication of two raw words, rather than evaluation of a singleton, will encode the product in H through (33).

7.2 Codes and finite rule tables

First consider any index \eta. The auxiliary monoid \mathcal P has decidable equality by Lemma 6.1.

Let Y be the disjoint union of X_\eta and a fixed finite generating alphabet for \mathcal P. For a Y-word v, write v_K,v_{\mathcal P} for its projections, obtained by deleting the letters of the other alphabet. Its tested class is zero if N_\eta(v_K)=\Omega; otherwise it is the pair consisting of N_\eta(v_K) and the value of v_{\mathcal P} in \mathcal P. This is at present a partial test. For the second type of code, fix a finite monoid generating alphabet Z for \widehat G, including the inverses of a finite group generating set, and test words by their values in \widehat G. This second test is total by the hypothesis of Theorem 6.2.

Choose computably an integer D_0>M such that 2^{D_0-1}\ge\max\{|Y|,|Z|\}. Encode the letters of Y, in their chosen order, by distinct words beginning with \mathtt b_T and followed by D_0-1 letters from \{\mathtt a_T,\mathtt c_T\}, in lexicographic order. Encode Z in the same way using the other triple. Write C(v) for concatenation of the appropriate codes and put C(\varepsilon)=\varepsilon. The type of a nonempty code sequence is unambiguous. Codes preserve shortlex comparison and have length D_0 per generator.

Enumerate all nonempty finite ordered tuples

of distinct \Sigma-words avoiding \zeta; the empty word is allowed as a member. Choose integers N_j recursively so that

These inequalities concern all potential earlier envelopes, regardless of which rules will be selected. The increasing sequence N_j is computable without performing any tested-class evaluation.

We now define a partial procedure F(\eta,w). Put n=|w| and form the following finite rule table \mathcal R_n.

1. 1.

   Include \zeta a\to\zeta and a\zeta\to\zeta for every letter a\in\Sigma. For each nonempty Y-word v with D_0|v|\le n, test its class. If it is zero, include C(v)\to\zeta. Otherwise find the shortlex least word v' of the same tested class among all words of length at most |v|, including the empty word; include C(v)\to C(v') if v'\ne v. Do the same for Z-words using equality in \widehat G, with no zero case. Call these the static rules.

2. 2.

   Process the tuples with N_j\le n in order. If every member of tuple j has no reducible occurrence under the static rules and previously selected rules, include

   \mathtt d\mathtt l^{N_j}w_i^{(j)}\mathtt r^{N_j}\mathtt h \longrightarrow \begin{cases} \varepsilon,&i=1,\\ \zeta,&i>1. \end{cases} \tag{35}

   Some of these left sides may be longer than n; they simply cannot act on the input.

3. 3.

   Reduce w until no rule applies, using a fixed deterministic choice of occurrence and rule.

Whenever the tests terminate, the last step terminates: every rule decreases shortlex. In particular a nonempty code reduced to \zeta shortens, since D_0>2. All other non-code rules shorten as well. Thus F is uniformly partial computable.

7.3 The fixed point and its length induction

Effective substitution of parameters gives a total computable index transformation \tau(\eta) for the function F(\eta,-). Kleene’s Recursion Theorem [12] supplies an index with

as partial functions. Here is the short parameterization argument. Let U be universal evaluation and let d(a) be an effectively obtained index for the partial function w\mapsto U(U(a,a),w). Choose an index b computing the total function a\mapsto\tau(d(a)). For \eta=d(b),

Only now fix the presentation alphabet and code length belonging to this particular \eta. There is no advance bound on the machine’s size or working space. Write f=f_\eta and K=K_\eta.

7.4 The two monoids and their embeddings

Let H be the monoid on \Sigma whose equations are the union of all the rule tables. Every word is related to its computed normal form, which is irreducible for this union by stability. Conversely, a contextual use of any one equation preserves that form: choose a bound containing both endpoints and the equation, and apply stability and confluence from Lemma 7.2. Thus two words represent the same element of H if and only if their literal f-outputs agree. This proves decidability. The empty word and the single letter \zeta are distinct irreducibles; they represent the identity and the absorbing zero of H.

The budget hypotheses now hold at every length, so Lemma 7.1 gives an equality test for K. In particular its identity and zero are distinct. The tested product classes are now the actual elements of

with coordinatewise multiplication and every pair having first coordinate \Omega collapsed to zero. Here a letter of X_\eta acts in the first coordinate and a generator of \mathcal P in the second; the letter \Omega maps to 0_T. Thus Y generates T.

For a nonzero element of T, take its least shortlex Y-representative v. The code C(v) is irreducible: a subcode rule would either force the element to be zero or produce a smaller representative; no selector or absorption side occurs in a pure code word. Every other representative reduces by its whole-word rule to this same code, and every zero-class code reduces to \zeta. Consequently coding defines an injective zero-preserving monoid map

It is unital because the least representative of the identity is empty, and it is multiplicative because codes concatenate. The identical argument for Z-words embeds \widehat G unitally in H. Its image consists of units, since the products of mutually inverse group words have the empty representative. This includes the trivial group and does not require a nonempty generating set.

Let z\in H be represented by the separator \mathtt z. For least representatives v,v' of nonzero elements of T, the words

are irreducible. No code crosses the separator; each code portion is already irreducible; and there are no selector markers or \zeta. These literal words recover the ordered pair, including when one or both representatives are empty. They are nonzero because none equals \zeta. This proves the separator assertion of Theorem 6.2.

7.5 Selectors and multiplication by raw words

Take any ordered tuple of distinct nonzero elements h_1,\ldots,h_s of H, and let w_1,\ldots,w_s be their normal words. These words avoid \zeta, since any word containing it reduces to the zero word. Their tuple occurs in the enumeration, say at stage j. A word irreducible for the final rule set is irreducible for the static and selected rules present at stage j. Hence this tuple passes its test. With

as elements of H, the selected equations give Lh_1R=1 and Lh_iR=\zeta for i>1. The argument includes a tuple containing the identity, whose normal representative is empty.

Finally define a multiplicative map in the opposite direction by

The normal-form characterization of H makes this well-defined. Every raw singleton is its own literal N_\eta-output. Distinct normal words therefore give distinct elements of K, and none of these elements is its identity or its zero. For normal words u,v, (33) gives

Thus c is injective and multiplicative, as required. It is not unital: even c(1)=[\operatorname{raw}(\varepsilon)] is distinct from 1_K. Also c(\zeta)\ne\Omega; it is absorbing only within c(H). The finite presentation of K came from the compiler, while the finite alphabet and normal-form procedure give the claimed finite generation and decidability of H. All conclusions of Theorem 6.2 are proved.

A The finite compiler

We prove Lemma 7.1. The input is a program index \eta for a partial function f_\eta:\Sigma^*\rightharpoonup\Sigma^* on the fixed finite alphabet \Sigma. We construct a finite monoid presentation and its partial evaluator. The main issue is to control arbitrary words in that presentation, including malformed machine configurations.

Encoding a finite machine by contextual equations, and checking the consequences of using those equations in reverse, are classical ideas [17, pp. 3–6]. Murskii used finite machine presentations to embed finitely generated recursively presented semigroups in finitely presented semigroups [15, Theorem 1.2 and Section 1.5]; his construction also controls malformed initial configurations [15, Section 2.4]. For the present construction we also need a single evaluator on all presentation words, normalization paths that never increase grade, and invariance under equations in arbitrary contexts within the grade bound. We prove these properties explicitly below.

Fix a deterministic one-tape machine for f_\eta, with tape cells indexed by the nonnegative integers. A left move at cell zero stays there. The input begins at cell zero and is followed by blanks; a returned string also begins at zero and ends at its first blank. We use an effective compilation of the acceptable programming system into this convention. The resulting finite transition table is part of the compiler’s input; constructing the presentation never runs the program.

A.1 Cells, paths, and the validator

A cell consists of an immutable base in \Sigma\sqcup\{\mathsf C,\mathsf D,\mathsf W\} and a finite tag. Bases in \Sigma are called anchors. The other bases mark two cuts and a workspace cell. A tag has an anchor-read bit, a workspace-filled bit, a work symbol from the compiled machine’s finite tape alphabet, an output-reading bit, and an output mark in \Sigma\sqcup\{\mathrm{none}\}. The clean tag has every bit unset, work symbol blank, and output mark none. All these fields may be included on every base; fields not used there are simply left unchanged. A bare cell base in a rule means the cell with its entire tag clean.

The presentation has a zero letter \Omega and the arrows of the quiver in Figure 2. There are arrows \alpha:O\to L and \omega:R\to O, head arrows L\to R, and two loop copies b_L,b_R of every tagged cell b, at L,R, respectively. There are no vertex-identity generators: the empty word is the global identity. Add the equations making \Omega absorbing and making every incompatible pair of arrows equal to \Omega.

A nonempty path is cut at every \omega\alpha into sectors. Each contains at most one head, since returning from R to L requires such a cut. A headed sector has optional \alpha, left loops, a head, right loops, and optional \omega. Sectors without heads are allowed. Thus the same notation describes complete computations and words with missing boundaries.

Assign grade zero to \Omega and workspace cells, grade two to cut cells with base \mathsf C, and grade one to all other generators. Tags do not affect grade. Extend grade additively to words, writing \gamma. The maximum generator grade is therefore M=2. Workspace can be added without increasing grade, although it increases literal word length.

Use raw and quota heads \mathsf Q,\mathsf P, validator heads \mathsf I,\mathsf J,\mathsf J',\mathsf N,\mathsf V, a disjoint set of machine heads, and a cleanup head \mathsf Z. For an anchor word x, the notation x_L or x_R means its sequence of clean cell copies. A sector is full raw if it has the form

The word x is its payload. To combine two such sectors, first impose

In the following validator equations, the arrows specify the forward direction used to analyze the machine; the defining relations are equations in both directions:

The anchor rules range over a\in\Sigma.

An entry has head \mathsf I immediately before clean \mathsf D_R. The validator reaches q_{\rm start} from an entry only when that entry has the complete form

Indeed the first left sweep checks precisely the clean workspace up to \mathsf C, and the next checks only clean anchors up to \alpha. The rightward sweeps then check these anchors, the first cut, the workspace, the second cut, and only clean anchors up to \omega. Thus both boundaries and every tag are checked. At the handoff all cells are on the left of the head.

These relations prepare a raw product for computation. Slide the first head across x, merge the two adjacent heads, insert s workspace cells, and enter the validator. The simulation and cleanup defined below will complete the following passage whenever f_\eta(xy) is defined and has length at most |xy|, provided s is sufficiently large:

The first passage is the preparation just described; the second is validation, simulation on the workspace, and cleanup. The two anchor blocks retain the input xy and provide space for its output letters.

Successful computations alone do not control the presented monoid, because each equation can also be used in reverse. The validator and simulator will preserve the ordered cell bases and have finitely many tags and head states. Consequently their transitions on any fixed sector form a finite graph, even if the simulated program never halts. We will search its whole weak component—allowing transitions in either direction—to normalize arbitrary configurations. The component analysis will distinguish those that contain an entry from those that do not. Quota insertion is kept outside this finite graph.

A.2 A finite transition table for the computation

We specify the remaining machine equations explicitly through finite scan instructions. This makes the construction uniform in \eta while avoiding a separate list of rules for each tape symbol.

Every state has one designated reading side. A right-reading state has, for each tested tagged cell, at most one rule of either form

a left-reading state uses the mirrored forms. These instructions cross the cell or stay in the same gap, respectively. The cells b,b' always have the same base. Boundary tests are stationary rules \alpha q\to\alpha q' or q\omega\to q'\omega on the designated side. A failed test has no rule. A finite cell predicate expands into the list of tagged cells satisfying it; complementary cases are disjoint. Finite registers are incorporated into the state set by a finite Cartesian product.

Here are the scan instructions used below, together with their complete expansion convention.

• •

  To rewind, cross every cell on the left unchanged. At \alpha, change state without moving and start the specified right-reading continuation. If \alpha is absent, the scan gets stuck at the left end of the word.

• •

  To find the first cell satisfying a predicate, test cells on the right. At a failure cross unchanged and repeat. At a match use the specified stationary update and continuation. At \omega, use the specified end continuation, or get stuck if failure was prescribed.

• •

  To go to the right boundary, cross all right cells unchanged and use the specified stationary continuation at \omega.

All invocations are expanded with distinct phase states, apart from explicit repetitions of a loop. In particular q_{\rm start} is fresh: its only incoming rule is the validator handoff, and its only outgoing rule is q_{\rm start}\omega\to q_{\rm rewind}\omega, where q_{\rm rewind} starts the first rewind. No continuation returns to q_{\rm start} or to a validator state.

The following finite control program supplies all further internal machine equations.

1. 1.

   Copy the input. Rewind, and find the first anchor whose read bit is unset. Set that bit, carry its base a in finite state, rewind, and find the first workspace cell whose filled bit is unset. Write a on its work track and set its filled bit. Failure to find that workspace cell is stuck. Rewind and repeat the anchor search.

   When the anchor search reaches \omega, rewind and check that an unfilled workspace cell remains; otherwise get stuck. Rewind once more and locate the first workspace cell for simulation. On (43) this writes exactly xy in anchor order into the initial workspace cells, followed by a blank.

2. 2.

   Run the given machine. The simulated head reads a workspace cell on its right. For each machine state and work symbol, expand its single transition using (45). A stationary move writes and stays. A right move writes and crosses the current cell, and the next simulation state requires another workspace cell on the right. A left move first writes without crossing, then enters a left-reading intermediate state. That state crosses an immediately left workspace cell unchanged, or stays if the immediately left base is \mathsf C; any other case is stuck. It then returns to a right-reading simulation state. This implements the left-end convention. A halt is recognized only at a workspace cell in bounds.

3. 3.

   Read the output. After halt, rewind and find the first workspace cell whose output-reading bit is unset. A blank work symbol ends the output. For a work symbol a\in\Sigma, set that bit, carry a in finite state, rewind, and place output mark a on the first anchor whose output mark is none. Failure to find such an anchor is stuck. Rewind and repeat. An invalid output symbol, or exhaustion of the workspace without a blank, is stuck. When output ends, go to \omega and enter a fresh state q_{\rm ok}, with no outgoing internal transition.

Each instruction uses only the finite predicates, finite registers, and updates just specified. Expanding all cases gives a finite list of equations computable from the machine table. Each state tests only its designated side and has disjoint cases. Consequently the internal forward transition relation has outdegree at most one on every sector, including sectors with missing boundaries and arbitrary tags. Every transition preserves the number and ordered bases of the cells.

On a passing entry, simulation success computes f_\eta(xy) genuinely. Conversely, if f_\eta(xy) is defined and has length at most |xy|, then some finite quota s permits success: take more workspace cells than the input length, the largest tape index visited by the halting computation, and the output length. The extra cell supplies its blank delimiter. There are |xy| anchors for the output marks. This includes empty input: at least one workspace cell is supplied, and a length bound forces the output to be empty.

Add the exit equation q_{\rm ok}\omega\to\mathsf Z\omega and the following cleanup equations. An anchor cell b with output mark a\in\Sigma has

For every other tagged cell use b_L\mathsf Z\to\mathsf Z, and add \alpha\mathsf Z\to\alpha\mathsf Q. Cleanup is deterministic and never increases grade, even on dirty data. Applied to a successful passing entry, it leaves

The leftward sweep places successive output letters on its right in the correct order. All unused anchors and all nonanchor cells disappear.

A.3 Finite components on arbitrary sectors

We now analyze sectors with arbitrary tags and optional boundaries. For a validator or machine sector, form the graph of internal forward transitions, excluding entry from \mathsf P and exit to \mathsf Z. We use its entire weak connected component. The ordered bases of its cells and its boundary flags are fixed. If there are k cells and h internal head states, with at most c tags per cell, there are at most (k+1)h c^k possible configurations with these data. Its weak component can therefore be found by a finite search through elementary compiled steps. This search does not call f_\eta or wait for a computation to halt. In particular, the quota insertion rule is excluded: finite grade alone would not bound the number of grade-zero workspace cells.

A.4 The partial evaluator

The component lemma leaves a choice when both an entry and a successful terminal occur. Returning to the entry, removing its quota, and undoing the merge, then sliding the raw heads left, gives \operatorname{raw}(x)\operatorname{raw}(y); cleaning up the terminal gives \operatorname{raw}(f_\eta(xy)). We give the entry priority, so that internal equations have identical preprocessing outputs. The final combination of consecutive raw sectors will identify the two routes in (44), using the contextual identity assumed in Lemma 7.1 when other raw sectors are adjacent.

This priority also applies to a failed or malformed entry; in that case quota removal need not produce two full raw sectors. Conversely, a successful component without an entry need not encode a genuine input computation. It can use its unique terminal cleanup directly. The following algorithm includes all these cases.

The algorithm N_\eta preserves the empty word. It sends every word containing \Omega, and every nonpath, to \Omega, using the zero relations. For a nonempty path, first preprocess its sectors as follows.

1. 1.

   Leave sectors without heads unchanged. Move \mathsf Q to its leftmost reachable gap using (40), across clean anchors only.

2. 2.

   If \mathsf P has clean \mathsf D_R immediately right, remove all immediately preceding clean \mathsf W_L by the quota equation. If clean \mathsf C_L is then immediately left, unmerge \mathsf C_L\mathsf P\mathsf D_R into \mathsf Q\omega\alpha\mathsf Q and normalize the two resulting raw heads as above. Otherwise keep the trimmed sector. A \mathsf P without immediately right clean \mathsf D_R is kept.

3. 3.

   Run \mathsf Z cleanup until it is stuck or becomes \mathsf Q; in the latter case normalize that raw head.

4. 4.

   For any validator or machine head, find its finite internal weak component. If there is an entry, move to it along a weak path, revert to \mathsf P, and use the preceding rule. If there is no entry but there is a sector ending in q_{\rm ok}\omega, move there and use cleanup. If neither exists, use the least sector in the component in shortlex order.

Lemma A.1 makes the choices in the last rule unambiguous. The ordering is fixed independently of any grade budget. All these operations preserve the original outer boundaries; only unmerge creates an interior \omega\alpha and splits a sector.

Replace each maximal run of t\geq2 consecutive full raw sectors, with payloads u_1,\ldots,u_t, by

A run of length one is left unchanged, without evaluating f_\eta. This completes the definition of N_\eta. Its only calls to that function are in (48).

Assume now the budget hypothesis of Lemma 7.1 at m. Every preprocessing operation has a derivation that never raises grade. Internal component paths preserve every base and hence grade. Raw slides and entry reversal preserve grade. Quota cells have grade zero. Unmerge preserves grade because

Cleanup preserves or decreases it. Each argument in (48) has length at most the original total grade, since every anchor contributes one. Thus all required calls terminate for an input of grade at most m.

The replacement of two full raw sectors is also derivable without raising grade. Move the first head right across its anchors, merge at \mathsf Q\omega\alpha\mathsf Q, insert a sufficient grade-zero workspace quota, enter, simulate successfully, and clean up. The result is the raw word for f_\eta(u_1u_2). Repeating this operation gives (48), because the budget hypothesis implies

and the analogous identities for longer runs. The successive arguments to f_\eta have length at most |u_1|+\cdots+|u_t|, because f_\eta is length-nonincreasing. Each elementary derivation step preserves or decreases grade, including the insertion of grade-zero workspace. Thus every call and every intermediate word remains within its required budget. This proves termination and the asserted grade-nonincreasing normalization path.

A.5 Invariance under equations and contexts

We verify that one contextual equation step preserves N_\eta when both endpoints have grade at most m. All nonzero equation sides are nonempty paths with the same initial and terminal vertices. This includes the deletion b_L\mathsf Z\to\mathsf Z. A replacement therefore preserves whether the whole word is a path. Zero equations and nonpaths give \Omega on both sides, so it remains to compare paths, using their sectors in the whole contextualized word.

Raw slides have the same leftmost reachable gap. Quota changes have the same trimmed sector. Entry from \mathsf P has the same preprocessing on both sides, since the internal component gives priority to its entry, even if that entry is malformed and validation fails. Internal validator or machine equations leave the weak component unchanged. Cleanup equations give the same result by forward determinism, including the last step to \mathsf Q. A merge is immediately undone by quota preprocessing before normalizing its two raw heads. This remains true when the two sectors have incomplete outer boundaries or dirty cells. In each case the preprocessed sector list is identical, so its subsequent raw-run replacements agree.

The only remaining equation is q_{\rm ok}\omega\to\mathsf Z\omega. If its internal component has no entry, both sides use the same unique terminal cleanup. If it has an entry, Lemma A.1 says that the entry is (43) and its computation returns f_\eta(xy). Entry-priority preprocessing on one side gives two full raw sectors for x,y; cleanup on the other gives a single full raw sector for f_\eta(xy). With no full raw neighbors, the pair is replaced by exactly that singleton. Otherwise let a,b be the concatenations of the neighboring raw words on the left and right. The final runs have outputs

which agree by the budget hypothesis. The anchor count |axyb| on the entry side is at most the original grade, so this use is legitimate. Passing validation forces both \alpha and \omega; an incomplete sector cannot occur in this exceptional comparison. This proves equation-step invariance in every context.

If N_\eta(u)=N_\eta(v) and both xuy,xvy have grade at most m, transplant the nonincreasing normalization paths of u and v into x(-)y. Additivity keeps every intermediate word within budget. Equation-step invariance identifies each input’s answer with the answer of its contextualized normal form. Those two middle strings are literally equal, proving bounded context compatibility. This argument does not require sector boundaries to survive the attachment of context.

If the hypotheses hold at every budget, every finite derivation is covered by some budget. Invariance then implies that equal monoid words have equal N_\eta answers. The converse follows from each word’s derivation to its answer. Thus N_\eta is an exact word-problem evaluator. Its definition always leaves each raw singleton \alpha\mathsf Q u_R\omega literal, distinct from \Omega and from the empty word; on two such sectors it gives the raw encoding of f_\eta(uv) whenever the relevant budget hypothesis holds. All parts of Lemma 7.1 follow.