7 ms·

(noob rant warning) What bugs me about the decidability thing, is Turing proved 2-undecidability in the action space {halt, loop}, but I still feel like we miss

(noob rant warning) What bugs me about the decidability thing, is Turing proved 2-undecidability in the action space {halt, loop}, but I still feel like we miss an opportunity to try 3-decidability {halt, loop, paradox} and throw out the functions upon which his proof hinged, namely, the ones that invoke the is_halting function and do the opposite. Also, the whole, "we make this other program that does the opposite" argument implies the test of `is_halting` is actually a test of some other function "do_opposite" that wraps "is_halting" and does the opposite. That's not exactly fair, that's a test of the opposite function, not the "is_halting" function. Furthermore, the inner "do_opposite" evaluated by is_halting, is a different invocation of the do_opposite source. (I.E. Fregeian Sense and Reference, a different referent for the same sense). Just because somebody outside the is_halting function can do something counterproductive, doesn't necessarily mean the specific invocation of do_opposite within the closure of is_halting is impossible to classify. Furthermore, is_halting could theoretically refuse to play ball and crash the program at runtime, or induce a compile error before the game can even begin, if we try to create a paradox. Has anyone actually even witnessed a real paradox in real life? Maybe the universe is deeply anti-paradox and the whole argument is a bunch of humbug. Can someone please tell me how I'm fooling myself? Cuz I'm neck deep in coding this thing and building all the helper functions and it would save a bunch of time to know why it's wrong. Every proof seems to boil down to "muh contradiction" which feels like, ok, so what? If the caller wants to do_opposite, that's their problem, not on is_opposite. A function which can decide halting for all the non_opposite functions (which is, every one that matters in practice, right?) Plus, who knows what an anti-paradox machine can accomplish? Maybe there's one weird trick quantum scientists or thermodynamic reversible computer engineers hate, and you can solve hard problems by finding the ones which both halt and don't. Just feels weird how we all accept this quasi-religious belief that we shouldn't even try to decide if programs halt simply because you can't categorize every single program into 2 buckets. What about 3 buckets i.e. 3-decidability of the ternary halting problem? sorry for long comment, fuck it, ill post code, it sucks and doesn't run, just tinkering, but https://github.com/bionicles/halts https://github.com/bionicles/halts published for your pleasure. No promise it will ever actually work.

