prolog - Prolog中的合一算法

Question

我正在尝试在 Prolog 中编写合一算法以验证两个表达式是否可以通过返回 bool 值 True/False 来合一:

编辑。我发现这个实现很有用:来自:http://kti.mff.cuni.cz/~bartak/prolog/data_struct.html

unify(A,B):-
   atomic(A),atomic(B),A=B.
unify(A,B):-
   var(A),A=B.            % without occurs check
unify(A,B):-
   nonvar(A),var(B),A=B.  % without occurs check
unify(A,B):-
   compound(A),compound(B),
   A=..[F|ArgsA],B=..[F|ArgsB],
   unify_args(ArgsA,ArgsB).
   
unify_args([A|TA],[B|TB]):-
   unify(A,B),
   unify_args(TA,TB).
unify_args([],[]).```

Answer 1

这是在 https://en.wikipedia.org/wiki/Unification_(computer_science)#A_unification_algorithm 中描述的类似 Martelli 和 Montanari 统一算法的部分实现。 .每个部分的注释引用算法中相应的重写规则。请注意，不需要明确的冲突规则，如果没有其他规则适用，我们可以直接失败。

% assuming a universe with function symbols g/2, p/2, q/2

% identical terms unify (delete rule)
unify(X, Y) :-
    X == Y,
    !.

% a variable unifies with anything (eliminate rule)
unify(X, Y) :-
    var(X),
    !,
    X = Y.

% an equation Term = Variable can be solved as Variable = Term (swap rule)
unify(X, Y) :-
    var(Y),
    !,
    unify(Y, X).

% given equal function symbols, unify the arguments (decompose rule)
unify(g(A, B), g(X, Y)) :-
    unify(A, X),
    unify(B, Y).
unify(p(A, B), p(X, Y)) :-
    unify(A, X),
    unify(B, Y).
unify(q(A, B), q(X, Y)) :-
    unify(A, X),
    unify(B, Y).

例子:

?- unify(q(Y,g(a,b)), p(g(X,X),Y)).
false.

?- unify(q(Y,g(a,b)), q(g(X,X),Y)).
false.

?- unify(q(Y,g(a,a)), q(g(X,X),Y)).
Y = g(a, a),
X = a.

你还有一两件事要做:

• 概括分解规则以处理任意项。您可能会发现 =.. 运算符很有用。例如:

    ?- Term = r(a, b, c), Term =.. FunctorAndArgs, [Functor | Args] = FunctorAndArgs.
    Term = r(a, b, c),
    FunctorAndArgs = [r, a, b, c],
    Functor = r,
    Args = [a, b, c].
  

  您将需要检查两个项是否具有相同的仿函数和相同数量的参数，以及所有对应的参数对是否统一。

• 了解您的教授是否希望您实现发生检查，如果是，请实现。