From ryoung@utdallas.edu Wed Mar 2 17:52:57 EST 1994 Article: 9815 of comp.lang.prolog Xref: glinda.oz.cs.cmu.edu comp.lang.prolog:9815 Path: honeydew.srv.cs.cmu.edu!das-news.harvard.edu!noc.near.net!MathWorks.Com!europa.eng.gtefsd.com!howland.reston.ans.net!cs.utexas.edu!convex!news.utdallas.edu!ryoung From: ryoung@utdallas.edu (Young U Ryu) Newsgroups: comp.lang.prolog Subject: Re: most general unifier Date: 28 Feb 1994 21:25:29 GMT Organization: Univ. of Texas at Dallas Lines: 41 Message-ID: <2ktng9\$jq9@news.utdallas.edu> References: <2kjmh7\$6b4@apollo.it.luc.edu> NNTP-Posting-Host: apache.utdallas.edu In article <2kjmh7\$6b4@apollo.it.luc.edu> pchhabr@orion.it.luc.edu (Nick Chhabra) writes: >I was wondering if someone has a prolog code for > >MOST GENERAL UNIFIER > >Or does anyone know the book I can find the code in. > Following K.R. Apt ... A substitution s is a finite mapping from variables xi to terms ti (where i = 1,2, ..., n) under the restrictions that: 1. x1, ..., xn are different. 2. For all i, xi \= ti. Given two substitutions s1 (from xi to ti, for i=1,...,n) and s2 (from yi to ui, for i=1,...,m), the composition s1s2 is defined as: {x1/t1s2, ..., xn/tns2} union s2 minus {xi/tis2 | xi = tis2}} minus {yi/ui | yi in {x1,...,xn}} A substitution s1 is more general than a substitution s2 if for some substitution s3, s2=s1s3. A unifier of two atoms A and B, or two terms A and B is a substitution s that makes As=Bs. A unifier of A and B is called a most general unifier if it is more general than any other unifiers of A and B. ================================================ For details, see: J.W.LLoyd. (1987). Foundations of Logic Programming. 2nd Edition. Sprinter-Verlag. Young Article 9821 of comp.lang.prolog: Xref: glinda.oz.cs.cmu.edu comp.lang.prolog:9821 Path: honeydew.srv.cs.cmu.edu!nntp.club.cc.cmu.edu!news.mic.ucla.edu!library.ucla.edu!agate!msuinfo!harbinger.cc.monash.edu.au!aggedor.rmit.EDU.AU!goanna.cs.rmit.oz.au!not-for-mail From: ok@goanna.cs.rmit.oz.au (Richard A. O'Keefe) Newsgroups: comp.lang.prolog Subject: Re: most general unifier Date: 1 Mar 1994 16:46:28 +1100 Organization: Comp Sci, RMIT, Melbourne, Australia Lines: 62 Message-ID: <2kukrk\$sug@goanna.cs.rmit.oz.au> References: <2kjmh7\$6b4@apollo.it.luc.edu> NNTP-Posting-Host: goanna.cs.rmit.oz.au NNTP-Posting-User: ok pchhabr@orion.it.luc.edu (Nick Chhabra) writes: >I was wondering if someone has a prolog code for MOST GENERAL UNIFIER most_general_unifier(X, X). If you want it done properly, with the occurs check: % free_of(Variable, Term) % is true iff Variable does not occur anywhere in Term. free_of(Variable, Term) :- ( var(Term) -> Variable \== Term ; functor(Term, _, Arity), free_of1(Arity, Term, Variable) ). free_of1(N, Term, Variable) :- ( N < 1 -> true ; arg(N, Term, Arg), free_of(Variable, Arg), M is N - 1, free_of1(M, Term, Variable) ). unify(X, Y) :- ( var(X) -> ( var(Y) -> X = Y ;/* nonvar(Y) */ free_of(X, Y), X = Y ) ; var(Y) /* & nonvar(X) */ -> free_of(Y, X), Y = X ;/* nonvar(X) & nonvar(Y) */ functor(X, F, N), functor(Y, F, N), unify_args(N, X, Y) ). unify_args(N, X, Y) :- ( N =:= 0 -> true ; arg(N, X, Xn), arg(N, Y, Yn), unify(Xn, Yn), M is N - 1, unify_args(M, X, Y) ). If you don't want to actually _do_ the unification but to find out what the most general common instance of X and Y is, do most_general_common_instance(X, Y, I) :- setof(X, unify(X, Y), [I]). -- Richard A. O'Keefe; ok@goanna.cs.rmit.oz.au; RMIT, Melbourne, Australia. The last good thing written in C was Franz Schubert's Symphony number 9.