Das Halteproblem

für Oberon-Unterprogramme

 

Gibt es eine Prozedur oder eine boolesche Funktionsprozedur, die folgendes leistet:
Ist p ein Unterprogramm und x eine Zeichenfolge, so entscheidet die Prozedur (die Funktionsprozedur) ob das Unterprogramm p bei Eingabe von x terminiert?

Grobentwurf für die Oberon-Funktionsprozedur haelt:
PROCEDURE haelt(p,x:text):BOOLEAN;

BEGIN
   IF <p terminiert bei Eingabe von x> THEN
      haelt:=TRUE
   ELSE
      haelt:=FALSE
   END;
END haelt;

Unterprogramm Seltsam:
PROCEDURE seltsam;

PROCEDURE haelt(p,x:text):BOOLEAN;

BEGIN
   IF <p terminiert bei Eingabe von x> THEN
      haelt:=TRUE
   ELSE
      haelt:=FALSE
   END;
END haelt;

BEGIN 
   lies(p);
   WHILE haelt(Seltsam.Mod,Seltsam.Mod) DO
     (* Das ist eine Endlosschleife! *)
   END;
   Out.String('Fertig! ');
END seltsam;
 

Satz von Turing (für Oberon-Unterprogramme):
Es gibt keine Oberon-Funktionsprozedur, das für ein beliebiges Unterprogramm p und eine beliebige Eingabe x die Frage beantwortet, ob p auf x angewendet nach endlich vielen Schritten anhält oder nicht.

Allgemein:
Die Halteeigenschaft für Programme ist unentscheidbar.
Die Verantwortung für das Anhalten (die Terminierung) von Programmen wird niemals einer Maschine übertragen werden können; sie bleibt beim Menschen.

Entscheidbar sind:


Unentscheidbar:

Zurck