Repeated Word List

RepWL graph for non-halting TM 0RB0LC_1LA1RB_1RD0RE_1LC1LA_---0LD (bbch) showing a closed graph.

Repeated Word List (short RepWL, also called RepWL_ES where ES means ExecState) is a decider first introduced as part of Coq-BB5. It is a subset of the general CTL method and works by generating a graph of TM configurations, if the graph is shown to be closed, the TM is proven non-halting.

Method

It works by splitting the tape contents into blocks ("words") of a given length $l$. Consecutive blocks grouped into powers by multiplicity. If there are more consecutive repeating blocks than a predefined repeat threshhold $T$, the exponent is given as $T+$. Consecutive blocks with no $+$ in their exponent are called constant blocks. The simulation begins on the blank tape. When the TM head is facing a constant block, the TM is simulated until it either leaves the constant block, halts, or exceeds a predefined step limit $B$. This simulation inside a constant block is called block simulation. Once the TM has left the constant block, identical contiguous blocks are regrouped into powers. If the TM head is facing a group of blocks with a $+$ in its exponent, the block directly faced by the TM head is separated from the group and the simulation splits into two branches: One where the original group's multiplicity is reduced to $T-1$ and one where it stays at $T+$. This splitting is called regex branching. The decider constructs a graph of all instances of block simulation (called macro steps) and regex branching up to a predefined limit on the amount of nodes which are allowed to be visited, $N$. If the graph of a TM contains less than $N$ nodes, the graph is closed. If the graph of a TM is closed and contains no halting configurations, the TM is proven non-halting.

Variants

RWLAcc

RWLAcc is a block-based accelerated simulator similar to Quick_Sim capable of supporting L0 and L1 inductive rules. It is part of mxdys's BB(6) Rocq decider set: https://github.com/ccz181078/busycoq/blob/BB6/verify/RWLAcc.v

History

• In April 2024, RepWL is first introduced by mxdys as part of Coq-BB5.
• In May 2024, Repeated Word List is reproduced by savask.
• In October 2024, Tristan Stérin reproduces Repeated Word List again.

See also

• Halting Segment
• Finite Automata Reduction