numbervars/3 silently refuses to number vars

[Jean-Luc-Picard-2021]

Some testing:

/* GNU Prolog 1.5.0 */
?- X = f(A,X), numbervars(X, 0, _), write_canonical(A), nl.
_24
cannot display cyclic term for X

/* SWI-Prolog 9.1.16 */
?- X = f(A,X), numbervars(X, 0, _), write_canonical(A), nl.
'$VAR'(0)
X = f(A, X),
A = A.

Bug or feature?

[jp-diegidio]

This is (only, AFAICT) documented in para "8.4.7 acyclic_term/1" of the manual.

In particular, that states:

If acyclic_term(Term) fails, Term contains a cycle and processing Term is not safe, because GNU Prolog does not support the unification of cyclic terms but permits their creation. Cycles can be safely undone by failing over their creation. The use of acyclic_term/1 shall thus be reserved to protect critical predicates against cyclic terms. [my emphasis]

[jp-diegidio]

I have given you a definite answer for this one, so it is rightly completed.

But you are also closing all the ones where you didn't get feedback, especially since you are marking them "completed", while those are issues that should be considered and maybe addressed. This is an open project, indeed the official GNU Prolog project, so anybody can pick it up, code and issues and all, it is never going to die...

[Jean-Luc-Picard-2021]

The error is silent refusal to do something in the sense of:

• The predicate numbervars/3 succeeds
• The predicate numbervars/3 didn't number the variable A

The error is better seen when you do it as follows, if you add this clause:

?- [user].
test(A) :- call(X = f(A,X)), numbervars(X, 0, _).
^D

And then perform this query:

?- test(A), var(A).
yes

I think this is a bug somehow. It doesn't need the concept
of "unification of cyclic terms", which is missing in GNU Prolog,
because A itself is not cyclic, its just an uninstantiated variable.

The numbervars/3 should instantiate it to '$VAR'(0). Or otherwise
fail or throw an error. But not succeed.

[jp-diegidio]

You still have a unification involving a cyclic term, and that "does not support the unification of cyclic terms" more explicitly reads the proverbial "it is not supported and results are undefined", as in anything can happen if you use it. Which to me quite closes it and anything that depends on it: past that point it is a feature request, about unification of cyclic terms.

[Jean-Luc-Picard-2021]

You are talking nonsense, this here from my test case
is not unification of two cyclic terms. Also elsewhere there
is nowhere unification of two cyclic terms in my example:

call(X = f(A,X))

The left hand side X is not a cyclic term and the right hand
side f(A,X) is not cyclic term, it is what GNU Prolog allows, namely
GNU Prolog permits the creation of cycles, you cited it

yourself. Its just (=)/2 without occurs check, allow (=)/2 to
happend, when a variable meets a term. This is how cyclic
terms are created in a Prolog system:

If acyclic_term(Term) fails, Term contains a cycle and
processing Term is not safe, because GNU Prolog does not
support the unification of cyclic terms but permits their creation.
Cycles can be safely undone by failing over their creation.
The use of acyclic_term/1 shall thus be reserved to protect
critical predicates against cyclic terms.

You even emphasized the passage. Next time if you emphasize
something, please also try to understand it. Unification between
cyclic terms is more complex, here is an example:

/* GNU Prolog */
?- X = [1,1|X], Y = [1,1,1|Y].
cannot display cyclic term for X
cannot display cyclic term for Y

?- X = [1,1|X], Y = [1,1,1|Y], X = Y.
%%% hangs

/* SWI-Prolog */
?- X = [1,1|X], Y = [1,1,1|Y], X = Y.
true

The first two (=)/2 are creating of cyclic terms, and the third (=)/2
is unification between two cyclic terms. SWI-Prolog terminates
in the third unification, and succeeds. GNU Prolog allows the first

two unifications, the cycle creation, but goes astray in third
unification the unification between two cyclic terms. My test case
only uses creation of cycles and not cyclic term unification.

[jp-diegidio]

Now try X = [A|X]. or X = [A,X].

= is unification: with just X it "creates" a cyclic term bound to X, with A it is also "unifying" with A. Also every call involves unification. The manual is not that formal and not very explicit, but the result is the same.