Prolog 中不统一的匹配模式

Question

我需要在 Prolog 中匹配一个模式和几个不同的术语，但我不想在匹配它们时统一任何变量。我找到了一种可能的方法来做到这一点，但它似乎效率低下：

:- 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]).

不调用term_variables/2和length/2两次就可以解决这个问题吗？

Answer 1

这里需要的是句法单面统一。这是通过 ISO-builtin 提供的 subsumes_term(General, Specific) 哪个

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

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

请注意，匹配的概念通常仅以 Specific 为基础来定义。在这种情况下，要求

就足够了

Generalθ and Specific are identical

有多种方法可以扩展这种匹配，但大多数情况下会忽略细则，例如 Specific 被研磨的条件被简单地丢弃。这会导致非常意外的行为，因为 General = X, Specific = s(X) 现在 "match"，其中 θ = {X → s(X)}。

在不提供subsumes_term/2的（旧）系统中，可以像这样轻松实现：

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

更快的实现可能会避免完全统一和创建变量列表。此实现需要有理树统一。在不支持有理树的 ISO 实现中使用 unify_with_occurs_check/2 替换 \= 和 =。

Answer 2

你的问题得到了肯定的回答：

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

在实用程序中找到了 fastfail 解决方案。 @false 的解决方案的缺点是
它调用 General = Specific，这可能会不必要地执行完全统一
在模式匹配失败的情况下也是如此。

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).

在理查德·奥基夫斯之后松散：
http://www.picat-lang.org/bprolog/publib/metutl.html

Prolog 中不统一的匹配模式

Matching patterns without unification in Prolog

prolog

pattern-matching

iso-prolog