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
• CPS

• Repeated Word List (RWL_mod; more detailed description for RWLAcc)

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

Closed Position Set (CPS) is a Closed Set decider invented by Skelet and introduced to the bbchallenge.org community by savask. Since that introduction, there are many variations of the decider that have been used, notably "ngram CPS" which was used in the Coq-BB5 proof. It creates a set of tape configurations, if the set is shown to be closed without containing any halting configurations, the TM has been proven non-halting.

Method

CPS splits the tape into three separate regions: a left chain of segments of some length $L$, a right chain of segments of length $R$ and a central segment. The segments themselves are of some fixed width $w$. The head is always between segments, pointing either left or right. During simulation, only a three segment wide window is considered. Valid positions are windows where the head is either between the left and central segments and is pointing to the left, or is between the central and right segment and is pointing to the right. The decider begins the simulation from the blank tape, simulating from one valid position to the next. If the simulation leaves the window, the window must be shifted to the side where it left, creating an unknown segment in the process. What segments can be substituted into the unknown is determined by two graphs (one for the left edge, one for the right).

These graphs are constructed in the following way: Initially both only contain the vertice $0^w$ <-- / --> $0^w$ (<-- for the left side graph, --> for the right side graph) where $w$ is the chosen segment size.

See also

• The closed position set decider, reverse-engineered from Skelet's program: savask's Oct 2022 Haskell implementation of CPS with extensive descriptive comments.
• bb-simple-n-gram-cps: Nathan Fenner's n-gram CPS description and code
• Thoughts on Closed Position Set: Shawn Ligocki's investigation into the connection with CTL (regular languages).

Implementations

Traditional CPS:

• Turing.hs: in Haskell by savask
• skelet_cps.rs in Rust by Pavel Kropitz
• CPS.py in Python by Shawn Ligocki
• skeletcps.py in Python by Mateon1

n-gram CPS:

• bb-simple-n-gram-cps in Rust by Nathan Fenner
• Decider_NGramCPS.v in Rocq by mxdys