Problem ohne Selbstreferenz stoppen: Warum reicht dieses Argument nicht aus (oder reicht es aus)?

Ich versuche einen Weg zu finden, um die Idee des Halting Problem-Beweises so zugänglich wie möglich zu erklären (für CS-Studenten). Das einfachste Argument, das ich gefunden habe, ist dieses ; Dies ist genau die Art der Behandlung, die ich anstrebe. Die Selbstreferenz (insbesondere die Überprüfung, ob ein Programm auf sich selbst anhält) ist jedoch nicht die didaktischste.

Als Beweisskizze frage ich mich, warum wir nicht noch weiter vereinfachen und sagen könnten: Wenn wir ein Programm H(P,I)für das Halteproblem annehmen , das mit true P(I)anhält, wenn angehalten wird, und ansonsten mit false anhält, könnten wir ein Programm erstellen der Form:

def Q(J):
  if H(Q,J) then loop forever
  else halt

... was genau dann ein gültiges Programm ist, wenn das Halteproblem ein gültiges Programm ist. Wir können dann fragen: Wofür sollte H(Q,J)ein beliebiger Wert zurückgegeben werden J? Wir sehen in beiden Möglichkeiten einen Widerspruch, und wir schließen daraus, dass ein Programm der Form nicht existieren kann , da die Existenz von Hes uns ermöglicht, das widersprüchliche Programm zu konstruieren .QH

Es gibt hier immer noch eine Selbstreferenz darin, dass das Programm Qprüft, ob es bei der aktuellen Eingabe anhält oder nicht (und das Gegenteil tut), aber für mich scheint dies viel intuitiver zu sein, als eine Situation einzurichten, in der wir einen Aufruf des benötigen Form P(P)oder H(P,P)usw. Ich habe jedoch nicht gesehen, dass dieses einfachere Argument verwendet wird, und ich denke, es wäre gewesen, wenn es gültig gewesen wäre. Daher sind meine Fragen:

• Reicht das obige Argument als Beweis (Skizze) für das Halteproblem aus?
  • Wenn ja, warum gehen so viele Argumente mit einem verwirrenden Schritt des Formulars einher P(P)oder H(P,P)? (Ist es nur, um die unwichtige "Eingabe" aus der Gleichung zu entfernen?)
  • Wenn nicht, was fehlt?

Zu diesem Thema gibt es eine Vielzahl verwandter Fragen, z. B.:

• Problem ohne Selbstreferenz stoppen
• Gibt es einen intuitiveren Beweis für die Unentscheidbarkeit des Halteproblems als die Diagonalisierung?

Ich fand auch Erwähnung des Beweises, der auf Berrys Paradoxon basiert, was sehr ansprechend ist. Trotzdem habe ich es noch nicht geschafft, mich davon zu überzeugen, ob das obige spezifische Argument funktioniert oder nicht (auch wenn dies nur zu meinem eigenen Verständnis ist; ich habe das Gefühl, dass mir vielleicht etwas Dummes fehlt und ich möchte wissen, was es ist).

Ich denke nicht, dass dies ein guter Weg ist, um das Problem des Anhaltens darzustellen, da es ein kritisches Problem auf hinterhältige Weise unter die Decke fegt. Ich schlage vor, bei einer Standardpräsentation zu bleiben, wie der, die Sie verlinkt haben. Wenn Sie einen Weg finden möchten, dies so zu erklären, dass der technische Inhalt minimiert wird, ist die Präsentation in diesem Video überraschend zugänglich und bleibt der Logik des Standardbeweises treu.

Weiter zu den Schwierigkeiten mit Ihrem Vorschlag. In Ihrem Vorschlag ist es nicht trivial, den Code für eine solche zu notieren Q. Überlegen Sie, was es bedeutet, die Leitung zu haben

  if H(Q,J) then loop forever 

