bts@unc.UUCP (Bruce Smith) (10/19/83)
I'm interested in anything new on unification algo-
rithms. In case some readers don't know what I'm talking
about, I'll give a short description of the problem and some
references I know of. Experts-- the ones I'm really
interested in reaching-- may skip to the last paragraph.
Given a set of terms (in some language) containing
variables, the unification problem is to find a 'unifier',
that is, a substitution for the variables in those terms
which would make the terms equal. Moreover, the unifier
should be a 'most general unifier', that is, any other unif-
iers should be extensions of it. Resolution theorem-provers
and logic programming languages like Prolog depend on
unification-- though the Prolog implementations I'm familiar
with "cheat". (See Clocksin and Mellish's "Programming in
Prolog", p. 219.)
Unification seems to be a very active topic. The paper
"A short survey on the state of the art in matching and
unification problems", by Raulefs, Siekmann, Szabo and
Unvericht, in the May 1979 issue of the SIGSAM Bulletin,
contains a bibliography of over 90 articles. And, "An effi-
cient unification algorithm", by Martelli and Montanari, in
the April 1982 ACM Transactions on Programming Languages and
Systems, gives a (very readable) discussion of the effi-
ciency of various unification algorithms. A programming
language has even been based on unification: "Uniform-- A
language based on unification which unifies (much of) Lisp,
Prolog and Act1" by Kahn in IJCAI-81.
So, does anyone out there in network-land have a unifi-
cation bibliography more recent that 1979? If it's on-line,
would you please post it to USENET's net.ai? If not, where
can we get a copy?
Bruce Smith, UNC-Chapel Hill
decvax!duke!unc!bts (USENET)
bts.unc@udel-relay (other NETworks)decot@cwruecmp.UUCP (Dave Decot) (10/21/83)
An "Efficient Unification Algorithm"?!? This is amazing! I'll have to go read that article right away, because if the title is not misleading, and you have accurately described what a unification algorithm is, P == NP! The Satisfiability problem is solvable by any algorithm that does what you require of your most general unification algorithm, so your problem is NP-complete. The set of terms to be unified contains only two terms, one is simply "1" and the other is the expression to be satisfied. Your problem is in NP as long as the terms with substituted variables can be evaluated in polynomial time. At any rate, your problem is at least as "hard" as Satisfiability. Since your problem can be solved efficiently, it must be not only in NP, but also in P (the set of problems solvable in time proportional to a polynomial function of the length of its instances) by today's normal computers. The most logical explanation is that the algorithm in that paper is not a full implementation of your desired "most general" algorithm. ---------------------------------------- Dave Decot ..!decvax!cwruecmp!decot