CODEWITHSUNDEEP
prologunification
Computer
Computer

Reputation: 21

Does it matter what is unification terms sequence?

Lets consider I have two terms T1 and T2. I unified two terms and got result.

My question is: If I change places of terms and unify terms T2 and T1 - whether result will be the same or different?

I tried to change terms and got the same result. But in theory I can read: in Prolog sequence is important.

So how do you think - is the result the same or different and why?

Upvotes: 2

Views: 142

Answers (1)

false
false

Reputation: 10102

A difference that shows simply by replacing X = Y by Y = X is highly unlikely.

As long as you consider syntactic unification (using the occurs-check) or rational tree unification, the only differences might be some minimal performance differences.

More visible differences are surfacing when going beyond these well defined relations:

  • when mixing both, unification may not terminate. I can only give you somewhat related examples in SWI and Scryer:

?- X = s(X), unify_with_occurs_check(X, s(X)).
   X = s(X).
?- unify_with_occurs_check(X, s(X)), X = s(X).
   false.

Above, commutativity of goals is broken. But then, we are mixing two incompatible theories with one another. So, we can't really complain.

?- Y = s(Y), unify_with_occurs_check(X-X,s(X)-Y).
   false.
?- Y = s(Y), unify_with_occurs_check(X-X,Y-s(X)).
   Y = s(Y), X = s(Y)    % Scryer
|  Y = X, X = s(X).      % SWI

And here we just exchange the order of arguments. It is general intuition that exchanging (consistently) arguments of a functor should not produce a difference, but helas, here again the incompatible mix is the culprit.

  • when constraints and side-effects are involved. Still, I fail to produce such a case just replacing X = Y by Y = X.

Upvotes: 4

Related Questions