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 configurations is shown to be closed, the TM is proven non-halting.
Method
It only evaluates the tape in a fixed radius 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 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 ). 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) 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.[1][2]
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 of the last pairs of tape symbols and the state that read it which were seen on that cell. The zero configuration for this augmentation is 0, [].[2]
Least Recent Usage history (LRU):
Using the Least Recent Usage history (LRU), each tape cell encodes its current tape symbol and the set of state-symbol pairs seen on that cell, ordered by when they were last seen with the most recently seen pair being first. Unlike with the Fixed-length history augmentation, the amount of encoded state-symbol pairs is not limited by some fixed number, but by the amount of states times the amount of symbols. The zero configuration for this augmentation is 0, [].[2]
History
- In February 2023, n-Gram CPS is first introduced by Nathan Fenner as a variant of CPS.[1]
- In April 2024, mxdys reproduces and improves n-Gram CPS in Coq (now Rocq).[3]
See also
References
- ↑ 1.0 1.1 https://github.com/Nathan-Fenner/bb-simple-n-gram-cps
- ↑ 2.0 2.1 2.2 https://arxiv.org/pdf/2509.12337 Determination of the fifth Busy Beaver value
- ↑ https://github.com/ccz181078/Coq-BB5/tree/main