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
CPS
Polygon (talk | contribs)
1,849 edits
Added CPS variants
 
(11 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.
== 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"