🚀 go-pugleaf

In article <1992Dec18.175714.3917@cs.sfu.ca> jamie@cs.sfu.ca (Jamie Andrews) writes:
>I seem to dimly remember someone having
>characterized the precise theory solved by some unification
>without occurs check.  Does anyone remember the reference?
@ARTICLE{jaffar-stuckey,
	AUTHOR = {Joxan Jaffar and Peter J. Stuckey},
	TITLE = {Semantics of Infinite Tree Logic Programming},
	JOURNAL = {Theoretical Computer Science},
	YEAR = {1986},
	VOLUME = {46},
	PAGES = {141-158}
}
>     Also, I sometimes tell people that Martelli and Montanari's
>and Paterson and Wegman's linear unification algorithms are not
>used because either (a) the constant factor is too high or (b)
>the space requirements are too high.
(a) is a problem, but the main problem is that those algorithms are linear
on the *sum* of the sizes of the two terms being unified, while
(in most practical cases) the Robinson unification algorithm without
the occurs check is linear on the size of the *smaller* term. Notice
that most such unifications in Prolog involve some arbitrarily large
constructed term and a clause head, which is tyoically small, and
of bounded size. I say above "in most practical cases" because
the Robinson algorithm without occurs check is linear on the size of
the *tree unfolding* of the smaller term, but the tree unfolding of
a term may be exponential on the size of the (graph representation of)
the term and thus on the number of variable substitution steps needed
to construct the term. In contrast, the linear unification algorithms,
as well as the most efficient algorithms for rational term unification
(all in one way or another based on some version of UNION-FIND) keep
track of which subterms they have visited and they don't revisit them.
Another source of overhead for the rational term unification algorithms
is that in general they side-effect not just the leaves (variable cells)
but also internal (complex term) nodes (at least all that I have seen
do). These side effects must be kept track of to be undone on backtracking.

Fernando Pereira
2D-447, AT&T Bell Laboratories
600 Mountain Ave, PO Box 636
Murray Hill, NJ 07974-0636
pereira@research.att.com