Closed Position Set

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 and, 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 head ends up at one of the edges), 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: For both graphs, vertices are segments, and edges between vertices (segments) mean that they can appear adjacent to each other. Initially both only contain the edge $0^w$ <-- / --> $0^w$ (<-- for the left side graph, --> for the right side graph) where $w$ is the chosen segment size. When a window is shifted, one side will become too short (where the unknown segment is generated) and the other side will become too long (containing too many segments). On the graph for the side with too many segments, an edge is added from the second outermost segment to the outermost segment of the window. If the initial segment on the corresponding side (before the simulation which left too many segments) was adjacent to some segment XXXX in that sides graph, an edge must be added from it to all such segments XXXX.

The unknown segment can be substituted by all segments on the same side as the unknown segment which are connected by an edge with the original outermost segment on that side. CPS also generates a Position Set which is formatted as a graph, where the beginning of an edge is a position, and the end of an edge is the window after simulating the machine till it runs over window's edge.

If, during this simulation, the decider enters a loop or encounters an undefined transition, it will leave the machine undecided. A TM is decided to be non-halting by CPS if the adjacency graphs and the position set stop growing (are closed).

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