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 = tsuch

thatXis a variable andtis a non-variable term

which contains this variable, then exit with failure (not,

unifiablepositive 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(athen replace it by the set of equations_{1},a_{2}, ...a_{N}) =

f(b_{1},b_{2}, ...b_{N})

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, otherwiseif

`unify_sto(X,Y)`

succeeds then also`X = Y`

succeedsif

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