algorithm - 与 STO 检测的统一

Question

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

7.3.3 Subject to occurs-check (STO) and not subject
to occurs-check (NSTO)

A set of equations (or two terms) is "subject to occurs-
check" (STO) iff there exists a way to proceed through
the steps of the Herbrand Algorithm such that 7.3.2 g
happens.

A set of equations (or two terms) is "not subject to
occurs-check" (NSTO) iff there exists no way to proceed
through the steps of the Herbrand Algorithm such that
7.3.2 g happens.

...

这一步 7.3.2 g 内容如下:

g) If there is an equation of the form X = t such
that X is a variable and t is a non-variable term
which contains this variable, then exit with failure (not
unifiable, positive occurs-check).

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

请注意，引入了新方程式:

d) If there is an equation of the form f(a₁,a₂, ...a_N) =
f(b₁,b₂, ...b_N) then replace it by the set of equations
a_i = b_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 性。

我的问题是双重的。首先，它是关于 unify_sto(X,Y)(仅使用第 1 部分的 defined built-ins)在 ISO Prolog 中的实现，以下内容适用:

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

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

• 如果 unify_sto(X,Y) 失败，那么 X = Y 也会失败

我的第二个问题是关于在这种情况下要发出的具体错误。参见 ISO 的 error classes .

---

这是一个简单的开始步骤:所有成功案例都包含在 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.