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
      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.