Matching patterns without unification in Prolog

Question

I need to match one pattern with several different terms in Prolog, but I don't want to unify any of the variables when matching them. I found one possible way to do this, but it seems inefficient:

:- initialization(main).
:- set_prolog_flag('double_quotes','chars').

main :-
    Pattern = (A>B;B<A),
    match_without_unify(Pattern,(1>A1;A1<1)),
    match_without_unify(Pattern,(2>4;4<2)).

match_without_unify(A,B) :-
    %copy the terms, unify them, and count the number of variables
    copy_term([A,B],[A1,B1]),
    term_variables(B1,L1),
    length(L1,L),
    A1=B1,
    term_variables(B1,L2),
    length(L2,L),
    writeln([L1,L2]).

Is it possible to solve this problem without calling term_variables/2 and length/2 twice?

Answer 1

What you need here is called syntactic one-sided unification. This is provided via the ISO-builtin subsumes_term(General, Specific) which

... is true iff there is a substitution θ such that

a) Generalθ and Specificθ are identical, and
b) Specificθ and Specific are identical

Note that the notion of matching is usually only defined with Specific being ground. In such a context it suffices to demand that

Generalθ and Specific are identical

There are various ways how this kind of matching may be extended, but most of the time the fine print is neglected as in the case when the condition of Specific being ground is simply discarded. This leads to quite unexpected behaviour since General = X, Specific = s(X) now "match", with θ = {X → s(X)}.

In (old) systems that do not provide subsumes_term/2, it can be easily implemented like so:

subsumes_term(General, Specific) :-
   \+ General \= Specific, % optimization, which sometimes makes it slower ...
   \+ \+ (  term_variables(Specific, Vs1),
            General = Specific,
            term_variables(Specific, Vs2),
            Vs1 == Vs2
         ).

A faster implementation may avoid full unification and the creation of the variable lists. This implementation requires rational tree unification. Replace \= and = using unify_with_occurs_check/2 in an ISO-implementation that does not support rational trees.