统一化与STO检测

Question

统一化与STO检测

algorithmprologunificationiso-prologoccurs-check

38

在ISO Prolog中，一致性仅针对那些不受出现检查限制的情况（NSTO）进行定义。其背后的思想是覆盖程序中大多数使用的一致性情况，并且所有Prolog系统都实际支持这些情况。更具体地，ISO/IEC 13211-1:1995如下所述：

7.3.3 受出现检查（STO）和不受出现检查（NSTO）的主题

如果存在通过Herbrand算法步骤进行处理的方式，则一组方程（或两个术语）是“受到出现检查”（STO）。发生7.3.2 g。

如果不存在通过Herbrand算法步骤进行处理的方式，则一组方程（或两个术语）为“不受出现检查”（NSTO），使7.3.2 g无法发生。

...

此步骤7.3.2 g如下所述：

如果有形如X = t的方程，其中X是一个变量，而t是包含该变量的非变量项，则以失败（不可统一，正出现检查）退出。完整算法称为Herbrand算法，通常被称为Martelli-Montanari统一算法 - 其本质上通过非确定性方式重写一组方程。请注意，新方程式引入方式如下：如果存在等式f(a₁,a₂, ...a_N) = f(b₁,b₂, ...b_N)，则用a_i = b_i替换它。

这意味着具有相同功能符但不同维度的两个复合术语永远不会对STO-ness产生贡献。

这种非确定性是使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错误的情况。这就是事情开始变得困难的地方...

- false

您IP地址为143.198.54.68，由于运营成本限制，当前对于免费用户的使用频率限制为每个IP每72小时10次对话，如需解除限制，请点击左下角设置图标按钮（手机用户先点击左上角菜单按钮）。 - pasaba por aqui

对于像 A = s(A) 这样的情况，A = B 是未定义的，而 unify_with_occurs_check(A, s(A)) 是明确定义的：它会失败。我不清楚你对 unify_sto/2 的定义是什么。有太多未被定义。 - false

5个回答

12

这里又来了一个尝试：

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”进行统一，如果不成功，则继续构建两个更通用的术语，遍历每个术语的结构。

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

然后，它再次尝试使用“unify_with_occurs_check”来测试无环统一并相应地抛出错误。

[*] 复合项中的arity测试是贪婪地进行的，因为OP声明只使用第一部分定义的内置谓词link，其中不包括length/2，所以term_general1/4将递归失败。（编辑：添加了两个functor/3调用来测试functor和arity，然后再调用term_general1，以便在其arity不匹配时不尝试检查术语内部）

E.g:

?- 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))'

- gusbro

我不理解你的反例，能否用一个查询来举例说明？正如我在答案中所述，我的代码隐式地获取元数（我在为什么不使用length/2来获取元数的解释中写的“贪婪”部分）。当term_general1/4对具有不同元数的项失败时，会考虑复合项的元数。 - gusbro

@false：我只是稍微修改了答案，以便在进入一个术语之前使用functor/3来测试函数符号和元数。 - gusbro

反例：unify_sto(A+A,a(A)+b(A)) 明显是 STO，但会默默失败。 - false

现在应该已经修好了。它是 "term_general" 的"基本情况"。我已经删除了最后一个 unify_with_occurs_check/2，当其中一个术语不是复合时，这显然是必需的。 - gusbro

但是，请在新的回答中 :-) - false

显示剩余2条评论

8

好的，我会尽力为您提供帮助。请提供需要翻译的内容。

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”，如果不成功，然后它会为每个参数构建一个更通用的术语，然后尝试统一这样的术语并测试是否具有循环结构。如果存在循环结构，则会抛出acyclic类型错误。type_error。

例如：

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

- gusbro

反例：unify_sto(a(1)+X,b(1)+s(X)). 是STO，但上述定义会默默失败。 - false

s(X) 为尝试。如果您想再试一次，请写另一个答案。 - false

6

这是我用来测试@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), _))
   ).

- false

1

在SWI-prolog中：

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.

- pasaba por aqui

针对给定的示例unify_sto(1+A,2+s(A))，程序执行失败，本应该输出错误。 - false

请查看您正在使用的ISO内置函数，这些是SWI特定的bips。 - false

此外，不使用错误处理会使您的程序难以测试。 - false

网页内容由stack overflow 提供, 点击上面的

可以查看英文原文，
原文链接

- gusbro · Accepted Answer

第三次尝试。这主要是对以前答案中的漏洞进行修复（该答案已经进行了许多修改）。 编辑：06/04/2015

当我创建更通用的术语时，如果其中一个子项是变量，则会将两个子项都保持不变。现在，在这种情况下为“其他”子项构建一个更通用的术语，通过调用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.