[TheoInf] Reduktion von HALTING nach CORRECTNESS

SideWinder

In meinem Skript wird eine Reduktion von HALTING (wie bekannt, Halteproblem) nach CORRECTNESS (Does program P return I2 when run on input I1?) durchgeführt.

Mir einleuchtender Grund: Reduktion von HALTING nach CORRECTNESS zeigt, dass CORRECTNESS ebenfalls unentscheidbar ist. Klarerweise, weil: Würde eine Entscheidungsprozedur für CORRECTNESS existieren, würde zusammen mit der Reduktion von HALTING nach CORRECTNESS, auch HALTING entscheidbar sein, was bewiesenermaßen nicht der Fall sein kann.

Nun zu meiner Frage: Wir haben gelernt, dass eine Reduktion von A nach B auch damit "informal" umschrieben werden kann, dass A die Entscheidungsprozedur von B aufruft. Allerdings wird das im Skript nun genau umgekehrt gemacht:

(P, I) ... arbitrary instance of HALTING
construct (P', I1, I2) of CORRECTNESS by setting I1=I2=I and build P' from P as follows:

procedure P' (S) {
    P(S);
    return S;
}

Das sieht für mich aber nun so aus als würde die Prozedur für CORRECTNESS die Prozedur für HALTING aufrufen, das klingt doch mehr nach einer Reduktion von CORRECTNESS nach HALTING, oder?

Wo ist mein Denkfehler?

MfG SideWinder

Michael E.

Die Argumentation ist Folgende: Angenommen, es existiert eine Turingmaschine M für CORRECTNESS. Dann kann man damit eine Turingmaschine für HALTING konstruieren: Sei x Instanz des Halteproblems. Transformiere x in f(x), wie du beschrieben hast. Dieses f ist berechenbar. Nun gilt: x € HALTING <=> f(x) € CORRECTNESS. Da M die Frage f(x) € CORRECTNESS entscheiden kann, hast du eine TM für das Halteproblem, was ein Widerspruch ist.

Das ist auch im Prinzip das, was du nachher "informal" beschreibst, wenn A das Halteproblem ist.

Editwar: Um es nochmal deutlich zu sagen: Dein Code ist der vollständige Code einer Maschine für das Halteproblem, nicht für das Correctness-Problem.