Denken Sie daran, dass das erste Argument Heine Bitfolge ist, die den Code / Algorithmus / die Turingmaschine enthält - es ist kein Zeiger auf die Funktion, sondern eine Zeichenfolge. Naiv scheint dies zu bedeuten, dass wir eine fest codierte Zeichenfolge, die den Quellcode für enthält Q, in den Code von einfügen Q. Das ist aber nicht möglich. Angenommen, der Code für Qnimmt 100 Zeichen an. Dann müssen wir eine Zeichenfolgenkonstante mit 100 Zeichen innerhalb der Definition von fest Qcodieren. Außerdem benötigen wir für den Rest der Logik weitere Zeichen - und das ergibt mehr als 100 Zeichen. Wenn Sie darüber nachdenken, ist es offensichtlich, dass wir keine String-Konstante im Code haben können Q, deren Code der Code von ist Q, weil er zu lang wäre.

Vielleicht denkst du, dass du das nicht im Sinn hattest. Vielleicht haben Sie gedacht, dass die Programmiersprache eine integrierte API hat, um den Code der aktuellen Funktion abzurufen. Der Code, an den Sie gedacht haben, ist also ungefähr so:

def Q(J):
  if H(get_source_code_of_current_function(),J) then loop forever
  else halt

OK, gut. Dies beweist, dass das Problem des Anhaltens nicht für Code gelöst werden kann, der in einer Programmiersprache mit einer get_source_code_of_current_function()API geschrieben wurde. Meine Lieblingsprogrammiersprache hat jedoch keine solche API. Dieser Beweis beweist also nichts über meine Lieblingsprogrammiersprache - vielleicht ist das Problem des Anhaltens für meine Sprache lösbar, wer weiß? In ähnlicher Weise verfügen Turing-Maschinen nicht über eine solche API, sodass dies nicht beweist, dass das Stoppproblem für Turing-Maschinen unentscheidbar ist.

Und das ist ein großer Fehler in Ihrem Beweis. Und es ist ein Fehler, der subtil und überhaupt nicht offensichtlich ist. Ich denke nicht, dass es pädagogisch eine gute Idee ist, einen Beweis vorzulegen, der an der Oberfläche "gültig" aussieht, aber tatsächlich fehlerhaft ist, wenn man sich einmal tiefer damit befasst.

Nun, es ist möglich , Ihren vorgeschlagene Beweis zu retten. Es tatsächlich ist möglich , eine Funktion zu konstruieren Q, die die Art und Weise funktioniert , wie Sie gesagt; Sie brauchen es im Grunde, um eine Quine zu sein . Ich nehme an, Sie könnten im Prinzip die Idee von Quines erklären, dann Ihren Beweis vorlegen und erklären, wie eine Funktion mit diesen Ideen implementiert wirdQ . Aber das scheint mir aus pädagogischer Sicht eine schlechte Idee zu sein. Quines sind umwerfend und mysteriös und verdammt schwer zu verstehen. Ein Student, der Quines nicht versteht, wird Ihren Beweis nicht verstehen. Und es lässt den Beweis der Unentscheidbarkeit für das Halteproblem viel mysteriöser aussehen, als es sein muss. Dies scheint mir also kein zugänglicherer Weg zu sein, um das Problem des Anhaltens zu verstehen.

Ich sehe nicht, wie schwierig es ist, sich auf sich selbst zu beziehen. Das Barber-Paradoxon ist ziemlich leicht zu verstehen. Und Ihr Argument hat eine implizite Selbstreferenz, und ich finde es schwieriger zu verstehen als eine einfache Selbstreferenz. Darüber hinaus ist es inkohärent. Um H (Q, J) zu definieren, müssen Sie zuerst wissen, was Q ist, und um Q zu definieren, müssen Sie zuerst wissen, was H (Q, J) ist. Das geht nicht Bestenfalls können Sie behaupten, dass Q ein fester Punkt dieser selbstreferenziellen Definition ist, aber wenn Sie dann versuchen, etwas aus der widersprüchlichen Natur von Q abzuleiten, zeigen Sie nur, dass H nicht existiert ODER dass kein solcher fester Punkt existiert ;; Sie müssen jetzt beweisen, dass der Fixpunkt existieren müsste, wenn H existieren würde.