时间戳

首页 > 解决方案 > Prolog中的统一算法

prolog - Prolog中的统一算法

问题描述

我正在尝试在 Prolog 中对统一算法进行编程，以验证两个表达式是否可以通过返回布尔值 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([],[]).```

标签： prolog

解决方案

这是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].

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

  • 找出您的教授是否希望您实施发生检查，如果是，请实施。

推荐阅读