Re: When do two Prolog terms marry? (Was: The issue with free speech)

Amazingly simple and falling back again on Richard O'Keefes
subsumes/2. How to implement subsumes/2 directly is
for example found here:
%   File   : METUTL.PL
%   Author : R.A.O'Keefe
%   Updated: 15 September 1984
%   Purpose: meta-logical operations as described in my note
http://www.picat-lang.org/bprolog/publib/metutl.html
subsumes/2 has the advantages that it doesn't need
cyclic term capable unification to be implemented,
since it has no problems in refuting:
?- subsumes(X, f(X)).
fail.
It can be also used to easily bootstrap subsumes_term/2:
subsumes_term(X,Y) :-
    \+ \+ subsumes(X,Y).
Putting the two together we can define:
marry(X, Y) :-
    subsumes_term(X, Y),
    subsumes(Y, X).
Lets see some test cases:
?- marry(f(X,Y,Z,T), f(A,B,C,D)).
X = A, Y = B, Z = C, T = D.
?- marry(f(X,Y,Z,T), f(A,B,Z,D)).
X = A, Y = B, T = D.
?- marry(f(A,Y,Z,T), f(A,B,Z,D)).
Y = B, T = D.
?- marry(f(A,Y,Z,T), f(A,B,C,Z)).
fail.
?- marry(f(X,A,Z,T), f(A,B,Z,D)).
fail.
What can we do with it? I recently made
distinct/1 working based on marry/2:
d(_,_).
d(a,a).
d(_,_).
?- findall(X-Y,d(X,Y),L).
L = [_70340-_70341, a-a, _70346-_70347].
?- findall(X-Y,distinct(d(X,Y)),L).
L = [_71298-_71299, a-a].
Which is pretty cool!
Mild Shock schrieb:

Now I was struggling giving this predicate
a better name. Namely variant_term bootstrapped
as follows:
 variant_term(X, Y) :-
    subsumes_term(X, Y),
    subsumes_term(Y, X).
 Why does it need a better name? Well because it
is not really the variant, as realized by
for example SWI-Prolog's (=@=):
 For example I find:
 ?- variant_term(f(X,Y,Z,T), f(A,B,C,D)).
true.
?- variant_term(f(X,Y,Z,T), f(A,B,Z,D)).
true.
?- variant_term(f(A,Y,Z,T), f(A,B,Z,D)).
true.
?- variant_term(f(A,Y,Z,T), f(A,B,C,Z)).
fail.
?- variant_term(f(X,A,Z,T), f(A,B,Z,D)).
fail.
 The first 3 test cases match what variant/2
usually does. But the last 2 test cases don't
match what variant/2 usually does.
 So how can characterize the behaviour of
this weak variant. I came up with this observation:
 - A weak variant takes has variables that appear
   in the left hand side and in the right hand side,
   i.e. common variables, only obtaining an identity
   relation.
 - Othewise variables that are either specific to
   the right hand side or that are either specific
   to the left hand side, are associated by a
   bijection relation.
 I came up with names like "twin", "sibling" for
this relation. But I got also inspired by the
fact that builtins:variant/2 from Scryer Prolog
 leaves bindings. So looking for a name similar
like "unify", but only its weak variant and it
leaves a binding trace. My idea is to use "marry"!