Repeated Word List: Difference between revisions
Added regex branching |
diagram --> graph |
||
| (10 intermediate revisions by the same user not shown) | |||
| Line 1: | Line 1: | ||
'''Repeated Word List''' (short '''RepWL''') is a [[decider]]. It works by splitting the tape contents into blocks ("words") of a given length <math>l</math>. Consecutive blocks grouped into powers. If there are more consecutive repeating blocks than a predefined repeat threshhold <math>T</math>, the exponent is given as <math>T+</math>. Consecutive blocks with no <math>+</math> in their exponent are called constant blocks. 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 <math>B</math>. 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 <math>+</math> 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 | {{Stub}} | ||
[[File:RepWL 0RB0LC 1LA1RB 1RD0RE 1LC1LA ---0LD.png|thumb|500px|RepWL graph for non-halting TM {{TM|0RB0LC_1LA1RB_1RD0RE_1LC1LA_---0LD}} showing a closed graph.<ref>https://discord.com/channels/960643023006490684/1295401870298320977/1348277260221677641</ref>]] | |||
'''Repeated Word List''' (short '''RepWL''') is a [[decider]]. It works by splitting the tape contents into blocks ("words") of a given length <math>l</math>. Consecutive blocks grouped into powers by multiplicity. If there are more consecutive repeating blocks than a predefined repeat threshhold <math>T</math>, the exponent is given as <math>T+</math>. Consecutive blocks with no <math>+</math> 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 <math>B</math>. 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 <math>+</math> 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 <math>T-1</math> and one where it stays at <math>T+</math>. 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, <math>N</math>. If the graph of a TM contains less than <math>N</math> nodes, the graph is closed. If the graph of a TM is closed and contains no halting configurations, the TM is proven non-halting. | |||
== History == | |||
* In April 2024, RepWL is first introduced by mxdys as part of [[Coq-BB5]].<ref>https://github.com/ccz181078/Coq-BB5/blob/main/CoqBB5/BB5/Deciders/Decider_RepWL.v</ref> | |||
* In May 2024, Repeated Word List is reproduced by savask.<ref>https://gist.github.com/savask/c7546bb6384984b2fb3cb90fc7925697</ref> | |||
* In October 2024, [[User:Cosmo|Tristan Stérin]] reproduces Repeated Word List again.<ref>https://github.com/bbchallenge/bbchallenge-deciders/tree/main/decider-repeated-word-list-reproduction</ref> | |||
== See also == | |||
* [[Halting Segment]] | |||
* [[Finite Automata Reduction]] | |||
== References == | |||
[[Category:Deciders]] | [[Category:Deciders]] | ||
Latest revision as of 11:29, 21 February 2026
0RB0LC_1LA1RB_1RD0RE_1LC1LA_---0LD (bbch) showing a closed graph.[1]Repeated Word List (short RepWL) is a decider. It works by splitting the tape contents into blocks ("words") of a given length . Consecutive blocks grouped into powers by multiplicity. If there are more consecutive repeating blocks than a predefined repeat threshhold , the exponent is given as . 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 . 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 and one where it stays at . 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, . If the graph of a TM contains less than nodes, the graph is closed. If the graph of a TM is closed and contains no halting configurations, the TM is proven non-halting.
History
- In April 2024, RepWL is first introduced by mxdys as part of Coq-BB5.[2]
- In May 2024, Repeated Word List is reproduced by savask.[3]
- In October 2024, Tristan Stérin reproduces Repeated Word List again.[4]
See also
References
- ↑ https://discord.com/channels/960643023006490684/1295401870298320977/1348277260221677641
- ↑ https://github.com/ccz181078/Coq-BB5/blob/main/CoqBB5/BB5/Deciders/Decider_RepWL.v
- ↑ https://gist.github.com/savask/c7546bb6384984b2fb3cb90fc7925697
- ↑ https://github.com/bbchallenge/bbchallenge-deciders/tree/main/decider-repeated-word-list-reproduction