Halteproblem

Ok, erster Versuch ohne "Formelgedöns".

Ist daher grausam unexakt, bitte nicht schlagen,
aber es hilft vielleicht eine Ahnung zu kriegen, um was es überhaut grob gesehen geht
Und der Zweck heiligt ja bekanntermaßen alle Mittel ...

Endlosschleifen sind in der Praxis recht unangehm, kaum jemand baut sie beabsichtigt ein. Wenn sie zuschlagen, bleibt das Program "hängen". Nicht gut.
Man kann sich in der Regel nie 100% sicher sein, daß es sie nicht doch gibt, gut versteckt, nur für ganz bestimmte Inputs. Passiert jedem (irgendwann), auch den erfahrensten Profis.

Daher der Gedanke: Kann man nicht ein Programm bauen, daß für beliebe andere Programme als Input, überprüft ob es eine Endlosschleife enthält (Nicht hält) oder nicht (hält) ?
Wär' doch wunderbar ...

Aber der Clou ist eben, daß es so was PRINZIPIELL nicht geben KANN. Dh das Halteproblem zu lösen (wollen) ist sozusagen ein informatisches Perpetuum Mobile.
Daß kann man streng mathematisch beweisen.
Um das zu tun, muß man die Aufgabe (Halteproblem entscheiden) formalisieren, dh in Formeln/Formalismen/etc giessen, und dadurch wird's ein bisschen unverständlich/unzugänglich, für die die nicht in dieser Sprache geübt sind.

Zu erklären WARUM das so ist, ganz besodners OHNE "Formelgedöns", das ist etwas challenging, vorallem fehlt mir heut' die Zeit dazu.
Bei Bedarf melden

Mfg, LB

Zitat von SweetnSour

Meine Frage bezieht sich auf das "Halteproblem" was euch sicher allen ein Begriff ist. Kann mir das jemand so erklären, dass auch Informatikunbegabte es verstehen?

Ich kann's versuchen...

Frage: Kann man eine Funktion HÄLT(F,A) formulieren, die zuverlässig ermittelt, ob die Funktion F bei einem Aufruf mit dem Argument A terminiert?

Antwort: Nein.

Beweis: Durch Widerspruch. Wir nehmen an, dass die gefragte Funktion HÄLT tatsächlich existiert. Wir basteln uns davon ausgehend eine Funktion AUTSCH(A), die ungefähr wie folgt aussieht:

AUTSCH(A):
falls HÄLT(A,A) = NEIN: retourniere JA;
sonst: Endlosschleife;

Wir überlegen uns nun, ob AUTSCH(AUTSCH) terminiert:

Möglichkeit 1: AUTSCH(AUTSCH) terminiert. Dann muss offensichtlich HÄLT(AUTSCH,AUTSCH) die Antwort NEIN geliefert haben. HÄLT(AUTSCH,AUTSCH) tut aber laut Voraussetzung nichts anderes, als zu ermitteln, ob AUTSCH(AUTSCH) hält. AUTSCH(AUTSCH) hätte also eigentlich nicht terminieren dürfen. Widerspruch.

Möglichkeit 2: AUTSCH(AUTSCH) terminiert nicht. Da der Algorithmus HÄLT aber laut Voraussetzung immer terminiert, kann das aber nur daran liegen, dass HÄLT(AUTSCH,AUTSCH) die Antwort JA geliefert hat. HÄLT(AUTSCH,AUTSCH) tut aber laut Voraussetzung nichts anderes, als zu ermitteln, ob AUTSCH(AUTSCH) hält. AUTSCH(AUTSCH) müsste also eigentlich terminiert haben. Widerspruch.

Da die Annahme, HÄLT würde existieren, unmittelbar ins Paradoxe führt, kann es HÄLT offenbar nicht geben.

.

Ja, das da oben ist der "Standardbeweis", IMHO sehr gut & verständlich erklärt
Ein paar Bemerkungen dazu (die man eher selten explizit irgendwo lesen kann):

a) Widerspruchsbeweise sind natürlich immer - notwendigerweise - hochgradig nichtkonstruktiv.
Versuche mal "hält" - trotz des Wissens das es nicht geht - zu konstruieren.
Zu sehen woran es vermutlich scheitern wird, ist ganz lehrreich.

b) Klarerweise kann man sehr wohl (sehr einfach) eine Semi-Entscheidbare Variante von "Hält" bauen.

c) Man könnte vermuten: Das Programm vom Beweis ist ein extrem konstruierter pathologischer Spezialfall. Kann man das Problem eventuell doch lösen/entscheiden, wenn wir so was ausschliessen, z.B verbieten, daß man autsch mit sich selbst aufrufen kann u.v.m ? Hilft nix, ändert nix. Man kann das auch völlig anders beweisen.
(Das ist jetzt SEHR schwammig formuliert, will nur sagen daß der obige Beweis wenig Einsicht gibt wie tief verwurzelt das Problem wirklich ist bzw mit welchen Modifikationen es eventell doch lösbar ist bzw für welche Spezialfälle es immer noch unetscheidbar ist)

