Wie nah sind gängige Programmiersprachen daran, Turing nicht vollständig zu sein?

Der Begriff "Vollständigkeit" wurde in mehreren von mir belegten Informatikkursen erörtert. Ich habe jedoch nie ein intuitives Gefühl dafür bekommen, was die Vollständigkeit von Turing tatsächlich erfordert. Ich habe diese Frage gefunden, aber die Antworten sind etwas mathematischer als das, wonach ich suche.

Nehmen Sie eine gängige Programmiersprache wie C ++, Python, Java oder Lisp. Wie nah sind diese Sprachen daran, nicht vollständig zu sein? Haben diese Sprachen elementare Merkmale, die bei Entfernung dazu führen würden, dass die Sprache nicht vollständig ist? Oder könnten Sie eine Eigenschaft der Sprache ändern (z. B. etwas Zufälliges machen) und dadurch die Sprache nicht vollständig machen?

Gängige Programmiersprachen sind sehr sicher Turing-vollständig, wenn Sie eine idealisierte Ansicht vertreten, in der Programme eine beliebig große Menge an Speicher verwenden können. Es gibt normalerweise keine einzige Funktion, die Sie isolieren können, ohne die die Sprache nicht vollständig wäre.

Intuitiv gesehen erfordert die Vollständigkeit von Turing zwei Dinge:

• Eine Möglichkeit für Programme, eine Speichermenge zu bearbeiten, die nicht nur von der Größe der Eingabe abhängt. Jede Form von Objekterstellung , die größeren Objekte aus kleineren Objekten bauen kann , ist geeignet: Objekte, Strukturen, Paare, Listen malloc, newetc. Auch stapelbasierte Zuordnung ist genug vorausgesetzt, es ist ein Weg , um Zugriff auf Objekte in einem beliebigen Abstand von der Spitze des Stapels (mit nur stapelbasierter Zuordnung und nur Zugriff auf die Oberseite des Stapels erhalten Sie nur einen Pushdown-Automaten). Viele schwächere Formen der Datenmanipulation sind ebenfalls geeignet: In einer Sprache wie Lisp oder Python, in der Ganzzahlen keine begrenzte Größe haben, reichen die grundlegenden Ganzzahloperationen allein für die Vollständigkeit von Turing aus.
• Eine Möglichkeit für Programme, basierend auf einem Teil der Daten weiter zu laufen oder anzuhalten. Während Schleifen, Rekursion plus irgendeine Form von Bedingung (z. B. ifoder case/ switch) und gotoplus irgendeine Form von Bedingung die drei gebräuchlichen Wege sind, gibt es andere.

Ich denke, dass der beste Weg, um zu verstehen, was eine Sprache Turing-vollständig macht, darin besteht, Beispiele für Sprachen zu betrachten, die mächtig, aber nicht Turing-vollständig sind. Ich werde zwei Beispiele geben, die die beiden Hauptfamilien solcher Sprachen veranschaulichen (außer Sprachen, die im begrenzten Speicher arbeiten).

Betrachten wir ein imperativen Sprache mit Integer - Operationen und Arrays, sondern nur für die Schleifen ( for i = 1 to ngegebenen ikann nicht während der Schleife modifiziert werden), nicht willkürlich (while) Schleifen und keine Rekursion. BlooP und frühe Versionen von FORTRAN sind Beispiele. In einer solchen Sprache können Sie nur primitive rekursive Funktionen ausdrücken - Funktionen, bei denen der Rechenaufwand durch die Größe der Eingabe begrenzt ist. Die Sprache ist nicht Turing-vollständig - kann keine beliebigen rekursiven Funktionen ausdrücken - aufgrund der an die Rechenzeit gebundenen Zeit.

Eine funktionale Sprache kann nicht vollständig gemacht werden, indem die Rekursion durch ein Typsystem eingeschränkt wird, das alle zu terminierenden Funktionen einschränkt. Wenn das Typsystem entscheidbar ist (dh wenn es entscheidbar ist, ob das Programm gut typisiert ist), kann eine solche Sprache nicht vollständig abgeschlossen werden (da das Stoppproblem unentscheidbar ist). Sprachen, die für die Beweisführung von Theoremen verwendet werden, wie Coq und Agda , sind von dieser Art.

Siehe auch Was kann Idris nicht tun, wenn er die Vollständigkeit von Turing aufgibt?

Nebenbei bemerkt, Theoremprüfer verlangen vom Benutzer die Eingabe von Abschlussnachweisen (dh sie finden sie selbst nicht). Sie könnten also einen Theorembeweiser mit einem unentscheidbaren Typsystem erstellen: Wenn Sie einen korrekten Beweis erhalten, sind Sie glücklich, sonst geben Sie nach einer Weile auf. Aber es wäre nicht benutzerfreundlich. Die meisten Theoremprüfer haben ein entscheidbares Typsystem: Sie geben einen Begriff ein und entweder wird er akzeptiert oder Sie erhalten einen Typfehler zurück. Was Theorembeweiser nicht haben, ist eine entscheidbare Typinferenz : Wenn Sie einen Begriff mit partiellen Typinformationen eingeben und dieser abgelehnt wird, wissen Sie nicht, ob dies daran liegt, dass der Begriff nicht eingegeben werden kann oder dass die Inferenzmaschine nicht intelligent genug ist.