7 ms·

The Busy Beaver Game

112 points by mathgenius 10y ago

pohl 10y ago
Edit: whoa, they really buried the lede: the upper bound for the knowable values may be as low as BB(1919) as of May 15! I'm confused by the winning TM given for BB(2). It has 3 non-halt states, but N==2 should be a TM with 2, shouldn't it? Did they merely put the illustration for BB(3) in the wrong place? Edit: yeah, looks like they just put the illustration for BB(3) in the wrong place: https://en.wikipedia.org/wiki/Turing_machine#/media/File:State_diagram_3_state_busy_beaver_2B.svg https://en.wikipedia.org/wiki/Turing_machine#/media/File:Sta...
- 9911o9w8191 10y ago
  The author has the first name "John Carlos". Why not take an educated guess and use (gasp) gendered pronouns?
  - pohl 10y ago
    Because the byline wasn't easy to find on the device I read it on, and the possibility that someone might be offended by gender neutrality seemed far-fetched at the time.
  - random28345 10y ago
    > The author has the first name "John Carlos". Why not take an educated guess and use (gasp) gendered pronouns? Because the text of the article could have been generated by a Turing machine with the pseudonym "John Carlos". And on the internet, nobody knows if you're a man, woman, dog, or sufficiently complicated state machine. tl;dr: Non-gendered pronouns are inclusive and never inappropriate on the internet.
shmageggy 10y ago
I'm trying to get an intuition about why this whole game can even be played, and it's proving (ha) rather tricky. I'm ok with the idea that things sometimes cross into the realm of the impossible when transitioning from discrete/finite to continuous/infinite, or maybe from countably to uncountably infinite, but the notion that there's some constant threshold seems so counterintuitive. The link at the end of the article is pretty good [1] as is wikipedia [2], but I'm clearly missing some intuition here. Help! [1] https://johncarlosbaez.wordpress.com/2011/10/28/the-complexity-barrier/ https://johncarlosbaez.wordpress.com/2011/10/28/the-complexi... [2] https://en.wikipedia.org/wiki/Kolmogorov_complexity#Chaitin.27s_incompleteness_theorem https://en.wikipedia.org/wiki/Kolmogorov_complexity#Chaitin....
- ikeboy 10y ago
  You can't solve the halting problem. Therefore, if you take a program that takes a Turing machine as input, searches for a proof in ZFC (or your favorite alternative) that the program halts or that it doesn't, and if it doesn't find a proof either way then it runs forever, your program is not a halting solver. Therefore, there are some Turing machines which can't be proven to halt or run forever in any given consistent system that can be computed. (Because if every TM had a proof, then the program above would solve the unsolvable halting problem). Therefore, there is a smallest such program that's independent of ZFC. Does that help?
  - andrewflnr 10y ago
    Therefore, there are some Turing machines which can't be proven to halt or run forever in any given consistent system that can be computed. I feel like it's worth clarifying the quantifiers here. For all consistent systems, there exist Turing machines whose halting behavior can't be proven in that system. Unless I have some disastrous misunderstanding...
    - ikeboy 10y ago
      Well a consistent system that can't be computed can prove things about all Turing machines. E.g. ZFC plus an infinite set of axioms of the sort "machine X halts" for all machines that halt. We can't compute all the axioms, but the system is perfectly consistent. We could compute the axioms if we had a halting Oracle. It wouldn't be able to prove the halting behavior of some Turing machines that have halting oracles attached, though.
  - pdkl95 10y ago
    > Therefore, there is a smallest such program that's independent of ZFC. http://www.scottaaronson.com/blog/?p=2725 http://www.scottaaronson.com/blog/?p=2725 we give a 7,918-state Turing machine, called Z (and actually explicitly listed in our paper!), such that: Z runs forever, assuming the consistency of a large-cardinal theory called SRP (Stationary Ramsey Property), but Z can’t be proved to run forever in ZFC [...], assuming that ZFC is consistent. edit: Just saw that this was linked at the bottom of the article. As pohl mentioned, the article really buried the lede.