klyrs 3y ago
Does the following terminate for all n? def foo(n): if n <= 1: return elif n & 1: return foo(3*n+1) else: return foo(n//2)
- deleted 3y ago
  [deleted]
- bl0rg 3y ago
  Running it for larger and larger numbers, will report back soon...
- bionhoward 3y ago
  Collatz is not "theoretically undecidable" because of a paradox, it's "practically undecidable" because it has an infinite domain, so "is_halting" implemented via simulation would take infinite time to try every number. Would you give an engineer an infinitely large project, criticize them for being unable to complete it, and use their 'failure' to support cancellation of a finite, smaller project with potential benefit? Seems like just another lame argument to me.
  - klyrs 3y ago
    Okay. So you acknowledge that your approach will never solve the hard part of the halt/loop/paradox problem that your code hopes to solve. But instead of recognizing this as a fundamental limitation to your approach, you've gone on to create a new class of algorithm: lame. Do you suppose you can come up an algorithm to classify programs as halt/loop/paradox/lame in finite time? Or, how about this one: def foo(n): if n <= 1: return elif n & 1: return foo(n//3) else: return foo(n//2) I can trivially prove this halts for all n. Can your code?
thethirdone 3y ago
It is not clear to me what you would define as the reason to return paradox from `halts`. It is pretty clear you can make a `halts` function that returns halts, loop or unsure. Renaming unsure to paradox would give a valid version of your 3-decidable `halts`. A concrete definition in terms of turing machines is necessary if you want to displace the halting problem. > (I.E. Fregeian Sense and Reference, a different referent for the same sense). For the traditional halting problem, all of the programs are encodings for some particular UTM and therefore we are only talking about referents. The halting problem is the statement that there does not exist a referent for the sense that is "Does referent P halt on input I?" > Just because somebody outside the is_halting function can do something counterproductive, doesn't necessarily mean the specific invocation of do_opposite within the closure of is_halting is impossible to classify. The problem is the inner call and the outer call are definitionally the same. The input to `halts` is an encoding a of turing machine and an input. The construction of the `do_opposite` function is possible no matter what the encoding of `halts` would be. So if `halts` has a valid encoding, there is a corresponding `do_opposite` that totally confuses it and forces the inner and outer eval to be the same. > Every proof seems to boil down to "muh contradiction" which feels like, ok, so what? I think you may misunderstand why everyone is like "muh contradiction". They are doing a proof by contradiction so as soon as they get to a contraction, the proof is complete. I will give a proof of the halting problem for python programs. Theorem: There does not exist a function `halts(program, inputs)` that correctly determines if a given program halts for EVERY input. For the sake of contraction, assume such a function `halts` exists. Then carefully construct a program `do_opposite` that intends to befuddle `halts` as follows: def do_opposite(inputs): if halts(do_opposite,inputs): while True: "Loop" else: return if `halts(do_opposite, inputs) == True` then `do_opposite` must loop forever because the if statement will be followed leading to the inner loop. if `halts(do_opposite, inputs) == False` then `do_opposite` must immediately return because the else statement will be executed. For any return value of `halts(do_opposite, inputs)` it must contradict the definition because it does not correctly behave on this particular input. Because this is a contradiction with the only assumption we have made, that assumption must be wrong. QED.

klyrs 3y ago

Does the following terminate for all n? def foo(n): if n <= 1: return elif n & 1: return foo(3*n+1) else: return foo(n//2)

deleted 3y ago
[deleted]
bl0rg 3y ago
Running it for larger and larger numbers, will report back soon...
bionhoward 3y ago
Collatz is not "theoretically undecidable" because of a paradox, it's "practically undecidable" because it has an infinite domain, so "is_halting" implemented via simulation would take infinite time to try every number. Would you give an engineer an infinitely large project, criticize them for being unable to complete it, and use their 'failure' to support cancellation of a finite, smaller project with potential benefit? Seems like just another lame argument to me.
- klyrs 3y ago
  Okay. So you acknowledge that your approach will never solve the hard part of the halt/loop/paradox problem that your code hopes to solve. But instead of recognizing this as a fundamental limitation to your approach, you've gone on to create a new class of algorithm: lame. Do you suppose you can come up an algorithm to classify programs as halt/loop/paradox/lame in finite time? Or, how about this one: def foo(n): if n <= 1: return elif n & 1: return foo(n//3) else: return foo(n//2) I can trivially prove this halts for all n. Can your code?

thethirdone 3y ago

It is not clear to me what you would define as the reason to return paradox from `halts`. It is pretty clear you can make a `halts` function that returns halts, loop or unsure. Renaming unsure to paradox would give a valid version of your 3-decidable `halts`. A concrete definition in terms of turing machines is necessary if you want to displace the halting problem. > (I.E. Fregeian Sense and Reference, a different referent for the same sense). For the traditional halting problem, all of the programs are encodings for some particular UTM and therefore we are only talking about referents. The halting problem is the statement that there does not exist a referent for the sense that is "Does referent P halt on input I?" > Just because somebody outside the is_halting function can do something counterproductive, doesn't necessarily mean the specific invocation of do_opposite within the closure of is_halting is impossible to classify. The problem is the inner call and the outer call are definitionally the same. The input to `halts` is an encoding a of turing machine and an input. The construction of the `do_opposite` function is possible no matter what the encoding of `halts` would be. So if `halts` has a valid encoding, there is a corresponding `do_opposite` that totally confuses it and forces the inner and outer eval to be the same. > Every proof seems to boil down to "muh contradiction" which feels like, ok, so what? I think you may misunderstand why everyone is like "muh contradiction". They are doing a proof by contradiction so as soon as they get to a contraction, the proof is complete. I will give a proof of the halting problem for python programs. Theorem: There does not exist a function `halts(program, inputs)` that correctly determines if a given program halts for EVERY input. For the sake of contraction, assume such a function `halts` exists. Then carefully construct a program `do_opposite` that intends to befuddle `halts` as follows: def do_opposite(inputs): if halts(do_opposite,inputs): while True: "Loop" else: return if `halts(do_opposite, inputs) == True` then `do_opposite` must loop forever because the if statement will be followed leading to the inner loop. if `halts(do_opposite, inputs) == False` then `do_opposite` must immediately return because the else statement will be executed. For any return value of `halts(do_opposite, inputs)` it must contradict the definition because it does not correctly behave on this particular input. Because this is a contradiction with the only assumption we have made, that assumption must be wrong. QED.