Entscheidbarkeit

Begriff und formale Definition

In der theoretischen Informatik heißt eine Eigenschaft auf einer Menge entscheidbar, wenn es ein Entscheidungsverfahren für sie gibt. Ein Entscheidungsverfahren ist ein Algorithmus, der für jedes Element der betrachteten Menge in endlich vielen Schritten feststellt, ob es die Eigenschaft besitzt oder nicht. Gibt es kein solches Verfahren, heißt die Eigenschaft unentscheidbar. Ein Entscheidungsproblem fragt danach, ob und wie ein solches Verfahren formuliert werden kann.

Formal ist eine Teilmenge T einer abzählbaren Menge M entscheidbar, wenn ihre charakteristische Funktion χ_T: M → {0,1} berechenbar ist. Sie ist definiert durch χ_T(t) = 1, falls t ∈ T, und χ_T(t) = 0, falls t nicht in T liegt. Der Begriff der Entscheidbarkeit wird damit auf den Begriff der Berechenbarkeit zurückgeführt.

Voraussetzung ist, dass die Elemente von M im Rechner dargestellt werden können. Die Menge M muss daher gödelisierbar sein. Für theoretische Vergleiche setzt man meist M = ℕ oder M = {0,1}* voraus. Im zweiten Fall wird das Entscheidungsproblem als Wortproblem einer formalen Sprache dargestellt. Für überabzählbare Mengen, etwa die reellen Zahlen, ist der Begriff der Entscheidbarkeit in dieser Form nicht definiert. Erweiterte Berechnungsmodelle wie das Blum-Shub-Smale-Modell versuchen jedoch, Berechenbarkeit auf reelle Zahlen auszudehnen.

Der Algorithmusbegriff setzt ein Berechnungsmodell voraus. Wenn nichts anderes angegeben ist, sind Turingmaschinen oder gleichwertige Modelle gemeint. Während wichtige syntaktische Eigenschaften von Programmen entscheidbar sind, sind nach dem Satz von Rice beliebige nichttriviale semantische Eigenschaften im Allgemeinen unentscheidbar. Semantische Eigenschaften betreffen dabei die Bedeutung oder das Verhalten eines Programms, beispielsweise seine Terminierung auf einer Eingabe oder die Funktionsgleichheit zweier Programme.

Abgrenzung zu ähnlichen Begriffen

Unentscheidbarkeit bedeutet nicht, dass eine Aussage grundsätzlich keinen Wahrheitswert besitzt oder dass ihre Wahrheit praktisch nicht festgestellt werden kann. Sie besagt lediglich, dass das betreffende Prädikat nicht durch einen Algorithmus berechnet werden kann.

Entscheidbarkeit ist eine Eigenschaft von Prädikaten, nicht von einzelnen Aussagen. Das Prädikat gilt dabei als wohldefiniert und liefert für jedes Element der Menge einen bestimmten Wahrheitswert. Aussagen können als nullstellige Prädikate betrachtet werden und sind in diesem Sinn immer entscheidbar, auch wenn ihr Wahrheitswert noch ungeklärt ist: Ist die Aussage wahr, entscheidet der Algorithmus, der immer 1 ausgibt; ist sie falsch, entscheidet der Algorithmus, der immer 0 ausgibt.

Davon zu unterscheiden sind drei Eigenschaften formaler Kalküle. Inkonsistenz bedeutet, dass ein Kalkül Widersprüche enthält. Die Russellsche Antinomie zeigte beispielsweise, dass die naive Mengenlehre widersprüchlich ist. Unabhängigkeit liegt vor, wenn sowohl eine Aussage als auch ihre Negation mit einem widerspruchsfreien Kalkül vereinbar sind; das Auswahlaxiom ist beispielsweise unabhängig von der Zermelo-Fraenkel-Mengenlehre. Unvollständigkeit bedeutet, dass es in einem konsistenten Kalkül, dessen Ausdrucksstärke mindestens der Arithmetik entspricht, wahre Aussagen gibt, die innerhalb des Kalküls nicht beweisbar sind.

Das Entscheidungsproblem und seine Geschichte

Ursprünglich bezeichnete das Entscheidungsproblem die Frage, ob die Allgemeingültigkeit von Ausdrücken festgestellt werden kann. Für eine gegebene deduktive Theorie sollte ein allgemeines, rein mechanisch anwendbares Verfahren angeben, ob ein vorgegebener Satz, der in den Begriffen der Theorie formuliert ist, innerhalb dieser Theorie bewiesen werden kann oder nicht. Entscheidend ist also die Existenz eines Algorithmus, der in endlich vielen Schritten klärt, ob eine Formel in einem System gültig ist.