rrobukef 10y ago
They created a Turing machine that may run forever. However we can't prove that. It could stop the next second, or tomorrow, or the day after. They also proved however that you'll never see it halt. Because that would be a proof of consistency. Wait. What?
- tromp 10y ago
  No; halting would be a proof of inconsistency. We expect it never to halt because we believe ZFC to be consistent.
  - rrobukef 10y ago
    Belief has nothing to do with it. I can believe ZFC is inconsistent and the world will not change a bit. You can't prove me wrong. (It's almost a religious argument) If I believe the inconsistency of ZFC then I believe the machine must halt. I can't ever observe it since I can't know the number of steps needed. There's almost a paradox but not quite.
    - Grue3 10y ago
      No, if ZFC is inconsistent, then you can know the number of steps needed. Every statement, true or false, is derivable from ZFC if it is inconsistent. If there's contradiction in ZFC, it can be found in finite time by enumerating all the theorems.
- deleted 10y ago
  [deleted]
- zodiac 10y ago
  If you're refering to Yedidia and Aaronson's machine, the machine searches for counterexamples in ZFC. We believe, but cannot prove, that ZFC is consistent. Also, we can prove that assuming ZFC is consistent, ZFC cannot prove that ZFC is consistent. Hence, since we believe ZFC is consistent, we believe that the machine will not halt, but we can't prove it. This implies that BB(7910) cannot be computed.
