An example, which is obscure too, but cannot be de-obscured in same way as you have done above, is:
Code: Select all
open core
class predicates
test : (unsigned X).
clauses
test(X) :-
tuple(A, X) = tuple(B, B), % throws errors: Variables "A", "B" are not completely bound
stdIO::write(A, ", ", B).
clauses
run() :-
test(1).
Both
A and
B are free initially, thus it cannot be re-written as:
Code: Select all
open core
class predicates
test : (unsigned X).
clauses
test(X) :-
A = B, % illegal
X = B,
stdIO::write(A, ", ", B).
clauses
run() :-
test(1).
Of course it is easy to see that it can be de-obscured in another way:
Code: Select all
open core
class predicates
test : (unsigned X).
clauses
test(X) :-
X = B,
A = B,
stdIO::write(A, ", ", B).
clauses
run() :-
test(1).
But that other way is obvious only because the example is very small. We could pump the code up by using many variables and algebraic expressions instead of only
A and
B, so that we obtain a complicated example, for which it is by no means easy to figure out, how to de-obscure it.
Hence de-obscuring an obscure unification means, that the programmer is performing a substantial part of the unification-computation in advance. However we have the expectation that the system does all the unification-computation by itself.