Talk:Unification

From Wikipedia, the free encyclopedia

Should this page be renamed, e.g., Unification (Prolog) or Unification (Computer Programming)? --Nate

No; this is essentially the same concept as is used in various theorem provers and type checkers, and is not specific to Prolog or to computer programming. (Although in most "mathematical" uses of unification, the example A=f(A) fails rather than returning an infinite term; the extra step in the unification algorithm which checks for this case and makes it fail is called the "occurs check".) Carl

I agree. This means that the dominance of Prolog should somehow be removed from the article. The right context to mention is First-order resolution; note that Prolog uses just a particular form of resolution. Higher-order unification should also be mentioned. --Tillmo 03:57, 24 August 2005 (UTC)

We really ought to distinguish between syntactic unification (discussed here) and E-unification (not yet discussed). E-unification is really important in automated theorem proving. Syntactic unification (and matching) also has important applications aside from Prolog; in ML-style languages, for instance. Perhaps some discussion of the problem of coverage analysis would also be useful?--Iwehrman 17:01, 27 Mar 2005 (UTC)

I have added some more general statements to the article, and corrected some typos. These generalities should lend credence to keeping it as its own topic. —Preceding unsigned comment added by 71.36.181.46 (talk) 08:07, 2 May 2008 (UTC)

Contents

[edit] link to non-compsci logic unification would be dandy

I've no luck finding a page on this kind of unification that doesn't assume the reader wants to do it in Prolog/Lisp/etc. If there are any good web pages that explain unification on logic with a series of clauses containing nothing but plain ol' variables (not even quantifiers, just variables) as you would do logic problems on paper, I think a link to that would be useful. --I am not good at running 21:32, 23 October 2005 (UTC)

[edit] Move unification in Prolog to the prolog article

The bit on prolog ought to be moved to Prolog and referenced, I think. The Prolog page doesn't deal with it sufficiently on its own, and it matters. 138.38.32.84 14:03, 17 January 2007 (UTC)

[edit] Correct the example given

To say that x^2 can be unified with y^3 is at best misleading because the argument that (z^3)^2 = (z^2)^3 = z^6 is semantic and unification is - as I understand it - purely syntactic. I am not enough of an expert to get this right but it seems to me that as *terms* x^2 and y^3 have to be written as m(x,x) and m(y,m(y,y)) where 'm' denotes multiplication. Can these terms be unified? I think so because they both begin with the same function symbol and have the same number of arguments, which - I believe - can themselves be unified. But the definition of unification given on this page does not cover binary (n-ary) functions. —Preceding unsigned comment added by Kilgore666 (talk • contribs) 03:01, 8 October 2007 (UTC)

I also find the polynomial example (in this version) confusing. Suppose x=0 and y=2. If we "unify" x2 with y3 as z6, as shown, we get z=0 to make x=z3 true, and z = \pm \sqrt 2 to make y=z2 true. What?? Is the example wrong or is the article leaving out a crucial piece of information? --Ben Kovitz (talk) 03:55, 27 December 2007 (UTC)

[edit] MGU

What about the Most General Unifier? This article even redirects here, but the page does not mention it -- 200.185.249.203 (talk) 18:07, 16 March 2008 (UTC)