In theoretical computer science , a property is called decidable on a set (also recursively , recursively derivable ) if there is a decision procedure for it. A decision procedure is an algorithm that can answer for each element of the set whether it has the property or not. If there is “no” such decision-making process, then the property is called undecidable . A decision problem is the question of whether and how a decision procedure can be formulated for a given property.
While the most important syntactic properties of programs can be decided, in general, according to Rice's theorem, any (non-trivial) semantic properties of programs are undecidable, for example the termination of a program on an input ( hold problem ) or the equality of functions of two programs ( equivalence problem ).
Originally meant specifically for the validity of formulas, the term is now used for any properties on countable sets. The concept of the algorithm presupposes a calculation model ; Unless otherwise stated, the Turing machines or an equivalent model are meant.
A subset of a countable set is called decidable if its characteristic function is defined by
is predictable . The concept of decidability is thus traced back to the concept of calculability.
This definition assumes that all elements of the set can be represented in the computer. The amount must be godelizable . In theory, for easier comparison, one assumes direct or presupposes. In the latter case, the problem has been presented as the word problem of a formal language .
Since only countable sets can be godelized, the concept of decidability is not defined for uncountable sets like that of real numbers . However, there have been attempts to extend the concept of calculability to real numbers through an extended machine model (e.g. the Blum-Shub-Smale model ).
Undecidability must not be confused with the practical or fundamental impossibility of assigning a truth value to a statement . In detail, the following terms are involved:
- Inconsistency: Paradoxes or antinomies show that a calculus contains contradictions, i.e. is not free of contradictions . The Russell's Paradox , for example, showed that naive set theory containing contradictions.
- Independence: Statements that can be added to a consistent calculation without creating a contradiction are called relatively free of contradictions in relation to this calculation. If its negation is relatively free of contradictions, then the statement is independent . For example, the axiom of choice is independent of the Zermelo-Fraenkel set theory .
- Incompleteness: In consistent calculi, which have at least the expressiveness of arithmetic , there are true statements that cannot be proven in the calculus. Such calculations are called incomplete .
Decidability is a property of predicates , not of statements. The predicate is assumed to be well-defined , so it delivers a defined truth value for each element of the set. Undecidability only means that the predicate cannot be calculated by an algorithm.
Statements viewed as zero-place predicates are always decidable, even if their truth value is still unclear. If the statement is true, then the algorithm that always returns one is a decision-making process. Otherwise the algorithm, which always returns zero, is a decision-making process.
The decision problem is "the problem of determining the generality of expressions". "It is a matter of specifying a general procedure for a given deductive theory which allows us to decide whether a given sentence, formulated in the terms of the theory, can be proven within the theory or not."
The decisive factor is whether there is a purely mechanical process, an algorithm , that clarifies in a finite number of steps whether an expression, a formula, is valid in a system or not.
According to Frege , Whitehead and Russell , the "central question of logicians and mathematicians was: Is there an algorithm [...] that determines from any formula of a logical calculus whether it follows from certain given axioms or not (the so-called decision problem)?"
Kurt Gödel published a work on the decision problem in 1931; The British Alan Turing (1912–1954) reformulated Gödel's results from 1931 in his work, On Computable Numbers, with an Application to the “Decision Problem” (May 28, 1936), which was fundamental for this branch of mathematics . He replaced Gödel's universal, arithmetic-based formal language with simple, formal devices that became known as the Turing machine .
The logician Heinrich Scholz (1884–1956) requested (and received) a copy of this work from Turing in 1936. On the basis of this work, Scholz held (according to Achim Clausing) "the world's first seminar on computer science".
All finite sets, the set of all even numbers and the set of all prime numbers are decidable. For every decidable set, its complement is also decidable. For two decidable sets, their intersection and their union can be decided.
The halt problem describes the question of whether an algorithm terminates with an input . Alan Turing demonstrated the undecidability of this question. More formally, the holding problem is the property of pairs of algorithm and inputs that the algorithm terminates for the input , that is, calculates only finitely long. The even holding problem, namely the property of algorithms to finally hold for every input, is also undecidable.
The stopping problem for many weaker calculation models, such as linearly constrained Turing machines , can, however, be decided.
Validity in propositional logic
The validity in the propositional calculus is decidable. The complement to this is known, the satisfiability problem of propositional logic . One decision-making process is the truth table method .
Validity in predicate logic
The special decision problem for predicate logic was posed by David Hilbert in 1928 (see Hilbert program ). Alan Turing and Alonzo Church found the problem in 1936 to be unsolvable (see holding problem ).
The decision problem is not solved for general predicate logic, but only for sub-areas of predicate logic, such as predicate logic with single-digit first-order predicates.
Solvability of Diophantine equations
A polynomial equation is called Diophantine if all coefficients are integers and only integer solutions are sought. The property of Diophantine equations to have a solution ( Hilbert's tenth problem ) is undecidable. The solvability of linear Diophantine equations, on the other hand, is decidable.
Post's correspondence problem
A finite list of pairs of non-empty words over a finite alphabet is called a problem case. One solution to a problem is a non-empty, finite sequence of numbers for word pairs in the list, so that the first components of the word pairs, when put together, result in the same word as the second components of the word pairs.
Example: has the solution because it applies .
The Postsche correspondence problem , that is the property of problem cases to have a solution that is undecidable.
According to Toby Cubitt, David Perez-Garcia, Michael Wolf, the following problem from quantum mechanical many-body theory is undecidable. The Hamilton function of a quantum mechanical many-body problem is given. Does the spectrum have a gap from the first excited state to the ground state or not? The authors explicitly constructed a family of quantum spin systems on a two-dimensional lattice with translation-invariant closest neighbor interaction, for which the question of the spectral gap is undecidable. They combined the complexity theory of Hamilton operators with techniques of aperiodic tiling and translated the problem into a holding problem of a Turing machine. Other low-energy properties of the system are also undecidable.
A more general class than the decidable sets are the recursively enumerable or semi-decidable sets , where the only requirement for “yes” is that the computation should stop in finite time. If both a set and its complement are semi-decidable, then the set is decidable. The stopping problem is semi-decidable, because the answer “yes” can always be given by running the program. However, the complement of the holding problem is not semi-decidable.
- Equivalence problem
- Finiteness problem
- Emptiness problem
- Post correspondence problem
- Semi-decidable set
- Lothar Czayka : Formal logic and philosophy of science. Introduction for economists. Oldenbourg, Munich a. a. 1991, ISBN 3-486-20987-6 , p. 45 ff.
- Willard Van Orman Quine : Principles of Logic. 8th edition. Suhrkamp, Frankfurt am Main 1993, ISBN 3-518-27665-4 , p. 142 ff. ( Suhrkamp-Taschenbuch Wissenschaft 65), in detail.
- Paul Hoyningen-Huene : Formal Logic. A philosophical introduction. Reclam, Stuttgart 1998, ISBN 3-15-009692-8 , p. 226 ff. ( Reclam's Universal Library 9692)
- Hartley Rogers: Theory of recursive functions and effective computability . McGraw-Hill, 1967.
- Uwe Schöning : Theoretical Computer Science - in a nutshell . 4th edition. Spectrum, 2000, ISBN 3-8274-1099-1 , pp. 122 ff .
- ↑ Arnim Regenbogen, Uwe Meyer (Ed.): Dictionary of philosophical terms. Special edition. Meiner, Hamburg 2006, ISBN 3-7873-1761-9 , “decidable”.
- ↑ David Hilbert , W. Ackermann : Fundamentals of theoretical logic. 6th edition. Springer, Berlin a. a. 1972, ISBN 0-387-05843-5 , p. 119 ( The Basic Teachings of Mathematical Sciences 27).
- ^ Alfred Tarski : Introduction to Mathematical Logic. 5th edition, expanded to include the article "Truth and Evidence". Vandenhoeck & Ruprecht, Göttingen 1977, ISBN 3-525-40540-5 , p. 145 ( Modern mathematics in elementary representation 5).
- ^ Patrick Brandt, Rolf-Albert Dietrich, Georg Schön: Linguistics. A common thread for studying the German language. 2nd revised and updated edition. Böhlau, Cologne a. a. 2006, ISBN 3-412-00606-8 , p. 14 ( UTB 8331).
- ↑ It was found by Achim Clausing at the Institute for Computer Science at the Westphalian Wilhelms University in Münster ( Westfälische Nachrichten . January 28, 2013: In the footsteps of a pioneer: Original prints by computer scientist Alan Turing are in the Münster University Library ; online ).
- ^ Hilbert / Ackermann: Basic features. 6th edition. (1972), p. 119.
- ↑ Willard Van Orman Quine : Fundamentals of Logic. 8th edition. Suhrkamp, Frankfurt am Main 1993, ISBN 3-518-27665-4 , p. 247.
- ↑ Lothar Czayka: Formal logic and philosophy of science. Introduction for economists. Oldenbourg, Munich a. a. 1991, ISBN 3-486-20987-6 , p. 45.
- ↑ Cubitt, Perez-Garcia, Wolf, Undecidability of the spectral gap, Nature, Volume 528, 2015, p. 207, Arxiv Preprint