Difference between two variant implementations

Question

Is there any logical difference between these two implementations of a variant predicate?

variant1(X,Y) :-
 subsumes_term(X,Y),
 subsumes_term(Y,X).

variant2(X_,Y_) :-
  copy_term(X_,X),
  copy_term(Y_,Y),
  numbervars(X, 0, N),
  numbervars(Y, 0, N),
  X == Y.

Answer 1

Neither variant1/2 nor variant2/2 implement a test for being a syntactic variant. But for different reasons.

The goal variant1(f(X,Y),f(Y,X)) should succeed but fails. For some cases where the same variable appears on both sides, variant1/2 does not behave as expected. To fix this, use:

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

The goal variant2(f('$VAR'(0),_),f(_,'$VAR'(0))) should fail but succeeds. Clearly, variant2/2 assumes that no '$VAR'/1 occur in its arguments.

---

ISO/IEC 13211-1:1995 defines variants as follows:

7.1.6.1 Variants of a term

Two terms are variants if there is a bijection s of the
variables of the former to the variables of the latter such
that the latter term results from replacing each variable X
in the former by Xs.

NOTES

1 For example, f(A, B, A) is a variant of f(X, Y, X),
g(A, B) is a variant of g(_, _), and P+Q is a variant of
P+Q.

2 The concept of a variant is required when defining bagof/3
(8.10.2) and setof/3 (8.10.3).

Note that the Xs above is not a variable name but rather (X)s. So s is here a bijection, which is a special case of a substitution.

Here, all examples refer to typical usages in bagof/3 and setof/3 where variables happen to be always disjoint, but the more subtle case is when there are common variables.

In logic programming, the usual definition is rather:

V is a variant of T iff there exists σ and θ such that

• Vσ and T are identical
• Tθ and V are identical

In other words, they are variants if both match each other. However, the notion of matching is pretty alien to Prolog programmers, that is, the notion of matching as used in formal logic. Here is a case which lets many Prolog programmers panic:

Consider f(X) and f(g(X)). Does f(g(X)) match f(X) or not? Many Prolog programmers will now shrug their shoulders and mumble something about the occurs-check. But this is entirely unrelated to the occurs-check. They match, yes, because

f(X){ X ↦ g(X) } is identical to f(g(X)).

Note that this substitution replaces all X and substitutes them for g(X). How can this happen? In fact, it cannot happen with Prolog's typical term representation as a graph in memory. In Prolog the node X is a real address somehow in memory, and you cannot do such an operation at all. But in logic things are on an entirely textual level. It's just like

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

except that one can also replace variables simultaneously. Think of { X ↦ Y, Y ↦ X}. They have to be replaced at once, otherwise f(X,Y) would shrink into f(X,X) or f(Y,Y).

So this definition, while formally perfect, relies on notions that have no direct correspondence in Prolog systems.

Similar problems happen when one-sided unification is considered which is not matching, but the common case between unification and matching.

According to ISO/IEC 13211-1:1995 Cor.2:2012 (draft):

8.2.4 subsumes_term/2

This built-in predicate provides a test for syntactic one-sided unification.

8.2.4.1 Description

subsumes_term(General, Specific) is true iff there is a substitution θ such that

a) Generalθ and Specificθ are identical, and
b) Specificθ and Specific are identical.

Procedurally, subsumes_term(General, Specific) simply succeeds or fails accordingly. There is no side effect or unification.

For your definition of variant1/2, subsumes_term(f(X,Y),f(Y,X)) already fails.