delsarto 10y ago
Numberphile did a great video on Busy Beaver which I found easy to follow - https://youtu.be/CE8UhcyJS0I https://youtu.be/CE8UhcyJS0I
quantumtremor 10y ago
I made a small implementation of the Busy Beaver game in React a while ago: http://rajk.me/static/busybeaver.html http://rajk.me/static/busybeaver.html. (Click the rules to toggle them). Start with 1-state, and 2-state is a decent challenge. Not sure if 3-state is possible by hand.
deleted 10y ago
[deleted]
millstone 10y ago
The article says "if the usual axioms of set theory are consistent, we can never use them to determine the value of BB(7910)." But why does this imply that BB(7910) is uncomputable? Perhaps another axiomatic system could compute its value?
- wolfgke 10y ago
  > Perhaps another axiomatic system could compute its value? Of course another axiomatic system could. If you could tell us such an axiomatic system for which you can prove that it can determine the value of BB(7910) and have strong arguments why it is probably consistent (by Gödel one will not be able to prove this property if it is able to express basic arithmetic) mathematicians would love to get to know it, since they really have no idea how such a system might look like.
  - ikeboy 10y ago
    It's easy to specify such a system that's more powerful than ZFC and has strong arguments for its consistency: ZFC+con(ZFC), which is consistent iff ZFC is consistent. And it's easy to go one level up, I.e that system plus it's own consistency. These systems will be stronger than ZFC, and will prove the machine in question halts. Of course, the lowest unknowable from ZFC BB number is probably around BB(15), so likely none of those systems get that high, but they do probably give us more than just ZFC does. See also http://www.scottaaronson.com/blog/?p=697 http://www.scottaaronson.com/blog/?p=697 for some limitations on this. Also, there are large cardinal axioms which imply the consistency of ZFC and are believed to be consistent, but I'm not so familiar with them. I think mathematicians would consider those axioms as "what such a system would look like".
  - hyperpape 10y ago
    I think they do have some ideas. You might look at Believing The Axioms (http://cs.umd.edu/~gasarch/BLOGPAPERS/belaxioms1.pdf http://cs.umd.edu/~gasarch/BLOGPAPERS/belaxioms1.pdf, but it's two parts) which studies set theorists who are investigating new axioms for set theory, especially large cardinal axioms, iirc. Honestly, that work is a ways beyond what I can understand, but it's clear that it's an active area of research. You might also read about Hugh Woodin has a very developed program arguing for axioms which would imply the negation of the Continuum Hypothesis. (This doesn't necessarily apply to this specific question, but in general, research into axiomatic foundations of math is ongoing).
csl 10y ago
FWIW, I implemented some BB code in Python and made some pretty neat plots: https://github.com/cslarsen/busy-beaver https://github.com/cslarsen/busy-beaver Of course I cheat by knowing S(n).
pkrumins 10y ago
I wrote an interesting article a while ago with graphs of how the beaver walks across the tape, and other interesting info. http://www.catonmat.net/blog/busy-beaver/ http://www.catonmat.net/blog/busy-beaver/

112 points by mathgenius 10y ago

pohl 10y ago

Edit: whoa, they really buried the lede: the upper bound for the knowable values may be as low as BB(1919) as of May 15! I'm confused by the winning TM given for BB(2). It has 3 non-halt states, but N==2 should be a TM with 2, shouldn't it? Did they merely put the illustration for BB(3) in the wrong place? Edit: yeah, looks like they just put the illustration for BB(3) in the wrong place: https://en.wikipedia.org/wiki/Turing_machine#/media/File:State_diagram_3_state_busy_beaver_2B.svg https://en.wikipedia.org/wiki/Turing_machine#/media/File:Sta...

9911o9w8191 10y ago
The author has the first name "John Carlos". Why not take an educated guess and use (gasp) gendered pronouns?
- pohl 10y ago
  Because the byline wasn't easy to find on the device I read it on, and the possibility that someone might be offended by gender neutrality seemed far-fetched at the time.
- random28345 10y ago
  > The author has the first name "John Carlos". Why not take an educated guess and use (gasp) gendered pronouns? Because the text of the article could have been generated by a Turing machine with the pseudonym "John Carlos". And on the internet, nobody knows if you're a man, woman, dog, or sufficiently complicated state machine. tl;dr: Non-gendered pronouns are inclusive and never inappropriate on the internet.

shmageggy 10y ago

I'm trying to get an intuition about why this whole game can even be played, and it's proving (ha) rather tricky. I'm ok with the idea that things sometimes cross into the realm of the impossible when transitioning from discrete/finite to continuous/infinite, or maybe from countably to uncountably infinite, but the notion that there's some constant threshold seems so counterintuitive. The link at the end of the article is pretty good [1] as is wikipedia [2], but I'm clearly missing some intuition here. Help! [1] https://johncarlosbaez.wordpress.com/2011/10/28/the-complexity-barrier/ https://johncarlosbaez.wordpress.com/2011/10/28/the-complexi... [2] https://en.wikipedia.org/wiki/Kolmogorov_complexity#Chaitin.27s_incompleteness_theorem https://en.wikipedia.org/wiki/Kolmogorov_complexity#Chaitin....

ikeboy 10y ago
You can't solve the halting problem. Therefore, if you take a program that takes a Turing machine as input, searches for a proof in ZFC (or your favorite alternative) that the program halts or that it doesn't, and if it doesn't find a proof either way then it runs forever, your program is not a halting solver. Therefore, there are some Turing machines which can't be proven to halt or run forever in any given consistent system that can be computed. (Because if every TM had a proof, then the program above would solve the unsolvable halting problem). Therefore, there is a smallest such program that's independent of ZFC. Does that help?
- andrewflnr 10y ago
  Therefore, there are some Turing machines which can't be proven to halt or run forever in any given consistent system that can be computed. I feel like it's worth clarifying the quantifiers here. For all consistent systems, there exist Turing machines whose halting behavior can't be proven in that system. Unless I have some disastrous misunderstanding...
  - ikeboy 10y ago
    Well a consistent system that can't be computed can prove things about all Turing machines. E.g. ZFC plus an infinite set of axioms of the sort "machine X halts" for all machines that halt. We can't compute all the axioms, but the system is perfectly consistent. We could compute the axioms if we had a halting Oracle. It wouldn't be able to prove the halting behavior of some Turing machines that have halting oracles attached, though.
- pdkl95 10y ago
  > Therefore, there is a smallest such program that's independent of ZFC. http://www.scottaaronson.com/blog/?p=2725 http://www.scottaaronson.com/blog/?p=2725 we give a 7,918-state Turing machine, called Z (and actually explicitly listed in our paper!), such that: Z runs forever, assuming the consistency of a large-cardinal theory called SRP (Stationary Ramsey Property), but Z can’t be proved to run forever in ZFC [...], assuming that ZFC is consistent. edit: Just saw that this was linked at the bottom of the article. As pohl mentioned, the article really buried the lede.

rrobukef 10y ago

They created a Turing machine that may run forever. However we can't prove that. It could stop the next second, or tomorrow, or the day after. They also proved however that you'll never see it halt. Because that would be a proof of consistency. Wait. What?

tromp 10y ago
No; halting would be a proof of inconsistency. We expect it never to halt because we believe ZFC to be consistent.
- rrobukef 10y ago
  Belief has nothing to do with it. I can believe ZFC is inconsistent and the world will not change a bit. You can't prove me wrong. (It's almost a religious argument) If I believe the inconsistency of ZFC then I believe the machine must halt. I can't ever observe it since I can't know the number of steps needed. There's almost a paradox but not quite.
  - Grue3 10y ago
    No, if ZFC is inconsistent, then you can know the number of steps needed. Every statement, true or false, is derivable from ZFC if it is inconsistent. If there's contradiction in ZFC, it can be found in finite time by enumerating all the theorems.
