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, if the set is shown to be closed without containing any halting configurations, the TM has been proven non-halting.

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