TIL: <Halting problem is not a limitation of compu...
# linking-together
n
TIL: Halting problem is not a limitation of computability but an inconsistency of specification:
We have no reason to believe that a program in a Turing-Machine-Equivalent programming language cannot be written to determine halting for all programs in a Turing-Machine-Equivalent programming language. We just have to ensure that the programs being analyzed cannot call the program doing the analysis.
😮 1
❤️ 3
The video explainer is fantastic (51 minutes): http://www.cs.utoronto.ca/~hehner/PwHvideo.mp4 This doesn't seem to be a mainstream view yet but I found Hehner's argument persuasive.
p
I watched most of the video, skipping some of the parts at the beginning. I'm not at all convinced. In particular, I don't follow how he is able to dismiss the hypothetical translation of the halting function between languages. In his example, the behavior of the function changes when it gets translated due to being "subjective," but the definition of accurate translation is that the behavior does not change, so how a halting function that says yes in Python can be accurately translated into one that says no in Pascal for the same inputs baffles me. The standard proofs begin with a generalized halting function because that is the thing we wish existed. The complexity that he criticizes is a consequence of the goal of the proof. It seems to me that the order in which the functions are specified matters. If you assume that a halting function exists, and then construct the twist function, the twist function does not need to be able to call the halting function. It could contain the algorithm in line, for example. In this case it absolutely would not matter whether the functions were written in different languages or not. The point isn't that there is no halting function that works for a given twist. The point is that for any hypothetical halting function, there exists a twist upon which it does not work. Some of the examples he gives demonstrating that the same reasoning can be used to prove the uncomputability of other results, including a made-up behavior that he invented, just look like roundabout proofs of Rice's Theorem to me.
n
g
The halting problem is equivalent to Gödel’s Theorems (in the sense that either is easily demonstrated from the other). So there’s also that.
m
@Personal Dynamic Media I think you may have missed the fragment that starts at 15:10 in the video (https://www.cs.utoronto.ca/~hehner/PwHvideo.mp4). This is the key point. The author says that the "computability" property brings nothing to the halting problem and could be simply replaced with "is true". Then the halting problem becomes equivalent to the liar's paradox - a statement that negates itself. The argument doesn't involve the details of the halting function - because it could be replaced with any other statement: "X is omnipotent" gives the omnipotence paradox, "X terminates" gives halting problem, "X is provable" gives incompleteness theorem, etc.
p
@Marek Rogalski I saw that part. It was the liar's paradox and the incompleteness theorem that I skimmed. The fact that an undecidability proof reduces to the liar's paradox doesn't strike me as evidence that the proof is invalid. All proofs by contradiction or contrapositive reduce to a statement of the form x and not x.
m
If we remove the "halting" requirement from the halting problem and still get a paradox (a false statement) then what does it prove?
p
@Marek Rogalski
If we remove the "halting" requirement from the halting problem and still get a paradox (a false statement) then what does it prove?
Rice's theorem. https://en.m.wikipedia.org/wiki/Rice%27s_theorem
all non-trivial semantic properties of programs are undecidable
m
I don't follow. How does this emerge from the liar's paradox?
p
At 18:00 when he talks about printing and "calumating" (something he made up), he argues that the proof is based on an inconsistent specification because it leads to contradictions when he takes out halting and puts in anything else. However, since questions about what a program prints or whether a program executes the calumate procedure refer to non-trivial properties, I was saying that it seems to me that all he has done is prove a few other special cases of Rice's theorem, not demonstrated a flaw in the structure of the proof.
m
Can you correctly answer no to this question? I could answer for you by saying "no", but you can't say that yourself as it would create a contradiction. What does this make you think about validity of subjectively defined problems? (which include halting problem and Rice's theorem) I'll chime in my own takeaway from his lecture: halting problem may very well have an answer, but when a program under question changes its own behavior depending on the answer, then that only makes the problem ill-specified (because the answer is now subjective). The root of the paradox is not that we cannot determine halting (the
halts
function may be perfectly fine) but that the program changes its own behavior based to be the opposite of the answer (the
twist
function contradicts itself). The same can be said about the proofs on Rice's theorem Wikipedia page. These paradoxes have nothing to do with computers but instead stem from the fact that subjectively defined problems are ill-specified.
p
I fear we may be going in circles because we are now back to my original point, which is that I believe he dismisses translation too casually. If there is a Python function that can accurately determine whether a Pascal program will halt, that Python function can be translated into a Pascal function that behaves in exactly the same way, and a Pascal function can be constructed that is guaranteed to not behave in the way that the Python function predicts. When that Pascal program is passed to that Python function, that Python function will give an incorrect answer. I don't see the significance of introducing subjectivity into the conversation. We are talking about a hypothetical implementation of a mathematical function. I will follow this thread, but I may not respond again unless I come up with something new to say.
m
> I don't see the significance of introducing subjectivity into the conversation. We are talking about a hypothetical implementation of a mathematical function. If I reformulate my last question that I asked you so that we're talking about hypothetical mathematical functions (into a
prints "No"
function), would it stop being subjective?
p
@Marek Rogalski I'm trying to say that I find the whole concept of subjectivity irrelevant to this discussion, since the functions and procedures we are discussing are 100% deterministic, meaning they can be translated with absolute fidelity. To take a broader perspective, it also makes intuitive sense that there are functions that cannot be computed, because there are an uncountable number of functions but there are a countable number of programs. It also makes intuitive sense that the halting problem cannot be solved, because if it could it would allow us to trivially answer many deep problems, including many unsolved problems. For example, we do not know if there are any odd perfect numbers. If we had a solution to the halting problem, we could write a program that tests all odd numbers and halts if it finds one that is perfect. We could then use our halts function to determine whether this program will ever find an odd perfect number. Or consider the Collatz Conjecture. Take a number. If it's even, divide by two. If it's odd, multiply by 3 and add 1. With enough repetition, do all positive integers converge to one? If we had a halts function, we could use it to write another function that determines whether an integer converges to one. We could then use that function to write a program that halts if it finds a number that does not converge to one. We could then use our halts function to determine whether that function halts and thus the truth of the conjecture. It would also be possible to write a program that tests all possible solutions to Fermat's Last Theorem and halts if it finds one. Again, our hypothetical halts function could tell us whether the theorem is true or false. The sheer power of such a function to easily solve so many questions that have remained unanswered for so long, questions which vary widely in the structure and concepts involved, makes it seem too good to be true.
m
@Marek Rogalski I'm trying to say that I find the whole concept of subjectivity irrelevant to this discussion, since the functions and procedures we are discussing are 100% deterministic, meaning they can be translated with absolute fidelity.
Is it though? How would you approach my last question then? The one about "prints No" function.
It also makes intuitive sense that the halting problem cannot be solved, because if it could it would allow us to trivially answer many deep problems, including many unsolved problems.
Nobody is saying that the solution would be trivial. The author of the video is just saying that the Turing's argument (and it's extensions) seem to be fundamentally flawed.
👍 1
p
@Marek Rogalski
Is it though? How would you approach my last question then? The one about "prints No" function.
If you write the function first, and commit to a particular Oracle when you write it, then I can create an Oracle that gives the correct answer for that particular function. All that proves is that the behavior of that one function is decidable. It does not invalidate the proof that it is not possible to create a generalized Oracle that always computes, in finite time, an accurate answer to the question of whether a program prints out "no." On the other hand, if I hypothesize an Oracle that accurately determines whether a program prints out "no," for any Oracle that I hypothesize it is possible to construct at least one program for which it gives an incorrect answer, meaning that no such Oracle can exist. The fact that the program could be on a different computer or could be written in a different language does not change the fact that a program can always be written for which the Oracle gives the wrong answer. My point is that order matters here. FIRST you must commit to an Oracle and THEN you can create a program for which it fails. Subjectivity provides a way to write the program first and then create an Oracle that works for a particular class of programs, but it does not address the core argument that assuming the existence of an Oracle leads to a contradiction.
Let me put it this way. If you give me an Oracle written in Python that analyzes Pascal programs and tells me whether they print "no" then I can translate that Oracle into Pascal and construct a program for which it gives the wrong answer. Even with the benefit of subjectivity, the Oracle still fails.