User:Polygon/Page for testing

List of incomplete pages:

• Coq-BB5
• Finite Automata Reduction
• CTL
• Irregular Turing Machine
• Meet-in-the-Middle Weighted Finite Automata Reduction (MITMWFAR)
• Skelet 1

List of missing pages:

• nGram CPS

1RB2LA1RC3RA_1LA2RA2RB0RC_1RZ3LC1RA1RB

{{machine|1RB2LA1RC3RA_1LA2RA2RB0RC_1RZ3LC1RA1RB} {{TM|1RB2LA1RC3RA_1LA2RA2RB0RC_1RZ3LC1RA1RB} is a non-halting BB(4,3) TM discovered by Pavel Kropitz in May 2023.<ref>https://discord.com/channels/960643023006490684/1095740122139480195/1113545691994783804</ref In April 2024, Shawn Ligocki showed the TM to follow an infinite pentational rule, proving it non-halting.<ref>https://discord.com/channels/960643023006490684/1095740122139480195/1230591736829575282</ref

Analysis by Shawn Ligocki

https://discord.com/channels/960643023006490684/1095740122139480195/1230591736829575282

Let D(a, b, c, d, e) = 0^inf 1 2^a 1 3^b 1 01^c 1 2^d <A 2^2e+1 0^inf

Level 1: D(a, b, c, 2k+r, e)  ->  D(a, b, c, r, e+2k)
Level 2: D(a, b, c, 1, e)  ->  D(a, b, 0, 1, f2(c, e))
  where f2(c, e) = rep(λx -> 2x+5, c)(e)  ~= 2^c
Level 3: D(a, b, 0, 1, e)  ->  D(a, 0, 0, 1, f3(b, e))
  where f3(b, e) = rep(λx -> f2(x+2, 1), b)(e)  ~= 2^^b
Level 4: D(2a+r, 0, 0, 1, e)  ->  D(r, 0, 0, 1, f4(a, e))
  where f4(a, e) = rep(λx -> f3(2x+7), a)(e)  ~= 2^^^a
Level 5: D(0, 0, 0, 1, e)  ->  D(0, 0, 0, 1, f4(4e+19, f3(1, 1)))


where the last rule repeats forever.

=== References

NGram CPS

NGram CPS is a decider and a subset of the general CTL method. It generates a set of local configurations in a fixed radius around the TM head, if the set of these local configuration is shown to be closed, the TM is proven non-halting.

Method

It only evaluates the tape in a fixed radius $n$ around the central cell which the TM head is on, called the local configuration. Local configurations contain the state the TM is in, the symbol the TM head is on aswell as the next $n$ symbols to the left and right. On a transition, the TM will move outside of its local configuration (one side of it will have length $<n$). For one side, the new local configuration will be too long, there, the last tape entry is "dropped off" while the last (closest to outer edge) $n$ entries of the local configuration are saved as an n-Gram. For the other side, the new local configuration will be too short, there, an unknown tape entry is added. To fill this unknown entry, one must search all previously encountered n-Grams of that side of the tape, only considering those for which the entries still in the local configuration match. The valid n-Grams then create new possible local configurations which will have to be further explored. During this process, all n-Grams which are saved, are stored into separate sets for both left and right of the TM head based on where they occured. The decider also creates a set of all visited local configurations. Eventually, the decider will either reach an undefined transition, in which case the machine is left as undecided, or it will stop adding new local configurations showing that the set of local configurations is closed, which proves the TM non-halting.

Augmentations

Fixed-length history:

Using the Fixed-length history augmentation, each tape cell encodes its current tape symbol, aswell as a list of fixed length $l$ of the last $l$ pairs of tape symbols and the state that read it which were seen on that cell.

Least Recent Usage history (LRU):

TODO

• https://github.com/Nathan-Fenner/bb-simple-n-gram-cps
• https://arxiv.org/pdf/2509.12337

History

TODO