4 ms·

Is this what we mean when we says BB are uncomputable? That as BB grows they incompass all of maths, requiring us to prove everything?

noqc 3y ago
If BB is a computable function, then you can solve the halting problem by running every turing machine with n states for BB(n), and the ones that don't halt by then don't halt at all.
gpm 3y ago
Sort of. There are math problems that we "know" we can't prove or disprove, unless we can prove every statement both true and false (this is Godel's first incompleteness theorem). If we can prove every statement both true and false then our proof system just sucks and proving something means nothing so we should choose another proof system where that's not the case, so we assume we're in the first case (there are math problems that we know we can't prove or disprove). Incidentally Godel's second incompleteness theorem is that we can't ever prove we are in the first case. And then ya, BB being incomputable means that as BB grows at some point they start to be able to encode programs that halt if and only if a problem we can't prove or disprove is true. So we can't prove that program does or doesn't halt. Now, technically, proving/disproving something you can't prove or disprove would be proving false, which in turn could be used to "prove" every statement, and would therefore "encompass all maths", so what you said is in a sense correct. It's a threshold condition though, and one that kicks in well before you have turing machines large enough to encode "every" math problem. And in fact there is no finite number of states sufficient to encode every math problem (I can just make longer and longer strings of arithmetic for instance)...
- pjot 3y ago
  So is this (BB) then just an exercise demonstrating our inability to reasonably solve the problem? I suppose what I’m asking is what is its significance? Or why does this matter? As a self taught programmer, I realize I have definite gaps in the more theoretical realms of computer science.
  - gpm 3y ago
    The collatz conjecture isn't a problem that we think is unsolvable, it probably (maybe even definitely?) has a solution. It is a problem that a lot of really good mathematicians have sunk a lot of time into and made basically no progress. Collectively the mathematical community has more or less decided that we don't know how to even approach solving this kind of problem yet, and probably won't be able to solve it in the foreseeable future. This article is saying that solving for BB(3, 3) requires solving a collatz-conjecture like problem, so it's probably also beyond our current abilities in mathematics. It's not saying it's unsolvable, just that we probably won't figure out the solution anytime soon. As for why solving BB(3, 3) matters... it doesn't really. It's just an intellectual curiosity. We've figured out some busy beaver numbers. We've proven some upper bounds on the biggest ones we can figure out, but there's a big gap between what we've solved and what we've shown we can't solve for. Making that gap smaller is something of a game.
    - pjot 3y ago
      Got it. Thanks for adding context!
  - sligocki 3y ago
    The Busy Beaver problem sits somewhere on the range from "intellectual curiosity" to "lens that allows us to view the edges of uncomputability". I would guess that the majority of people doing work here are hobbyists (including myself). In fact, when Tibor Rado first introduced BB, he introduced it as the "Busy Beaver Game", so it has had a playful energy since the beginning :)
kmeisthax 3y ago
Sort of. Uncomputable functions exist because the halting problem exists. So any function whose definition includes anything to do with halting also becomes uncomputable. e.g. BB is uncomputable because you have to determine all the TMs that would halt given n and m. The entire rest of mathematics is smuggled into BB via the halting problem: you can write programs that only halt if arbitrary mathematical conjectures are true or false, so anything that wants to solve the halting problem or solve BB has to be able to know all maths[0]. Of course, this is possible because Turing-completeness is the boundary of computability. Anything that can have a computer in it is itself a computer. [0] This isn't actually the thing that makes halting undecidable. Undecidability comes from programs that "pull themselves into the halting problem" by only halting if a hypothetical halting problem decider would claim that they don't halt.
- penteract 3y ago
  > you can write programs that only halt if arbitrary mathematical conjectures are true or false I don't think this is quite right - you can write programs that halt iff arbitrary mathematical conjectures are provable (in a suitable system of logic/axioms such as ZFC), but there are problems (such as questions about Turing machines with a halting problem oracle[0]) for which we can't straightforwardly construct a program which halts iff they are true. [0] https://en.wikipedia.org/wiki/Oracle_machine#Oracles_and_halting_problems https://en.wikipedia.org/wiki/Oracle_machine#Oracles_and_hal...
- luc4 3y ago
  > Uncomputable functions exist because the halting problem exists. Uncomputable functions exist because there are only countably many Turing machines. There are problems that stay uncomputable even if the halting problem were computable.
deleted 3y ago
[deleted]
CJefferson 3y ago
Greatly simplifying, the most important result in comparability is “the halting problem”, which means we have no way of telling, for any program, if given some input it will halt or run forever. After that, it’s not surprising there is some BB we can’t solve, and it’s interesting to investigate which we can, and can’t, solve.
- nine_k 3y ago
  Not "for any program", but "for an arbitrary program". We can trivially prove that a program that always goes to the next step, without branching, always terminates. With more effort we can prove termination of certain segments with conditional jumps, certain forms of recursion and loops, etc. This is not purely theoretic: e.g. EBPF programs in the Linux kernel are only admitted if the kernel can prove that they terminahe. What we can't do is to prove it in an arbitrary case, without putting limits on the program's structure.

