Declarative meaning of `more generic than`?

General
1

With a hope to decrease the number of occurrences of my uses of the cut like “a(…):-!, …”
I started a late learning on recent SSU (=>) features. As an initial step, I check the
subsumes_term/2, though I am not sure on relationship between them.

My question is on subsumes_term/2.

?- subsumes_term(X, g(X)).
false.

which confused me. I thought X is more generic than g(X), i.e, X subsumes g(X) in my naive understanding, though I think I understand the procedural explanation in the
doc (?-help(subsumes_term), which is clear. What am I missing on generic relation between terms ?

2

The test for subsumes_term/2 includes “can the two terms be unified?” – unifying X and g(X) results in a circular term, so it’s neither more general or less general.
On the other hand:

?- subsumes_term(X, f(a)).
true.

?- subsumes_term(X, f(_)).
true.
3

Thanks for the comment.

If I remember correctly, a term t is more generic than t’ if the set [[t’]] of ground instances of t’ is the subset [[t]] for t. Perhaps the definition assumes that t and t’ have no variable in common, for which my example is not appropriate. I will check later about this on the net.

edit
If t and t’ above has no variable in common, the the subsume_term/2 is correct
in the sense ‘t is more generic than t’ ', I guess.

4

I could not find definition of "t is more generic than t’ " on the net
in the sense of ground instances, which might be only in my bad
memeory.

However, still I think the following 1 and 2 are equivalent
for terms t and t’ with no variable in common.

1 The set of ground instances of t’ is a subset of that of t.

2 Initial equivalence relation, say R’, on V(t’) does not change
at all during unification process on t and t’,
where V(t’)/R’ = { {x} | x in V(t’)}.

IMO, ground instances of t and t’ should be defined independent
to each other, for example, the ground instances of f(X) is a subset of
the ground instances of X.

To make the unification performed in subsumes_term(t, t’)
return correct answers for that declarative semantics using ground
instances, the unification shoud be taken on t and a variant of t’,
a fresh copy of t’. Then subsume_term(X, f(X)) would return
the right answer “true”.

5

As is, the comment says (pl-prims.c):

subsumes is defined as

subsumes(General, Specific) :-
	term_variables(Specific, SVars),
	General = Specific,
	term_variables(SVars, SVars).

In simple terms, this says that unifying the two may not cause Specific to become more specific. Note that term_variables(SVars, SVars). fails if a variable is bound, including bindings to some other variable in Svars.

6

I thought the subsumes/2 should be related to logically meaningful property, for example,
like this.

That p(X) susumes p(f(X)) shoud be equivalent
to that forall X p(X) → forall X p(f(X)) is valid.

As the query

?- subsumes(p(X), p(f(X))).

fails, the subsumes/2 is something different from what I expected.

However, to be honest, the meaning of subsumes/2 is not clear for me
for now, but as the four simple lines of subsumes codes looks fresh and impressive,
I would like to take time to learn and digest it in my way.

Thanks.

edit.
Now I see what the subsumes does, which seems almost what I expected,
except that renaming Specific could be necessary so that the subsume/2 has logical
parallel property of implication. Also I think the subsumes/2 should be used
as a subsumption checker on clause-based first-order theorem prover.

7

You can bootstrap subsumes_term/2 via numbervars/3:

subsumes_term2(X, Y) :- \+ \+ (numbervars(Y, 0, _), X = Y).

Here are some test cases:

subsumes_term subsumes_term2
(a, a) true true
(f(A,B), f(Z,Z)) true true
(f(Z,Z), f(_,_)) false false
(g(X), g(f(X))) false false
(X, Y), (Y, f(X)) true true

But I guess subsumes_term/2 exists because the numbervars/3
solution might not work with attributed variables.

8

Sounds a reasonable explanation because, I guess, unification with an attributed variables might cause unexpected another unification which could affect result and not be undone.

However, your subsumes_term2 still says that, for example, “g(X) is NOT more specific than X”, which might not be your point.

IMO, the notion subsumes should be ‘variant’ independent: if t subsumes t’ then t subsumes any variant of t’.

For example, as subsumes_term2(A, g(B)) is true and g(A) is a variant of g(B), subsumes_term2(A, g(A)) should return true.

The above variant independent requirement on the notion subsumes fits
more on the first-order logic, I think. Also general-specific relation could be defined in more declarative and rigorous way using ground instances without using the procedural unification.

EDIT
The subsumes/3 below borrows your idea on subsumes_term2/2.

subsumes_term3(X, Y)
is true if and only if the set GY of ground instances of Y is a subset of GX for X,
in other words, X is more generic than Y.

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

% ?- subsumes_term3(X, f(X)).
%@ true.
% ?- subsumes_term3(X, f(_)).
%@ true.
% ?- subsumes_term3(f(X), X).
%@ false.
11

AFAIK, subsumes_term/2 is in one of the ISO revisions. All I could find is ISO work in progress (it was later renamed to subsumes_term/2), that says

8.2Term unification
8.2.4subsumes/2
8.2.4.1
Description
subsumes(General, Specific) is true iff there is a substitution, including the
empty substitution, θ such that the term General is instantiated to Generalθ =
Specific. This predicate provides a one-way unification.

The examples do not deal with sharing variables between the two arguments.

Yes. Whether it would lead to faster code is unsure. We are talking about head unification that is performed using VM instructions. It we want to fail early we have three options, none of which is necessarily better than what we have now. We can

  • Set the available trail space to 0, such that an attempt to bind some variable raises a trail overflow and then handle that carefully. That might be the simplest.
  • Add some VM state to prevent the switch to unification “write” mode.
  • Create dedicated instructions. That avoids the problems associated with state (which also applies to faking a full trail stack), but introduces quite a few new unification instructions that duplicate a lot of work (though they are a bit simpler). Making the VM larger results in more cache misses and thus slows things down.

All three are a bit messy and the resulting speedup is unclear, so for now I didn’t implement these.

14

ISO seems not care about sharing variables between arguments General and Specfic, and according the ISO definition, susumes(X, f(X)) would succeed with a substitution Specific f(X) with General X.

IMO, ISO seems define the general-specific relation in terms
of the set of ground instances in their mind, and ISO is wise
in doing with substitution instead of going into defining ground instaces, which depends on the domain (Herbrand, rational, etc).

16

To make it the case that X subsumes f(X), based on what I read
the ISO doc, I would like to propose the following predicates borrowing codes posted in this thread. Of course, this is tentative, and I do not intend at all to suggest any change on the current SSU (=>) implementation, which is completely black box for me for now,
but wanted only to know what the generic-specific relation in non-procedural meaning.

% ?- unify_generic(X, f(X)).
%@ X = f(_).

unify_generic(X, Y):- subsumes_term(X, Y, Z),
	X = Z.

% ?- subsumes_chk(X, f(X)).
%@ true.
subsumes_chk(X, Y):- subsumes_term(X, Y, _).

% ?- subsumes_term(X, f(X), Z).
subsumes_term(X, Y, Z):-
	term_variables(Y, Vs),
	copy_term(Vs, Y, Ws, Z),
	 \+ \+ (numbervars(Ws, 0, _), X = Z).
17

But the solution X = f(_) is wrong, because applying this
substitution θ to X doesn’t give f(X), it only gives f(_).

18

Yes, unify_generic(Generic, Specific) tries to find a substitution s
such that output s(Generic) is a variant of the given Specific.

unify_generic may be redundant and not necessary, because the answer Generic
must be the Specific when it succeeds. It is only to show to view
how variables in Generic is instantiated to be made equal to the Specific.

19

You cannot implement fibonacci anymore:

fib(0, R) => R=1.
fib(1, R) => R=1.
fib(N, R) => 
   M is N-1, fib(M, A), L is M-1, fib(L, B), R is A+B.

?- fib(10, X).
X = 89.

Now with unify_generic/2 it becomes, doesn’t work anymore:

fib2(P,Q) :- unify_generic((0,R), (P,Q)), !, R = 1.
fib2(P,Q) :- unify_generic((1,R), (P,Q)), !, R = 1.
fib2(P,Q) :- unify_generic((N,R), (P,Q)), !, 
   M is N-1, fib2(M, A), L is M-1, fib2(L, B), R is A+B.

unify_generic(X, Y) :- copy_term(Y, Z), subsumes(X, Z).

?- fib2(10, X).
ERROR: Arguments are not sufficiently instantiated

On the other hand it works with subsumes/2, does the same as (=>)/2:

fib3(P,Q) :- subsumes((0,R), (P,Q)), !, R = 1.
fib3(P,Q) :- subsumes((1,R), (P,Q)), !, R = 1.
fib3(P,Q) :- subsumes((N,R), (P,Q)), !, 
   M is N-1, fib3(M, A), L is M-1, fib3(L, B), R is A+B.

?- fib3(10, X).
X = 89.
20

How about this ?

% ?- fib3(10, X).
%@ X = 89.

fib3(P,Q) :- unify_with_subsumes_chk((0,R), (P,Q)), !, R = 1.
fib3(P,Q) :- unify_with_subsumes_chk((1,R), (P,Q)), !, R = 1.
fib3(P,Q) :- unify_with_subsumes_chk((N,R), (P,Q)), !,
   M is N-1, fib3(M, A), L is M-1, fib3(L, B), R is A+B.

unify_with_subsumes_chk(X, Y):- subsumes_term(X, Y, _), !, X=Y.

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

Anyway, unify_generic/2 seems useless, at most. I’m not sure
about subsumes_term/3 at this moment.

21

(Nothing of importance)

22

In this thread, efficiency is not my interest, but my question was why that query fails． Of course I could imagine that such case should never happen practically.

% ?- subsumes_term(X, p(X)).
%@ false.

The ISO doc on subsumes/2 quoted by Jan W. solved my question as I posted in this thread. Then I “invented” what returns true instead for that query, which is more close to the ISO requirement, I thought.

% ?- subsumes_term(X, p(X), R).
%@ R = p(_).

The essential part of subsumes_term/3 is borrowed from Jan B. codes, and efficiency was out of my interest.

23

(Nothing of importance)

24

In cases like SSU and most practical cases, the two arguments do not share, so there is no problem. I guess that in logical terms, this should be a sound definition of variant/2, right?

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

If that is the case, there is indeed a problem because variant/2 has an accepted semantics if the arguments share subterms (including variables). AFAIK, most Prolog systems implement variant/2 ignoring the issue with sharing, but they acknowledge this is wrong. Note that the semantically correct implementation of variant/2 is, AFAIK.

variant(A,B) :-
    \+ \+ variant_(A,B).

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

My answer without contexts is YES. I have not yet read in necessary details.
But it sounds like a new lemma for me that I missed.

I think my subsumes_term/3 can not be
used for SSU, for example, subsumes_term(X, f(X), _) only checks that
X is more generic than f(X), but should not unify with X with f(X) as everyone see.

However similar predicate might be used as subsumption checker in clausal FOL provers,
and I would like to use it for that. I hope it would not be ULTRA slow.