algorithm - 与 STO 检测统一

Question

在 ISO Prolog 中，统一仅针对 NSTO（不受发生检查）的情况定义。背后的想法是涵盖那些主要用于程序中并且实际上被所有 Prolog 系统支持的统一案例。更具体地说，ISO/IEC 13211-1:1995 内容如下：

7.3.3 受发生检查（STO）和不受
发生检查（NSTO）

一组方程（或两个项）是“服从发生
检查”（STO），如果存在通过
Herbrand 算法的步骤进行的方法，使得 7.3.2 g
发生。

一组方程（或两项）是“不受
发生检查”（NSTO）的，如果没有办法继续执行
Herbrand 算法的步骤，从而
发生 7.3.2 g。

...

此步骤 7.3.2 g 内容如下：

g) 如果存在X = t形式的方程，其中
X是一个变量，t是一个包含该变量的非变量项
，则以失败退出（不可
统一，正发生检查）。

完整的算法称为 Herbrand 算法，也就是通常所说的Martelli-Montanari 统一算法——它本质上是通过以非确定性方式重写方程组来进行的。

请注意，新方程的引入如下：

d) 如果存在f(a ₁ ,a ₂ , ...a _N ) =
f(b ₁ ,b ₂ , ...b _N )形式的方程，则将其替换为方程组
a _i =我。_{_}

这意味着具有相同函子但不同元数的两个复合术语永远不会对 STO 产生影响。

这种不确定性是 STO 测试难以实施的原因。毕竟，仅测试是否需要发生检查是不够的，但要证明对于执行算法的所有可能方式，这种情况永远不会发生。

这里有一个案例来说明情况：

?- A/B+C*D = 1/2+3*4.

统一可以从 开始A = 1，也可以从任何其他对开始，并以任何顺序继续。为确保 NSTO 属性，必须确保没有可能产生 STO 情况的路径。考虑一个对于当前实现来说没有问题的案例，但这仍然是 STO：

?- 1+A = 2+s(A).

Prolog 系统首先将这个方程重写为：

?- 1 = 2, A = s(A).

现在，他们选择

• 1 = 2这使得算法失败退出，或者

• A = s(A)其中步骤 g 适用并且检测到 STO-ness。

我的问题是双重的。首先，它是关于 ISO Prolog 中的一个实现unify_sto(X,Y)（仅使用第 1 部分定义的内置函数），它适用于以下内容：

• 如果统一是 STO，则unify_sto(X,Y)产生错误，否则

• 如果unify_sto(X,Y)成功则也X = Y成功

• 如果unify_sto(X,Y)失败则也X = Y失败

我的第二个问题是关于在这种情况下发出的具体错误。请参阅 ISO 的错误类别。

---

这是一个简单的开始步骤：所有成功案例都包含在unify_with_occurs_check(X,Y). 剩下要做的是区分 NSTO 故障和 STO 错误情况。那是事情开始变得困难......

Answer 1

第三次尝试。这主要是先前答案中的错误修复（已经有很多修改）。 编辑：2015 年 6 月 4 日

在创建更通用的术语时，如果它们中的任何一个是变量，我都会将两个子术语保持原样。现在，在这种情况下，我通过调用term_general/2.

unify_sto(X,Y):-
  unify_with_occurs_check(X,Y) -> true ;
  (
   term_general(X, Y, unify(X,Y), XG, YG),
   \+unify_with_occurs_check(XG,YG),
   throw(error(type_error(acyclic, unify(X,Y)),_))
  ).

term_general(X, Y, UnifyTerm, XG, YG):-
  (var(X) -> (XG=X, term_general(Y, YG)) ;
  (var(Y) -> (YG=Y, term_general(X, XG)) ;
  ((
    functor(X, Functor, Len),
    functor(Y, Functor, Len),
    X=..[_|XL],
    Y=..[_|YL],
    term_general1(XL, YL, UnifyTerm, NXL, NYL)
  ) ->
  (
    XG=..[Functor|NXL],
    YG=..[Functor|NYL]
  ) ;
  ( XG=_, YG=_ )
  ))).

term_general1([X|XTail], [Y|YTail], UnifyTerm, [XG|XGTail], [YG|YGTail]):-
  term_general(X, Y, UnifyTerm, XG, YG),
  (
    \+(unify_with_occurs_check(XG,YG)) ->
        throw(error(type_error(acyclic,UnifyTerm),_)) ;
        term_general1(XTail, YTail, UnifyTerm, XGTail, YGTail)
  ).
term_general1([], [], _, [], []).

term_general(X, XG):-
  (var(X) -> XG=X ;
  (atomic(X) -> XG=_ ;
  (
     X=..[_|XL],
     term_general1(XL, XG)
  ))).

