[net.lang.prolog] Unification Query

bts@unc.UUCP (10/19/83)

     This is a question for Prolog implementors, I suppose,
or anyone else brave enough to read the source of his (of
her) favorite Prolog interpreter:

     What kind of unification algorithm does your Prolog
use?  Or, for that matter, does it really do unification?
(See the comment on p. 224 of Clocksin & Mellish's "Program-
ming in Prolog", or just try giving your Prolog system the
goal

          ?- X = f(X).

sometime when you've nothing better to do.)

     The traditional algorithm (see "Computational logic:
the unification algorithm", by J. Robinson, in Machine
Intelligence #6) takes, in the worst case, time exponential
in the length of the terms it's trying to unify.  There are
algorithms by Paterson and Wegman, Huet, or Martelli and
Montanari (see "An efficient unification algorithm", by Mar-
telli and Montanari, in ACM ToPLaS, April 1982, for a dis-
cussion of these three) which are better asymptotically.
But, is anyone using them?

     Bruce Smith, UNC-Chapel Hill
     decvax!duke!unc!bts   (USENET)
     bts.unc@udel-relay (other NETworks)