noqc 3y ago

If BB is a computable function, then you can solve the halting problem by running every turing machine with n states for BB(n), and the ones that don't halt by then don't halt at all.

gpm 3y ago

Sort of. There are math problems that we "know" we can't prove or disprove, unless we can prove every statement both true and false (this is Godel's first incompleteness theorem). If we can prove every statement both true and false then our proof system just sucks and proving something means nothing so we should choose another proof system where that's not the case, so we assume we're in the first case (there are math problems that we know we can't prove or disprove). Incidentally Godel's second incompleteness theorem is that we can't ever prove we are in the first case. And then ya, BB being incomputable means that as BB grows at some point they start to be able to encode programs that halt if and only if a problem we can't prove or disprove is true. So we can't prove that program does or doesn't halt. Now, technically, proving/disproving something you can't prove or disprove would be proving false, which in turn could be used to "prove" every statement, and would therefore "encompass all maths", so what you said is in a sense correct. It's a threshold condition though, and one that kicks in well before you have turing machines large enough to encode "every" math problem. And in fact there is no finite number of states sufficient to encode every math problem (I can just make longer and longer strings of arithmetic for instance)...

pjot 3y ago
So is this (BB) then just an exercise demonstrating our inability to reasonably solve the problem? I suppose what I’m asking is what is its significance? Or why does this matter? As a self taught programmer, I realize I have definite gaps in the more theoretical realms of computer science.
- gpm 3y ago
  The collatz conjecture isn't a problem that we think is unsolvable, it probably (maybe even definitely?) has a solution. It is a problem that a lot of really good mathematicians have sunk a lot of time into and made basically no progress. Collectively the mathematical community has more or less decided that we don't know how to even approach solving this kind of problem yet, and probably won't be able to solve it in the foreseeable future. This article is saying that solving for BB(3, 3) requires solving a collatz-conjecture like problem, so it's probably also beyond our current abilities in mathematics. It's not saying it's unsolvable, just that we probably won't figure out the solution anytime soon. As for why solving BB(3, 3) matters... it doesn't really. It's just an intellectual curiosity. We've figured out some busy beaver numbers. We've proven some upper bounds on the biggest ones we can figure out, but there's a big gap between what we've solved and what we've shown we can't solve for. Making that gap smaller is something of a game.
  - pjot 3y ago
    Got it. Thanks for adding context!
- sligocki 3y ago
  The Busy Beaver problem sits somewhere on the range from "intellectual curiosity" to "lens that allows us to view the edges of uncomputability". I would guess that the majority of people doing work here are hobbyists (including myself). In fact, when Tibor Rado first introduced BB, he introduced it as the "Busy Beaver Game", so it has had a playful energy since the beginning :)

kmeisthax 3y ago

Sort of. Uncomputable functions exist because the halting problem exists. So any function whose definition includes anything to do with halting also becomes uncomputable. e.g. BB is uncomputable because you have to determine all the TMs that would halt given n and m. The entire rest of mathematics is smuggled into BB via the halting problem: you can write programs that only halt if arbitrary mathematical conjectures are true or false, so anything that wants to solve the halting problem or solve BB has to be able to know all maths[0]. Of course, this is possible because Turing-completeness is the boundary of computability. Anything that can have a computer in it is itself a computer. [0] This isn't actually the thing that makes halting undecidable. Undecidability comes from programs that "pull themselves into the halting problem" by only halting if a hypothetical halting problem decider would claim that they don't halt.

penteract 3y ago
> you can write programs that only halt if arbitrary mathematical conjectures are true or false I don't think this is quite right - you can write programs that halt iff arbitrary mathematical conjectures are provable (in a suitable system of logic/axioms such as ZFC), but there are problems (such as questions about Turing machines with a halting problem oracle[0]) for which we can't straightforwardly construct a program which halts iff they are true. [0] https://en.wikipedia.org/wiki/Oracle_machine#Oracles_and_halting_problems https://en.wikipedia.org/wiki/Oracle_machine#Oracles_and_hal...
luc4 3y ago
> Uncomputable functions exist because the halting problem exists. Uncomputable functions exist because there are only countably many Turing machines. There are problems that stay uncomputable even if the halting problem were computable.

deleted 3y ago

[deleted]

CJefferson 3y ago

Greatly simplifying, the most important result in comparability is “the halting problem”, which means we have no way of telling, for any program, if given some input it will halt or run forever. After that, it’s not surprising there is some BB we can’t solve, and it’s interesting to investigate which we can, and can’t, solve.

nine_k 3y ago
Not "for any program", but "for an arbitrary program". We can trivially prove that a program that always goes to the next step, without branching, always terminates. With more effort we can prove termination of certain segments with conditional jumps, certain forms of recursion and loops, etc. This is not purely theoretic: e.g. EBPF programs in the Linux kernel are only admitted if the kernel can prove that they terminahe. What we can't do is to prove it in an arbitrary case, without putting limits on the program's structure.