BB(2,4): Difference between revisions
(Adding additional information on proving the BB(2,4) result and software used to get to zero unknown TMs.) |
(Added a section, "Current Work", and moved my recent additions there.) |
||
| Line 1: | Line 1: | ||
BB(2,4) was unofficially found to be 3,932,964 on April 10, 2023 by the bbchallenge project, when deciders made for solving BB(5) eliminated the last BB(2,4) holdouts. The champion machine M, with S(M) = 3,932,964 and Σ(M) = 2,050, was found by [[User:tjligocki|Terry]] and [[User:sligocki|Shawn Ligocki]] in February 2005. | BB(2,4) was unofficially found to be 3,932,964 on April 10, 2023 by the bbchallenge project, when deciders made for solving BB(5) eliminated the last BB(2,4) holdouts. The champion machine M, with S(M) = 3,932,964 and Σ(M) = 2,050, was found by [[User:tjligocki|Terry]] and [[User:sligocki|Shawn Ligocki]] in February 2005. | ||
== History == | |||
* Brady found a steps and ones champion in 1988, establishing S(2,4) ≥ 7195 and Σ(2,4) ≥ 90.<ref>Brady A.H. (1988) The busy beaver game and the meaning of life in: The Universal Turing Machine: A Half-Century Survey, R. Herken (Ed.), Oxford University Press, 1988, 259-277.</ref> | |||
* Terry and Shawn Ligocki found the current champion in 2005. | |||
== Current Work == | |||
Work formalizing this result is ongoing. A successful proof specifically for BB(2,4) has been added to the [Coq-BB5] proof. Although this solves the BB(2,4) problem, investigations are ongoing to make a simpler proof tot better capture the complexity of this problem. | Work formalizing this result is ongoing. A successful proof specifically for BB(2,4) has been added to the [Coq-BB5] proof. Although this solves the BB(2,4) problem, investigations are ongoing to make a simpler proof tot better capture the complexity of this problem. | ||
| Line 35: | Line 41: | ||
|} | |} | ||
== Champion == | == Champion == | ||
Revision as of 17:39, 26 August 2024
BB(2,4) was unofficially found to be 3,932,964 on April 10, 2023 by the bbchallenge project, when deciders made for solving BB(5) eliminated the last BB(2,4) holdouts. The champion machine M, with S(M) = 3,932,964 and Σ(M) = 2,050, was found by Terry and Shawn Ligocki in February 2005.
History
- Brady found a steps and ones champion in 1988, establishing S(2,4) ≥ 7195 and Σ(2,4) ≥ 90.[1]
- Terry and Shawn Ligocki found the current champion in 2005.
Current Work
Work formalizing this result is ongoing. A successful proof specifically for BB(2,4) has been added to the [Coq-BB5] proof. Although this solves the BB(2,4) problem, investigations are ongoing to make a simpler proof tot better capture the complexity of this problem.
One successful attempt to run an existing enumerator and existing deciders is shown in the next table. This is far from minimal but it does reduce the number of unknown TMs to zero. The "Commands Used" needs to be explained more fully. This will happen when the a more minimal set of commands is used.
| Number of TMs | Command Used | ||||
| Input | Output | ||||
| Total | Halt | Infinite | Unknown | ||
| 1 | 348,261 | 116,844 | 205,066 | 26,351 | lr_enum 2 4 1000 BB2x4.halt.txt BB2x4.inf.txt BB2x4.unk.txt false |
| 26,351 | 26,351 | 0 | 10,136 | 16,215 | Reverse_Engineer_Filter.py |
| 16,215 | 16,215 | 0 | 13,138 | 3,072 | Enumerate.py --block-size=2 --max-loops=1_000 --lin-steps=0 --no-ctl --no-reverse-engineer |
| 3,072 | 3,072 | 0 | 2,982 | 90 | CPS_Filter.py --min-block-size=1 --max-block-size=6 |
| 90 | 90 | 0 | 15 | 75 | Enumerate.py --max-loops=10_000 --lin-steps=0 --no-ctl --no-reverse-engineer |
| 75 | 75 | 0 | 31 | 44 | CTL_Filter.py --type=CTL2 --max-block-size=6 --all-offsets |
| 44 | 44 | 0 | 13 | 31 | Enumerate.py --recursive --max-loops=10_000 --lin-steps=0 --no-ctl --no-reverse-engineer |
| 31 | 31 | 0 | 18 | 13 | Enumerate.py --recursive --max-loops=10_000 --block-size=2 --lin-steps=0 --no-ctl --no-reverse-engineer |
| 13 | 13 | 0 | 1 | 12 | Enumerate.py --recursive --max-loops=10_000 --block-size=3 --lin-steps=0 --no-ctl --no-reverse-engineer |
| 12 | 12 | 0 | 12 | 0 | MITMWFAR -n=14 |
Champion
S(2,4) = 3,932,964 and Σ(2,4) = 2050 and both are achieved by only one champion (in TNF):
1RB2LA1RA1RA_1LB1LA3RB1RZ(bbch)
Enumeration
The top 20 longest running BB(2,4) TMs (in TNF-1RB) are:
Standard Format Steps Σ 1RB2LA1RA1RA_1LB1LA3RB1RZ 3932964 2050 1RB3LA1LA1RA_2LA1RZ3RA3RB 7195 90 1RB3LA1LA1RA_2LA1RZ3LA3RB 6445 84 1RB3LA1LA1RA_2LA1RZ2RA3RB 6445 84 1RB2RB3LA2RA_1LA3RB1RZ1LB 2351 60 1RB3RA1LA2RB_2LA3LA1RZ1RA 1021 53 1RB3LA1RZ0RB_2LB2LA0LA0RA 1001 26 1RB2LA1RZ3LA_2LA2RB3RB2LB 770 30 1RB2LB1RZ3LA_2LA2RB3RB2LB 708 29 1RB2LA0RB1LB_1LA3RA1RA1RZ 592 24 1RB3LA3RA0LA_2LB1LA1RZ2RA 392 20 1RB3LA1LA1RA_2LA1RZ2RB3RB 376 21 1RB3LA1LA1RA_2LA1RZ0LA3RB 376 21 1RB3LA3RB0LA_2LA1RZ1LB3RA 374 22 1RB1RA1LB0RA_2LA3RB2RA1RZ 335 18 1RB2LA3LA1LB_2LA1RZ2RB0RA 292 18 1RB0RB1RZ0LA_2LA3RA3LA1LB 289 13 1RB1LA1RZ0LB_2LA3RB1RB2RA 283 18 1RB3LA3RA0LA_2LB1LA1RZ3RA 266 19 1RB2RB1RZ1LB_2LA2LB3RB0RB 241 15
For the top 100 halting BB(2,4) TMs, see: https://github.com/sligocki/busy-beaver/blob/main/Machines/bb/2x4.txt
- ↑ Brady A.H. (1988) The busy beaver game and the meaning of life in: The Universal Turing Machine: A Half-Century Survey, R. Herken (Ed.), Oxford University Press, 1988, 259-277.