Berechenbarkeit

Hilberts Frage

1928 stellte David Hilbert das Entscheidungsproblem: Gibt es ein mechanisches Verfahren, das für jede mathematische Aussage entscheidet, ob sie aus den Axiomen folgt? Wenn ja, wäre Mathematik im Prinzip automatisierbar. Turing und unabhängig davon Alonzo Church zeigten 1936: Nein. Turings Weg dorthin war genau die Frage, die diese Seite behandelt.

Dass es unlösbare Probleme geben muss, sieht man schon durch Zählen. Jedes Programm ist eine endliche Zeichenkette – man kann alle Programme durchnummerieren: erst die der Länge 1, dann die der Länge 2 und so weiter. Ja/Nein-Probleme über natürliche Zahlen dagegen gibt es so viele wie unendliche 0-1-Folgen, und die lassen sich nach Cantors Diagonalargument nicht durchnummerieren. Es gibt also mehr Probleme als Programme – die allermeisten Probleme hat kein Programm. Offen bleibt nur, ob auch ein interessantes darunter ist.

Das Halteproblem

Angenommen, jemand liefert eine Methode haelt(programm, eingabe), die immer nach endlicher Zeit antwortet und immer recht hat. Turings Beweis zeigt, dass es sie nicht geben kann – durch einen Widerspruch. Klick dich durch:

Das Muster heißt Diagonalisierung: Man füttert ein Programm mit sich selbst und dreht die Antwort um – dieselbe Idee wie bei Cantor und beim Lügner-Paradox („Dieser Satz ist falsch“). Gödels Unvollständigkeitssatz von 1931 beruht auf einer verwandten Konstruktion.

Wichtig ist, was der Satz nicht sagt: Für viele einzelne Programme kann man sehr wohl entscheiden, ob sie anhalten. Unmöglich ist nur ein Verfahren, das für alle Programme funktioniert. Und es ist kein Geschwindigkeitsproblem – auch ein unendlich schneller Rechner könnte das Halteproblem nicht lösen.

Warum ein Halte-Orakel die Mathematik lösen würde

Wie viel ein solches haelt wert wäre, zeigt ein harmloses Programm. Nimm eine Zahl; ist sie gerade, halbiere sie, sonst nimm sie mal 3 plus 1. Wiederhole, bis 1 herauskommt:

while (n != 1) n = (n % 2 == 0) ? n / 2 : 3 * n + 1;

Ob diese Schleife für jeden Startwert endet, ist die Collatz-Vermutung – seit 1937 offen. Mit Computern wurde sie für astronomisch viele Startwerte geprüft, bewiesen ist sie nicht. Ein Halte-Orakel würde hier sofort helfen: Für jeden einzelnen Startwert könnte es sagen, ob die Schleife endet. Noch direkter bei der Goldbach-Vermutung: Ein Programm prüft jede gerade Zahl ab 4, ob sie Summe zweier Primzahlen ist, und hält beim ersten Gegenbeispiel. Ob dieses Programm hält, ist genau die Frage, ob die Vermutung falsch ist – eine einzige Frage an das Orakel, und ein Jahrhundertproblem wäre gelöst. Dass es so einfach nicht geht, ist kein Zufall.

Reduktion: ein Beweis für viele

Hat man ein unentscheidbares Problem, bekommt man weitere geschenkt. Die Technik heißt Reduktion: Man zeigt, dass ein Verfahren für Problem X auch das Halteproblem lösen würde. Da es für das Halteproblem keines gibt, kann es auch für X keines geben. Beispiel: „Gibt dieses Programm irgendwann ‚Hallo‘ aus?“ Nimm ein beliebiges Programm, ersetze alle seine Ausgaben durch nichts und hänge am Ende print("Hallo") an. Es gibt genau dann „Hallo“ aus, wenn das ursprüngliche Programm anhält. Wer die Hallo-Frage beantworten kann, beantwortet also das Halteproblem.

So entstand eine lange Liste unentscheidbarer Probleme, darunter erstaunlich konkrete: ob eine Gleichung mit ganzzahligen Koeffizienten eine ganzzahlige Lösung hat (Hilberts zehntes Problem, 1970 gelöst – mit „unentscheidbar“), ob sich eine Menge von Kacheln lückenlos zu einer unendlichen Fläche fügt, oder ob zwei kontextfreie Grammatiken dieselbe Sprache beschreiben.

Der Satz von Rice

Henry Rice zog 1953 die allgemeinste Konsequenz: Jede nichttriviale Eigenschaft dessen, was ein Programm tut, ist unentscheidbar. „Nichttrivial“ heißt nur: Manche Programme haben die Eigenschaft, andere nicht. „Was es tut“ heißt: Es geht um das Verhalten, nicht um den Text. Ob ein Programm mehr als 100 Zeilen hat, ist entscheidbar. Ob es jemals eine NullPointerException wirft, ob es sortiert, ob es Daten an Dritte schickt, ob es dasselbe tut wie die alte Version – unentscheidbar.

Für Werkzeuge heißt das: Ein Analysewerkzeug kann nicht gleichzeitig alle echten Fehler finden, nie falschen Alarm schlagen und immer fertig werden. Eins davon muss es opfern. Probier zwei Strategien an sechs Codestücken aus:

Für Entwickler übersetzt

Schon der Java-Compiler arbeitet mit dieser Grenze. Seine Prüfung, ob eine Variable vor dem Lesen belegt ist, ist bewusst einfach und vorsichtig – er lehnt auch Code ab, der in Wahrheit korrekt ist:

int x;
if (b)  x = 1;
if (!b) x = 2;
System.out.println(x);   // Fehler: variable x might not have been initialized
                         // obwohl einer der beiden Zweige immer greift

while (true) { }
System.out.println("nie");   // Fehler: unreachable statement
if (false) { System.out.println("nie"); }   // erlaubt – die Regeln sind festgelegt, nicht „klug“

Die Sprachspezifikation legt genau fest, wie weit der Compiler denkt – damit alle Compiler dieselben Programme akzeptieren. Klüger könnte er sein, vollständig nie.

Häufige Irrtümer

Verwandte Begriffe