UnificationSlide 2Recall Prolog TermsSlide 4Slide 5Slide 6Slide 7Slide 8InstantiationsRevised Definition 1/3Revised Definition 2/3Revised Definition 3/3Prolog unification: =/2Slide 14Slide 15How will Prolog respond?Slide 17Example with complex termsSlide 19Slide 20Slide 21One more exampleUnification Algorithm as a set of 5 rulesComplexity of unificationComposition of substitutionsProlog and unificationInfinite termsSlide 28Occurs CheckProgramming with UnificationSlide 31Slide 32Slide 33Slide 34Slide 35Exercise: unificationUnification–Unification–Unification in PrologUnification•Recall previous example, where we said that Prolog unifies woman(X) with woman(mia) thereby instantiating the variable X with the atom mia.TermsSimple Terms Complex TermsConstants VariablesAtoms NumbersRecall Prolog TermsUnification•Working definition:•Two terms unify if they are the same term or if they contain variables that can be uniformly instantiated with terms in such a way that the resulting terms are equal.Unification•This means that:•mia and mia unify•42 and 42 unify•woman(mia) and woman(mia) unify•This also means that:•vincent and mia do not unify•woman(mia) and woman(jody) do not unifyUnification•What about the terms:•mia and XUnification•What about the terms:•mia and X•woman(Z) and woman(mia)Unification•What about the terms:•mia and X•woman(Z) and woman(mia)•loves(mia,X) and loves(X,vincent)Instantiations•When Prolog unifies two terms it performs all the necessary instantiations, so that the terms are equal afterwards•This makes unification a powerful programming mechanismRevised Definition 1/31. If T1 and T2 are constants, then T1 and T2 unify if they are the same atom, or the same number.Revised Definition 2/31. If T1 and T2 are constants, then T1 and T2 unify if they are the same atom, or the same number.2. If T1 is a variable and T2 is any type of term, then T1 and T2 unify, and T1 is instantiated to T2. (and vice versa)Revised Definition 3/31. If T1 and T2 are constants, then T1 and T2 unify if they are the same atom, or the same number.2. If T1 is a variable and T2 is any type of term, then T1 and T2 unify if T1 = T2 or T1 does not occur in T2.3. If T1 and T2 are complex terms then they unify if:a) They have the same functor and arity, andb) all their corresponding arguments unify, andc) the variable instantiations are compatible.Prolog unification: =/2?- mia = mia.yes?-Prolog unification: =/2?- mia = mia.yes?- mia = vincent.no?-Prolog unification: =/2?- mia = X.X=miayes?-How will Prolog respond??- X=mia, X=vincent.How will Prolog respond??- X=mia, X=vincent.no?-Why? After working through the first goal, Prolog has instantiated X with mia, so that it cannot unify it with vincent anymore. Hence the second goal fails.Example with complex terms?- k(s(g),Y) = k(X,t(k)).Example with complex terms?- k(s(g),Y) = k(X,t(k)).X=s(g)Y=t(k)yes?-Example with complex terms?- k(s(g),t(k)) = k(X,t(Y)).Example with complex terms?- k(s(g),t(k)) = k(X,t(Y)).X=s(g)Y=kyes?-One more example?- loves(X,X) = loves(marsellus,mia).Unification Algorithmas a set of 5 rules•Let x, y denote variables, s, t denote terms, f, g, denote functors.•Let X = { s =? t }, where s and t are to be unified.•Deletion: { t =? t } U X  X•Decomposition: { f(s1, …, sn) = ? f(t1, …, tn) } U X  { s1 =? t1, …, sn = tn } U X.•Clash: { f(s1, …, sn) =? g(t1, …, tm) } U X  fail•Occur check: { x =? f(..x..) } U X  fail•Substitution: { x =? t } U X  { x  t } U X[x  t]Complexity of unification•Depending on the order of rules and the representation of the unifiers, the complexity can be either linear (in terms of the size of terms) or exponential.•Example: •t = g(x1, g(x2, g(x3, …g(xn, a))))•s = g(f(x2,x2), g(f(x3,x3), g(f(x4,x4), …g(a, a))))Composition of substitutions•A substitution is a mapping from variables to terms.•If a, b and g are substitutions and g(t) = b(a(t)) for any term t, then we say g = a.b, a composition of a and b.•Given two terms s and t, we say a is the most general unifier of s and t, if for any unifier g of s and t, there exists b such that g = a.b.Prolog and unification•Prolog does not use a standard unification algorithm•Consider the following query:?- father(X) = X.•Do these terms unify or not?Infinite terms?- father(X) = X.X=father(father(father(father(father(father(father(father(father(father(father(father(father(father(father(father(father(father(father(father(father(father(father(father(father(father(father(father(father(father(father(father(father(father(father(father(father(father(father(father(father(father(father(father(father(father(father(father(Infinite terms?- father(X) = X.X=father(**)yes?-Occurs Check•A standard unification algorithm carries out an occurs check•If it is asked to unify a variable with another term it checks whether the variable occurs in the term•In Prolog:?- unify_with_occurs_check(father(X), X).noProgramming with Unificationvertical( line(point(X,Y), point(X,Z))).horizontal( line(point(X,Y), point(Z,Y))).Programming with Unificationvertical( line(point(X,Y), point(X,Z))).horizontal( line(point(X,Y), point(Z,Y))).?-Programming with Unificationvertical( line(point(X,Y), point(X,Z))).horizontal( line(point(X,Y), point(Z,Y))).?- vertical(line(point(1,1),point(1,3))).yes?-Programming with Unificationvertical( line(point(X,Y), point(X,Z))).horizontal( line(point(X,Y), point(Z,Y))).?- vertical(line(point(1,1),point(1,3))).yes?- vertical(line(point(1,1),point(3,2))).no?-Programming with Unificationvertical( line(point(X,Y), point(X,Z))).horizontal( line(point(X,Y), point(Z,Y))).?- horizontal(line(point(1,1),point(1,Y))).Y = 1;no?-Programming with Unificationvertical( line(point(X,Y), point(X,Z))).horizontal( line(point(X,Y), point(Z,Y))).?- horizontal(line(point(2,3),Point)).Point = point(_554,3);no?-Exercise: