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
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(a1,a2, ...aN) =
f(b1,b2, ...bN) then replace it by the set of equations
ai = bi.
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 = 2which 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
unify_sto(X,Y)succeeds then also
X = Ysucceeds
unify_sto(X,Y)fails then also
X = Yfails
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...