The Busy Beaver function is fascinating. Seemingly so easy to define: Of all possible turing machines with N states that eventually halt, what's the number of steps that the longest-running one takes?
It's not "just" that this is uncomputable, given the halting problem. Lots of things in mathematics are uncomputable. What's special about this function is that it will eventually blast through the limits of what any given formalization of mathematics can prove at all, no matter how powerful -- like ZFC + CH + whatever other axioms you come up with.[1]
To be honest, I can't fully wrap my head around what this means. Given that some of these powerful set theoretic axioms are independent from each other, I'm not sure whether ZFC+CH could have a different idea about BB(8000) than ZFC+notCH would. That wouldn't make much sense to me at least, because a Turing machine halting or not halting feels like a concrete fact that shouldn't depend on assumptions about weird infinite sets. But I don't know.
> because a Turing machine halting or not halting feels like a concrete fact that shouldn't depend on assumptions about weird infinite sets
Think about it this way. If a particular Turing machine halts, that’s a finitary fact: you can prove it by exhibiting a finite sequence of valid states for the Turing machine which ends in a halt. But if it doesn’t halt, that’s an infinitary statement: it doesn’t halt after N steps, for any N. And no finite enumeration of steps can prove that it doesn’t halt eventually.
Since the statement is infinitary, it’s liable to avoid being probable if our axioms don’t capture it - and so computable set of axioms captures all true statements.
And if we can’t prove that a particular Turing machine of N states doesn’t halt, we can’t prove any value for BB(N), as otherwise we could just staple the first BB(N) states of the Turing machine to show it doesn’t halt, which we can’t prove.
> Think about it this way. If a particular Turing machine halts, that’s a finitary fact: you can prove it by exhibiting a finite sequence of valid states for the Turing machine which ends in a halt. But if it doesn’t halt, that’s an infinitary statement: it doesn’t halt after N steps, for any N.
Machines that halt can always be proved to halt, as you say just by exhibiting them running to halting. (In principle at least; in practice this can be quite difficult.)
Machines that don't halt fall into two groups: those that can be proved not to halt and those that cannot be proved not to halt. Provably non-halting machines are not rare or strange. For example, a machine can wind up getting stuck in one state that just moves off to the edge of the tape forever. If this happens, it's obvious that the machine will never halt, and that's provable.
Sometimes non-haltingness has an infinitary character, but not always.
The incompleteness proof depends on the input to the program under consideration, BB is limited to programs that don’t have any input which makes the incompleteness proof irrelevant.
For similar reasons you can have a solution to the halting problem given a program of infinite size that is only considering programs of finite size with finite inputs.
This is not a material distinction: for every pair (M, input) you can create a machine M’ which has no actual input and instead first writes down the input to M onto the empty tape, and then runs M. This technique practically allows you to perform most of the same proofs on inputless machines.
> For similar reasons you can have a solution to the halting problem given a program of infinite size.
Sorry, what is a “program of infinite size” in context of Turing machines?
> This technique practically allows you to perform most of the same proofs on inputless machines.
Emulating a machine allows you to know stuff that the machine being emulated can’t such as the width the the data written to the tape. It seems reasonable that you can still prove incompleteness, but I suspect it’s non trivial.
> Sorry, what is a “program of infinite size” in the context of Turing machines.
“The choice of which replacement symbol to write and which direction to move is based on a finite table that specifies what to do for each combination of the current state and the symbol that is read.” https://en.wikipedia.org/wiki/Wikipedia
I might be misunderstanding something, but I don't think an infinite table makes sense? Each machine has a finite set of states and operates on a finite alphabet, so the size of the table will always be at most the product of those two numbers.
Still confused — aren't we talking about a particular machine? Obviously the number of possible states in any given machine is unbounded, but the number of states in one particular machine is finite.
Ahh, realized I wasn’t clear about this. By definition a touring machine has finite internal states, that’s also changed to infinity.
Think of a machine that:
1 Knows it’s position on the tape
2 looks that position up on a table
3 writes the resulting cell to the tape
4 moves one position to the right
5 repeats from 1
With a finite table it’s going to run out of bounds, with an infinite table and the ability to store arbitrary position it’s always going to be possible to have a unique cell.
Well yes, and a proof system with the omega rule also escapes incompleteness, but I never yet saw anyone prove a theorem by checking it held for every natural number.
Infinitary in the sense that a proof of non-halting must be strong enough to establish something about all natural numbers (does not halt after 1 step, does not halt after 2 steps, does not halt after 3 steps…) which cannot be done on a case-by-case (“finitary”) way. In contrast to a proof of halting, which can be so done.
The usual way to deal with an infinite number of cases is to group them into a finite number of cases and then deal with those. That's how induction works. So if you can prove that (1) the machine is in a certain condition at some step and (2) whenever the machine is in that condition at some step it will get back into that same condition at a later step, then you can prove that the machine will never halt.
Right, the act of iterating a cycle might be infinite but the cycle itself is finite. Proving that nothing can break the cycle is possible in many simple cases.
"Given that some of these powerful set theoretic axioms are independent from each other, I'm not sure whether ZFC+CH could have a different idea about BB(8000) than ZFC+notCH would."
It can not. The TMs can only be affected by things that affect them at a finite level. To put it another way that may be easier to see, for them to have a different idea about a given BB number, there must be two otherwise identical machines facing their decision about what state to transfer into, but the one armed with the CH must choose one state and one without it must choose another. (There must always be some such first state, even if it is the very first transition.) There's nowhere to encode that inside a TM state transition table.
That is the "outside" mechanics of a TM, which are fully defined by the problem itself. The "inner" mechanics of a TM, where we talk about what the machine is "really doing", may have such effects, but that's a bit more mundane. And not even necessarily relevant; while you may have two machines, one with ZFC+CH and one with ZFC without CH, they're both going to be hammered by a machine doing "something" that definitely isn't just running a clearly-defined axiomatic system over propositions, but something "mixed up" beyond all human understanding.
What can affect the BB number is oracles. This is also in some sense "why" oracles are defined as essentially function calls that TMs can make with a sort of equivalent of a system call operation that user space code can use to invoke a kernel's functionality... you can easily encode that into a single finite state transfer. BB relative to an external oracle can be (and is) different than conventional BB. However, while the numbers are larger... much, much, much (etc.) larger... I think in some sense it's also less mathematically interesting and returns to just being "yet another large number generator"; BB is interesting precisely as the boundary between computability and non-computability, and BB+oracle is just straight-up uncomputable. But that's not that interesting, really; there's an infinite number of already-uncomputable functions anyhow.
I disagree but am open to being corrected. It's possible that for a TM named X there is a proof that it halts in ZFC+CH and there is a proof that it does not halt in ZFC+notCH. This would mean that X does not actually halt but that ZFC+CH contains a non-standard model of the integers [1] where BB(n) = some non-standard integer.
That might affect your proving power but it won't affect the Turing Machine itself. That Turing Machine either will or will not halt after the given number of steps, regardless of whether or not you "hand it" the CH or not. To change the result of BB requires not a change of how you are approaching the proof but the behavior of the TMs themselves, but the TMs are well-defined. Regardless of the computability of the number, BB(10,000,000) is a particular number, regardless of what proof system you try to approach it with.
Amusingly, this opens up the distinct possibility of a wrong proof. You take the CH as an axiom, or, perhaps more likely, some other attractive axiom more relevant to the task at hand, and you "prove" a result with that axiom, but then you never find out that your proof is wrong and in fact the TM's behavior is other than what you proved, because... how are you supposed to run a TM for 10^10^10^10^10^10^10^10^10^10^10^10^10^10^10 steps to check your proof anyhow? (Especially since that number would be the tiniest insignificant baby steps for the BB(7) winner.)
Again, if you want to change the BB number, you need to change the Turing Machines themselves, most commonly by adding an oracle to them to result in BB*.
But that's not what OP said and you're stating something that is very different. OP said the following:
"I'm not sure whether ZFC+CH could have a different idea about BB(8000) than ZFC+notCH would."
And the answer to that is yes, it's in principle possible that ZFC+CH contains a proof that a given TM halts after N steps while ZFC+notCH contains a proof that said TM does not halt after N steps. If that were the case and assuming that both are consistent it will be the case that said TM does not in fact halt (period) and that ZFC+notCH uses a model of non-standard arithmetic in its proof.
You mention the possibility of a wrong proof, but that is mixing up the notion of proof and truth which are not the same things. The proofs in ZFC+notCH and ZFC+CH are both correct since a proof is nothing more than a syntactic structure that adheres to certain rules. It's that ZFC+notCH is using a model of natural numbers that is not what most people normally consider to be a natural number, it's using a model of natural numbers that admits for the possibility of incredibly large numbers that are larger than any ordinary/standard natural number. In effect ZFC+CH would contain a proof that after some unimaginably large number of steps the Turing machine halts whereas ZFC+notCH does not allow for the existence of numbers that large.
So the main concept here is that two formal systems may have different notions of what a natural number is. We humans share some idea of what a natural number is supposed to be and we call those the standard natural numbers but the problem is that there is no formal way to precisely pin down those numbers without also allowing for the possibility of bizarre non-standard natural numbers as well. In this hypothetical case we would conclude that ZFC+notCH comes closer to modelling what we consider the actual natural numbers compared to ZFC+CH, but nevertheless it's impossible for any first order formal system to fully specify the natural numbers and only the natural numbers.
Again, in order to affect the TM's execution time, the "proof difference" must have a first step where your TM with CH takes a different step than the one without CH does. There can be no such first step. There is no room in the TM specification for that. It doesn't matter what you prove or don't prove, the TM "with CH" and the TM "without CH" must take the exact same steps.
You are messing up proof vs. truth. Your proof doesn't affect how long a TM runs for. Your axioms do not affect how long the TM runs for. Show me, in the state table of the TM, where the CH or any other axiom you use for analysis affects the truth table or the execution time of the TM. No amount of analysis can change how many steps a TM runs for. The numbers may be large, but they are finite and completely determined. The only thing it can affect is whether you can know the number, but the number exists regardless.
Even more concretely: Show me how your choice of axioms affects BB(4). Show me how it affects the number of steps, without redefining BB. Forget CH; take any axiom you like... for the analysis. Just don't affect the TM itself; that's a given for you. Take anything else you like and show me how it changes the BB(4) number. You can't. You can easily take axioms that will produce a wrong result; most notably we could just take as an axiom that BB(4) = -4. The resulting analysis will show that BB(4) is -4. It will also be wrong.
I am confident my explanation addresses OPs original question, which is whether two different (and consistent) formal systems can disagree about whether a given TM halts or not (and hence differ about what the value of BB(N) for some N), and the answer is yes they can. The source of that disagreement would come down to two different models of natural numbers where the theory that proves that a given TM halts only models non-standard natural numbers whereas the theory that proves that the given TM does not halt contains a standard model of the naturals.
What you're discussing is a completely different matter that while is interesting, does not address OP's issue and is something I already responded to by stating that one must be very careful to differentiate between what is actually true versus what can be proven by a formal system. You are blurring the lines between the two but that distinction is critical to understanding the point being made.
I'm the OP. That was exactly my question, great explanation. I've been confused by similar apparent paradoxes before, where I didn't clearly distinguish something being true inside the theory and outside of it.
It seems to me that the two formal systems can disagree about BB(n) for some n without disagreeing about the state of any given Turing machine at any specific time step. For example, ZFC+CH might non-constructively predict that some machine M halts, while ZFC+notCH might predict that M does not halt. If all machines other than M can be either run to completion or proven not to halt, then the value of BB(n) would be provable in ZFC+notCH but undecidable in ZFC+CH.
> For example, ZFC+CH might non-constructively predict that some machine M halts, while ZFC+notCH might predict that M does not halt.
Just to add, this can only happen for a Turing machine M that does not actually halt. If you take a system which cannot prove that M does not halt, you can consistently add a new axiom that M halts - but the number of steps to halt, and thus BB(n), will be a non-standard number.
> For example, ZFC+CH might non-constructively predict that some machine M halts, while ZFC+notCH might predict that M does not halt.
In general, this can happen, but not with this particular choice of example: If ZFC+CH proves that some machine halts, then so does ZFC (and, in fact, so do ZF and IZF). This is because a given Turing machine halting is a mere number-theoretic statement, such statements "are absolute between V and L" and CH holds in L.
So there exists a Turing machine (with some finite number of states N, naturally) that is just complex enough to encode ZF(C) and first-order logic such that it can enumerate all theorems of ZF(C). But because of Gödel, at some point it must necessarily either get stuck in a loop or return "can’t prove or disprove this" for some candidate theorem. As I understand it, the result relayed by Scott proves that N=7198 – as in a state space of merely 13 bits – is sufficient to construct a Gödel-territory TM (but this is just an upper bound)! Having an unbounded tape as a scratch space helps, of course.
BB(n) involves the class of all n-state 2-symbol Turing machines.
Encoding such a machine in binary amounts to encoding each of its n*2 transitions that depend on the current state and symbol read. A transition specifies a new symbol to write, a direction to move in (left or right) and a new state to move to, or halt. That takes 1 + 1 + ceil (log (n+1)) bits per transition.
So BB(6) machines are described by 12*(2+3) = 60 bits.
Instead of Turing machines, one can also take the lambda calculus as model of computation. Sequence A333479 in the Online Encyclopedia of Integer Sequences [1] shows the Busy Beaver for binary lambda calculus as the maximum normal form size of any closed lambda term of size n bits.
Using bits instead of states gives a more fine-grained scale of un-computability.
The latest BB(6) result suggests a challenge for functional programmers: what's the smallest n for which A333479(n) can be shown at least 10^10^10^10^10^10^10^10^10^10^10^10^10^10^10 ?
I'm interested in that as well. On the other hand, all of that can only account for constant factors (in the limit, I can use some extra states to encode a lambda calculus interpreter in my Turing machine). Even for Turing machines, two symbols tapes might not be the most efficient in terms of BB steps per encoded machine bit.
Having said all that, your encoding is a bit wasteful, so let's optimize. ;)
First, there's really no need for the encoded states to end on bit boundaries. To give an example, to encode 9 numbers between 0 and 9 (inclusive), you don't need 9*ceil(log2(10))=36 bits, you only need ceil(9*log2(10))=30 bits by treating the digits as a large decimal number and converting that to binary.
Second, if you're going to halt anyway, there's no need (at least for the BB problem) to write a symbol and move the tape on the last transition, so we can simply treat that as an alternative to encoding a transition.
Armed with both of those, the size of an encoded machine goes down to ceil(2 * 6 * log2(2 * 2 * 6 + 1)) = 56 bits. (In general for n states and k symbols, ceil(k * n * log2(2 * k * n + 1)). The 2 is for the directions, the + 1 is the halting transition.)
Yes, it's a bit wasteful. But importantly, it's straightforward, and it's what efficient universal Turing Machines would use in their input, so it makes sense for a comparison.
Even the binary lambda coding allows for some optimization, like coding for variable 2 at depth 2 as 111 rather than 1110 since an occurrence of variable >= 3 would not make the term closed.
> so we can simply treat that as an alternative to encoding a transition
That's fine for the shift number but a lot of BB research concerns the number of 1s written rather than the number of steps taken, and there it matters. They prefer to use a single model for all variants.
Interesting. Is there a good motivation for using maximum normal form size, instead of number of steps (e.g. under left-to-right eager evaluation)? My first impression is that A333479(n) is not immediately comparable to BB(n), because of measuring size instead of steps.
EDIT: Oh, perhaps there's multiple common definitions for Turing machine busy beaver? Doing some searches, I've seen both (1) number of steps, and (2) number of 1s on the tape when it halts. Perhaps the second notion is more directly comparable to maximum normal form sizes of lambda terms?
I wanted to have a definition that's independent of evaluation strategy, and thus somewhat more robust.
It also makes it easier to comprehend and verify results, such as a(36) corresponding to Church numeral n=2^2^2^3, of size 5*n+6 bits, where I would have a hard time figuring out how long a left-to-right eager evaluation would take.
That is indeed closer to the conventional definition of BB(n) as number of consecutive 1s on output on halting.
Follow-up question, assuming we define BB(n) = max number of 1s written to tape for a halting machine of n states.
Does it make sense to compare BB(n) against A333479(n)?
It seems like A333479(n) grows much faster... my mind is jumping to the classic "problem" of being able to construct a lambda term of size O(2^n) using only O(n) steps. For a Turing machine, writing a symbol requires at least one step. But for lambda, you can generate large terms very quickly.
(Of course, this isn't a fundamental issue with lambda calculus, and there are other notions of size that are more "realistic". But focusing on just lambda calculus normal form sizes, how do we resolve this?)
> Does it make sense to compare BB(n) against A333479(n)?
No, for proper comparison both should measure the argument size in bits.
That's why my top comment talks about the number of bits needed to encode an n-state TM in a straightforward manner.
So compare BB(n) with A333479(n*2*(2+ceil(log(n+1)))).
> In my 2020 survey, I’d relayed an open problem posed by my then 7-year-old daughter Lily: namely, what’s the first n such that BB(n) exceeds A(n), the nth value of the Ackermann function?
The most mind-bending thing to me about the Busy Beaver problem is that once N gets big enough (probably into the low hundreds of states) the machines can start to examine all of mathematics itself, and so likely are posing extremely interesting questions like whether a particular set of finite axioms is complete and consistent, and checking all possible proofs until finally discovering a gigantic theory smaller than PA or ZFC but still far larger than any finite systems we can ever imagine, and halting once all the possible proofs are enumerated. Depending on how our universe turns out to work on a fundamental level, busy beavers may contain a record of the evolution of our universe (and all the alternatives from different initial conditions) from the big bang until the heat death as a trivial lemma in a larger proof. They'll be full of proofs or disproofs of mathematical conjectures in fancy formal systems we'll never have time to discover even with the infinite axiom schemas available to us.
At least that's the most complex, longest-lasting and most bits-written-to-tape task I can imagine specifying in a few hundred bits. The neat thing is that BB(N) considers all the interesting and answerable questions anyone could ever think to ask with N states worth of bits. Sure, maybe there's some trivial rote task that is truly the biggest for a given N (which I doubt; it seems like rote tasks would fall out of an exploration of a larger conceptual space) but some of its neighbors will be absolutely amazing.
> ...longstanding conjecture that BB(5)=47,176,870... Tristan and Damien still count 1.5 million (!) holdout machines...
I assume that if one tries all 1.5 million machines, they either (1) stop before 47,176,870 or (2) run longer, and don't stop for some observable time?
> Kropitz and Michel’s discovery doesn’t settle the question—titanic though it is, the new lower bound on BB(6) is still less than A(6) (!!)
Doesn't the Ackermann function take two arguments? Anyway, what I'm actually more curious about than the result (impressive though it is) is the maths behind verifying these numbers. Does anyone know a gentle introduction to the relevant maths?
> by a combination of automated methods and case-by-case cleverness, people managed to find proofs of non-termination for all the non-halting ... machines
So it's very ad-hoc. You study a particular machines's behaviour and formulate hypotheses about how it can keep going on forever and then try to prove them.
Down here at BB(6) you can feel fairly sure the machine doesn't express anything inherently problematic because it's just too simple. But as the parameter goes up, the machines get sophisticated and very quickly the machines express ideas like "Look at all the positive multiples of seven in turn, halt when Fermat's conjecture is wrong for this value of n" and in that particular case we know the answer is "This never halts" but even thirty years ago the best we can say is "Probably not?".
You only need one "Probably?" or "Probably not?" to be screwed, now you can't even figure out if this machine is a candidate or not.
> Down here at BB(6) you can feel fairly sure the machine doesn't express anything inherently problematic because it's just too simple.
One of the shocking results of Busy Beaver research is that this is actually false. Even with as few as four states there are machines that are complicated and difficult to understand. Turing machine "states" are really GOTO targets, and with six states it's possible to create control flow that is beyond incomprehensible.
Perhaps it means that there is some kind of new and useful (or, interesting at least) generic control flow primitive waiting to be discovered there-- and with it the control flow is again 'simple'. :)
This is really mind boggingly, meaning that there is an actual discrete valicable limit of what can be determined and what can't. Turing machine with 4 states? Cool. Turing machine with 5 states? Sorry, it goes beyond ZFC maths!
The big numbers don't impress me, but the fact that such tiny machines can correspond to complex and even meaningful theorems is fascinating. I wonder what the smallest number of states you need to encode a pre-existing well-known mathematical conjecture is.
They've found a 43-state machine that encodes the Goldbach Conjecture, and proposed but not verified that it can be compressed 27 states. I would consider the Goldbach Conjecture to be "well-known" as far as math theorems go, since it was referenced on Futurama.
It's not "just" that this is uncomputable, given the halting problem. Lots of things in mathematics are uncomputable. What's special about this function is that it will eventually blast through the limits of what any given formalization of mathematics can prove at all, no matter how powerful -- like ZFC + CH + whatever other axioms you come up with.[1]
To be honest, I can't fully wrap my head around what this means. Given that some of these powerful set theoretic axioms are independent from each other, I'm not sure whether ZFC+CH could have a different idea about BB(8000) than ZFC+notCH would. That wouldn't make much sense to me at least, because a Turing machine halting or not halting feels like a concrete fact that shouldn't depend on assumptions about weird infinite sets. But I don't know.
[1] Also from Scott Aaronson's blog, BB(8000) and above are independent from ZFC: https://scottaaronson.blog/?p=2725