8 ms·

the question that fascinates me is - what is the property of a program that makes it undecidable? I've been playing around with the idea of trying to make a pro

the question that fascinates me is - what is the property of a program that makes it undecidable? I've been playing around with the idea of trying to make a program that determines halts/doesn't halt/don't know, given some representation of a program. I'm running into some interesting implications when I incorporate dependent typing, but it feels like there must be something theoretical that's already out there.

lisper 8y ago
> what is the property of a program that makes it undecidable? That is itself an undecidable question! There are a lot of programs for which you can tell that they halt (programs with no loops, for example). Likewise there are a lot of programs for which you can tell that they do not halt (any program whose main body is a WHILE TRUE loop in a language that does not have exceptions, for example.) And then there are lots of more complicated cases for which the answer can be found. But there are some cases where we just don't know. The best known is this: https://en.wikipedia.org/wiki/Collatz_conjecture https://en.wikipedia.org/wiki/Collatz_conjecture Not only do we not know the answer, but we don't know if it is even possible to find the answer! We know (because Turing) that there exist programs for which we cannot find the answer, but we don't know whether the Collatz problem is one of them. And in general we cannot know, because if we could then we could use that knowledge to solve the halting problem itself! (We might be able to prove undecidability for particular programs, just as we can prove halting or non-halting for particular programs, but deciding undecidability for any particular program is in general undecidable!)
- beaconstudios 8y ago
  but that's exactly my point - there are clear-cut halting, clear-cut non-halting, and "we don't know yet" programs. My interest is in delineating the properties that separate the 3. The collatz conjecture is exactly the example I use when explaining the "we don't know yet" programs. If I could build a logic system that can positively prove halting, and one that can positively prove non-halting, then anything that remains is "dunno". The halting problem is basically showing that you can never prove the category of "dunno" to be empty. Which is pretty self-evident given there are unsolved bounding problems like the collatz conjecture in mathematics. For a minimal example, if I create a program that takes an AST and runs it through two truth functions, one that checks if the AST === "return;" and prints "it halts" and one that checks if the AST === "while(true) {}" and prints "it never halts", then we've already created such an application, just with a "dunno" space containing the majority of programs. Adding practical axioms to a logic system could grow the "halts" and "never halts" spaces to the point where only a subset of applications cannot be excluded from the "dunno" space, and my question is: what are the unique properties of those applications?
  - lisper 8y ago
    > the properties that separate the 3 But that is exactly my point: what separates these three classes is the state of our current mathematical knowledge, and that obviously changes over time. > Which is pretty self-evident No, that is not at all self-evident. (If it were, someone would have proven it long before Turing, and he wouldn't be famous for it.) I don't know what you mean by a "bounding" problem, but we can prove a lot of things about programs with a structure similar to Collatz. For example, we can prove that a program that searches for a prime larger than its input will always halt for any input.
    - beaconstudios 8y ago
      it's self-evident _at this point in time_, given you could feed such a machine the collatz conjecture as an algorithm and we just don't know if any arbitrary input will halt. I'm not claiming it is self-evident in perpetuity. By bounding problem I guess I mean the mathematical equivalent of knowing it can halt. I'm not a mathematician as I previously stated so I don't know the terminology. I don't think the space I'm talking about is equivalent to the state of all of our mathematical knowledge, as AFAIK not all problems relate directly to this space. But a subset of all mathematics, sure (perhaps computability, or logic in general although of a higher kind than first-order). My interest is in creating a static analyser based on the set of axioms or deductions that can be derived from that space.
      - lisper 8y ago
        > it's self-evident _at this point in time_ No, it's not. Just because you and I don't know the answer is not proof that no one knows the answer. Someone may have discovered the answer in the last five minutes. (In fact, for any mathematical discovery there is always necessarily a period time when only one person knows the answer.) > AFAIK not all problems relate directly to this space And I am telling you that you are wrong about that. If you think that there is anything about computation that does not relate to math then you have a deep misunderstanding of either computation or math (possibly both).
vignesh_m 8y ago
Turing machines output yes/no or indefinitely go on, so that might be like your possible outputs of halts/doesn't halt/don't know. I'm not really sure how much to assume you know, so the [wiki page](https://en.wikipedia.org/wiki/Halting_problem https://en.wikipedia.org/wiki/Halting_problem) might help
chriswarbo 8y ago
> what is the property of a program that makes it undecidable? It's important to keep in mind that undecidability and the halting problem only apply in general, not for some particular input or program. With that said, I think it's to do with program length. The Busy Beaver numbers tell us the maximum number of steps a turing machine can take before halting, when given a program of a certain length. No matter how clever we try to make our static analyser, we ultimately have to write it down as a program (e.g. a turing machine tape, or something more sane ;) ) and this will have a particular, finite size. Hence there is an upper bound on the number of steps that any static analyser can take (the Busy Beaver number for its program length), unless it runs forever without giving us an answer. Consider a particularly simple static analyser: it reads in a program, executes that program for N steps, and checks to see if it halted yet. If it halted, the static analyser halts with the answer "halts"; if it didn't halt, the static analyser halts with the answer "dunno". This static analyser can be improved by using a larger value of N; yet that necessarily requires a longer static analyser program (to contain the larger N value). That's what the Busy Beaver numbers tell us: calculating a number larger than BusyBeaver(X) requires a program more than X bits long; so we can't use a value of N that's larger than the Busy Beaver number of our static analyser's program length. If we want a bigger N, we will eventually need to make our program longer, since that's the only way to increase this bound caused by the Busy Beaver. Note that there is another way we could "improve" such a static analyser: we could remove the cutoff completely, and just run the given program until it halts. In this case, the static analyser itself may not halt, so we're back to square one ;) Now consider that there are infinitely many programs we might feed into a static analyser. These input programs can be arbitrarily long (much longer than our static analyser), and hence the limits imposed on them by the Busy Beaver numbers can be arbitrarily higher than the limits of the static analyser. In particular, their control flow can be arbitrarily complex, such that figuring out whether or not it halts can require an arbitrary amount of calculation steps. Since the number of steps any particular static analyser can perform is bounded by its Busy Beaver number, there will be infinitely many programs which that static analyser can't figure out; even though the same algorithm could figure them out, if given a larger limit to work with. In this sense, we can think of all static analysis algorithms as being like Busy Beaver approximators: they're trying to calculate the largest number they can, in order to reach the number of steps required to analyse whatever program they've been given. They can do this in two ways: by bloating out their codebase to be much bigger than the programs they analyse, or by making their code more complex than the programs they analyse. From a practical point of view, most human-written programs are incredibly simple and verbose; so these Busy Beaver limits aren't really a problem. Yet they're the reason that certain problems cannot be solved in the general case. Some nice links: https://www.scottaaronson.com/writings/bignumbers.html https://www.scottaaronson.com/writings/bignumbers.html https://en.wikipedia.org/wiki/Chaitin%27s_constant https://en.wikipedia.org/wiki/Chaitin%27s_constant https://en.wikipedia.org/wiki/Kolmogorov_complexity#Chaitin%27s_incompleteness_theorem https://en.wikipedia.org/wiki/Kolmogorov_complexity#Chaitin%...

