Unification with STO detection

Question

In ISO Prolog unification is defined only for those cases that are NSTO (not subject to occurs-check). The idea behind is to cover those cases of unifications that are mostly used in programs and that are actually supported by all Prolog systems. More specifically, ISO/IEC 13211-1:1995 reads:

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.

...

This step 7.3.2 g reads:

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

The complete algorithm is called Herbrand Algorithm and is what is commonly known as the Martelli-Montanari unification algorithm - which essentially proceeds by rewriting sets of equations in a non-deterministic manner.

Note that new equations are introduced with:

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.

Which means that two compound terms with the same functor but different arity will never contribute to STO-ness.

This non-determinism is what makes the STO-test so difficult to implement. After all, it is not sufficient to test whether or not an occurs-check might be necessary, but to prove that for all possible ways to execute the algorithm this case will never happen.

Here is a case to illustrate the situation:

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

Unification might start by A = 1, but also any of the other pairs, and continue in any order. To ensure the NSTO property, it must be ensured that there is no path that might produce a STO situation. Consider a case that is unproblematic for current implementations, but that is still STO:

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

Prolog systems start by rewriting this equation into:

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

Now, they pick either

• 1 = 2 which makes the algorithm exit with failure, or

• A = s(A) where step g applies and STO-ness is detected.

My question is twofold. First it is about an implementation in ISO Prolog of unify_sto(X,Y) (using only the defined built-ins of Part 1) for which the following holds:

• if the unification is STO, then unify_sto(X,Y) produces an error, otherwise

• if unify_sto(X,Y) succeeds then also X = Y succeeds

• if unify_sto(X,Y) fails then also X = Y fails

and my second question is about the specific error to issue in this situation. See ISO's error classes.

---

Here is a simple step to start with: All success cases are covered by the success of unify_with_occurs_check(X,Y). What remains to do is the distinction between NSTO failure and STO error cases. That's were things start to become difficult...

Answer 1

Third attempt. This is mainly a bugfix in a previous answer (which already had many modifications). Edit: 06/04/2015

When creating a more general term I was leaving both subterms as-is if either of them was a variable. Now I build a more general term for the "other" subterm in this case, by calling 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([], _).

And here the unit tests so far mentioned in this question:

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

Here is my version which I used to test against @gusbro's versions. The idea is to use Martelli-Montanari rather literally. By rewriting a list of equations [X1=Y1,X2=Y2|Etc], certain rewrite rules are applied immediately - using the ! for commitment. And for certain rules I was not that sure so I left them as non-determinate as the original algorithm.

Remark that rewrite_sto/1 will either fail or produce an error. We are not interested in the success case, which is handled without any search. Also, remark that an equation that leads to (immediate) failure, can be eliminated! That's a bit unintuitive, but we are only interested here to find STO cases.

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 3

In 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.

gives the following results:

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

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

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

Answer 4

Here goes another attempt:

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([], [], [], []).

It first tries to unify_with_occurs_check, and if it does not succeed then it proceed to build two more general terms, traversing the structure of each term.

• If either term is a variable it leaves both terms them as-is.
• If both terms are the same atom, or if they are both compund terms with the same functor and arity [*], it traverses its arguments making a more general term for them.
• Otherwise it assigns a fresh new variable to each term.

Then it tries again to unify_with_occurs_check the more general terms to test for acyclic unify and throw an error accordingly.

[*] The test for arity in compund terms is done greedily, as term_general1/4 will fail recursion as OP stated to only use builtin predicates defined in part 1 of this link with does not include length/2.. (edited: Added two functor/3 calls to test for functor and arity before calling term_general1, so as to not try inspect inside terms if their arity does not match)

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

Edit 06/02/2015:

The solution above fails for the query:

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

is it does not yield a unify error.

Here goes an improvement over the algorithm that deals with each subterm pairwise and yields the error as soon as it discovers it:

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

Test case for the query which yielded wrong results in the original answer:

   ?-  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 5

Here goes my attempt:

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([], []).

It first tries to unify_with_occurs_check, and if it does not succeed then it proceed to build a more general term for each argument, then it tries to unify such a term and test to see if it is cyclic. If it is cyclic a type_error of the kind acyclic is thrown.

E.g:

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