unify_with_occurs_check/2 and cyclic terms
Roberto Bagnara
How should the standard built-in unify_with_occurs_check/2 behave
when presented with cyclic terms?
I do not believe that the ISO standard can be invoked here since,
as far as I understand, the standard says that if you create cyclic
terms you are on your own. Nonetheless I believe that we should
strive for compatibility even beyond what is mandated by the
standard.
Here is my limited experience. On the query
?- X = [a|X], unify_with_occurs_check(X, X).
SICStus 3.8.5beta1 fails, while SWI-Prolog 3.4.0 and Yap 4.3.0 succeed,
However, on the query
?- X = [a|X], unify_with_occurs_check(X, Y).
SICStus 3.8.5beta1 still fails, while SWI-Prolog 3.4.0 and Yap 4.3.0 loop.
SICStus has a consistent behavior: as clearly written in the documentation
unify_with_occurs_check/2 succeeds if its arguments unify to a *non-cyclic*
term; otherwise it fails.
However, failure of unify_with_occurs_check(X, X) looks strange,
so to speak: one would expect any object to unify with itself.
I have always (erroneously?) believed that performing the occurs-check
amounts to have the unification fail as soon as a variable X has to
be unified with a (possibly cyclic) non-variable term containing X.
With this interpretation, the queries above should both succeed.
But no system seems to share this view.
The behavior of SWI-Prolog 3.4.0 and Yap 4.3.0 seems somewhat inconsistent.
So the question is: how should unify_with_occurs_check/2 behave?
Since wearing the lawyer's hat may not work in this case,
try wearing the hat of the language designer.
Note: the above tests could not be performed on BProlog 4.0 because
it seems to miss unify_with_occurs_check/2.
On the other hand, in Ciao-Prolog 1.6 and GNU Prolog 1.2.1
the creation of cyclic terms seems not possible: they both
loop on `?- X = f(X).', while, on
`?- f(X, X) = f(f(X, X), f(X, X)).' Ciao-Prolog 1.6 loops
and GNU Prolog 1.2.1 segfaults.
--
Roberto Bagnara
Department of Mathematics, University of Parma, Italy
http://www.cs.unipr.it/~bagnara/
mailto:bag...@cs.unipr.it
Jamie Andrews
Roberto Bagnara <bag...@cs.unipr.it> wrote:
>How should the standard built-in unify_with_occurs_check/2 behave
>when presented with cyclic terms?
OK, here's one semantics-based possibility. A query
succeeds only if there is some substitution of terms for
variables which makes it true. '='/2 is rational tree
equivalence, and it should succeed only if there is some
substitution which makes its two arguments equivalent rational
trees. (By extension, normal unification between a predicate
call and a clause head is also based on rational tree
equivalence.) unify_with_occurs_check/2 is finite tree
equivalence, and should succeed only if there is some
substitution which makes its two arguments identical finite
trees.
Therefore when we say "X = [a|X]", we should get success
because there is a rational tree which can be substituted for X
which makes the query true. However, when we say
"X = [a|X], unify_with_occurs_check(X, X)", we should get
failure because unify_with_occurs_check/2 requires finite trees,
but there is no finite tree which satisfies "X = [a|X]".
Similarly with "X = [a|X], unify_with_occurs_check(X, Y)".
Evidently this is not considered to be a real option in
practice, except in Prolog III ad seq. Perhaps the feeling is
that if you're going to address occurs-check inefficiency in a
semantically consistent way, it's better to do it with that
compile-time analysis to identify which occurs checks are
necessary, rather than implement rational tree unification.
(I can't remember who that analysis is due to... Peter van Roy?)
>I do not believe that the ISO standard can be invoked here since,
>as far as I understand, the standard says that if you create cyclic
>terms you are on your own. Nonetheless I believe that we should
>strive for compatibility even beyond what is mandated by the
>standard.
Yes, AFAIR, most implementations (except Sicstus?) don't
really do rational tree unification; they just ignore the occurs
check, which can lead to infinite loops in unification or
printout, even though we have long known (thanks to Colmerauer)
how to do rational tree unification without divergence. I don't
know if the standard says anything about this, but since the
standard was based at least somewhat on the implementations, I
doubt that it does.
>?- X = [a|X], unify_with_occurs_check(X, X).
>?- X = [a|X], unify_with_occurs_check(X, Y).
>
>I have always (erroneously?) believed that performing the occurs-check
>amounts to have the unification fail as soon as a variable X has to
>be unified with a (possibly cyclic) non-variable term containing X.
>With this interpretation, the queries above should both succeed.
>But no system seems to share this view.
Both queries should fail under the interpretation I gave above.
--Jamie.
andrews .uwo } Merge these two lines to obtain my e-mail address.
@csd .ca } (Unsolicited "bulk" e-mail costs everyone.)
Pascal Bouvier
>
> How should the standard built-in unify_with_occurs_check/2 behave
> when presented with cyclic terms?
Since the spirit of unify_with_occurs_check/2 in standard is to avoid
cyclic terms at this particular step, it must fail.
Please note that unify_with_occurs_check/2 is of no special use
in prolog handling cyclic terms (rational trees), since the unification
algorithm will not loop infinitely, and since some predicate used
to check the finiteness of trees is generally provided (or should be).
In these systems, unify_with_occurs_check/2 is only present for
compatibility with other prolog systems.
On prolog systems that does not handle rational trees, I don't
have any opinion about the behaviour of unify_with_occurs_check/2 in
this case.
> However, failure of unify_with_occurs_check(X, X) looks strange,
> so to speak: one would expect any object to unify with itself.
>
> I have always (erroneously?) believed that performing the occurs-check
> amounts to have the unification fail as soon as a variable X has to
> be unified with a (possibly cyclic) non-variable term containing X.
> With this interpretation, the queries above should both succeed.
> But no system seems to share this view.
Your definition of occur-check is true.
I think that people of the standard used 'occur-check' to express
everything with some rapport with cyclic terms.
> The behavior of SWI-Prolog 3.4.0 and Yap 4.3.0 seems somewhat inconsistent.
Yes, maybe they implement this?
unify_with_occurs_check(X, X).
> So the question is: how should unify_with_occurs_check/2 behave?
> Since wearing the lawyer's hat may not work in this case,
> try wearing the hat of the language designer.
If the unification of both arguments succeeds
then if it is an infinite tree,
then fail.
else success
else fail.
In Prolog IV, it is implemented like this (roughly):
unify_with_occurs_check(X, X) :- check_finite(X).
and I never use it ;-)
--
Pascal
Ulrich Neumerkel
Roberto Bagnara <bag...@cs.unipr.it> writes:
>
>How should the standard built-in unify_with_occurs_check/2 behave
>when presented with cyclic terms?
It should terminate in any case.
>?- X = [a|X], unify_with_occurs_check(X, X).
>
>SICStus 3.8.5beta1 fails, while SWI-Prolog 3.4.0 and Yap 4.3.0 succeed,
>However, on the query
>
>?- X = [a|X], unify_with_occurs_check(X, Y).
>
>SICStus 3.8.5beta1 still fails, while SWI-Prolog 3.4.0 and Yap 4.3.0 loop.
>
>SICStus has a consistent behavior: as clearly written in the documentation
>unify_with_occurs_check/2 succeeds if its arguments unify to a *non-cyclic*
>term; otherwise it fails.
>However, failure of unify_with_occurs_check(X, X) looks strange,
>so to speak: one would expect any object to unify with itself.
>
>I have always (erroneously?) believed that performing the occurs-check
>amounts to have the unification fail as soon as a variable X has to
>be unified with a (possibly cyclic) non-variable term containing X.
>With this interpretation, the queries above should both succeed.
>But no system seems to share this view.
Your idea is slightly more efficient than SICStus' approach
whose runtime is always linear in the term size.
In my experience, unify_with_occurs_check/2 is not very handy to use.
Instead, I prefer terms:acyclic/1 explicitely. This permits to
avoid many otherwise necessary occur checks.
--
Ulrich Neumerkel http://www.complang.tuwien.ac.at/ulrich/
Fernando Pereira
> I have always (erroneously?) believed that performing the occurs-check
> amounts to have the unification fail as soon as a variable X has to
> be unified with a (possibly cyclic) non-variable term containing X.
containing X. Therefore, when unify_with_occurs_check attempts to bind
X to X, it is attempting to unify a variable with a non-variable term
containing the variable, which as you say should fail.
-- F