Neither variant1/2 nor variant2/2 implements the test for the syntactic variant. But for various reasons.
The target variant1(f(X,Y),f(Y,X)) should succeed, but failed. In some cases, when the same variable appears on both sides, variant1/2 does not work as expected. To fix this, use:
variant1a(X, Y) :- copy_term(Y, YC), subsumes_term(X, YC), subsumes_term(YC, X).
The variant2(f('$VAR'(0),_),f(_,'$VAR'(0))) should fail, but succeed. Clearly, variant2/2 assumes that its arguments do not have '$VAR'/1 .
ISO / IEC 13211-1: 1995 defines options as follows:
7.1.6.1 Variants of expression
Two terms are options if there exists a bijection s variables of the first to the variables of the latter such that the last term is obtained from replacing each variable X with the previous one - 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 option 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 a bijection, which is a special case of substitution.
Here, all examples relate to typical customs in bagof/3 and setof/3 , where the variables always do not intersect, but the more subtle case is when there are common variables.
In logical programming, the usual definition is rather:
V is a variant of T if there exist σ and θ such that
V σ and T identicalT θ and V identical
In other words, they are options if both match each other. However, the concept of matching is quite alien to Prolog programmers, i.e. The concept of correspondence used in formal logic. Here is a case that allows many Prolog programmers to panic:
Consider f(X) and f(g(X)) . Does f(g(X)) f(X) match or not? Many Prolog programmers now shrug and mumble about incident checking. But this is not completely related to checking for availability. They match, yes, because
f(X) { X ↦ g(X) } is identical to f(g(X)) .
Note that this permutation replaces all X and replaces them with g(X) . How can this happen? In fact, this cannot happen with the representation of the typical term Prolog as a graphic in memory. In Prolog, node X represents a real address somehow in memory, and you cannot perform such an operation at all. But in logic, everything is on a completely textual level. It's just like
sed 's/\<X\>/g(X)/g'
except that variables can be replaced at the same time. Think of { X ↦ Y, Y ↦ X} . They must be replaced immediately, otherwise f(X,Y) will be reduced to f(X,X) or f(Y,Y) .
Thus, this definition, formally perfect, is based on concepts that do not have a direct correspondence in Prolog systems.
Similar problems arise when one-sided unification is considered, which does not correspond, but the general case is between unification and comparison.
According to ISO / IEC 13211-1: 1995 Cor.2: 2012 ( draft ):
8.2.4 subsumes_term / 2
This built-in predicate provides syntax checking for one-way unification.
8.2.4.1 Description
subsumes_term(General, Specific) true if & theta; such that
a) General ? and Specific ? identical and
b) Specific ? and Specific identical.
Procedurally, subsumes_term(General, Specific) simply successful or unsuccessful. No side effect or association.
For your definition, variant1/2 , subsumes_term(f(X,Y),f(Y,X)) no longer works.