Unification

Syntactic Unification

The aim is to make terms syntactically equivalent by substituting constants for variables in the most general way.

Usually these variables and constants represent first order terms (arity=0), but there is also higher order unification where we might have variables representing functions.

This subject is about unifying expressions with terms containing constants and variables such as:

which might be unified to:

Unification is a generalisation of pattern matching where the constants and variables may be in either expression.

These expressions are tree structures and we are substituting subtrees with other subtrees. The unification problem could also be formulated with a graph or other mathematical structure.

So 'f' is a binary expression and 'x', 'y', '4' and '5' are unary expressions

unify diagram
Here is a classical unification algorithm to generate the most general unification (MGU) of two terms.
unify : t:term -> s:term -> substitution
unify t s =
  if t=s then return {}
  if (isVariable t) & (isVariable s) then return {t<-s}
  if (isVariable t) then
    if (aVariableIn t s) // is t a variable in term s
      then return fail // can't have cycle
      else return {t<-s}
  if (isVariable s) then
    if (aVariableIn s t) // is s a variable in term t
      then return fail // can't have cycle
      else return {s<-t}
  if (t.name = s.name) & (t.arity = s.arity)
      // function name and arity must match
      // constants are 0-arity functions
    then // generate substitution for each parameter
      r={}
      for a1 in t for a2 in s do
        r = concatinate r (unify a1 a2) // combine substitutions
      return r
    else return fail // function don't match

 

Equational Unification

Make terms equationally equivalent.

The expressions must be matched 'modulo E' where E is the equations (identities) that must hold.

So we could take the previous example but this time use say '+' which has other properties. It is commutative (x+y)=(y+x) so this allows other solutions.

unify diagram

 

Other Sites


metadata block
see also:

 

Correspondence about this page

This site may have errors. Don't use for critical systems.

Copyright (c) 1998-2022 Martin John Baker - All rights reserved - privacy policy.