term_general1([X|XTail], [XG|XGTail]):-
  term_general(X, XG),
  term_general1(XTail, XGTail).
term_general1([], _).

到目前为止，这个问题中提到的单元测试在这里：

unit_tests:-
  member([TermA,TermB], [[_A+_B,_C+_D], [_E+_F, 1+2],
                         [a(_G+1),a(1+_H)], [a(1), b(_I)],
                         [A+A,a(B)+b(B)], [A+A,a(B,1)+b(B)]]),
  (unify_sto(TermA, TermB)->Unifies=unifies ; Unifies=does_not_unify),
  writeln(test(TermA, TermB, Unifies)),
  fail.
unit_tests:-
     member([TermA,TermB], [[A+A,B+a(B)], [A+A,A+b(A)],
                            [A+A,a(_)+b(A)], [1+A,2+s(A)],
                            [a(1)+X,b(1)+s(X)]]),
  catch(
   (
     (unify_sto(TermA, TermB)->true;true),
     writeln(test_failed(TermA, TermB))
   ), E, writeln(test_ok(E))),
   fail.
unit_tests.

Answer 2

这是另一个尝试：

unify_sto(X,Y):-
  unify_with_occurs_check(X,Y) -> true ;
  (
    term_general(X, Y, XG, YG),
    \+(unify_sto1(XG,YG)),
    throw(error(type_error(acyclic,unify(X,Y)),_))
  ).

unify_sto1(X, Y):-
   unify_with_occurs_check(X,Y).
unify_sto1(X, Y):-
   X\=Y.

term_general(X, Y, XG, YG):-
  ((var(X) ; var(Y)) ->  (XG=X, YG=Y) ;
  ((
    functor(X, Functor, Len),
    functor(Y, Functor, Len),
    X=..[_|XL],
    Y=..[_|YL],
    term_general1(XL, YL, NXL, NYL)
  ) ->
  (
    XG=..[Functor|NXL],
    YG=..[Functor|NYL]
  ) ;
  ( XG=_, YG=_ )
  )).

term_general1([X|XTail], [Y|YTail], [XG|XGTail], [YG|YGTail]):-
  term_general(X, Y, XG, YG),
  term_general1(XTail, YTail, XGTail, YGTail).
term_general1([], [], [], []).

它首先尝试 unify_with_occurs_check，如果不成功，则继续构建两个更通用的术语，遍历每个术语的结构。

• 如果任一术语是变量，则将这两个术语保持原样。
• 如果这两个术语是同一个原子，或者它们都是具有相同函子和元数 [*] 的复合术语，它会遍历其参数，为它们创建一个更通用的术语。
• 否则，它会为每个术语分配一个新的变量。

然后它再次尝试 unify_with_occurs_check 更通用的术语来测试非循环统一并相应地抛出错误。

[*]在复合术语中对 arity 的测试是贪婪地完成的，因为 OP 声明只使用在此链接term_general1/4的第 1 部分中定义的内置谓词与不包含的内置谓词将失败递归。length/2. （已编辑：在调用 term_general1 之前 添加了两个functor/3测试函子和参数的调用，以便在它们的参数不匹配时不尝试检查内部术语）

例如：

?- unify_sto(s(1)+A,A+s(B)).
A = s(1),
B = 1
?- unify_sto(1+A,2+s(A)).
ERROR: Type error: `acyclic' expected, found `unify(1+_G5322,2+s(_G5322))'
?- unify_sto(a(1)+X,b(1)+s(X)).
ERROR: Type error: `acyclic' expected, found `unify(a(1)+_G7068,b(1)+s(_G7068))'

编辑 2015 年 6 月 2 日：

上述解决方案对查询失败：

unify_sto(A+A,a(A)+b(A)).

是否不会产生统一错误。

这里对处理每个子项成对并在发现错误时立即产生错误的算法进行了改进：

unify_sto(X,Y):-
  unify_with_occurs_check(X,Y) -> true ;
  (
   term_general(X, Y, unify(X,Y), XG, YG),
   \+unify_with_occurs_check(XG,YG),
   throw(error(type_error(acyclic,unify(X,Y)),_))
  ).

unify_sto1(X, Y):-
   unify_with_occurs_check(X,Y).
unify_sto1(X, Y):-
   X\=Y.

term_general(X, Y, UnifyTerm, XG, YG):-
  ((var(X) ; var(Y)) ->  (XG=X, YG=Y) ;
  ((
    functor(X, Functor, Len),
    functor(Y, Functor, Len),
    X=..[Functor|XL],
    Y=..[Functor|YL],
    term_general1(XL, YL, UnifyTerm, NXL, NYL)
  ) ->
  (
    XG=..[Functor|NXL],
    YG=..[Functor|NYL]
  ) ;
  ( XG=_, YG=_ )
  )).

