User:Hakerh400/What we could do if we could solve the halting problem

From Esolang
Jump to navigation Jump to search

In this article the author provides his opinion about the halting problem and what people could do if they find a way to solve it in finite time.

What is the halting problem?

The halting problem asks whether a given Turing machine will ever halt. Assuming the reader knows what a Turing machine is. The problem of determining whether a Turing machine halts is proven to be uncomputable. It means that for any algorithm we implement (in a Turing-complete language), there will always be a Turing machine for which the algorithm will never halt. The uncomputability in this case comes from the fact that a Turing machine can simulate another Turing machine, so it can simulate the algorithm itself and thus can halt or not halt depending on the result of the algorithm.

However, we need some deeper understanding of what "uncomputable" and "undecidable" means, and what the differences between them are. We explained what "uncomputable" means. However, the term "will never halt" is actually not precisely defined. One may ask what we mean by "to never halt". We can define it in the following way: a Turing machine halts if either it halts at the first step, or there exists a natural number such that the machine does not halt in steps, but halts in steps. Similarly, we can say that a Turing machine never halts if it does not halt in the first step and from the assumption that it does not halt in steps for some integer , the we can conclude that it also does not halt in steps.

So, if we define it that way, the question would be: if we prove that it does not halt in the first step and we prove that not halting in steps implies not halting in steps, does it represent a sufficient argument that the Turing machine never halt? In order to answer this question, we first need to define what "to prove something" actually means. We can define some formal mathematical system and then use axiom schemas and inference rules to either prove or disprove a statement. However, it has been proven that, no matter what formal system we define, it cannot prove all true statements about natural numbers, nor can it prove its own consistency (of course, in finite number of steps). But we see the problem appearing again: we are talking about determining whether some natural number (number such that some given Turing machine halts in steps) exists (and by "exists" we mean "it is finite"), but we concluded that in order to determine whether a number is finite, we need to use a formal mathematical system, and it has been proven that the existence of a finite number of steps needed to prove a statement is "proven" to be false. But how do we define "finite number of steps" (and by "step" we mean axiom application, or inference rule application)? And does it make any sense proving anything via a system whose consistency is proven (within itself) to be unprovable?

