Stop problem

from Wikipedia, the free encyclopedia

The stop problem describes a question from theoretical computer science .

If several calculation steps are carried out according to fixed rules for a calculation, a calculation rule, a so-called algorithm, is created . In theoretical computer science, abstract machines are used to execute algorithms . A typical abstract machine is the Turing machine . The stall problem describes the question of whether the execution of an algorithm comes to an end. Although this can easily be answered for many algorithms, the mathematician Alan Turing was able to prove that there is no algorithm that answers this question for all possible algorithms and any input. He performed this proof on a Turing machine. The halting problem is therefore algorithmically not decidable . The result plays a fundamental role in predictability theory . The term holding problem was not coined by Turing, but later by Martin Davis in his book Computability and Unsolvability .

meaning

In formal systems of mathematics there are provable statements .

Example: The sum of the interior angles of any plane triangle is 180 degrees .

If formal systems reach a certain level of complexity, statements can be made that can neither be proven nor refuted. The proof of this property was published in 1931 by the Austrian mathematician Kurt Gödel ( Gödel's incompleteness theorem ). In doing so, Gödel demonstrated the impossibility of the Hilbert program . With this, David Hilbert wanted to base mathematics on a complete and consistent system of axioms (unproven basic assumptions) in 1920 .

According to Alan Turing's findings, the following applies: In every formal system that contains Turing machines, statements can be formulated that can neither be proven nor refuted. The holding problem describes such a statement. From the unsolvability of the holding problem it follows that there are mathematical functions that are well-defined, but whose values ​​cannot be calculated for every parameter . A well-known example of such a function is the Radó function .

The Church-Turing thesis states that everything that can be calculated intuitively can also be calculated by a Turing machine. If this statement is true, the holding problem cannot in principle be decided algorithmically. This leads to the philosophically far-reaching statement that not every problem can be solved, even if one knows all the relevant information and strictly adheres to a mathematically convincing formalism.

From the fact that the halt problem cannot be decided it follows that in general an automated determination of logical statements ( “this fact is true” ) - by a program logic - is not possible. In particular, it is generally not possible to automatically determine which programs will ever come to an end ( proof of termination ). For certain classes of Turing machines, however, the halt problem can be decided (for example for programs without loops). Many programs and procedures occurring in practice are therefore structured in such a way that an automated proof of termination can be made on the basis of this structure .

illustration

With many programs, it's easy to tell if they will eventually stop. However, there are also programs for which, based on the current state of knowledge, it is not yet possible to predict whether they will stop at every possible input. The following program stops for every input (at and ) if the previously unproven Collatz conjecture is correct. The Collatz conjecture says that such a loop would sooner or later always produce the sequence of numbers 4, 2, 1, which would lead to the program being stopped with the termination condition "up to n = 1" given here.

wiederhole
  falls n gerade:  n := n / 2
  sonst:           n := (3 * n) + 1
bis n = 1

Mathematical description

Problem

If the stopping problem can be decided, there is a Turing machine that decides for every Turing machine with every input whether it will stop at some point or continue endlessly. The input for consists of a coded description of the machine and its input .

Alan Turing proved in 1937 that such a machine does not exist.

Proof idea

The holding problem can be decided precisely when both the holding problem and its complement are semi- decidable . The stopping problem is obviously semi-decidable: A universal Turing machine that receives a description of a Turing machine and a character string as input stops exactly when it stops with input . It must therefore be shown that the complement of the stopping problem is not semi-decidable, i.e. that there is no Turing machine that always outputs 1 on input if it does not stop on input .

g ( i , w ) w = 1 w = 2 w = 3 w = 4 w = 5 w = 6
i = 1 1 U U 1 U 1
i = 2 U U U 1 U U
i = 3 U 1 U 1 U 1
i = 4 1 U U 1 U U
i = 5 U U U 1 1 1
i = 6 1 1 U U 1 U
g ( i , i ) 1 U U 1 1 U
f ( i ) 1 U U 1 1 U
Clear representation of functions g and f . U stands for “undefined”.

This is achieved through a diagonal argument . For this, it is initially assumed that the complement of the stopping problem is semi-decidable. (So ​​the proof is indirect .) Instead of a Turing machine, one can also consider the function that is calculated by it. The Turing machine calculates the partial function

The diagonal of is calculated by the following function .

Let be the number of a Turing machine that computes the function . So the function value of at that point is

  • 1, if , if it does not hold on input . This is a contradiction, however, because it calculates and must hold and output 1.
  • undefined, if undefined, i.e. if stops when entering . This is also a contradiction because it is undefined and calculated at this point .

Evidence sketch

The proof is based on Marvin Minsky's construction .

Step 1: The diagonal language is not semi-decidable

The set of all Turing machines that do not hold up when they receive their own coding as input is called the diagonal language . The proof that the diagonal language is not semi-decidable is done by a contradiction proof . One assumes that there is a machine that semi-decides the diagonal language, and shows that this leads to a logical contradiction.

Suppose there is a Turing machine , which when entering the description of a Turing machine, the value outputs, when the Enter key is not holding, and does not consider, when at the input of holding. Then have when entering stop and spend when on input does not stop, and do not hold when in input stops. This is a contradiction, so such a machine cannot exist.

Step 2: The complement of the holding problem is not semi-decidable

If the complement of the holding problem were semi-decidable, then the diagonal language would also be semi-decidable.

Suppose there is a Turing machine , which when entering the description of a Turing machine , and a character string outputs 1 when the Enter key is not holding, and does not consider, when at the input of holding. One can assume without loss of generality that the input has for the form . Here is a character string that does not appear in the description of the Turing machine or in its input . A Turing machine can be constructed from, which semi-decides the diagonal language. When entering a description of a Turing machine, it simply starts with the entry .

If the complement of the holding problem semi-decides, the diagonal language semi-decides . Since there is such a machine can not give the construction of out but certainly possible, it may, such a machine not give.

Step 3: The holding problem cannot be decided

If the holding problem were decidable, then its complement would be semi-decidable.

Assume that there is a Turing machine that outputs 0 when entering the description of a Turing machine and a character string , if it does not hold with input , and outputs 1 if it holds when entering . Then there would also be a Turing machine that semi-decides the complement of the holding problem. When entering a description of a Turing machine, it simply starts with the same entry . If 0 outputs, then 1 outputs . If 1 returns, it goes into an endless loop.

If the holding problem decides, the complement of the holding problem semi-decides . Since there is such a machine can not give the construction of out but certainly possible, it may, such a machine not give.

Graphical representation of the evidence construction
 Machine input 
Machine input
Machine input
does not hold keeps display of
 results 
keeps display of
 results 
holds keeps display of
 results 
does not hold

An equivalent formulation

The halting problem with empty input tape ( English blank-tape halting problem- , BTHP , also known as zero-halting problem), is the question of whether a Turing machine stops with an empty input tape. The BTHP is just as severe as the holding problem. This is intuitively the case because an input can also be coded in the start state of a Turing machine.

Obviously, any machine that decides the stopping problem for any Turing machine with any input can also decide the BTHP for . But a machine that decides the BTHP for each Turing machine can already decide the general stopping problem. To decide the halting problem for the Turing machine with input , consider the Turing machine , which is defined as follows. first writes on the input tape, then behaves like . in particular stops on the empty tape when input stops.

literature

  • Alan Turing: On computable numbers, with an application to the Decision Problem, Proceedings of the London Mathematical Society, 2, 42 (1937), pp. 230-265. Online version

Web links

Wikiversity: Halting Problem  - Course Materials
Wiktionary: Haltingproblem  - explanations of meanings, word origins, synonyms, translations

Individual evidence

  1. Martin Davis: Computability and Unsolvability , McGraw-Hill, New York 1958, reprinted with a new foreword and afterword 1983, Dover Publications Inc., ISBN 978-0-486-61471-7
  2. Douglas R. Hofstadter, for example, offers an easily understandable description of the connections and consequences of Gödel's work: Review by Alan Turing: The Enigma , in Metamagicum , Klett-Cotta, Stuttgart 1988, ISBN 3-608-93089-2 , p. 519– 528
  3. lecture notes of Old Dominion University , accessed 13 July 2011