term_general1([X|XTail], [Y|YTail], UnifyTerm, [XG|XGTail], [YG|YGTail]):-
  term_general(X, Y, UnifyTerm, XG, YG),
  \+(unify_with_occurs_check(XG,YG))-> throw(error(type_error(acyclic,UnifyTerm),_)) ;
  term_general1(XTail, YTail, UnifyTerm, XGTail, YGTail).
term_general1([], [], _, [], []).

在原始答案中产生错误结果的查询的测试用例：

   ?-  unify_sto(A+A,a(A)+b(A)).
    ERROR: Type error: `acyclic' expected, found `unify(_G6902+_G6902,a(_G6902)+b(_G6902))'
   ?- unify_sto(A+A, a(_)+b(A)).
    ERROR: Type error: `acyclic' expected, found `unify(_G5167+_G5167,a(_G5173)+b(_G5167))'

Answer 3

这是我的尝试：

unify_sto(X,Y):-
  unify_with_occurs_check(X,Y) -> true ;
  (
    term_general(X, XG),
    term_general(Y, YG),
    \+(unify_sto1(XG,YG)),
    throw(error(type_error(acyclic,unify(X,Y)),_))
  ).

unify_sto1(X, Y):-
   unify_with_occurs_check(X,Y).
unify_sto1(X, Y):-
   X\=Y.

term_general(X, Y):-
  (var(X) ->  Y=X ;
  (atomic(X) -> Y=_ ;
  (
    X=..[Functor|L],
    term_general1(L, NL),
    Y=..[Functor|NL]
  ))).

term_general1([X|XTail], [Y|YTail]):-
  term_general(X, Y),
  term_general1(XTail, YTail).
term_general1([], []).

它首先尝试unify_with_occurs_check，如果不成功，则继续为每个参数构建一个更通用的术语，然后尝试统一这样的术语并测试它是否是循环的。如果它是循环的type_error，则抛出非循环的。

例如：

?- unify_sto(1+A,2+s(A)).
ERROR: Unhandled exception: error(type_error(acyclic,unify(1+_G3620,2+s(_G3620))))

Answer 4

这是我用来测试@gusbro 版本的版本。这个想法是从字面上使用 Martelli-Montanari。通过重写方程列表[X1=Y1,X2=Y2|Etc]，某些重写规则会立即应用 - 使用！为承诺。对于某些规则，我不太确定，所以我让它们像原始算法一样不确定。

rewrite_sto/1将失败或产生错误的备注。我们对成功案例不感兴趣，无需任何搜索即可处理。另外，请注意，可以消除导致（立即）失败的方程式！这有点不直观，但我们在这里只对查找 STO 案例感兴趣。

unify_with_sto_check(X,Y) :-
   (  \+ unify_with_occurs_check(X, Y)
   -> rewrite_sto([X=Y])  % fails or error
   ;  X = Y
   ).

rewrite_sto(Xs0) :-
   select(X=Y, Xs0,Xs),
   (  X == Y
   ;  nonvar(X), nonvar(Y),
      functor(X,F,A),
      \+ functor(Y,F,A)
   ;  var(X), var(Y),
      X = Y
   ),
   !,
   rewrite_sto(Xs).
rewrite_sto(Xs0) :-
   select(X=Y, Xs0, Xs1),
   nonvar(X), nonvar(Y),
   functor(X,F,A),
   functor(Y,F,A),
   !,
   X =.. [_|XArgs],
   Y =.. [_|YArgs],
   maplist(\Xi^Yi^(Xi=Yi)^true, XArgs, YArgs, XYs),
   append(XYs,Xs1,Xs),
   rewrite_sto(Xs).
rewrite_sto(Xs0) :-
   select(X=Y, Xs0,Xs),
   (  var(X), nonvar(Y) -> unify_var_term(X, Y)
   ;  nonvar(X), var(Y) -> unify_var_term(Y, X)
   ;  throw(impossible)
   ),
   rewrite_sto(Xs).

unify_var_term(V, Term) :-
   (  unify_with_occurs_check(V, Term) -> true
   ;  throw(error(type_error(acyclic_term, Term), _))
   ).

Answer 5

在 SWI 序言中：

unify_sto(X,Y) :-
  \+ unify_with_occurs_check(X,Y),
  X = Y,
  !,
  writeln('Error: NSTO failure'),
  fail.

unify_sto(X,Y) :-
  X = Y.

给出以下结果：

[debug]  ?- unify_sto(X,s(X)).
Error: NSTO failure
false.

[debug]  ?- unify_sto(X,a).
X = a.

[debug]  ?- unify_sto(b,a).
false.