EOPL - 2.3.4 - Exercise 2.25

Using the data type definitions from the previous exercise, it's easy to define the necessary additional operations and then complete the definition of the unification function.

let is_var_term t =
    match t with Id _ -> true | _ -> false
        
let unit_subst i t =
    extend_subst i t (empty_subst ())
    
let rec compose_substs s1 s2 =
    match s1 with
      EmptySub -> s2
    | ExtendedSub (i, t, s) -> ExtendedSub (i, t, compose_substs s s2)

let rec unify_term t u = 
    match t with
      Id tid -> if (is_var_term u) || 
                    (not (List.mem tid (term_all_ids u))) then
                    Some (unit_subst tid u)
                else
                    None
    | _ -> match u with
             Id _ -> unify_term u t
           | Constant udat -> 
              (match t with 
                 Constant tdat when tdat = udat -> Some (empty_subst ())
               | _ -> None)
           | App us -> (match t with
                          App ts -> unify_terms ts us 
                        | _ -> None)
and unify_terms ts us = 
    match ts, us with
      [], [] -> Some (empty_subst ())
    | ([], _) -> None
    | (_, []) -> None
    | (t :: ts', u :: us') -> 
        let subst_car = unify_term t u in
        match subst_car with
          None -> None
        | Some s -> let new_ts = subst_in_terms ts' s in
                    let new_us = subst_in_terms us' s in
                    let subst_cdr = unify_terms new_ts new_us in
                    match subst_cdr with
                      None -> None
                    | Some s' -> Some (compose_substs s s')

The occurs check is necessary, of course, to avoid infinity. I won't say more than that, to force people that arrive here looking for solutions to EOPL's exercises to think a little about it, at least.

And this concludes Chapter 2.