Declarative meaning of `more generic than`?

General
29

[quote=“jan, post:24, topic:6888”]
If that is the case, there is indeed a problem because variant/2 has an accepted semantics if the arguments share subterms (including variables).
[/quotel]

I am not sure the following query is what you think problem, but I ran some queries:

% ?- A = f(B), C=f(D), subsumes_chk(g(f(A), f(C)), g(f(C), f(A))).
%@ A = f(B),
%@ C = f(D).
% ?- A = f(B), C=f(D), subsumes_chk(g(f(C), f(A)), g(f(A), f(C))).
%@ A = f(B),
%@ C = f(D).
% ?- A = f(B), C=f(D), variant(g(f(A), f(C)), g(f(C), f(A))).
%@ A = f(B),
%@ C = f(D).
% ?- A = f(B), C=f(D), subsumes_term(g(f(A), f(C)), g(f(C), f(A))).
%@ false.

subsumes_chk(X, Y):-
	term_variables(Y, Vs),
	copy_term(Vs, Y, Ws, Z),
	 \+ \+ (numbervars(Ws, 0, _), X = Z).

IMO, the subsumes_term/2 should succeed for the query.
However I am not familiar with the subsumes_term enough to
see why and how this might be serious.

EDIT
Still it is not clear what Jan W. is worrying about . As far as I see,
there is no practical case in which Generic and Specific share a subterm with variables
I am missing something.

30

This definition runs almost as fast as the builtin variant/2, which was written in C.
It is surprising but a good news for me, who was involved to writing the variant.c
and forgot almost completely the codes.

% ?- test1(1000, 10000).
%@ % 29,999 inferences, 0.611 CPU in 0.978 seconds (62% CPU, 49136 Lips)
%@ true.
% ?- test2(1000, 10000).
%@ % 79,999 inferences, 0.759 CPU in 0.760 seconds (100% CPU, 105332 Lips)
%@ true.
% ?- test3(1000, 10000).
%@ % 90,000 inferences, 0.744 CPU in 0.745 seconds (100% CPU, 120932 Lips)
%@ true.
% ?- test4(1000, 10000).
%@ % 90,000 inferences, 0.754 CPU in 0.755 seconds (100% CPU, 119333 Lips)
%@ true.

test1(N, K) :- length(L, N), length(R, N),
			time(repeat(K, variant(L, R))).

test2(N, K) :- length(L, N), length(R, N),
			time(repeat(K, jvariant(L, R))).

test3(N, K) :- length(L, N), length(R, N),
			   last(L, a),
			time(repeat(K, jvariant(L, R))).

test4(N, K) :- length(L, N), length(R, N),
			   last(L, a),
				time(repeat(K, jvariant(L, R))).

jvariant(A,B) :- % by Jan W.
    \+ \+ variant_(A,B).

variant_(A,B) :-
    copy_term(A,C),
    numbervars(B, 0, _),
    numbervars(C, 0, _),
    B == C.
31

For the case it is a variant, yes. In case one can early detect it is not a variant, your version is much faster. That is to be expected. Your C implementation does one rather complicated pass if I recall correctly. The Prolog alternative runs 4 passes, but each is much simpler and pretty well optimized. Failure in the Prolog version only happens in the last pass though, so a failing variant call still takes at least about 3/4 of the time of a passing one.

32

An example might say more than 1000 words. Take for example, this pair:

X+Y       and             Y+Z

are they variants of each other? Yes or no? The two terms share the term Y.

Now make this definition:

variant2(A, B) :- 
    subsumes_term(A ,B), 
    subsumes_term(B, A).

Now observe for SWI-Prolog:

/* SWI-Prolog 9.1.16 */
?- variant2(X+Y, Y+Z).
false.

?- variant(X+Y, Y+Z).
true.

Which one is the “correct” answer?

33

If you are only up to implementing variant2/2 you could
implement it as follows, a little sketch:

variant2(A, B) :-
    unifiable(A, B, L), is_variable_bijection(L).

Mostlikely implementable in as many passes as an ordinary unification
needs, only watching that the unification generates a variable bijection.

This also explains why variant2/2 fails for the pair X+Y and Y+Z.
Since we get the following result:

?- unifiable(X+Y, Y+Z, L).
L = [Z=X, Y=X].

And L is not a bijection. It maps both Z and Y to X.

34

I imagined subsumes_term/2 is used only as substitute of the standard head unification
where Generic and Specific do not share variables in nature. I vaguely remember such uses for unfolding goal as partial evaluation. But I have little knowledge of partial evaluation in prolog. As far as I see, as you illustrated, it could be dangerous to apply for pairs with shared variables

35

Interesting thought. I fear it will fail as it assumes that the elements of L are terms V1=V2, where V1 originates from A and V2 from B. Given subterm sharing and cycles, that is unlikely to be the case. I’m afraid I post the code to validate the current variant/2 implementation using random terms and the simple, slow but reliable alternative as oracle. I leave that as an example to the user :slight_smile:

36

Interesting.

However, unifiable/3 seems to be changed to keep
information so that the variable belong to which side.

% ?- unifiable(f(A, A, B), f(B, A, A), L).
%@ L = [B=A].

If we have L = [A-B, A-A, B-A], then we know L is not a bijection
to judge that f(A, A, B) and f(B, A, A) is not variant pair.

38

Unifiable performs the unification and then inspects the trail to find the unifications performed by this unification (and unbinds them again). If you inspect the code for unification and see how it deals with variable age, sharing and cycles, you’ll see there are no promises except that each term has the shape Var = Something.

40

Thank @jan W.

I think I understand your comment well, thanks,
though I was afraid my English is correct to tell what I had in mind to tell you.

I am not urgent, but I appreciate if someone will answer my naive question
on subsumes_term/2:

Is there any practical case in which ‘subsumes_term/2’ actually
is applied to shared pair of Generic and Specific like subsumes_term(A+B, B+A) ?
Even in such a case, renaming Specific is enough to avoid possible trouble ?
Short answer would be welcome.

41

I don’t know. I’ve never seen a practical case in my own coding, but that also applied to variant/2 :slight_smile: And yes, copying one of the sides might get the semantics you want. I would copy Generic, as it is likely to be smaller. I don’t know whether anyone in the ISO team considered sharing between the arguments or they had only single sided unification in mind. Neither do I know the current official text. Might be somewhere in Ulrich Neumerkels ISO archives.