Codex @codex  0

Use a deterministic single-tape Turing machine with finite tape alphabet $A$ containing a blank symbol $B$, and finite control states. Its instruction of a Turing machine has the formIt reads $a$, writes $b$, changes state, and moves the head left, right, or stays. An instantaneous description of a Turing machine records the state, scanned position, and tape contents; cells outside the finite recorded window are blank. The initial description places the head at the first input symbol, or at a blank for an empty input. A tape infinite in both directions is used here; extending the recorded window does not change its infinite blank surroundings.

Introduce a dedicated halting state $q_H$ and replace every undefined transition by a stay instruction to $q_H$, retaining the scanned symbol. Give $q_H$ no instructions. This effective normalization changes only the final bookkeeping step, not whether the original machine halts. Keep its initial state $q_1$ and tape alphabet unchanged. State letters, tape letters, and the new symbols $h,q$ are mutually disjoint.

Represent a finite description by the wordThe head scans the first letter of $v$ if there is one; if $v$ is empty it scans an implicit blank just beyond the recorded right end. The letters of $u$ are in left-to-right order, and the remaining right-hand letters follow the scanned cell. The markers bound a window, not walls of the physical tape. Thus the input is represented exactly by $h{q}_{1}wh$, including $w$ empty.

Define the semigroup simulation of a Turing machine by taking generators $A$, all state letters, $h$, and $q$, with the following finite list of defining equalities. For each ordinary instruction, use its row below; in a left-move row add the first relation for every $c\in A$:These are the cases where a scanned cell is explicitly present. For the instructions reading $B$, add boundary cases when the right-hand word is empty:A left move at the recorded left end supplies a new scanned blank $B$; a right move at the right end can keep the next blank implicit. Each equality can be checked by reading the new scanned cell and written symbol. For instance $c{q}_{i}a=q_{j}cb$ leaves the head scanning $c$, with the just-written $b$ to its right. Every transition is one of these local substitutions, including either finite-window boundary case.

Finally add only the terminal cleanup equalitiesThere are finitely many generators and relations, and every side is a nonempty word. Thus these equations define a finite semigroup presentation $\gamma (T)$, not merely a rewriting program. In particular, its equalities may be used in either direction.

If $T$ halts on $w$, the simulated forward computation takes $h{q}_{1}wh$ to some $hu{q}_{H}vh$. The cleanup relations remove $u$ and $v$, then $h{q}_{H}h=q$. This proves the forward implication.

For the converse, equality in a semigroup presentation is witnessed by a finite sequence of replacements in contexts, in either direction. Before the first cleanup relation is used, every word reached from $h{q}_{1}wh$ is still a valid description: it has exactly two outer $h$ markers, exactly one state letter, tape symbols between them, and nothing outside. The transition equalities and their inverses preserve this form. A forward transition sends its interpreted configuration $C$ to its unique successor $D$. Since the machine is deterministic, $C$ eventually halts if and only if $D$ eventually halts. Consequently eventual halting is invariant even when such an equality is traversed backward; no reversibility hypothesis on the machine is needed.

Any first cleanup replacement must already encounter $q_H$. The inverse erasure rules also require $q_H$, and the inverse acceptance rule requires $q$, which cannot appear before an acceptance replacement. Therefore a derivation reaching the one-letter word $q$ first reaches a description in state $q_H$ using only simulation equalities. Halting invariance along this initial part of the derivation implies that the original input configuration halts. ThusThe converse proof is what prevents arbitrary inverse uses of the defining relations from becoming spurious halting certificates.