CODEWITHSUNDEEP
prologpattern-matchingiso-prolog
Anderson Green
Anderson Green

Reputation: 31810

Matching patterns without unification in Prolog

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?

Upvotes: 2

Views: 301

Answers (2)

user502187
user502187

Reputation:

Your question has an affirmative answer:

solve this problem without calling term_variables/2 and length/2 twice?

A fastfail solution is found in an utility. The solution by @false has the drawback that
it calls General = Specific, which might unneccessarely perform a full unification
also in cases where pattern matching fails.

subsumes(X, Y) :-
    term_variables(Y, S),
    subsumes(X, Y, S).

subsumes(X, Y, S) :- var(X), member(V, S), V == X, !,
    X == Y.
subsumes(X, Y, _) :- var(X), !,
    X = Y.          %  binds
subsumes(X, Y, S) :-
    nonvar(Y),          %  mustn't bind it
    functor(X, F, A), functor(Y, G, B),
    F/A = G/B,
    X =.. [_|L],
    Y =.. [_|R],
    subsumes_list(L, R, S).

subsumes_list([], [], _).
subsumes_list([X|L], [Y|R], S) :-
   subsumes(X, Y, S),
   subsumes_list(L, R, S).

Loosly after Richard O'Keefes:
http://www.picat-lang.org/bprolog/publib/metutl.html

Upvotes: 1

false
false

Reputation: 10102

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.

Upvotes: 3

Related Questions