In theoretical computer science a property on a set is called decidable ( recursively recursively derivable ) if there is a decision procedure for them. A decision procedure is an algorithm that can be answered for each element of the set, if it has the property or not. If there is not such a ruling, then called the property undecidable. As a decision problem is referred to the question of whether, and how, for a given property a decision procedure can be formulated.
While the main syntactic properties of programs are decidable, by the theorem of Rice all ( non-trivial ) semantic properties of programs, for example, the termination of a program on an input ( halting problem ) or the functional equality of two programs are undecidable, (equivalence problem).
Originally meant specifically for the validity of formulas, the term is now used for arbitrary properties on countable sets. The concept of the algorithm requires a calculation model; unless the contrary is stated, the Turing machine or an equivalent model are meant.
A subset of a set is called decidable if its characteristic function defined by
Is computable. The Entscheidbarkeitsbegriff is thus attributed to the notion of computability.
In this definition is assumed that all members of the set can be represented in the computer. The amount must be gödelisierbar. In theory, it is easier to compare prices directly or advance. In the latter case one has shown the problem as the word problem of a formal language.
Since only countable sets are gödelisierbar, the notion of decidability for uncountable sets such as the real numbers is not defined. However, there are attempts to extend through an extended machine model the notion of computability on real numbers (eg, the Blum - Shub - Smale model).
Undecidability should not be confused with the practical or fundamental impossibility to assign a truth value of a statement. It covers in detail by the following terms:
Decidability is a property of predicates, and not statements. The predicate is assumed to be well defined, so it provides for each element of the set a definite truth value. Undecidability indicates only that the predicate can not be calculated by an algorithm.
Statements are always decidable considered as zero -place predicates, even if its truth value is still unclear. If the statement is true, then the algorithm always outputs one is a decision procedure. Otherwise, the algorithm always returns zero, a decision procedure.
The decision problem is " the problem, determine the generality of expressions ". "It is the problem of providing a given deductive theory, a general method which allows us to decide whether a given, formulated in terms of the theory set, it can be proved within the theory or not. "
According to Frege / Whitehead / Russell was the " core issue of logicians and mathematicians: Is there an algorithm ... which determines by any formula of a logical calculus if she follows certain predefined axioms or not ( the so-called decision problem )? "
Kurt Gödel (1906-1978) published in 1931 a work on the decision problem; Briton Alan Turing (1912-1954) formulated in his basic work for this branch of mathematics On Computable Numbers, with an Application to the " decision problem " (28 May 1936) Gödel's results for 1931 new. He replaced it Gödel's universal arithmetic- based formal language through simple, formal devices, which became known as the Turing machine.
The logician Heinrich Scholz (1864-1956) asked for ( and received ) by Turing in 1936 a copy of this work on the basis of this work kept Scholz (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 amount also its complement is decidable. For two decidable sets whose intersection and their union are decidable.
The halting problem describes the question of whether an algorithm with an input terminated. Alan Turing proved the undecidability of this question. Formal the halting problem is the property of pairs of algorithm and inputs that the algorithm terminates for the input, that is, only a finite time into account. Also, the uniform halting problem, which is to hold the property of algorithms for each input finally is undecidable.
The halting problem for many weaker computational models such as linear bounded Turing machines, however, is decidable.
Validity in propositional logic
The validity of the propositional calculus is decidable. Known is the complement to the satisfiability problem of propositional logic. A decision procedure is the method of truth tables.
Validity in predicate logic
The (special ) decision problem for the predicate calculus was made in 1928 by David Hilbert ( see Hilbert program). Alan Turing and Alonzo Church have found the problem in 1936 that it is intractable (see halting problem ).
The decision problem is not for the general predicate logic, but only for parts of predicate logic, such as predicate logic solved " with predicates, stage 1".
Solvability of Diophantine equations
A polynomial equation is called diophantine if all the 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, however, is decidable.
The Postsche correspondence problem
This is called a finite list of pairs of non-empty words over a finite alphabet a case. A solution to a problem case is a non-empty finite sequence of numbers for word pairs in the list, so that the first components of the pairs of words composed of the same word found as the second component of the word pairs.
For example, has the solution, because it is.
The Postsche correspondence problem, ie, the property of problem cases to have a solution is undecidable.
A more general class than the decidable sets are recursively enumerable quantities or semi- decidable, in which only either only for " yes " or just "no" it is required that the calculation stops in finite time. If both a set and its complement are semi- decidable, then the amount is decidable. The halting problem is semi- decidable, because the answer is " yes " can always be added by running the program. However, the complement of the halting problem is semi- decidable.