Live data from Hacker News

What Computers Cannot Do: The Consequences of Turing-Completeness

yzena.com

21–30 of 61 posts

Re: What Computers Cannot Do: The Consequences of Turing-Completeness

#21

(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"…

Does the following terminate for all n?

  def foo(n):
    if n 

Re: What Computers Cannot Do: The Consequences of Turing-Completeness

#22

(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"…

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.

Re: What Computers Cannot Do: The Consequences of Turing-Completeness

#23

(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"…

The more tractable problem is {halt, loop, unknown}. That problem us trivially solvable, and solved by every static analysis tool and optimizing compiler. Or at least, the generalized {yes, no, maybe} problem for various properties is.

The real question is, how small can you make the set of instances that results in "maybe", and how small can you make the intersection of that set, and the set of instances we actually care about.

And, it turns out, you can typically make that intersection pretty small.

Regarding the question as you stated it. If you define "paradox" as whatever situation your algorithm cannot handle, then it us trivial. If you define "paradox" as the smallest possible set of "maybe", then determining what instances belong in paradox is equivalent to solving the halting problem.

Re: What Computers Cannot Do: The Consequences of Turing-Completeness

#26
post #15

To quickly summarize: A Turing machine program or method can't solve the Entscheidungsproblem, which means you can't have a general algorithm to prove all possible statements true or or false (or equivalent) within a formal system. For example you can't have a general program that you feed in any 2 mathematical statements and tells you if they're equal. From what I understand this is proven for "regular math" but not…

[deleted]

Re: What Computers Cannot Do: The Consequences of Turing-Completeness

#28

I will never understand how people think like that. Sure, there are things computers cannot compute, but that's because those things are _uncomputable_ in general

It's obvious to you because of people like Church and Turing. Until their work on the Entscheidungsproblem was published, it was not only common, but mainstream to believe that nothing was inherently incomputable. They not only demonstrated that there were things that weren't, they did so by proving that the set of everything computable was the same set of things their approaches could compute and that certain problems were outside that set.

Re: What Computers Cannot Do: The Consequences of Turing-Completeness

#29
I don't quite understand what big point this is trying to make. It's very down on formal verification, but does that mean all formal verification should be thrown away?

Strong static typing? It's generally possible to write valid programs (i.e., that would run successfully without runtime errors) that don't type-check successfully. So the set of type-safe programs is smaller than the set of useful programs. Is that an argument for discarding type safety? No, because the vast majority of programs we want to write can be type-checked and it's useful to do so.

Termination checking? This post has a nice example of an effectively-non-terminating loop in Bazel. Bazel's control language doesn't have unbounded loops, so the author just nests a bunch of very long loops. It's fun, but "it's possible to write a Bazel build script that takes an infeasibly long time to run, effectively infinite" doesn't seem like a problem in practice. It's still hard to write such a thing accidentally!

Re: What Computers Cannot Do: The Consequences of Turing-Completeness

#30
post #21

(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"…

Does the following terminate for all n? def foo(n): if n

[deleted]
Post reply on HN