Процедурная семантика swi-пролога: непонимание результирующей замены

Question

Я не могу понять поведение swi-пролога, когда база данных

включена (a, b).

запрашивается с

: - включено (A, B), включено (C, D).

Насколько я понимаю, что должно произойти, так это следующее: во-первых, самая левая цель в запросе сопоставляется с базой данных. Это сразу же происходит успешно, что приводит к удалению указанной цели из запроса, а также к замене

[A = a, B = b]

Далее замена применяется к оставшейся цели, которая ничего не делает, так как ни A, ни B не появляются во второй цели. Теперь оставшаяся цель сопоставляется с базой данных, что снова успешно. Теперь мы закончили, и мы должны остаться с заменой

[A = a, B = b, C = a, D = b]

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

[A = C, B = D, C = a, D = b]

Если вы очень щедры, Вы могли бы сказать, что «оба ответа означают одно и то же», но я никогда не щедро отношусь к пониманию того, что делает программа, и я столкнулся с этим в контексте, где это действительно имеет значение. Поэтому я был бы очень признателен, если бы кто-то мог помочь мне выяснить, что происходит.

Answer 1

Что-то близкое к желаемому выходу, но с использованием обычного представления пары Пролог:

bindings(Query, Bindings) :-
    term_variables(Query, Variables),
    copy_term(Query, Copy),
    term_variables(Copy, VariablesCopy),
    call(Copy),
    pairs_keys_values(Bindings, Variables, VariablesCopy).

Пример вызова:

?- bindings((on(A,B),on(C,D)), Bindings).
Bindings = [A-a, B-b, C-a, D-b].

Единственный нестандартный предикат - pairs_keys_values/3, но это доступно в нескольких библиотеках. Выше я использовал library(pairs) от SWI-Prolog. Logtalk (который можно запустить с большинством систем Prolog) предоставляет библиотечный объект pairs с предикатом keys_values/3 с той же семантикой и порядком аргументов.

Answer 2

Но две замены являются одинаковыми.

Мы можем узнать вещь только по ее взаимодействию; для любой допустимая реализация substitute( Term, Substitution, Substituted_term ) не наблюдается никакой разницы ни с одной из двух отображаемых вами форм.

Таким образом, это чисто вопрос репрезентации. Любое представление может быть выбрано до тех пор, пока наблюдаемые результаты остаются прежними.

Answer 3

Обратите внимание, что результат даже действителен для:

on(a,b).
on2(a,b).

?- on(A,B),on2(C,D).
A = C, C = a,
B = D, D = b.

В любом случае было бы лучше написать Пролог

A = C = a,
B = D = b.

Вот схема из ранее адаптированной мной. Я понятия не имею, реализованы ли такие вещи, может быть, указатели NULL используются, когда переменная "fre sh"? Это не важно.