PeteOlcott wrote: ↑Fri May 17, 2019 5:32 am
I don't understand any of these things at all.
I did find an execution trace of the conventional halting problem proof that no one ever noticed before.
I had to study the same two pages of a single textbook off and on for a total of about 2000 hours
over 14 years to notice this execution trace. It took me another three years to turn this
discovery into the source code for H and H^.
http://liarparadox.org/Peter_Linz_HP(Pages_318-319).pdf
With an OCD level of persistence "impossible" things can be accomplished.
Then you are a paragon for demonstrating why empiricism trumps scholasticism.
It doesn't take 3 years from idea to writing proof-of-concept code. Modern proof assistants like Coq support
automatic code generation.
If you write a valid proof, you will get a corresponding algorithm for free (and in seconds). Talk about automating human effort, eh?
It's like writing unit tests in
Behaviour-driven development only better.
But there is a key distinction that you seem to be missing here. The halting problem is not about execution traces. It's about a-priori prediction of whether a program will halt without actually having to run it.
If you remove self-reference from your language specification - recursion becomes impossible and then your language is no longer able to answers to questions like "What is the Nth number in the Fibonacci sequence?"
You don't seem to understand the difference between the
Declarative and
Imperative paradigms.
Mathematical proofs are declarative.
Mathematical objects which
realize the proof-properties are imperative.
In fact, all this reminds me of a popular quote by Mark Twain.
"I can teach anybody how to get what they want out of life. The problem is that I can't find anybody who can tell me what they want.”
Writing a proof is much like declaring what you want.
Writing an algorithm is much like declaring HOW to get what you want.