🚀 go-pugleaf

In article <1992Dec18.175714.3917@cs.sfu.ca> jamie@cs.sfu.ca (Jamie Andrews)
 writes:

   >However, there are still completeness problems, with cases
   >like
   >  x=f(x), y=f(y), x=y
   >where such systems typically loop instead of succeeding, and
   >even cases like
   >  x=f(x,g(x)), y=f(y,h(y)), x=y
   >where such systems may loop where they should fail.

  Yes, and "unification without occur check" is of course a poor way of
dealing with rational trees. Sicstus supports unification of rational
trees, and thus treats the above cases correctly. However, the argument
I criticized might as well have been applied to a proper implementation
of rational trees.