🚀 go-pugleaf

Well, I won't claim any generality, but the Rhet language (a prolog
deviant) does allow you to turn the occurs check on and off, and also
shows only about a 15% degradation in general when on. However, this is
using an interpreted system, with a very general unification operator.
Current work on a compiled replacement leads me to beleive that compiled
specialized unification would indeed degrade by many-fold if it (always)
needed to do an occurs check, but it is less than clear that this is in
fact the case (i.e. the compiler may be able to detect when an occurs
check provably isn't needed for a substantial subset of the cases that
occur in day-to-day prolog type code). I do not yet have any numbers to
back up this opinion, however, looking at the problem more abstractly...
(and keeping in mind that I'm a AI/lisp hacker, not a theoretician :-)...

Graph Unification that does not detect infinite unifiablity can run in
linear time O(E+V) where E and V are the number of edges and vertecies
in the graph. (Prolog terms can be represented as graphs, obviously).
Reference: M.S. Paterson and M.N. Wegman, "Linear unification," J.
Comput. Syst. Sci., vol. 16, pp. 158-167, Apr. 1978

Graph Unification that DOES detect infinite unifiability can run in just
over linear time (specifically O(alphaE + V) where alpha is the inverse
ackerman's function. This result is mentioned in the above paper, but an
example is given in Vitter J.S. and Simons R.A., "New Classes for
Parallel Complexity: A Study of Unification and Other Complete Problems
for *P*" IEEE Trans. on COmp. Vol. c35, no. 5 May 1986 pp 403-417. Note
that this function does not come up with the substitution, it just
detects unifiable, infinitely unifiable, or neither.

Essentially what this tells us is that detecting infinite unifiability
and coming up with a substitution (stronger than just an occurs check,
is only "slightly worse" than not doing so. For practical problems, the
inverse ackerman's function is a constant, after all. HOWEVER, this does
not discuss the all-important "constant factor" by which we really live
our daily lives (e.g. even if I gave you a polynomial function for
reducing NP complete problems to P problems, it would be of tremendous
theoretical importance, but little practical importance if it looked
like (((10**10)**10)**10)n**312875. So it is really in this constant
factor that the occurs check becomes important, and that is where we are
hard pressed to look to theory for any concrete answers (it's easy to
show that checking that a substitution is valid is linear, but it's hard
to show any sort of constant factors for anything since that becomes
architecture-dependant). We can only come up with experiments, and say
things like "so far, it looks pretty bad to me".

If you want to argue against the efficiency position, it really isn't an
argument to say that in this particular program, it makes little
difference, you have to come up with an algorithm for doing compiled
unification & infinite unification that is at least as efficient as the
best known work for doing unification, on a particular architecture.
Such work are not really solid theoretical results, since someone else
can come along with a better way of doing straight unification, but such
is science...

Personally, I feel compelled by the early prolog results too, so I've
never pushed hard to even try to do infinite unification efficiently.
I'd love it if someone pushed through an interesting result!

Regards,
Brad Miller