È una lista infinita di quelli sani?

Question

In Prolog, l'unificazione X = [1|X] è un modo sano per ottenere una lista infinita di quelli? SWI-Prolog non ha alcun problema con esso, ma GNU Prolog si blocca semplicemente.

So che nella maggior parte dei casi ho potuto sostituire l'elenco con

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

ma la mia domanda è esplicitamente se è lecito usare l'espressione X = [1|X], member(Y, X), Y = 1 in un'implementazione Prolog "sano".

Answer 1

In Prolog, è l'unificazione X = [1|X] un modo sano per ottenere una lista infinita di quelli?

Dipende dall'opportunità o meno di produrre un elenco infinito. In ISO-Prolog una unificazione come X = [1|X] è soggetta a verifica di presenza (STO) e quindi non è definita. Cioè, un programma conforme alla norma non deve eseguire un tale obiettivo. Per evitare che ciò accada, c'è unify_with_occurs_check/2, subsumes_term/2. E per proteggere le interfacce dal ricevere termini infiniti, c'è acyclic_term/1.

Tutte le implementazioni correnti terminano per X = [1|X]. Anche GNU Prolog termina:

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

no 

Ma per i casi più complessi, è necessario un albero di unificazione razionale. Confronta questo con Haskell dove repeat 1 == repeat 1 causa il blocco di ghci.

Per quanto riguarda l'utilizzo di alberi razionali nei normali programmi Prolog, questo è piuttosto interessante all'inizio ma non si estende molto bene.Ad esempio, si è creduto per qualche tempo all'inizio degli anni '80 che le grammatiche saranno implementate usando alberi razionali. Purtroppo, le persone sono abbastanza felici con i DCG da soli. Uno dei motivi per cui questo non sta lasciando la ricerca, è, perché molte nozioni che i programmatori Prolog suppongono esistano, non esistono per gli alberi razionali. Prendiamo ad esempio l'ordinamento lessicografico che non ha un'estensione per alberi razionali. Cioè, ci sono alberi razionali che non possono essere confrontati usando un normale termine. (In pratica ciò significa che ottieni risultati quasi casuali). Ciò significa che non puoi produrre una lista ordinata contenente tali termini. Il che significa ancora che molti built-in come bagof/3 non funzionano più in modo affidabile con termini infiniti.

Per la vostra query di esempio, si consideri la seguente definizione:

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. 

Così a volte ci sono modi semplici per sfuggire non terminazione. Ma il più delle volte non ce ne sono.

Answer 2

Non si ottiene un numero infinito di quelli, naturalmente, ma quello che è chiamato un ciclico termine razionale o . Tuttavia, non tutti i sistemi Prolog supportano i termini ciclici. I sistemi che forniscono supporto per termini razionali includono CxProlog, ECLiPSe, SICStus, SWI-Prolog e YAP. Ma sappi che ci sono delle differenze tra loro per quanto riguarda i calcoli che puoi eseguire con termini razionali.

Un'interrogazione come:

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

richiede sostegno coinduzione. Hai una implementazione portabile di coinduzione in Logtalk, che puoi usare con tutti i sistemi sopra menzionati. La coinduzione richiede che il sistema Prolog possa creare termini razionali (utilizzando una query come X = [1|X]), che unifichi i termini razionali e che possa stampare i binding con termini razionali in un modo non ambiguo.

Per un esempio su enumerazione (o test) gli elementi di una lista razionale, vedi:

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

Due query di esempio per questo esempio:

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

Se siete interessati in termini razionali e di coinduzione, l'esempio di Logtalk coinduction include diversi esempi individuali e riferimenti bibliografici.