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.

Method

It only evaluates the tape in a fixed radius $n$ around the central cell which the TM head is on, called the local context. Local contexts also contain the state the TM is in. On a transition, the TM will move outside of its local context (one side of it will have length $<n$). For one side, the new local context will be too long, there, the last tape entry is "dropped off" while the last (closest to outer edge) $n$ entries of the local context are saved as an n-Gram. For the other side, the new local context 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 context match. The valid n-Grams then create new possible local contexts. During this process, all n-Grams which are saved after the local context becomes too long on a side, are saved into separate sets for both left and right of the TM head. The decider also creates a set of all visited local contexts. 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 contexts showing that the set of local contexts is closed, which proofs 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