与STO检测统一

Question

在ISO Prolog中,仅针对NSTO(不受发生检查)的情况定义统一.背后的想法是涵盖那些主要用于程序并且实际上得到所有Prolog系统支持的统一案例.更具体地说,ISO/IEC 13211-1:1995读取:

7.3.3发生检查(STO)但不受
发生检查(NSTO)

如果存在通过
Herbrand算法的步骤以便
发生7.3.2g 的方式,则一组方程(或两个项)是"经历发生 - 检查"(STO).

如果没有办法继续
Herbrand算法的步骤使得7.3.2g发生,则一组方程(或两个项)"不受发生检查"(NSTO)
.

...

此步骤7.3.2 g读取:

克)如果存在形式的公式X =吨这样
即X是一个变量,吨是非可变术语
包含该变量,然后用失败(退出不
unifiable,正发生检查).

完整的算法被称为Herbrand算法,并且通常被称为Martelli-Montanari统一算法 - 其基本上通过以非确定性方式重写方程组来进行.

请注意,引入了新的方程式:

d)如果存在形式为f(a ₁,a ₂,... a _N)=
f(b ₁,b ₂,... b _N)的等式,则将其替换为等式集
a _i = b _我.

这意味着具有相同算符但具有不同arity的两个复合词将永远不会对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错误案例.事情开始变得困难......

Answer 1

第三次尝试.这主要是前一个答案中的错误修正(已经有很多修改). 编辑: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.

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,如果它没有成功,那么它继续构建两个更通用的术语,遍历每个术语的结构.

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

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

[*]以compund方式进行的arity测试是贪婪地完成的,因为term_general1/4OP声明只使用在此链接的第1部分中定义的内置谓词而不包括length/2..(编辑:在调用term_general1之前 添加了两个functor/3调用functor和 arity的调用,以便在他们的arity不匹配时不尝试检查内部术语)

例如:

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

编辑06/02/2015:

上面的解决方案对查询失败:

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), _))
   ).