Hi,
I’d like to know why this program terminates, with regard to the lack of default occurs check:
X = f(X).
I would have expected this to result in an infinite loop. Are there improvements to naive unification enabled by default to prevent that?
Thanks!
X = f(X) terminates in any Prolog system. What is more interesting is what happens on other operations on the resulting cyclic term (also called infinite tree). Virtually all SWI-Prolog’s built-in predicates either handle such terms properly or raise an exception. So,
?- X = f(X), Y = f(Y), X = Y.
nicely terminates. Not all Prolog systems handle this correctly and either get into an infinite loop or run out of (stack) resources and possibly crash.
Thanks! Could you maybe point me to resources or papers explaining how such cases are handled in SWI?
I’m afraid not. When I needed this stuff Bart Demoen told me how to do it. He claimed (I think back at about 2003) it was widely known but never published. That may of course have changed. The approach for unification is described in pl-prims.c near the start of the file. For most other predicates that operate on two possibly cyclic terms the story is similar. Predicates that act on a single term typically mark which parts have already been visited.