Prolog中的统一算法

Question

我试图在Prolog中对统一算法进行编程，以验证两个表达式是否可以通过返回布尔值True/False来统一：

编辑。我发现这个实现很有用: from：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.

有一两件事留给你去做：

• 将分解规则推广到处理任意项。您可能会发现=..运算符很有用。例如：

?-项= r(a，b，c)，项=.FunctorAndArgs，函子x Args = FunctorAndArgs.r(a，b，c)，FunctorAndArgs = r，a，b，c，函子= r，Args = a，b，c。

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

• 找出您的教授是否希望您实现发生检查，如果是，则执行它。