deleted 10y ago
[deleted]
zodiac 10y ago
If you're refering to Yedidia and Aaronson's machine, the machine searches for counterexamples in ZFC. We believe, but cannot prove, that ZFC is consistent. Also, we can prove that assuming ZFC is consistent, ZFC cannot prove that ZFC is consistent. Hence, since we believe ZFC is consistent, we believe that the machine will not halt, but we can't prove it. This implies that BB(7910) cannot be computed.

delsarto 10y ago

Numberphile did a great video on Busy Beaver which I found easy to follow - https://youtu.be/CE8UhcyJS0I https://youtu.be/CE8UhcyJS0I

quantumtremor 10y ago

I made a small implementation of the Busy Beaver game in React a while ago: http://rajk.me/static/busybeaver.html http://rajk.me/static/busybeaver.html. (Click the rules to toggle them). Start with 1-state, and 2-state is a decent challenge. Not sure if 3-state is possible by hand.

deleted 10y ago

[deleted]

millstone 10y ago

The article says "if the usual axioms of set theory are consistent, we can never use them to determine the value of BB(7910)." But why does this imply that BB(7910) is uncomputable? Perhaps another axiomatic system could compute its value?

wolfgke 10y ago
> Perhaps another axiomatic system could compute its value? Of course another axiomatic system could. If you could tell us such an axiomatic system for which you can prove that it can determine the value of BB(7910) and have strong arguments why it is probably consistent (by Gödel one will not be able to prove this property if it is able to express basic arithmetic) mathematicians would love to get to know it, since they really have no idea how such a system might look like.
- ikeboy 10y ago
  It's easy to specify such a system that's more powerful than ZFC and has strong arguments for its consistency: ZFC+con(ZFC), which is consistent iff ZFC is consistent. And it's easy to go one level up, I.e that system plus it's own consistency. These systems will be stronger than ZFC, and will prove the machine in question halts. Of course, the lowest unknowable from ZFC BB number is probably around BB(15), so likely none of those systems get that high, but they do probably give us more than just ZFC does. See also http://www.scottaaronson.com/blog/?p=697 http://www.scottaaronson.com/blog/?p=697 for some limitations on this. Also, there are large cardinal axioms which imply the consistency of ZFC and are believed to be consistent, but I'm not so familiar with them. I think mathematicians would consider those axioms as "what such a system would look like".
- hyperpape 10y ago
  I think they do have some ideas. You might look at Believing The Axioms (http://cs.umd.edu/~gasarch/BLOGPAPERS/belaxioms1.pdf http://cs.umd.edu/~gasarch/BLOGPAPERS/belaxioms1.pdf, but it's two parts) which studies set theorists who are investigating new axioms for set theory, especially large cardinal axioms, iirc. Honestly, that work is a ways beyond what I can understand, but it's clear that it's an active area of research. You might also read about Hugh Woodin has a very developed program arguing for axioms which would imply the negation of the Continuum Hypothesis. (This doesn't necessarily apply to this specific question, but in general, research into axiomatic foundations of math is ongoing).

csl 10y ago

FWIW, I implemented some BB code in Python and made some pretty neat plots: https://github.com/cslarsen/busy-beaver https://github.com/cslarsen/busy-beaver Of course I cheat by knowing S(n).

pkrumins 10y ago

I wrote an interesting article a while ago with graphs of how the beaver walks across the tape, and other interesting info. http://www.catonmat.net/blog/busy-beaver/ http://www.catonmat.net/blog/busy-beaver/