🚀 go-pugleaf

In article <189@qt.cs.utexas.edu>, bradley@cs.utexas.edu (Bradley L.
Richards) writes:
|> According to the proper definition for unification, these terms should
|> not unify.  However, for "efficiency" reasons, most Prolog implementations
|> omit the "occurs" check (i.e. here Y appears in foo(Y)), and blindly
|> unify these terms.  This is, in fact, an error--and one worth fussing
|> at the manufacturer of your Prolog about.  Implementing the occurs
|> check isn't really that costly....

Quoting from the C-Prolog User's manual, edited by Fernando Pereira, 1984:

                The absence of the occur check  is   not   a   bug   or
           design   oversight,   but   a  conscious   design  decision.
           The reason for this decision is that  unification  with  the
           occur  check  is at best linear on the sum of the  sizes  of
           the  terms being  unified,   whereas   unification   without
           the occur check is linear on the size of the smallest of the
           terms  being  unified.   In   any   practical    programming
           language,   basic  operations  are supposed to take constant
           time.  Unification  against a variable should be thought  of
           as the basic operation of Prolog, but this can take constant
           time only if the occur check is omitted.   Thus the  absence
           of  a occur check is essential to make Prolog into a practi-
           cal programming language.  The inconvenience caused by  this

Unless there is some technique I'm not aware of to make the occurs check
sub-linear, I'd say that the above argument against the occur check sound
pretty reasonable.

----
Andreas Stolcke
International Computer Science Institute	stolcke@icsi.Berkeley.EDU
1957 Center St., Suite 600, Berkeley, CA 94704	(415) 642-4274 ext. 126