[HN Gopher] Busy Beaver Updates: Now Even Busier
___________________________________________________________________
Busy Beaver Updates: Now Even Busier
Author : nsoonhui
Score : 118 points
Date : 2022-08-31 10:13 UTC (12 hours ago)
(HTM) web link (scottaaronson.blog)
(TXT) w3m dump (scottaaronson.blog)
| tromp wrote:
| 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 hoping it can be under 60 bits...
|
| [1] https://oeis.org/A333479
| tromp wrote:
| Actually it is well under 60 bits!
|
| We have A333479(53) exceeding an exponential tower of 256 2s
| [1].
|
| We also have A333479(114) exceeding Graham's number, which
| would require a 10-state TM to remain competitive.
|
| [1] https://mathoverflow.net/questions/353514/whats-the-
| smallest...
| shwestrick wrote:
| 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?
| shwestrick wrote:
| 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?)
| tromp wrote:
| > 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)))).
| tromp wrote:
| 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.
| codeflo wrote:
| 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.)
| tromp wrote:
| 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.
| codeflo wrote:
| 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.
|
| [1] Also from Scott Aaronson's blog, BB(8000) and above are
| independent from ZFC: https://scottaaronson.blog/?p=2725
| Sharlin wrote:
| 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 Godel, 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
| Godel-territory TM (but this is just an upper bound)! Having an
| unbounded tape as a scratch space helps, of course.
| karatinversion wrote:
| > 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.
| nickdrozd wrote:
| > 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.
| karatinversion wrote:
| 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.
| nickdrozd wrote:
| 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.
| Retric wrote:
| 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.
| xyzzyz wrote:
| 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?
| Retric wrote:
| > 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
|
| Replace "finite table" with "infinite table".
| karatinversion wrote:
| 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.
| jakelazaroff wrote:
| 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.
| Retric wrote:
| You need the table before the machine starts, so "current
| state" is finite but possible states isn't.
|
| Think a given natural number X is finite Aka 2, a list of
| all natural numbers is infinite.
| jakelazaroff wrote:
| 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.
| Retric wrote:
| 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.
| jerf wrote:
| "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.
| Kranar wrote:
| 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.
|
| [1] https://en.wikipedia.org/wiki/Non-
| standard_model_of_arithmet...
| hakuseki wrote:
| 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.
| karatinversion wrote:
| > 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.
| IngoBlechschmid wrote:
| > 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.
| lisper wrote:
| Here is the proof of the result:
|
| https://www.sligocki.com/2022/06/21/bb-6-2-t15.html
|
| It is very accessible and makes fascinating (by geek standards)
| reading.
| vanderZwan wrote:
| > _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?
| H8crilA wrote:
| It's A(6,6)
| vanderZwan wrote:
| Thank you for clearing that up
| tromp wrote:
| As Scott says in his blog comment section [1]
|
| > 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.
|
| [1] https://scottaaronson.blog/?p=6673#comment-1942654
| tialaramex wrote:
| 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.
| ElCheapo wrote:
| 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!
| a_shovel wrote:
| 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.
| lmkg wrote:
| 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.
|
| https://en.wikipedia.org/wiki/Busy_beaver#Notable_instanc
| es
| nickdrozd wrote:
| > 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.
|
| I wrote up some rambly notes about this:
| https://nickdrozd.github.io/2021/09/25/spaghetti-code-
| conjec...
| tialaramex wrote:
| Wow. The BBB(4) example was impressive in particular. I
| stand corrected.
| nullc wrote:
| 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'. :)
| avmich wrote:
| > 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?
|
| Time for some pedagogical articles?
| benlivengood wrote:
| 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.
| [deleted]
| avmich wrote:
| > ...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?
___________________________________________________________________
(page generated 2022-08-31 23:01 UTC)