Regarding the question whether not halting in the first step and not halting in steps implying not halting in steps is a sufficient argument that some given Turing machine never halts, we can clearly see that it is a mathematical induction, which can be expressed via Peano axioms. However, it has been proven that some statements are true, but unprovable via Peano axioms (such as Goodstein's theorem, which requires Transfinite induction up to ordinal ε0). The main reason it is unprovable via finite induction is because the " implies " for some statement is sufficient argument for a proof that is true for all natural numbers. However, it is a sufficient argument, but not the only possible argument. What if we define a new type of induction: if is true and is unprovable within the system, then ? This new type of induction is obviously more stronger than finite induction, but the author is not sure whether it is even stronger than the transfinite induction. The main problem here is that "unprovable within the system" implicitly requires us to prove that the system is consistent (because otherwise all statements are provable), but it is, in general, impossible in finite number of steps. We can only start from an assumption that the system is consistent and prove that if is provable, then the system would be inconsistent.

Real-world usage

Despite the math asserting some truths about the logical construction of the world, we can clearly observe that the real-world application of math statements can be more useful than the mathematician's forecast (like NFL theorem, which asserts that optimizations are useless, but people still do optimizations because they work very good for real-world problems). Similarly, despite the fact that solving the general halting problem is uncomputable, we can solve it for some concrete Turing machines.

Here is real-world example. Imagine you are developing a spaceship, which is intended to go very far beyong the Solar system and stay there for thousands of years, exploring the space. You want to program it, but you also want to make sure that it will always work as expected (assuming the ability to expand the memory (via stardust material) if needed and assuming unlimited energy (via solar panels)). You want to prove that your spaceship will never do anything unexpected (as long as the hardware is not broken). In other words, you want to prove thet the spaceship's Turing machine will never halt (for example). So, you hire a professional mathematician and tell him to prove that your Turing machine will never halt. After a week, the mathematician tells you that he proved that your question is undecidable. How would you feel? Would it be enough reason for you to believe that no problems with your spaceship will ever occur? You may think this way: the fact that my mathematician proved that the question whether my Turing-machine will ever halt is an undecidable problem means that, even if it ever halts, it cannot be proven via a finite number of mathematical symbols. If you suppose that the machine will halt, it is only a finite time between the launching and the halting of the machine, so each computational step of the machine can be represented within the mathematical system (used by the mathematician) and therefore it would be possible to determine it via a finite number of mathematical symbols. So, if the problem is undecidable (from within some mathematical system), if you believe that the mathematical system is consistent, it would be enough argument for you that your machine will never halt. Why would you then care whether the statement is proven to be true, or proven to be undecidable? In both cases, you know that your machine will never halt and your spaceship will always work as expected.

Is it possible to ever solve the halting problem?

Theoretically, yes, it may be possible. At least, it would not be paradoxical (mathematics does not deny the possibility of solving the halting problem). However, the question is, even if that would be possible, how a machine that could solve the halting problem would work?

We do not know the nature of all particles that exist in the universe. It may be possible that there exists some bizarre particle that could solve the Halting problem in constant time. Let's call that particle Haltino. It would behave in the following way:

  1. First, you write a program in some Turing-complete language.
  2. Then you encode your program using some prefix-free binary encoding.
  3. For each you prepare a single neutron.
  4. For each you prepare a single positron.
  5. Then for each bit of the encoded program, you shoot the Haltino with corresponding particle (neutron or positron)
  6. After you shoot the last particle (and since it is prefix-free, Haltino can detect the end fo the program), the Haltino particle immediately emits a positron if the encoded program halts, otherwise emits a neutron.

The main problem here is that we would never be able to prove that Haltino will always give the correct answer. We would need to believe that it works as we expect. However, Haltino would not be able to solve the halting problem involving a super-Turing machine that uses another Haltino. We would need a super-Haltino for that. But the author believes that a single Haltino would be enought to solve the majority of today real-world problems.

What we could do with it?

We could create a computer that contains Haltino particle inside it and we can use it to solve the halting problem. Here are some examples of what we could do with it:

  • We could determine whether ZFC is consistent. It can be done by writing a program that implements ZFC axioms and inference rules and then searches for inconsistencies. The program halts iff a contradiction is found.
  • We could solve P vs NP problem, Hodge conjecture, Riemann hypothesis, Yang–Mills existence and mass gap, Navier–Stokes existence and smoothness, Birch and Swinnerton-Dyer conjecture, Collatz conjecture and a lot more, or at least prove that they are unprovable within ZFC or some other system we use.
  • We could find out whether there is a winning strategy in Chess, Go, Dots and Boxes and many other board games. It can be done by implementing the Minimax algorithm and checking all possible moves.
  • We could "reverse" any hash (find the shortest string that produces the given hash). It can be done by first using a binary search to determine the shortest string length, then for each bit we ask whether it is or , so we can reconstruct the string.
  • It can be used in complex rendering engines to determine each bit of each pixel of each frame, so we can reconstruct the entire video in constant time, regardless of the complexity of the animation itself.
  • Similarly, it can be used in real-time 3D games.
  • It can be used to solve TSP problem in constant time, which can then be applied in industry to find an optimal way to do something, or can be applied in self-driving cars or GPS.
  • Millitary forces can use it to find an optimal way to create a very powerful nuclear weapon and destroy the entire universe. The author of this article hopes it will never happen.

Conclusion

A particle such as Haltino would be very powerful. Much more powerful that any force currently known to us. It could give us answer to any super-computable question, which is, in fact, what we actually need. It may be a good idea to make some science fiction movie regarding Haltino or some other bizarre particle with such features.