lisper 8y ago

> what is the property of a program that makes it undecidable? That is itself an undecidable question! There are a lot of programs for which you can tell that they halt (programs with no loops, for example). Likewise there are a lot of programs for which you can tell that they do not halt (any program whose main body is a WHILE TRUE loop in a language that does not have exceptions, for example.) And then there are lots of more complicated cases for which the answer can be found. But there are some cases where we just don't know. The best known is this: https://en.wikipedia.org/wiki/Collatz_conjecture https://en.wikipedia.org/wiki/Collatz_conjecture Not only do we not know the answer, but we don't know if it is even possible to find the answer! We know (because Turing) that there exist programs for which we cannot find the answer, but we don't know whether the Collatz problem is one of them. And in general we cannot know, because if we could then we could use that knowledge to solve the halting problem itself! (We might be able to prove undecidability for particular programs, just as we can prove halting or non-halting for particular programs, but deciding undecidability for any particular program is in general undecidable!)

beaconstudios 8y ago
but that's exactly my point - there are clear-cut halting, clear-cut non-halting, and "we don't know yet" programs. My interest is in delineating the properties that separate the 3. The collatz conjecture is exactly the example I use when explaining the "we don't know yet" programs. If I could build a logic system that can positively prove halting, and one that can positively prove non-halting, then anything that remains is "dunno". The halting problem is basically showing that you can never prove the category of "dunno" to be empty. Which is pretty self-evident given there are unsolved bounding problems like the collatz conjecture in mathematics. For a minimal example, if I create a program that takes an AST and runs it through two truth functions, one that checks if the AST === "return;" and prints "it halts" and one that checks if the AST === "while(true) {}" and prints "it never halts", then we've already created such an application, just with a "dunno" space containing the majority of programs. Adding practical axioms to a logic system could grow the "halts" and "never halts" spaces to the point where only a subset of applications cannot be excluded from the "dunno" space, and my question is: what are the unique properties of those applications?
- lisper 8y ago
  > the properties that separate the 3 But that is exactly my point: what separates these three classes is the state of our current mathematical knowledge, and that obviously changes over time. > Which is pretty self-evident No, that is not at all self-evident. (If it were, someone would have proven it long before Turing, and he wouldn't be famous for it.) I don't know what you mean by a "bounding" problem, but we can prove a lot of things about programs with a structure similar to Collatz. For example, we can prove that a program that searches for a prime larger than its input will always halt for any input.
  - beaconstudios 8y ago
    it's self-evident _at this point in time_, given you could feed such a machine the collatz conjecture as an algorithm and we just don't know if any arbitrary input will halt. I'm not claiming it is self-evident in perpetuity. By bounding problem I guess I mean the mathematical equivalent of knowing it can halt. I'm not a mathematician as I previously stated so I don't know the terminology. I don't think the space I'm talking about is equivalent to the state of all of our mathematical knowledge, as AFAIK not all problems relate directly to this space. But a subset of all mathematics, sure (perhaps computability, or logic in general although of a higher kind than first-order). My interest is in creating a static analyser based on the set of axioms or deductions that can be derived from that space.
    - lisper 8y ago
      > it's self-evident _at this point in time_ No, it's not. Just because you and I don't know the answer is not proof that no one knows the answer. Someone may have discovered the answer in the last five minutes. (In fact, for any mathematical discovery there is always necessarily a period time when only one person knows the answer.) > AFAIK not all problems relate directly to this space And I am telling you that you are wrong about that. If you think that there is anything about computation that does not relate to math then you have a deep misunderstanding of either computation or math (possibly both).

vignesh_m 8y ago

Turing machines output yes/no or indefinitely go on, so that might be like your possible outputs of halts/doesn't halt/don't know. I'm not really sure how much to assume you know, so the [wiki page](https://en.wikipedia.org/wiki/Halting_problem https://en.wikipedia.org/wiki/Halting_problem) might help

chriswarbo 8y ago

> what is the property of a program that makes it undecidable? It's important to keep in mind that undecidability and the halting problem only apply in general, not for some particular input or program. With that said, I think it's to do with program length. The Busy Beaver numbers tell us the maximum number of steps a turing machine can take before halting, when given a program of a certain length. No matter how clever we try to make our static analyser, we ultimately have to write it down as a program (e.g. a turing machine tape, or something more sane ;) ) and this will have a particular, finite size. Hence there is an upper bound on the number of steps that any static analyser can take (the Busy Beaver number for its program length), unless it runs forever without giving us an answer. Consider a particularly simple static analyser: it reads in a program, executes that program for N steps, and checks to see if it halted yet. If it halted, the static analyser halts with the answer "halts"; if it didn't halt, the static analyser halts with the answer "dunno". This static analyser can be improved by using a larger value of N; yet that necessarily requires a longer static analyser program (to contain the larger N value). That's what the Busy Beaver numbers tell us: calculating a number larger than BusyBeaver(X) requires a program more than X bits long; so we can't use a value of N that's larger than the Busy Beaver number of our static analyser's program length. If we want a bigger N, we will eventually need to make our program longer, since that's the only way to increase this bound caused by the Busy Beaver. Note that there is another way we could "improve" such a static analyser: we could remove the cutoff completely, and just run the given program until it halts. In this case, the static analyser itself may not halt, so we're back to square one ;) Now consider that there are infinitely many programs we might feed into a static analyser. These input programs can be arbitrarily long (much longer than our static analyser), and hence the limits imposed on them by the Busy Beaver numbers can be arbitrarily higher than the limits of the static analyser. In particular, their control flow can be arbitrarily complex, such that figuring out whether or not it halts can require an arbitrary amount of calculation steps. Since the number of steps any particular static analyser can perform is bounded by its Busy Beaver number, there will be infinitely many programs which that static analyser can't figure out; even though the same algorithm could figure them out, if given a larger limit to work with. In this sense, we can think of all static analysis algorithms as being like Busy Beaver approximators: they're trying to calculate the largest number they can, in order to reach the number of steps required to analyse whatever program they've been given. They can do this in two ways: by bloating out their codebase to be much bigger than the programs they analyse, or by making their code more complex than the programs they analyse. From a practical point of view, most human-written programs are incredibly simple and verbose; so these Busy Beaver limits aren't really a problem. Yet they're the reason that certain problems cannot be solved in the general case. Some nice links: https://www.scottaaronson.com/writings/bignumbers.html https://www.scottaaronson.com/writings/bignumbers.html https://en.wikipedia.org/wiki/Chaitin%27s_constant https://en.wikipedia.org/wiki/Chaitin%27s_constant https://en.wikipedia.org/wiki/Kolmogorov_complexity#Chaitin%27s_incompleteness_theorem https://en.wikipedia.org/wiki/Kolmogorov_complexity#Chaitin%...