Ist eine unendliche Liste von denen gesund?

Question

In Prolog, ist die Vereinigung X = [1|X] ein vernünftiger Weg, um eine unendliche Liste von Einsen zu bekommen? SWI-Prolog hat damit kein Problem, aber GNU Prolog hängt einfach.

Ich weiß, dass in den meisten Fällen, die ich mit

one(1). 
one(X) :- one(X). 

aber meine Frage der Liste ersetzen könnte, ist explizit, wenn man den Ausdruck X = [1|X], member(Y, X), Y = 1 in einer „gesunden“ Prolog-Implementierung verwenden kann.

Answer 1

In Prolog, ist die Vereinigung X = [1|X] ein vernünftiger Weg, um eine unendliche Liste von Einsen zu erhalten?

Es hängt davon ab, ob Sie es für vernünftig halten, eine unendliche Liste überhaupt zu erstellen. In ISO-Prolog unterliegt eine Vereinheitlichung wie X = [1|X] der Vorkommnisprüfung (STO) und ist somit undefiniert. Das heißt, ein standardkonformes Programm darf ein solches Ziel nicht ausführen. Um dies zu vermeiden, gibt es unify_with_occurs_check/2, subsumes_term/2. Und um Interfaces gegen den Empfang von unendlichen Termen zu schützen, gibt es acyclic_term/1.

Alle aktuellen Implementierungen enden für X = [1|X]. Auch GNU Prolog beendet:

| ?- X = [1|X], acyclic_term(X). 

no 

Aber für komplexere Fälle, rationale Baum Vereinigung erforderlich. Vergleichen Sie dies mit Haskell, wo repeat 1 == repeat 1ghci zum Einfrieren verursacht.

Wie für rationale Bäume in regulären Prolog-Programmen, das ist am Anfang ziemlich interessant, aber nicht sehr gut.Als Beispiel wurde Anfang der 1980er Jahre angenommen, dass Grammatiken unter Verwendung von rationalen Bäumen implementiert werden. Leider sind die Menschen mit DCG allein zufrieden. Ein Grund, warum dies die Forschung nicht verlässt, ist, weil viele Begriffe, von denen Prolog-Programmierer annehmen, dass sie existieren, für rationale Bäume nicht existieren. Nehmen Sie als Beispiel die lexikografische Termordnung, die keine Erweiterung für rationale Bäume hat. Das heißt, es gibt rationale Bäume, die nicht mit der Standard-Term-Reihenfolge verglichen werden können. (Praktisch bedeutet dies, dass Sie quasi zufällige Ergebnisse erhalten.) Dies bedeutet, dass Sie keine sortierte Liste mit solchen Begriffen erstellen können. Das bedeutet wiederum, dass viele Einbauten wie bagof/3 nicht mehr zuverlässig mit unendlichen Termen arbeiten.

Für Ihre Beispielabfrage, sollten Sie die folgende Definition:

memberd(X, [X|_Xs]). 
memberd(E, [X|Xs]) :- 
    dif(E,X), 
    memberd(E, Xs). 

?- X = 1, Xs=[1|Xs], memberd(X,Xs). 
X = 1, 
Xs = [1|Xs] ; 
false. 

So manchmal gibt es einfache Möglichkeiten, Nicht-Beendigung zu entkommen. Aber meistens gibt es keine.

Answer 2

Sie haben nicht eine unendliche Anzahl von Einsen, natürlich, aber was für einen rational oder zyklischen Begriff genannt wird. Nicht alle Prolog-Systeme unterstützen jedoch zyklische Begriffe. Zu den Systemen, die rationale Begriffe unterstützen, gehören CxProlog, ECLiPSe, SICStus, SWI-Prolog und YAP. Beachten Sie jedoch, dass es Unterschiede zwischen den Berechnungen gibt, die Sie mit rationalen Termen durchführen können.

Eine Abfrage wie:

X = [1|X], member(Y, X), Y = 1. 

Unterstützung für coinduction erfordert. Sie haben eine portable Implementierung von Coinduction in Logtalk, die Sie mit allen oben genannten Systemen verwenden können. Coinduction erfordert, dass das Prolog-System rationale Terme (unter Verwendung einer Abfrage wie X = [1|X]) erstellen kann, die rationale Terme vereinheitlichen können, und die Bindings mit rationalen Termen in einer nicht-mehrdeutigen Weise drucken können.

Ein Beispiel über Aufzählen (oder Prüfung) die Elemente einer rationalen Liste finden Sie unter:

https://github.com/LogtalkDotOrg/logtalk3/blob/master/examples/coinduction/lists.lgt

Zwei Beispielabfragen für dieses Beispiel:

?- {coinduction(loader)}. 
... 
% (0 warnings) 
true. 
?- X = [1|X], lists::comember(Y, X), Y = 1. 
X = [1|X], 
Y = 1 ; 
false. 

?- X = [1, 2, 3| X], lists::comember(Y, X). 
X = [1, 2, 3|X], 
Y = 1 ; 
X = [1, 2, 3|X], 
Y = 2 ; 
X = [1, 2, 3|X], 
Y = 3 ; 
false. 

Wenn Sie interessiert sind In rationaler Hinsicht und Koinduktion enthält das Beispiel von Logtalk coinduction mehrere einzelne Beispiele und bibliographische Referenzen.