Coq-BB5: Difference between revisions
→Deciders: augmentations |
→Deciders: description of halt-decider |
||
| (3 intermediate revisions by the same user not shown) | |||
| Line 1: | Line 1: | ||
{{Stub}} | {{Stub}} | ||
'''Coq-BB5''' is a [https://en.wikipedia.org/wiki/Rocq Rocq] (previously known as Coq) proof that BB(5) = 47,176,870. It combines many deciders and individual TM proofs that the [[bbchallenge.org]] community developed and described over the years 2022-2024. It is maintained by mxdys and includes a snapshot of [[BusyCoq]] maintained by meithecatte. Coq-BB5 also contains proofs of the values of [[BB(2)]], [[BB(3)]], [[BB(4)]], [[BB(2,3)]] and [[BB(2,4)]]. | '''Coq-BB5''' is a [https://en.wikipedia.org/wiki/Rocq Rocq] (previously known as Coq) proof that BB(5) = 47,176,870. It combines many [[deciders]] and individual TM proofs that the [[bbchallenge.org]] community developed and described over the years 2022-2024. It is maintained by mxdys and includes a snapshot of [[BusyCoq]] maintained by meithecatte. Coq-BB5 also contains proofs of the values of [[BB(2)]], [[BB(3)]], [[BB(4)]], [[BB(2,3)]] and [[BB(2,4)]]. | ||
== Individual proofs == | == Individual proofs == | ||
| Line 7: | Line 7: | ||
== Deciders == | == Deciders == | ||
* [https://github.com/ccz181078/Coq-BB5/blob/main/CoqBB5/BB5/Deciders/Decider_Halt.v Halt.v] | * [https://github.com/ccz181078/Coq-BB5/blob/main/CoqBB5/BB5/Deciders/Decider_Halt.v Halt.v], simulates machines for a fixed number of steps, only checks for halting. | ||
* [https://github.com/ccz181078/Coq-BB5/blob/main/CoqBB5/BB5/Deciders/Decider_Halt_BB5.v Halt_BB5.v] | * [https://github.com/ccz181078/Coq-BB5/blob/main/CoqBB5/BB5/Deciders/Decider_Halt_BB5.v Halt_BB5.v] | ||
* [https://github.com/ccz181078/Coq-BB5/blob/main/CoqBB5/BB5/Deciders/Decider_Loop.v Loop.v] | * [https://github.com/ccz181078/Coq-BB5/blob/main/CoqBB5/BB5/Deciders/Decider_Loop.v Loop.v], this decider simulates TMs for a fixed number of steps, checking for halting and [[Translated cycler|Lin recurrence]]. | ||
* [https://github.com/ccz181078/Coq-BB5/blob/main/CoqBB5/BB5/Deciders/Decider_NGramCPS.v NGramCPS.v], Coq-BB5 uses regular [[NGram CPS]] aswell as the Fixed-length history and Least Recent Usage history (LRU) augmentations. | * [https://github.com/ccz181078/Coq-BB5/blob/main/CoqBB5/BB5/Deciders/Decider_NGramCPS.v NGramCPS.v], Coq-BB5 uses regular [[NGram CPS]] aswell as the Fixed-length history and Least Recent Usage history (LRU) augmentations. | ||
* [https://github.com/ccz181078/Coq-BB5/blob/main/CoqBB5/BB5/Deciders/Decider_RepWL.v RepWL.v], see [[Repeated Word List]] for details. | * [https://github.com/ccz181078/Coq-BB5/blob/main/CoqBB5/BB5/Deciders/Decider_RepWL.v RepWL.v], see [[Repeated Word List]] for details. | ||
Latest revision as of 10:55, 3 April 2026
Coq-BB5 is a Rocq (previously known as Coq) proof that BB(5) = 47,176,870. It combines many deciders and individual TM proofs that the bbchallenge.org community developed and described over the years 2022-2024. It is maintained by mxdys and includes a snapshot of BusyCoq maintained by meithecatte. Coq-BB5 also contains proofs of the values of BB(2), BB(3), BB(4), BB(2,3) and BB(2,4).
Individual proofs
The individual TM proofs are - except for Skelet 17 - all contained within the included snapshot of BusyCoq. TMs which have individual proofs in BusyCoq are: The "finned" machines (Finned #1 (proof), Finned #2 (proof), Finned #3 (proof), Finned #4 (proof) and Finned #5 (proof)) and Skelet machines 1 (proof), 10 (proof), 15 (proof), 26 (proof), 33 (proof), 34 (proof) and 35 (proof).[1] Coq-BB5 imports these proofs from BusyCoq. The individual proof of non-halting for Skelet 17 (proof)(description) is contained within Coq-BB5 itself.[2]
Deciders
- Halt.v, simulates machines for a fixed number of steps, only checks for halting.
- Halt_BB5.v
- Loop.v, this decider simulates TMs for a fixed number of steps, checking for halting and Lin recurrence.
- NGramCPS.v, Coq-BB5 uses regular NGram CPS aswell as the Fixed-length history and Least Recent Usage history (LRU) augmentations.
- RepWL.v, see Repeated Word List for details.
See: https://github.com/ccz181078/Coq-BB5/tree/main
TODO: Give wiki links to these deciders and individual TM proofs.