It can be shown that Turing machines, μ-recursive functions and reasonable programming languages can compute/decide the same problems. I wonder why we then still proof the halting problem with Turing machines.
Isn't it much easier to argue that the function halts
below cannot exist in e.g. python since then I would be able to write the following program which is a contradiction.
def halts(source):
...
if __name__ == "__main__":
this_file = open(__file__)
if halts(this_file.read()):
while True:
pass
else:
return 1
Why is this proof not as good as the TM diagonal argument?
Edit: I read https://cs.stackexchange.com/a/94235/119946
OK, fine. This proves that the halting problem can't be solved for code written in any programming language that has a get_source_code_of_current_function() API. However, my favorite programming language doesn't have such an API. So, this proof doesn't prove anything about my favorite programming language -- perhaps the halting problem is solvable for my language, who knows? Similarly, Turing machines don't have such an API, so this doesn't prove that the halting problem for Turing machines is undecidable.
I mean by that argument I can say the TM proofs only shows that the halting problem cannot be decided by Turing machines, but does not show anything about python. Isn't the crucial part, that (as I wrote) TM and modern programming languages can compute/decide the same problems? If one can decide the halting problem, then all other can do so as well and vice versa.
def
,return
,open
,read
,__name__
,==
, etc. etc. Sounds like a lot of pain. 2) Python is Turing-complete, i.e. you can simulate TM with python. The halting problem says that you can't say whether the TM halts $\implies$ whether the simulation halts $\implies$ whether your python program halts. $\endgroup$I can say the TM proofs only shows that the halting problem cannot be decided by Turing machines, but does not show anything about python
. I explained it does show the same thing about Python.The keywords you mentioned are already defined in the python spec
sure, they probably are. And all these definitions must be taken into account when you try to proof stuff about your code. You need to formally define the semantics, and instead of 1 page for TM it'll be hundreds? of pages of specification. $\endgroup$I mean by that argument, ...
part while quoting me. I disagreed with the cited answer, and with 1) as my "proof" above is easier than the diagonal argument. The spec is already written and it follows whether python halts $\implies$ wether the TM simulation of it halts $\implies$ whether the TM halts. $\endgroup$