Is an infinite list of ones sane?

Question

In Prolog, is the unification X = [1|X] a sane way to get an infinite list of ones? SWI-Prolog does not have any problem with it, but GNU Prolog simply hangs.

I know that in most cases I could replace the list with

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

but my question is explicitly if one may use the expression X = [1|X], member(Y, X), Y = 1 in a "sane" Prolog implementation.

Answer 1

In Prolog, is the unification X = [1|X] a sane way to get an infinite list of ones?

It depends on whether or not you consider it sane to produce an infinite list at all. In ISO-Prolog a unification like X = [1|X] is subject to occurs check (STO) and thus is undefined. That is, a standard-conforming program must not execute such a goal. To avoid this from happening, there is unify_with_occurs_check/2, subsumes_term/2. And to guard interfaces against receiving infinite terms, there is acyclic_term/1.

All current implementations terminate for X = [1|X]. Also GNU Prolog terminates:

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

no

But for more complex cases, rational tree unification is needed. Compare this to Haskell where repeat 1 == repeat 1 causes ghci to freeze.

As for using rational trees in regular Prolog programs, this is quite interesting in the beginning but does not extend very well. As an example, it was believed for some time in the beginning 1980s that grammars will be implemented using rational trees. Alas, people are happy enough with DCGs alone. One reason why this isn't leaving research, is, because many notions Prolog programmers assume to exist, do not exist for rational trees. Take as an example the lexicographic term ordering which has no extension for rational trees. That is, there are rational trees that cannot be compared using standard term order. (Practically this means that you get quasi random results.) Which means that you cannot produce a sorted list containing such terms. Which again means that many built-ins like bagof/3 no longer work reliably with infinite terms.

For your example query, consider the following 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 sometimes there are simple ways to escape non-termination. But more often than not there are none.