Background for Unification

---

• Terms made from constructors and variables (for the simple first order case)
• Constructors may be applied to arguments (other terms) to make new terms
• Variables and constructors with no arguments are base cases
• Constructors applied to different number of arguments ($\text{arity}$) considered different
• Substitution of terms for variables

Simple Implementation Background

---

type term = Variable of string 
                | Const of (string * term list)
let x = Variable "a";; 
let tm = Const ("2", []);;

let rec subst var_name residue term = 
    match term with Variable name -> 
        if var_name = name then residue else term 
    | Const (c, tys) -> 
        Const (c, List.map (subst var_name residue) tys);;

Unification Problem

---

Given a set of pairs of terms (“equations”)

$$\{(s_1,t_1),(s_2,t_2),...,(s_n,t_n)\}$$

$\text{(the }\text{unification problem}\text{) }\text{ does there exist}$

$\text{a substitution }\sigma \text{(the }\text{ unification solution)}$

$\text{of terms for variables such that}$

$$\sigma (s_i)=\sigma (t_i)$$

$\text{for all }i=1,...,n?$

Uses for Unification

---

• Type Inference and type checking
• Pattern matching as in OCaml
• Can use a simplified version of algorithm
• Logic Programming - Prolog
• Simple parsing

Unification Algorithm

---

• $\text{Let }S=\{(s_1=t_1),(s_2=t_2),...,(s_n=t_n)\}$ $\text{ be a unication problem.}$
• $\text{Case }S=:\text{Unif}(S)$ $\text{ = Identity function (i.e., no substitution)}$
• $\text{Case }S=\{(s,t)\}\cup S^{\prime }$ $\text{ : Four main steps}$

• $\text{ Delete}$: If $s=t$ (they are the same term) then $\text{ Unif(S) = Unif(S’)}$
• $\text{ Decompose}$: $\text{ if }s=f(q_1,...,q_m)$ and $t=f(r_1,...,r_m)$ $\text{ (same f, same m!), then }$ $\text{Unif(S)}=\text{Unify}(\{(q_1,r_1),...,(q_m,r_m)\}\cup S^{\prime })$
• $\text{ Orient}$: $\text{it }\text{ t = x}\text{ is a variable, and s is not a variable, }$ $\text{Unify(S) = Unify}(\{(x=s)\}\cup S^{\prime })$