Czy nieskończona lista osób zdrowych psychicznie?

Question

W Prologu, czy zjednoczenie jest dobrym sposobem na uzyskanie nieskończonej listy? SWI-Prolog nie ma z tym żadnego problemu, ale GNU Prolog po prostu się zawiesza.

wiem, że w większości przypadków mógłbym wymienić listy z

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

ale moje pytanie jest jawnie jeśli można użyć wyrażenia X = [1|X], member(Y, X), Y = 1 w „sane” realizacji Prolog.

Answer 1

W Prologu, czy ujednolicenie jest sposobem na uzyskanie nieskończonej listy?

To zależy od tego, czy uważasz za rozsądne stworzenie nieskończonej listy w ogóle. W ISO-Prolog unifikacja taka jak X = [1|X] podlega kontroli (STO) i dlatego jest niezdefiniowana. Oznacza to, że program zgodny ze standardami nie może realizować takiego celu. Aby tego uniknąć, istnieje unify_with_occurs_check/2, subsumes_term/2. Aby chronić interfejsy przed otrzymywaniem nieskończonych warunków, istnieje acyclic_term/1.

Wszystkie bieżące implementacje kończą się na X = [1|X]. Również GNU Prolog kończy:

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

no 

Jednak w bardziej skomplikowanych przypadkach potrzebne jest racjonalne zjednoczenie drzew. Porównaj to z Haskellem, gdzie repeat 1 == repeat 1 powoduje zamrożenie.

Jeśli chodzi o używanie racjonalnych drzew w zwykłych programach Prologu, jest to dość interesujące na początku, ale nie rozszerza się bardzo dobrze.Przykładowo, przez jakiś czas sądzono, że na początku lat 80. XX wieku gramatyki będą wdrażane z użyciem drzew racjonalnych. Niestety, ludzie są zadowoleni z samych DCG. Jednym z powodów, dla których nie jest to pozostawienie badań, jest, ponieważ wiele pojęć programiści zakładają, że istnieją, nie istnieją dla drzew racjonalnych. Jako przykład można podać uporządkowanie terminów leksykograficznych, które nie ma rozszerzenia dla drzew racjonalnych. Oznacza to, że istnieją racjonalne drzewa, których nie można porównywać przy użyciu standardowej kolejności terminów. (Praktycznie oznacza to, że otrzymujesz quasi-losowe wyniki.) Oznacza to, że nie możesz utworzyć posortowanej listy zawierającej takie terminy. Co znowu oznacza, że ​​wiele wbudowanych, takich jak bagof/3, nie będzie działało niezawodnie z nieskończonymi terminami.

Dla przykładu zapytanie, należy rozważyć następującą definicję:

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. 

Więc czasami istnieją proste sposoby ucieczki non-zakończenie. Ale częściej niż nie ma ich wcale.

Answer 2

Nie dostaniesz nieskończoną liczbę tych, oczywiście, ale co się nazywa racjonalne lub cykliczny termin. Jednak nie wszystkie systemy Prolog obsługują terminy cykliczne. Systemy zapewniające pewne wsparcie dla racjonalnych pojęć obejmują CxProlog, ECLiPSe, SICStus, SWI-Prolog i YAP. Należy jednak pamiętać, że istnieją między nimi różnice dotyczące obliczeń, które można wykonywać na warunkach racjonalnych.

Zapytanie takie jak:

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

wymaga obsługi coinduction. Masz przenośną implementację funkcji Coinduction w Logtalk, której możesz używać we wszystkich wymienionych wyżej systemach. Coinduction wymaga, aby system Prolog mógł tworzyć racjonalne terminy (za pomocą zapytania takiego jak X = [1|X]), które mogą ujednolicać terminy racjonalne i które mogą drukować wiązania za pomocą terminów racjonalnych w sposób nie-ambiwalentny.

Na przykład o wyliczanie (lub testowaniu) elementy racjonalnego listy, patrz:

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

Dwa przykładowe zapytania dla tego przykładu:

?- {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. 

Jeśli jesteś zainteresowany w kategoriach racjonalnych i coinduction, przykład Logtalk w coinduction zawiera kilka indywidualnych przykładów i odniesień bibliograficznych.