Unification

Unification: the Basic Idea

• Two expressions, each containing information about an object of some sort, are matched against each other. If they do not match -- that is, if they cannot be describing the same object -- unification reports failure. If they do match, unification returns the combination of the information in the two inputs.
• In general, expressions that are unified may contain arbitrary sequences of atoms and lists. They may also include variables. A variable can represent the value in an attribute-value pair or an entire sub-expression. A variable in expression X can match anything in expression Y, but if it appears more than once in X, it must match the same sub-expressions everywhere in Y.
• Given expressions X and Y, unification works roughly in the following way:
  • It checks sub-expressions in X one at a time, looking for matching sub-expressions in Y in each case. If it fails to find a matching sub-expression in Y, what it does depends on the brand of unification.
  • If it encounters a variable for the first time in X, it binds that variable to the corresponding sub-expression in Y and adds the binding to a substitution, a list of current variable bindings. When a variable is encountered other than for the first time, it can only match the sub-expression that it is bound to in the substitution. When unification is done, the variables in X are replaced by their values in the current substitution.
  • Special kinds of sub-expressions such as sets or sequences need special-purpose unification procedures.

Some Examples

• ((gender fem) (number sing))
  ((number sing) (gender masc))
  ()
  ->
  no
  

• ((gender ?x) (number sing) (person 3))
  ((gender fem) (number sing))
  ()
  ->
  ((gender fem) (number sing) (person 3))
  

• ((subject (content (index ?i)))
   (pred (content ((reln sing) (singer ?i)))))
  ((subject (content (index sam)))
   (pred (content ((reln sing) (singer phyllis)))))
  ()
  ->
  no
  

• ((synsem ((content ((restriction (SET ((reln rock)
                                         (inst r1))
                                        ((color gray)
                                         (arg r1)))))))))
  ((phon "rock")
   (synsem ((content ((restriction (SET ((reln rock)
                                         (inst ?index))))
                      (index (?index
                              (gend neut)
                              (num sing))))))))
  ()
   -->
  ((phon "rock")
   (synsem ((content ((restriction (SET ((reln rock)
                                         (inst r1))
                                        ((color gray)
                                         (arg r1))))
                      (index (r1
                              (gend neut)
                              (num sing))))))))
  

• ((dtrs ((head-dtr ((synsem ((cat ((head verb))))))
                     (phon (SET (1 2 "gives"))))
          (comp-dtrs (LIST ((synsem ((cat ((head noun)))))))
                            (phon ?obj1_phon))
                           ((synsem ((cat ((head noun))))))
                            (phon ((SET (3 4 "Fido"))))))
   (phon ((ORD
  	 (?obj1_phon > (1 2 "gives"))
           ((3 4 "Fido") > ?obj1_phon))
  	(SET (1 2 "gives")
  	     (3 4 "Fido")))))
  
  ((phon ((SET (2 3 "Bob"))))
   (synsem ((cat ((head noun))))))
  
  (comp-dtrs 1)
  
   ==>
  
  ((dtrs ((head-dtr ((synsem ((cat ((head verb)))))
                     (phon ((SET (1 2 "gives"))))))
          (comp-dtrs (LIST ((synsem ((cat ((head noun)))))
                            (phon ((SET (2 3 "Bob")))))
                           ((synsem ((cat ((head noun)))))
                            (phon ((SET (3 4 "Fido")))))))))
   (phon ((SET (2 3 "Bob")
  	     (1 2 "gives")
  	     (3 4 "Fido")))))
  

nlp-unify

• Params: pat1, pat2, feat-path
  feat-path specifies which part of pat1 pat2 is to unify with
  Let pat1-part be this part and subst be all of the structure variable bindings which appear in pat1.
• Call unify on pat1-part, pat2, and subst
• If this fails, return no.
• Else substitute the returned bindings into pat1.

unify

• Params: pat1, pat2, substitution (a set of variable bindings)
• If pat1 and pat2 are identical, return substitution
• Else if pat1 or pat2 is a variable, call unify-var, returning either no or the new substitution
• Else if either pat1 or pat2 is an atom, return no
• Else if the first element of pat1 or pat2 is LIST or SET or UNIFY or APPEND or ORDER or OR, do various special things, returning either no or the updated substitution
• Else if the first element of pat1 or pat2 is a variable, unify-var variable with the rest of that pattern, then unify the rest of the pattern with the other pattern in the context of the new substitution, and return that result (either no or the new substitution)
• Else if pat1 is empty, create a "rest" variable for pat1, bind it to the list of all pairs in pat2 which are unaccounted for, add it to substitution and return this
• Else if pat2 is empty, return substitution
• Else find the feature-value pair of pat2 which has the same feature as the first element of pat1. If there is none, return the result of unifying the rest of pat1 with pat2. If there is, unify the corresponding pairs, and either return no if this fails or the result of unifying the rest of pat1 with pat2 in the context of the new substitution.

unify-var

• Params: var, pat, substitution
• If var has a binding in substitution, call unify with the new value and pat
• Else apply the substitution to pat and if var appears anywhere in pat, return no
• Else add the binding var = pat to substitution, and return the new substitution.

[L645 Syllabus]