/*********************************************************/ /* UNIFICATION ALGORITHM */ /* */ /* Taken from Sterling & Shapiro, with minor changes, */ /* pages 151-152. */ /* */ /* Example uses are: */ /* ?- unif(f(a), X). */ /* ?- unif(f(a, g(X)), f(Y, Z)) */ /* Compare the result of these with the in-built Prolog */ /* unification, i.e.: */ /* ?- f(a)=X. */ /* ?- f(a, g(X)) = f(Y, Z) */ /* In particular, to see the effect of the occurs check, */ /* compare the following: */ /* ?- unif(f(X), X). */ /* ?- f(X)=X. */ /*********************************************************/ unif(X, Y) :- var(X), var(Y), X=Y. unif(X, Y) :- var(X), nonvar(Y), not_occurs_in(X, Y), X=Y. unif(X, Y) :- var(Y), nonvar(X), not_occurs_in(Y, X), Y=X. unif(X, Y) :- nonvar(X), nonvar(Y), constant(X), constant(Y), X=Y. unif(X, Y) :- nonvar(X), nonvar(Y), compound(X), compound(Y), term_unif(X, Y). not_occurs_in(X, Y) :- var(Y), X \== Y. not_occurs_in(X, Y) :- nonvar(Y), constant(Y). not_occurs_in(X, Y) :- nonvar(Y), compound(Y), functor(Y, F, N), not_occurs_in(N, X, Y). not_occurs_in(N, X, Y) :- N > 0, arg(N, Y, Arg), not_occurs_in(X, Arg), N1 is N - 1, not_occurs_in(N1, X, Y). not_occurs_in(0, X, Y). term_unif(X, Y) :- functor(X, F, N), functor(Y, F, N), unif_args(N, X, Y). unif_args(N, X, Y) :- N > 0, unif_arg(N, X, Y), N1 is N - 1, unif_args(N1, X, Y). unif_args(0, X, Y). unif_arg(N, X, Y) :- arg(N, X, ArgX), arg(N, Y, ArgY), unif(ArgX, ArgY). constant(X) :- integer(X). constant(X) :- atom(X). compound(X) :- not atomic(X).