d) Die Historie dieses Problems ist auch recht interessant. Besonders weil es schon bewiesen wurde, BEVOR es die ersten (nicht mechanischen) Rechner gab.

e) Viele andere Unentscheidbarkeitsresultate, z.B (Output)Äquivalenz von 2 Programmen, ergeben sich unmittelbar aus der Unentscheidbarkeit des Halteproblems.

Mfg, LB

Zitat von Georg Kraml

AUTSCH(A):
falls HÄLT(A,A) = JA: retourniere NEIN;
sonst: Endlosschleife;

Möglichkeit 1: AUTSCH(AUTSCH) terminiert. Dann muss offensichtlich HÄLT(AUTSCH,AUTSCH) die Antwort NEIN geliefert haben.

Also für mich hat HÄLT offensichtlich JA gesagt in dem Fall. Ich vermute, das sollte "= NEIN" heißen, net "= JA". Dann ergibt alles einen Sinn.

Naja, die Aussage: Ich habs ned verstanden ist ein bissi unspezifisch.

Aber ok, das selbe nocheimal:
Falls das nicht hilft, spezifisch nachfragen.

Grundidee: Indirekter Beweis, dh die Annhame, daß das HP entscheidbar ist auf einen Widerspruch führen. Schlußfolgerung: Die Annahme ist falsch, dh das HP ist eben nicht entscheidbar.

Annahme: Ein fiktitves Programm
bool hält(X,Y)
existiert.
X: beliebiger Source codes in irgend einer fixen (turing vollständigen) Sprache Z, Y ein Input für X.
Es liefert true zurück falls das Programm X mit Input Y terminiert, ansosnten false.

Dann kann man klarerweise dieses Programm konstruieren:

bool komisch(X) ... X wieder beliebiger source code in Z.

komisch(X)
{
wenn hält(X,X) false liefert print("wahnsinn");
ansonsten endlosschleife;
}

Haaalt ...
hält(X,X) ???

Warum nicht !!!
Für die meisten Programme ist zwar der eigene Quellcode kein sinnvoller Input, aber "hält" muß ja auch für sinnlose Inputs das richtige Ergebnis liefern.

Nun rufen wir komisch mit seinem eigenen source code auf.
Und überlegen was passiert.
dh komisch(X); X=source_code(komisch);

Selbstanwendung ist natürlich auch nicht verboten, jeder beliebige Input ist erlaubt.

Nehmen wir an, komisch(source(komisch)) hält.
Dann muß hält(source(komisch)) falsch sein.
Denn nur für hält(..) false terminiert komisch.
Aber hält(source(komisch)) false bedeutet laut Definition von hält, daß komsich nicht hält.
Widerspruch.
Angenommen komisch(source(komisch)) hält nicht.
Dann muß hält(..) true liefern, anders kann komisch in keine Endlosschleife geraten.
Aber hält(source(komisch)) true heißt laut Definiton, daß hält termiert.
Widerspruch.

Das heißt, komisch terminert genau dann wenn komisch nicht terminiert.
Und das ist ... komisch.

Die Argumentation ist korrekt, dh es kann nur an der Annahme, daß hält existiert liegen.
Daher ist unsere Annhame falsch, hält kann nicht existieren, dh. das HP ist nicht entscheidbar.

Mfg, LB

Zitat von hal

Also für mich hat HÄLT offensichtlich JA gesagt in dem Fall. Ich vermute, das sollte "= NEIN" heißen, net "= JA". Dann ergibt alles einen Sinn.

Hast recht. Ist gefixt.

.

Zitat von Georg Kraml

Hast recht. Ist gefixt.

Du hast das falsche Flag invertiert, jetzt macht die ganze Geschichte noch weniger Sinn

:hewa:

Naja, war grad erst aufgestanden.

.

Zitat von Georg Kraml

Naja, war grad erst aufgestanden.

Ein echter Informatiker sollte sowas im Schlaf können

Sicherlich, bezweifelt auch keiner, daß (hier schreibende) Informatiker das im Schlaf können

Aber aufstehen zählt weder zum Wach noch Schlaf Zustand.
Das ist ein unangehemner, eigenständiger, metastabiler und manchmal durchaus den halben Tag andauernder Zustand, in dem sowas akzeptabel ist.
Jo!

Mfg, LB.

Würde mal sagen, weder noch
Ist nicht *völlig* daneben/mißverstanden, aber die Zusammenfassung paßt nicht.
(wenn ich's richtig verstanden hab).

Das Programm, daß für alle Programme feststellen soll ob sie terminieren, terminiert immer, per Definition. (wär' sinnlos Termination nicht zu verlangen)
Dh. wenn man es auf sich selbst anwendet liefert es immer "Ja, ich terminiere" zurück.
Damit hat man nicht viel gewonnen.

Deshalb braucht man ein zweites Programm, das dieses Program als Subroutine verwendet, und das zweite Programm wendet man auf sich selbst an.
Aber Selbstreferenz (und die Konstruktion des 2 Programms) ist definitv der Clou bei *diesem* Beweis.

Mfg, LB