8.6 Unentscheidbarkeit

Im vorherigen Teilkapitel haben wir die universelle Turingmaschine $U$ konstruiert, die eine andere Turingmaschine, deren Codierung und Inputwort sie als Input gegeben hat, simulieren kann. Technisch gesprochen: $U$ akzeptiert die Sprache

\begin{array}{r} (1) & {c w | c = enc (M) und M akzeptiert w} . \end{array}

Allerdings: wenn $M$ auf $x$ nicht terminiert, dann terminiert $U$ auf $enc (M) x$ auch nicht. $U$ akzeptiert die Sprache also, entscheidet sie aber nicht. Wäre es nicht schön, eine Turingmaschine zu haben, die diese Sprache entscheidet? Dann könnten wir jede Turingmaschine simulieren und gleichzeitig Endlosschleifen und eventuell ganz allgemein "Programmierfehler" vorhersagen und abfangen. Wir werden zeigen, dass dies leider nicht möglich ist. In der Literatur ist dies als die Unentscheidbarkeit des Halteproblems (englisch undecidability of the Halting problem bekannt).

Als vorbereitenden Schritt schauen wir uns kurz die Codierungsfunktion nochmal genauer an. Wir bezeichnen mit ${TM}_{Σ}$ die Menge aller Turingmaschinen mit Inputalphabet $Σ$ . Wir hatten die Codierungsfunktion $enc : {TM}_{Σ} \to Λ^{*}$ definiert, für das Codierungsalphabet $Λ := Σ \cup {0, 1, #,,, L, S, R,;}$ . In diesem Teilkapitel wird es nötig sein, die Turingmaschine über dem Alphabet $Σ$ selbst zu codieren. Dies ist nicht besonders schwierig, solange $Σ$ mindestens zwei Zeichen hat. Wenn z.B. $Σ$ die Zeichen $0$ und $1$ enthält, dann können wir alle Zeichen in $Λ$ wiederum als Strings in $Σ^{*}$ codieren. Wir müssen hier nur vorsichtig sein, dass der Code präfixfrei ist. Wenn wir zum Beispiel naiv $1$ als $1$ und $0$ als $0$ und $#$ als $01$ codieren, dann wissen wir nicht mehr, was mit dem Codewort $01$ gemeint ist. Am einfachsten geht das mit einem Blockcode, in dem alle Codewörter die gleiche Länge $k$ haben, also $Λ \to {0, 1}^{k}$ . Mit $k = ⌈ \log_{2} | Λ | ⌉$ ist das kein Problem. Unsere "neue" Codierungsfunktion $enc$ ist nun also $enc : {TM}_{Σ} \to Σ^{*}$ . Wir definieren nun die Haltesprache $H A L T \in Σ^{*}$ :

\begin{array}{r} H A L T := {enc (M) w | M akzeptiert w} . \end{array}

Wir können die universelle Turingmaschine $U$ leicht abwandeln, dass sie $H A L T$ akzeptiert; wir müssen nur einen Decodierungsschritt vorausschicken, der die neue Codierung $enc (M) \in Σ^{*}$ in unsere "alte" in $Λ^{*}$ übersetzt. Beachten Sie, dass das Zeichen $;$ , das wir auch blockcodiert haben, uns hilft, die Grenze zwischen $enc (M)$ und $w$ zu erkennen.

Wir zeigen nun, dass $H A L T$ unentscheidbar ist, dass es also keine Möglichkeit gibt, das Nichtterminieren einer Maschine $M$ auf Eingabe $x$ vorauszusehen und abzufangen.

Theorem 8.6.1 (Unentscheidbarkeit des Halteproblems). Die Sprache

H A L T

ist unentscheidbar.

Ich gebe erst einmal einen kurzen und knappen Widerspruchsbeweis. Falls das ihnen zu schnell ging, lesen Sie den zweiten Beweis, in dem ich mir mehr Zeit nehme.

Kurzer Beweis per Wiederspruch. Nehmen wir an, es gäbe eine Maschine $H$ , die $H A L T$ entscheidet. Dann wäre auch die Sprache

\begin{array}{r} Diag := {enc (M) | M akzeptiert enc (M)} \end{array}

entscheidbar. Warum? Wir können einfach schauen, ob das Eingabewort $c$ die Form $enc (M)$ hat und in diesem Fall das Wort $enc (M) enc (M)$ der Maschine $H$ übergeben. Die Sprache $Diag$ ist, salopp ausgedrückt, die Menge aller Turingmaschinen, die ihre eigene Codierung als Inputwort akzeptieren. Ebenso wäre auch

\begin{array}{r} NegDiag := {enc (M) | M akzeptiert enc (M) nicht} \end{array}

entscheidbar; wir müssen ja nur $Diag$ entscheiden und dann das Ergebnis negieren. $NegDiag$ ist sozusagen die Menge aller Turingmaschinen, die nicht ihre eigene Codierung als Inputwort akzeptieren. Da $NegDiag$ nach Annahme entscheidbar ist, gibt es eine Maschine $D$ , die $NegDiag$ entscheidet.

Wir fragen uns jetzt: gehört $enc (D)$ selbst zu $NegDiag$ ?

\begin{aligned} (nach Definition von NegDiag) & enc (D) \in NegDiag & ⟺ D akzeptiert enc (D) nicht \\ (Bedeutung der Notation L (D)) & ⟺ enc (D) \notin L (D) \\ (nach Annahme L (D) = NegDiag) & ⟺ enc (D) \notin NegDiag \end{aligned}

Also $enc (D) \in NegDiag ⟺ enc (M) \notin NegDiag$ , ein Widerspruch. Unsere Annahme, dass $H A L T$ entscheidbar sei, ist also falsch. $◻$

Ausführlicher Beweis. Ich finde Beweise durch Widerspruch immer etwas unintuitiv, weil man die ganze Zeit im Konjunktiv argumentieren muss. Daher hier ein Beweis ohne Widerspruch. Wir zeigen, dass

H A L T

unentscheidbar ist, indem wir für eine beliebige Turingmaschine

M

zeigen, dass sie

H A L T

nicht entscheidet, indem wir nämlich ein Eingabewort

z \in Σ^{*}

konstruieren, auf dem

M

scheitert, also entweder

$f_{H} (z) = accept$ aber $z \notin H A L T$ , oder
$f_{H} (z) = reject$ aber $z \in H A L T$ , oder
$f_{H} (z) = undefined$ , d.h. $H$ terminiert auf Eingabewort $z$ nicht.

Wir setzen nun

y := enc (D)

und

z := y y

, wobei

D

eine neue Turingmaschine ist, die wir auf Basis von

H

konstruieren werden. Also noch einmal. Für eine beliebige, uns gegebene Turingmaschine

H

, werden wir eine neue Turingmaschine

D

bauen und sie codieren als

y := enc (D)

, so dass entweder

$f_{H} (y y) = accept$ aber $y y \notin H A L T$ , oder
$f_{H} (y y) = reject$ aber $y y \in H A L T$ , oder
$f_{H} (y y) = undefined$ .

Wenn uns dies gelingt, so haben wir gezeigt, dass

H

nicht die Sprache

H A L T

entscheidet: im Fall 3 terminiert

H

ja nicht einmal; in Fall 1 und 2 liefert

H

zwar eine Antwort, aber die falsche. Der Code für

D

ist sehr einfach:

def D(x):
    if H(xx) == accept then 
        reject 
    else 
        accept

Zur Erinnerung: $y := enc (D)$ . Wir unterscheiden drei Fälle.

$H (y y) = reject$ . Dann geht der Aufruf von $D (y)$ also in den else-Teil in den Zeilen 4-5 und $D (y) = accept$ , somit $y y = enc (D) y \in H A L T$ Wir befinden uns in Fall 1: $y y \in H A L T$ aber $H (y y) = reject$ . Die Maschine $H$ hat eine falsche Antwort für $H A L T$ geliefert.
$H (y y) = accept$ . Dann geht der Aufruf von $D (y)$ in Zeile 3, und $D (y) = reject$ , somit $y y = enc (D) y \notin H A L T$ . Wir befinden uns in Fall 2: $y y \notin H A L T$ und $H (y y) = accept$ . Die Maschine $H$ hat abermals eine falsche Antwort geliefert.
$H (y y)$ terminiert nicht. Dann befinden wir uns in Fall 3: $H$ kann $H A L T$ nicht entscheiden, denn Mindestbedingung hierfür wäre ja, auf jedem Eingabewort zu terminieren.

In jedem Fall sehen wir, dass

H

auf dem Eingabewort

y y

einen Fehler macht und somit

H A L T

nicht entscheidet. Da das für jede Turingmaschine geht, schließen wir: keine Turingmaschine kann die Sprache

H A L T

entscheiden; sie ist unentscheidbar.

◻

Ein Student hat am 26. Juni 2024 angemerkt, dass die Sprache

\begin{array}{r} NegDiag = {enc (M) | M akzeptiert enc (M) nicht} \end{array}

ja eine extrem konstruierte, nicht wirklich relevante Sprache sei (da hatte er Recht). Insofern sei es auch nicht relevant, dass $NegDiag$ unentscheidbar ist. Das ist allerdings auch nicht, was uns interessiert: unser Ziel war, zu zeigen, dass $H A L T$ unentscheidbar ist, und die Unentscheidbarkeit von $NegDiag$ war ein Schritt auf diesem Weg. Dass $H A L T$ unentscheidbar ist, ist in der Tat relevant, denn daraus folgt (nicht direkt, aber mit ein paar technischen Tricks), dass im Prinzip jede nichttriviale Frage über das Verhalten eines Programmcodes unentscheidbar ist. Also sind auch Fragen wie "Kann das Programm abstürzen?" oder "Kann ein unautorisierter Nutzer Zugang zu XYZ erhalten?" unentscheidbar.

Das Wort Unentscheidbarkeit verwenden wir hier in seiner technischen Bedeutung, die wir definiert haben: es gibt keine Turingmaschine, die das Problem entscheidet, also auf jeder Eingabeinstanz terminiert und die richtige Antwort liefert. Es gibt also in der Tat Raum für Algorithmen, die Software untersuchen und diese gegebenenfalls verifizieren oder Fehler / Sicherheitslücken finden. Dies ist im Prinzip das sehr real existierende Forschungsfeld der Programmverifikation. Die Unentscheidbarkeit des Halteproblems impliziert nicht, dass man auf dem Feld der Programmverifikation keine Fortschritte erzielen kann; sie impliziert nur, dass es keinen ultimaten Programmverifikator bzw. Bugfinder gibt.