Main Page: Difference between revisions
No edit summary |
No edit summary |
||
| Line 32: | Line 32: | ||
|} | |} | ||
In the above table, <span style="background: orange">cells are highlighted in orange</span> when there are known machines | In the above table, <span style="background: orange">cells are highlighted in orange</span> when there are known [[Mathematically-hard machines]], machines that are believed hard to prove halting or non-halting (although, generally believed non-halting), such as [[Cryptids]]. | ||
=== [[bbchallenge.org]] === | |||
[[bbchallenge.org]] <ref name=":0" /> is a massively collaborative research project whose general goal is to obtain more knowledge on the [[Busy Beaver function]]. In practice, it mainly consists in collaboratively building [[Deciders]], programs that automatically prove that some [[Turing machines]] do not halt. Other efforts also include: | |||
* Formalising results using theorem provers (such as [https://en.wikipedia.org/wiki/Coq_(software) Coq]) | |||
* Proving the behavior of [[Individual Machines]] | |||
* Finding [[Mathematically-hard machines]] | |||
* Building [[Accelerators]] to simulate halting machines faster | |||
Notably, as part of [[bbchallenge.org]], in June 2024 the 5th busy beaver value [[BB(5)]] was formally proven equal to 47,176,870 in Coq, a value that was found in 1989<ref>H. Marxen and J. Buntrock. Attacking the Busy Beaver 5. | |||
Bulletin of the EATCS, 40, pages 247-251, February 1990. https://turbotm.de/~heiner/BB/mabu90.html</ref>. | |||
==Notes== | ==Notes== | ||
<references /> | <references /> | ||
Revision as of 10:32, 8 June 2024
The Busy Beaver function BB (called S originally) was introduced by Tibor Radó in 1962 [1] for 2-symbol Turing machines and later generalised[2] to m-symbol Turing machines:
| BB(n,m) = Maximum number of steps done by a halting m-symbol Turing machine with n states starting from all-0 memory tape |
The busy beaver function is not computable and, few of its values are known:
| 2-state | 3-state | 4-state | 5-state | 6-state | |
| 2-symbol | BB(2) = 6 | BB(3) = 21 | BB(4) = 107 | BB(5) = 47,176,870 | BB(6) > |
| 3-symbol | BB(2,3) = 38 | BB(3,3) > | BB(4,3) > | ||
| 4-symbol | BB(2,4) = 3,932,964 | BB(3,4) > 2(^15)5 + 14 | |||
| 5-symbol | BB(2,5) > 6.5 × |
In the above table, cells are highlighted in orange when there are known Mathematically-hard machines, machines that are believed hard to prove halting or non-halting (although, generally believed non-halting), such as Cryptids.
bbchallenge.org
bbchallenge.org [4] is a massively collaborative research project whose general goal is to obtain more knowledge on the Busy Beaver function. In practice, it mainly consists in collaboratively building Deciders, programs that automatically prove that some Turing machines do not halt. Other efforts also include:
- Formalising results using theorem provers (such as Coq)
- Proving the behavior of Individual Machines
- Finding Mathematically-hard machines
- Building Accelerators to simulate halting machines faster
Notably, as part of bbchallenge.org, in June 2024 the 5th busy beaver value BB(5) was formally proven equal to 47,176,870 in Coq, a value that was found in 1989[5].
Notes
- ↑ Rado, T. (1962), On Non-Computable Functions. Bell System Technical Journal, 41: 877-884. https://doi.org/10.1002/j.1538-7305.1962.tb00480.x
- ↑ Brady, Allen H, and the Meaning of Life, 'The Busy Beaver Game and the Meaning of Life', in Rolf Herken (ed.), The Universal Turing Machine: A Half-Century Survey (Oxford, 1990; online edn, Oxford Academic, 31 Oct. 2023), https://doi.org/10.1093/oso/9780198537748.003.0009, accessed 8 June 2024.
- ↑ https://bbchallenge.org/~pascal.michel/ha.html
- ↑ 4.0 4.1 https://bbchallenge.org/
- ↑ H. Marxen and J. Buntrock. Attacking the Busy Beaver 5. Bulletin of the EATCS, 40, pages 247-251, February 1990. https://turbotm.de/~heiner/BB/mabu90.html