Как стандарт ISO Prolog требует сохранения идентификатора переменной при преобразовании из условия в термин?

Question

Я что-то упускаю при чтении ISO / IEC 13211-1, подпункты 7.6.3 и 7.6.4:

7.6.3 Преобразование главы предложения в термин

Голова H с предикатным индикатором P/N может быть преобразован в термин T:

а) если N тогда ноль T это атом P,

б) если N ненулевой тогда T является переименованной копией (7.1.6.2) TT где TT это сложный термин, основной функтор которого P/N и аргументы H а также TT идентичны

7.6.4 Преобразование тела предложения в термин

Цель G который является предикатом с предикатным индикатором P/N может быть преобразован в термин T:

а) если N тогда ноль T это атом P,

б) если N ненулевой тогда T является переименованной копией (7.1.6.2) TT где TT это сложный термин, основной функтор которого P/N и аргументы G а также TT идентичны

в) если G контрольная конструкция, которая появляется в таблице 9, то T это термин с соответствующим главным функтором. Если главный функтор T является call/1 или же catch/3 или же throw/1 тогда аргументы G а также T идентичны, иначе, если главный функтор T является (',')/2 или же (;)/2 или же (->)/2 тогда каждый аргумент G также должны быть преобразованы в термин.

Предположим, у нас есть открытый (7.5.3) (например, динамический) пользовательский предикат a/1, определяется следующим единственным предложением:

a(X) :- b(X).

Очевидно, цель

?- clause(a(A), b(B)), A == B.

должен преуспеть. Цитирую часть определения clause/2 (8.8.1.1):

a) Выполняет последовательный поиск по каждой общедоступной пользовательской процедуре в базе данных и создает список L всех условий clause(H, B) такой, что

1) база данных содержит пункт, глава которого может быть преобразована в термин H (7.6.3), и чье тело может быть преобразовано в термин B (7.6.4) и

2) H объединяется с Head, а также

3) B объединяется с Body,

Преобразование заголовка вышеупомянутого пункта в термин, 7.6.3 b) применяется, и мы создаем переименованную копию a(A) из a(X), Точно так же применяется преобразование тела пункта, 7.6.4 b), и мы создаем переименованную копию b(B) из b(X),

Проблема в том, что a(A) а также b(B) отдельные переименованные копии. Как это требуется, что A а также B одинаковые переменные, как и следовало ожидать?

Тот же вопрос можно задать для оговорки

p :- q(X), r(X).

Когда мы преобразовываем основную часть этого условия в термин, применяется пункт 7.6.4 c), и основным функтором термина должен быть (',')/2 с двумя аргументами, являющимися целями q(X) а также r(X) преобразованы в условия. Но это предсказания, и применяется 7.6.4 b), поэтому снова два результирующих термина являются отдельно переименованными копиями.

Что мне не хватает?