User:Polygon/Page for testing: Difference between revisions

From BusyBeaverWiki
Jump to navigation Jump to search
← Older edit
VisualWikitext
Polygon (talk | contribs)
1,849 edits
→Method: more text
Polygon (talk | contribs)
1,849 edits
Added CPS variants
 
(9 intermediate revisions by the same user not shown)
Line 6: Line 6:
* [[Meet-in-the-Middle Weighted Finite Automata Reduction (MITMWFAR)]]
* [[Meet-in-the-Middle Weighted Finite Automata Reduction (MITMWFAR)]]
* [[Skelet 1]]
* [[Skelet 1]]
* [[CPS]]
* [[CPS]] (CPS_LRU, CPS_LRUH)




Line 36: Line 36:


=== References
=== 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|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 <math>L</math>, a right chain of segments of length <math>R</math> and a central segment. The segments themselves are of some fixed width <math>w</math>. 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).
== See also ==
* [https://gist.github.com/savask/1c43a0e5cdd81229f236dcf2b0611c3f The closed position set decider, reverse-engineered from Skelet's program]: savask's Oct 2022 Haskell implementation of CPS with extensive descriptive comments.
* [https://github.com/Nathan-Fenner/bb-simple-n-gram-cps bb-simple-n-gram-cps]: Nathan Fenner's n-gram CPS description and code
* [https://discuss.bbchallenge.org/t/thoughts-on-closed-position-set/116 Thoughts on Closed Position Set]: Shawn Ligocki's investigation into the connection with CTL (regular languages).
== Implementations ==
Traditional CPS:
* [https://gist.github.com/savask/1c43a0e5cdd81229f236dcf2b0611c3f Turing.hs]: in Haskell by savask
* [https://github.com/univerz/bbc/blob/skelet-cps/src/skelet_cps.rs skelet_cps.rs] in Rust by Pavel Kropitz
* [https://github.com/sligocki/busy-beaver/blob/main/Code/CPS.py CPS.py] in Python by Shawn Ligocki
* [https://gist.github.com/mateon1/b63eabc371ac35e2a14a9c5ce37413bc skeletcps.py] in Python by Mateon1
n-gram CPS:
* [https://github.com/Nathan-Fenner/bb-simple-n-gram-cps bb-simple-n-gram-cps] in Rust by Nathan Fenner
* [https://github.com/ccz181078/Coq-BB5/blob/main/CoqBB5/BB5/Deciders/Decider_NGramCPS.v Decider_NGramCPS.v] in Rocq by mxdys

Latest revision as of 10:46, 3 April 2026

List of incomplete pages:


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

Retrieved from "https://wiki.bbchallenge.org/w/index.php?title=User:Polygon/Page_for_testing&oldid=7008"