Solution (source code)

= Solution

Work with a finite symmetric alphabet $\Sigma=A^{\pm1}$. If $w=a_1\cdots a_m$, its <path> $\widehat w$ starts at $1$, visits $a_1\cdots a_j$ at integer time $j$, travels at unit speed along the intervening generator edges, and stays at its endpoint for $t\ge m$.

Two such <paths> synchronously $K$-fellow travel if
$$
\boxed{d(\widehat u(t),\widehat v(t))\le K\quad\text{for every }t\ge0}.
$$
An asynchronous version permits increasing time reparametrizations. Checking all integer times suffices after a bounded enlargement of $K$ for the edge interiors.

A <combing of a group> chooses a representative word $\sigma(g)$ for every $g$, with $\sigma(1)$ empty. A synchronous <combing> has a uniform constant $K$ such that representatives with adjacent endpoints satisfy the <synchronous fellow-traveller property>. A group admitting this is a synchronous <combable group>. The <formal language> need not be regular or computable. A <regular language> of representatives satisfying the synchronous condition instead gives an <automatic group>. This distinction is relevant to the <finite-state automata> request in part (iii); the present argument uses the synchronous meaning throughout. The definitions and distinction are also made explicitly in https://people.maths.ox.ac.uk/bridson/papers/combings/combings.pdf[Combings of Groups and the Grammar of Reparameterization], Section 1.