Nach Frege, Whitehead und Russell lautete die Kernfrage der Logiker und Mathematiker, ob ein Algorithmus für jede Formel eines logischen Kalküls entscheiden kann, ob sie aus vorgegebenen Axiomen folgt. Kurt Gödel veröffentlichte 1931 ein Werk zum Entscheidungsproblem. Alan Turing formulierte Gödels Ergebnisse in seiner Arbeit „On Computable Numbers, with an Application to the “Entscheidungsproblem”“, die am 28. Mai 1936 erschien, neu. Dabei ersetzte er Gödels universelle, arithmetisch basierte formale Sprache durch einfache formale Geräte, die als Turingmaschinen bekannt wurden.

Der Logiker Heinrich Scholz erhielt 1936 von Turing ein Exemplar dieser Arbeit und hielt auf ihrer Grundlage laut Achim Clausing das weltweit erste Seminar über Informatik.

Wichtige entscheidbare und unentscheidbare Probleme

Alle endlichen Mengen, die Menge aller geraden Zahlen und die Menge aller Primzahlen sind entscheidbar. Ist eine Menge entscheidbar, so ist auch ihr Komplement entscheidbar. Für zwei entscheidbare Mengen sind außerdem ihre Schnittmenge und ihre Vereinigungsmenge entscheidbar.

Das Halteproblem fragt, ob ein Algorithmus bei einer bestimmten Eingabe terminiert, also nur endlich lange rechnet. Alan Turing wies nach, dass diese Eigenschaft von Paaren aus Algorithmus und Eingabe unentscheidbar ist. Auch das gleichmäßige Halteproblem, ob ein Algorithmus für jede Eingabe schließlich hält, ist unentscheidbar. Für manche schwächeren Berechnungsmodelle, etwa linear beschränkte Turingmaschinen, ist das Halteproblem dagegen entscheidbar.

Die Gültigkeit im Aussagenkalkül ist entscheidbar. Das zugehörige Komplement ist das Erfüllbarkeitsproblem der Aussagenlogik. Ein Entscheidungsverfahren für die Gültigkeit ist die Methode der Wahrheitstafeln.

Für die allgemeine Prädikatenlogik ist das Entscheidungsproblem unlösbar. David Hilbert stellte dieses spezielle Entscheidungsproblem 1928; Alan Turing und Alonzo Church stellten 1936 fest, dass es unlösbar ist. Für Teilbereiche der Prädikatenlogik gibt es jedoch Entscheidungsverfahren, beispielsweise für die Prädikatenlogik mit einstelligen Prädikaten erster Stufe.

Eine diophantische Gleichung ist eine Polynomgleichung mit ganzzahligen Koeffizienten, für die nur ganzzahlige Lösungen gesucht werden. Die Eigenschaft, ob eine solche Gleichung eine Lösung besitzt, ist als Hilberts zehntes Problem unentscheidbar. Für lineare diophantische Gleichungen ist die Lösbarkeit dagegen entscheidbar.

Weitere Beispiele und semi-entscheidbare Mengen

Beim Postschen Korrespondenzproblem ist ein Problemfall eine endliche Liste von Paaren nichtleerer Wörter über einem endlichen Alphabet. Eine Lösung ist eine nichtleere endliche Folge von Nummern der Wortpaare, sodass die Verkettung der ersten Komponenten dasselbe Wort ergibt wie die Verkettung der zweiten Komponenten. Für die Liste (a, aba), (ab, bb), (baa, aa) ist (1,3,2,3) eine Lösung, denn es gilt: a · baa · ab · baa = abaaabbaa = aba · aa · bb · aa. Die Eigenschaft, eine Lösung zu besitzen, ist unentscheidbar.

Auch in der Physik gibt es unentscheidbare Probleme. Nach Toby Cubitt, David Perez-Garcia und Michael Wolf ist für bestimmte quantenmechanische Vielteilchensysteme unentscheidbar, ob das Spektrum der Hamiltonfunktion eine Lücke zwischen dem Grundzustand und dem ersten angeregten Zustand besitzt. Die Autoren konstruierten dafür eine Familie von Quantenspinsystemen auf einem zweidimensionalen Gitter mit translationsinvarianter Nächstnachbar-Wechselwirkung. Sie übersetzten die Frage mithilfe von Komplexitätstheorie für Hamiltonoperatoren und Techniken der aperiodischen Parkettierung in ein Halteproblem einer Turingmaschine. Auch andere Niedrigenergieeigenschaften dieser Systeme sind unentscheidbar.

Eine allgemeinere Klasse als die entscheidbaren Mengen bilden die rekursiv aufzählbaren oder semi-entscheidbaren Mengen. Für sie muss nur gelten, dass die Berechnung bei einer positiven Antwort „ja“ in endlicher Zeit anhält; für „nein“ ist ein Anhalten nicht erforderlich. Eine Menge ist genau dann entscheidbar, wenn sowohl sie selbst als auch ihr Komplement semi-entscheidbar sind. Das Halteproblem ist semi-entscheidbar, weil die Antwort „ja“ durch Ausführen des Programms bestätigt werden kann. Sein Komplement ist jedoch nicht semi-entscheidbar.