The braid group word problem is decidable by garside normal form

The positive-word calculus (a). (i) and (ii) restate [F1], which also supplies their effectivity: the recursion rules of $\mathrm{\Theta }$ reduce every query to finitely many letter-level values $\theta (s,t)$ and terminate for all pairs of positive words. For (iii), let $u$ be a positive word and $C$ the finite set of words $z$ with $\mathrm{\mid }z\mathrm{\mid }\le \mathrm{\ell }([u])$; by [F2] a class $[z]$ is a common left divisor of $[u]$ and $\mathrm{\Delta }$ if and only if it is the class of some $z\in C$ with $\mathrm{\Theta }(u,z)=\epsilon$ and $\mathrm{\Theta }({\mathrm{\Delta }}_{\mathrm{w}\mathrm{o}\mathrm{r}\mathrm{d}},z)=\epsilon$, both decidable by (i) and (ii). By [F2] the family $\{[u],\mathrm{\Delta }\}$ has a unique left-gcd $d$, which belongs to this finite set of candidates; and an element $z_0$ of the candidate set satisfies $[z]{\preccurlyeq }_L[z_0]$ for every candidate $z$ if and only if $[z_0]=d$ (as $d$ is a candidate and every common divisor divides $d$). Since divisibility between candidates is decidable by (ii), finitely many comparisons locate $d$. The same argument applies to any nonempty finite family of positive braid classes in place of $\{\mathrm{\Delta },[u]\}$: choose one member $b$ and enumerate words of length at most $\mathrm{\ell }(b)$, since every common left divisor divides $b$. The empty family has no left-gcd for $n\ge 2$: every ${\sigma }_1^k$ is then a common divisor, whereas the length of any proposed greatest one is finite.

Rewriting a signed word (b)(1). Let $w$ be a word in the letters ${\sigma }_i^{\pm 1}$. Replacing each occurrence of ${\sigma }_i^{-1}$ by the positive word $R_i$ followed by the formal symbol ${\mathrm{\Delta }}^{-1}$ (legitimate in $B_n$ by [F3]) produces a product of positive words and of symbols ${\mathrm{\Delta }}^{-1}$. Moving each ${\mathrm{\Delta }}^{-1}$ to the left past positive letters by $z{\mathrm{\Delta }}^{-1}={\mathrm{\Delta }}^{-1}\tau (z)$ [F3] and conjugating the positive blocks it crosses, induction on the number of ${\mathrm{\Delta }}^{-1}$ symbols rewrites $w$ as ${\mathrm{\Delta }}^{-j}A$ with $j\ge 0$ and $A$ a positive word; each move is an explicit word operation, so the procedure is effective.

Extracting the maximal power (b)(2). Suppose $x={\mathrm{\Delta }}^{-j}A$ with $A$ positive, so $x={\mathrm{\Delta }}^{p}A$ with $p:=-j$; by [F4] this is the maximal-$p$ decomposition precisely when $\mathrm{\Delta }\mathrm{̸}{\preccurlyeq }_L[A]$. If $\mathrm{\Delta }{\preccurlyeq }_L[A]$, then $[A]=d\cdot C$ with $d:=\mathrm{\Delta }$ and some $C\in B_n^{+}$, and since any positive word for $[A]$ has length $\mathrm{\ell }([A])$ and any positive word for $C$ has length $\mathrm{\ell }([A])-N$, a word for $C$ is found by searching the finitely many words of that length and testing $[A]{\equiv }^{+}[{\mathrm{\Delta }}_{\mathrm{w}\mathrm{o}\mathrm{r}\mathrm{d}}][C]$ with the decidable equality of (a)(i); then $x={\mathrm{\Delta }}^{-j+1}C$, so replacing $A$ by $C$ and $p$ by $p+1$ preserves the identity $x={\mathrm{\Delta }}^{p}A$ and lowers $\mathrm{\ell }([A])$ by $N\ge 1$. Hence after finitely many passes $\mathrm{\Delta }\mathrm{̸}{\preccurlyeq }_L[A]$, and by the uniqueness in [F4] the current pair is $(p(x),A(x))$.

The greedy factor list (b)(3). Assume $\mathrm{\Delta }\mathrm{̸}{\preccurlyeq }_L[A]$ and $[A]\mathrm{\ne }1$. By (a)(iii) $a_1:=\mathrm{\Delta }{\wedge }_L[A]$ is computable; by the computation of step 1.2 of [F4]'s proof (the first letter of a positive word for $[A]$ is an atom, and every atom divides $\mathrm{\Delta }$) one has $a_1\mathrm{\ne }1$, and $\mathrm{\Delta }\mathrm{̸}{\preccurlyeq }_L[A]$ gives $a_1\mathrm{\ne }\mathrm{\Delta }$; so $a_1$ is proper simple. Since $a_1{\preccurlyeq }_L[A]$, a positive word $C$ with $[A]{\equiv }^{+}[a_1][C]$ exists and has length $\mathrm{\ell }([A])-\mathrm{\ell }(a_1)$; searching the finitely many words of that length and testing the congruence with (a)(i) finds one. Replace $A$ by $C$ and repeat, appending each $a_i$ to the list. Length drops by $\mathrm{\ell }(a_i)\ge 1$ at each pass, so the loop halts at $[A]=1$ after $r$ passes with a list $a_1,\dots ,a_r$ satisfying $A(x)=a_1\cdots a_r$ and, by construction, $a_i=\mathrm{\Delta }{\wedge }_L(a_i\cdots a_r)$ for every $i$.

Correctness of the output (b) and (c). By steps 1.2, 2.1 and 3.1 the computed data satisfy $x={\mathrm{\Delta }}^p{a}_1\cdots a_r$ with every $a_i$ proper simple and $a_i=\mathrm{\Delta }{\wedge }_L(a_i\cdots a_r)$, i.e. they are exactly the left normal form of $x$; conversely [F4] says that any two elements equal in $B_n$ have equal left normal forms, so two signed words represent the same element if and only if the computed data $(p;a_1,\dots ,a_r)$ coincide, the comparisons $[a_i]=[a_i^{\mathrm{\prime }}]$ being decided by (a)(i). Each computation is a finite searches over explicitly bounded sets of words with decidable tests, together with the terminating right-reversing procedure, and $\mathrm{\Theta }$ is total, so the whole procedure terminates; no unbounded search and no choice principle is used.

Assembly. Part (a) is step 1.1, part (b) is steps 1.2, 2.1 and 3.1, and part (c) is step 4.1. All the algorithmic primitives invoked are finite: the reversing recursion, the length-bounded enumeration of positive words, the congruence test on positive words, and the divisibility test $\mathrm{\Theta }(u,v)=\epsilon$. The uniqueness of the left normal form is what makes the comparison of the computed data a decision of braid equality rather than merely a sufficient condition. No choice principle is used. ∎