BB(3, 4) > Ack(14)
Pavel has found a new 3-state 4-symbol Busy Beaver champion which can compute an “Ackermann-level” function and halts with exactly
\[(2 \uparrow^{15} 5) + 14\]non-zero symbols on the tape. With a number this large, Knuth up-arrow format is becoming a bit awkward, so we can approximate this bound as:
\[BB(3, 4) > Ack(14)\]where \(Ack(14)\) is the 14th Ackermann number defined as:
\[Ack(n) = n \uparrow^n n\]As far as I know, this is the first TM found “in the wild” that is able to simulate an Ackermann-level function.
The Machine
1RB3LB1RZ2RA_2LC3RB1LC2RA_3RB1LB3LC2RC
| 0 | 1 | 2 | 3 | |
|---|---|---|---|---|
| A | 1RB | 3LB | 1RZ | 2RA |
| B | 2LC | 3RB | 1LC | 2RA |
| C | 3RB | 1LB | 3LC | 2RC |
It halts with final configuration
\[0^\infty \;\; 3^{2 g_{15}^{3}(0) + 1} \;\; 2^{16} \;\; 1 \;\; \text{ Z> } \;\; 0^\infty\]which leaves exactly
\[\sigma = 2 g_{15}^{3}(0) + 18 = (2 \uparrow^{15} 5) + 14\]non-zero symbols on the tape. (The function \(g_k(m)\) will be defined below).
Attribution
This TM was discovered by Pavel Kropitz (@uni) and shared on Discord on 25 Apr 2024. His code was not able to specify a human-readable bound on the TM score and it was simply specified as Halt(SuperPowers(13)) indicating 13 layers of inductive rules needed to prove it. He began a validation of this result using my new “Inductive Proof Validator” (see discussion at end of article).
I completed this validation and was able to extract the precise definition of \(g_k^n(m)\) on 20 May 2024 (Discord link) and used that to get a bound of \(\sigma > 2 \uparrow^{15} 3\).
Matthew House (@LegionMammal978) discovered on 22 May 2024 (Discord link) the remarkably simple closed form evaluation:
\[g_k^n(0) = \frac{ 2 \uparrow^k (n+2) }{2} - 2\]which led me to rewrite this article with exact values for \(\sigma\)!
Analysis
Let
\[B(k, n, m) = 0^\infty \;\; 3^{2m+1} \;\; 2^k \;\; \text{ A> } \;\; 1^n\]then we can prove that
\[\begin{array}{lcl} 0^\infty \;\; \text{A>} \;\; 0^\infty & \xrightarrow{241} & B(16, 3, 0) \;\; 2 \;\; 0^\infty \\ B(k, n, m) & \to & B(k, 0, g_{k-1}^n(m)) & \text{if } k \ge 1 \\ B(k, 0, m) \;\; 2 & \xrightarrow{1} & 0^\infty \;\; 3^{2m+1} \;\; 2^k \;\; 1 \;\; \text{Z>} \\ \end{array}\]where
\[\begin{array}{l} g_0(m) & = & m + 1 \\ g_{k+1}(m) & = & g_k^{2m+2}(0) \\ \end{array}\]Proof by Double Induction
This TM is remarkably simple in the sense that its behavior can be almost completely described by one single rule:
\[B(k, n, m) \to B(k, 0, g_{k-1}^n(m))\]but that rule is a whopper requiring double induction to prove!
Lemma 1: For all \(k \ge 1\):
\[3 \;\; 2^k \;\; \text{<B} \;\; \xrightarrow{2k+1} \;\; 2^k \;\; \text{<B} \;\; 1\]Corollary 2: For all \(k \ge 1, m \ge 0\):
\[3^m \;\; 2^k \;\; \text{<B} \;\; \xrightarrow{(2k+1)m} \;\; 2^k \;\; \text{<B} \;\; 1^m\]Proofs left as an exercise to the reader.
Theorem 3: For all \(k \ge 1, n \ge 0, m \ge 0\):
\[B(k, n, m) \to B(k, 0, g_{k-1}^n(m))\]Proof by Induction on \(k\):
- Base Case (\(k = 1\))
- Goal: \(\forall n,m \ge 0: B(1, n+1, m) \to B(1, 0, g_0^{n+1}(m))\)
- Proof by induction on \(n\). Left as an exercise to the reader.
- Induction Case
- Assume \(H_k: \forall n,m \ge 0: B(k, n, m) \to B(k, 0, g_k^n(m))\)
- Goal: \(\forall n,m \ge 0: B(k+1, n, m) \to B(k+1, 0, g_{k+1}^n(m))\)
-
Proof by induction on \(n\):
- Base Case (\(n = 0\))
- Trivially true because \(g_{k-1}^0(m) = m\), so \(B(k, n, m) = B(k, 0, g_{k-1}^n(m))\)
- Induction Case
- Assume \(H_n: \forall m \ge 0: B(k+1, n, m) \to B(k+1, 0, g_{k+1}^n(m))\)
- Goal: \(\forall m \ge 0: B(k+1, n+1, m) \to B(k+1, 0, g_{k+1}^{n+1}(m))\)
- Base Case (\(n = 0\))
QED
Exact Values
Through what appears to be a remarkable series of coincidences, there is a relatively simple closed form evaluation of \(g_k\) using only Knuth up-arrows and arithmetic:
Theorem: For all \(k \ge 0, m \ge 0\):
\[2 g_{k+1}(m) + 4 = 2 \uparrow^k (2m+4)\](where we define \(a \uparrow^0 b = ab\))
Proof by Induction on \(k\):
- Base case (\(k = 0\)):
- Inductive case: Assume \(\forall m \ge 0: 2 g_{k+1}(m) + 4 = 2 \uparrow^k (2m+4)\):
QED
Note: This depends upon the coincidence that \(2 \uparrow^k 2 = 4\) for all \(k\). If the parameters had been slightly different and we’d ended up with \((2 \uparrow^k)^{2m+2} 5\) above, I don’t think it would have been possible to get a closed form expression.
Corollary: For all \(k \ge 0, n \ge 0\):
\[2 g_k^n(0) + 4 = 2 \uparrow^k (n+2)\]From which it follows directly that:
\[\sigma = 2 g_{15}^{3}(0) + 18 = (2 \uparrow^{15} 5) + 14\]Permutations
\[\begin{array}{lcl} 0^\infty \;\; \text{B>} \;\; 0^\infty & \xrightarrow{86} & B(7, 3, 0) \;\; 2 \;\; 0^\infty \\ 0^\infty \;\; \text{C>} \;\; 0^\infty & \xrightarrow{20} & B(1, 3, 0) \;\; 2 \;\; 0^\infty \\ \end{array}\]Therefore, we can see that if we switch to:
- Starting in state
B, the TM halts with a score of \(\sigma_B = 2 g_6^3(0) + 9 = (2 \uparrow^6 5) + 5\) - Starting in state
C, the TM halts with a score of \(\sigma_C = 2 g_0^3(0) + 3 = (2 \uparrow^0 5) - 1 = 9\) (which it does at step 72).
This first permutation (start state B) is another top BB(3, 4) TM. Converted into TNF it is:
1RB3RB1LC2LA_2LA2RB1LB3RA_3LA1RZ1LC2RA
| 0 | 1 | 2 | 3 | |
|---|---|---|---|---|
| A | 1RB | 3RB | 1LC | 2LA |
| B | 2LA | 2RB | 1LB | 3RA |
| C | 3LA | 1RZ | 1LC | 2RA |
Not Collatz
One interesting thing about this TM is how surprisingly simple it is. For example, the fact that it does not have any Collatz-like rules (rules which act differently depending on the remainder of some value). Is this the end of the domination of Collatz-like TMs? It is far too early to know, but my guess is that there are Collatz-like Ackermann-level TMs waiting for us, but we are not seeing them right away because of selection bias. Perhaps this was the first Ackermann-level TM found because it is simple enough to be proven halting without having to implement modular arithmetic on Ackermann-level functions.
Inductive Proof Validator
This TM was the perfect test case for an “inductive proof” validator I am currently developing. The goal of this project is to develop a standardized certificate format for “inductive proofs” (an umbrella term for all the sort of forward-reasoning, rule-based analyses that are ubiquitous on this blog). The idea is that anyone with an “inductive decider” could write out their rules in this format and then this validator can check these proofs. The system is still very clunky and not ready for prime time, but I have been able (with a little elbow grease) to use it to prove the behavior of many TMs including this one.