Правильный unify_with_occurs_check/2 в SWI-Prolog?

Question

Получил это странное поведение. Я запускал эти тестовые случаи:

      s1 :-
   Q=[[lambda,symbol(_3026),[cons,[quote,_3434],
     [quote,_3514]]],[quote,_3206]],
   P=[_3434|_3514],
   freeze(_3434, (write(foo), nl)),
   unify_with_occurs_check(P, Q).

s2 :-
   Q=[[lambda,symbol(_3026),[cons,[quote,_3434],
     [quote,_3514]]],[quote,_3206]],
   P=[_3434|_3514],
   freeze(_3434, (write(foo), nl)),
   freeze(_3514, (write(bar), nl)),
   unify_with_occurs_check(P, Q).

Теперь я получаю эти результаты, где результат s2неправильно. Результат неверен в двух отношениях: во-первых, он срабатывает, а во-вторых, unify_with_occurs_checkудается:

      SWI-Prolog (threaded, 64 bits, version 8.3.16)

?- s1.
false.

?- s2.
foo
bar
true.

Что _3434не должен срабатывать, следует из 7.3.2 Алгоритм Хербанда в базовом стандарте ISO. Согласно пункту 7.3.2 f) 1) конкретизация переменной X для терма t распространяется только в том случае, если X не встречается в t.

То, что унификация не удалась, следует из пункта 7.3.2 g). Таким образом, кажется, что в SWI-Prolog переменные с атрибутами в различных воплощениях, таких как заморозка/2, диф/2 и т. д., кажется, мешают unify_with_occurs_check.

Любое обходное решение?

Редактировать 06.02.2021:
ошибка была исправлена ​​в SWI-Prolog8.3.17 (разработка) и также
была перенесена в SWI-Prolog8.2.4 (стабильная).

Answer 1

Вот еще один несколько более простой обходной путь:

      unify(X,X) :-
   acyclic_term(X).

Конечно, это работает должным образом только в том случае, если два аргумента конечны с самого начала, но, по крайней мере, в этом случае это не зацикливается.

Answer 2

Одним из выходов может быть создание собственного unify_with_occurs_check/2. Мы можем написать это на самом Прологе, как это делалось в прошлом для систем на Прологе, в которых не было unify_with_occurs_check/2:

РАО'Киф, 15 сентября 1984 г.
http://www.picat-lang.org/bprolog/publib/metutl.html

Вот альтернативный вариант, использующий (=..)/2 и term_variables/2:

      unify(X, Y) :- var(X), var(Y), !, X = Y.
unify(X, Y) :- var(X), !, notin(X, Y), X = Y.
unify(X, Y) :- var(Y), !, notin(Y, X), X = Y.
unify(X, Y) :- functor(X, F, A), functor(Y, G, B),
   F/A = G/B,
   X =.. [_|L],
   Y =.. [_|R],
   maplist(unify, L, R).

notin(X, Y) :-
   term_variables(Y, L),
   maplist(\==(X), L).

Теперь я получаю ожидаемый результат:

      ?- s1.
false.

?- s2.
false.