Did you know ... Search Documentation:
Predicate subsumes_term/2
Availability:built-in
[ISO]subsumes_term(@Generic, @Specific)
True if Generic can be made equivalent to Specific by only binding variables in Generic. The current implementation performs the unification and ensures that the variable set of Specific is not changed by the unification. On success, the bindings are undone.72This predicate is often named subsumes_chk/2 in older Prolog dialects. The current name was established in the ISO WG17 meeting in Edinburgh (2010). The chk postfix was considered to refer to determinism as in e.g., memberchk/2. This predicate respects constraints.

See section 5.6 for defining clauses whose head is unified using single sided unification.

Tags are associated to your profile if you are logged in
Tags:
LogicalCaptain said (2021-05-17T23:26:13):0 upvotes 0 0 downvotes
Picture of user LogicalCaptain.

Some examples:

?- subsumes_term(f(_,_),f(1,2)).       % f(_,_) is definitely more generic than f(1,2)
true.

?- subsumes_term(f(2,_),f(1,2)).       % do not even unify
false.

?- subsumes_term(f(A,A),f(1,2)).       % do not even unify
false.

?- subsumes_term(f(1,B),f(A,2)).       % would unify, but Generic is not "more generic" (nor is Specific "more generic")
false.

?- subsumes_term(f(A,A),f(A,2)).       % unify but Generic is too constrained to give Specific by binding A
false.

?- subsumes_term(f(C,C),f(A,2)).       % same as above
false.

?- subsumes_term(f(A,A),f(A,A)).       % same on both sides
true.

?- subsumes_term(f(A,B),f(A,A)).       % would unify and Generic is more generic
true.

?- subsumes_term(f(A,B),f(a,g(b))).    % somewhat more complex
true.

?- subsumes_term(f(A,g(B)),f(a,g(b))).
true.

?- subsumes_term(f(A,g(b)),f(a,g(B))).
false.

?- subsumes_term(f(A,B),f(a,g(B))).    % unification would yield a cyclic structure
false.

?- subsumes_term(f(A,C),f(a,g(B))).
true.

?- subsumes_term(f(A,g(C)),f(a,g(B))).
true.

?- subsumes_term(f(A,g(B)),f(a,g(B))).
true.

?- subsumes_term(f(B,g(B)),f(a,g(B))).
false.

?- subsumes_term(f(B,g(B)),f(a,g(a))).
true.