Term Subsumption -- library(subsumes)

Term subsumption is a sort of one-way unification. Recall that terms S and T unify if they have a common instance, and that unification in Prolog instantiates both terms to that common instance. S subsumes T if T is already an instance of S. For our purposes, T is an instance of S if there is a substitution that leaves T unchanged and makes S identical to T.

Two terms are alphabetic variants if they are identical except for variable names, and all common variables appear in corresponding positions. For example,

     
     f(X,Y,X)  and  f(X,Z,X) are alphabetic variants;
     f(X,Y,X)  and  f(Y,X,Y) are not;
     f(X,Y,X)  and  f(X,Y,Y) are not;
     f(X,Y,X)  and  f(Z,V,Z) are
     

This file used to define subsumes_chk/2, but this is now a built-in predicate:


subsumes_chk(+General, +Specific)
is true when General subsumes Specific; that is, when Specific is already an instance of General. It does not bind any variables in General or in Specific.

There are currently two predicates in this file:


subsumes(?General, +Specific)
is true when General subsumes Specific, and instantiates General so that it becomes identical to Specific. It does not further instantiate Specific.
variant(?Term1, ?Term2)
is true when Term1 and Term2 are alphabetic variants. That is, variant(Term1, Term2) holds precisely when subsumes_chk(Term1, Term2) and subsumes_chk(Term2, Term1) both hold.