Разница между двумя вариантами реализации

Ни variant1/2, ни variant2/2 не реализуют тест на синтаксический вариант. Но по разным причинам.

Цель variant1(f(X,Y),f(Y,X)) должна быть достигнута, но не удалась. В некоторых случаях, когда одна и та же переменная отображается с обеих сторон, variant1/2 ведет себя не так, как ожидалось. Чтобы исправить это, используйте:

variant1a(X, Y) :-
   copy_term(Y, YC),
   subsumes_term(X, YC),
   subsumes_term(YC, X).

Цель variant2(f('$VAR'(0),_),f(_,'$VAR'(0))) должна быть неудачной, но успешной. Ясно, что variant2/2 предполагает, что в его аргументах нет '$VAR'/1.

ISO/IEC 13211-1:1995 определяет варианты следующим образом:

7.1.6.1 Варианты термина

Два термина являются вариантами, если существует биекция s переменных
первого на переменные второго таким образом,
что последний термин является результатом замены каждой переменной X
в первом на Xs.

ПРИМЕЧАНИЯ

1 Например, f(A, B, A) — это вариант f(X, Y, X),
g(A, B) — это вариант g(_, _), а P+Q — это вариант
P+Q.

2 Концепция варианта требуется при определении bagof/3
(8.10.2) и setof/3 (8.10.3).

Обратите внимание, что Xs выше — это не имя переменной, а скорее (X)s. Таким образом, s здесь является биекцией, которая является частным случаем подстановки.

Здесь все примеры относятся к типичному использованию в bagof/3 и setof/3, где переменные всегда не пересекаются, но более тонкий случай - это когда есть общие переменные.

В логическом программировании обычно используется следующее определение:

V является вариантом T тогда и только тогда, когда существуют σ и θ такие, что

• Vσ и T идентичны
• Tθ и V идентичны

Другими словами, они являются вариантами, если оба соответствуют друг другу. Однако понятие сопоставления довольно чуждо программистам на Прологе, т. е. понятие сопоставления, используемое в формальной логике. Вот случай, который заставляет паниковать многих программистов на Прологе:

Рассмотрим f(X) и f(g(X)). f(g(X)) соответствует f(X) или нет? Многие программисты на Прологе теперь пожмут плечами и пробормотают что-нибудь о проверке возникновения. Но это совершенно не связано с проверкой возникновения. Они совпадают, да, потому что

f(X){ X ↦ g(X) } идентично f(g(X)).

Обратите внимание, что эта замена заменяет все X и заменяет ими g(X). Как это может произойти? На самом деле, этого не может произойти с типичным для Пролога представлением термов в виде графа в памяти. В Прологе узел X является каким-то реальным адресом в памяти, и вы вообще не можете выполнить такую ​​операцию. Но в логике все находится на чисто текстовом уровне. Это как

sed 's/\<X\>/g(X)/g' 

за исключением того, что можно также заменить переменные одновременно. Подумайте о { X ↦ Y, Y ↦ X}. Их нужно заменить сразу, иначе f(X,Y) сожмется в f(X,X) или f(Y,Y).

Таким образом, это определение, формально совершенное, опирается на понятия, которые не имеют прямого соответствия в системах Пролога.

Аналогичные проблемы возникают, когда рассматривается односторонняя унификация, которая не соответствует, а является общим случаем между унификацией и сопоставлением.

Согласно ISO/IEC 13211-1:1995 Cor.2:2012 (черновик):

8.2.4 subsumes_term/2

Этот встроенный предикат обеспечивает тест на синтаксическую одностороннюю унификацию.

8.2.4.1 Описание

subsumes_term(General, Specific) истинно, если существует замена такая, что

а) General и Specific идентичны, и
б) Specific и Specific идентичны.

Процедурно, subsumes_term(General, Specific) просто успешно или неудачно соответственно. Нет никакого побочного эффекта или унификации.

Для вашего определения variant1/2 subsumes_term(f(X,Y),f(Y,X)) уже не работает.