Lab Session 4

Unification Problem

Unification, in computer science and logic, is an algorithmic process of solving equations between symbolic expressions. In the following text, we shall give out its formal definiton in maths and programming language ATS.

Expression and Substitution

Definition of language of expressions:
exp    ::=  VAR    // variable (leaf)
exp    ::=  INT    // integer (leaf)
exp    ::=  ID (explst)  // constructor (branch)
explst ::= 
explst ::=  exp explst
VAR    ::=  x, y, z, ...  // strings of characters
INT    ::=  ..., -1, 0, 1, ...  // integers
ID     ::=  x, y, z, ...  // strings of characters

Encode the language of expressions in ATS

datatype exp =
| VAR of (string)
| INT of (int)
| CONS of (string (*constructor id*), explst)
where
explst = list0 (exp)
Algorithm (equality =): The following algorithm can determine whether two expressions are equivalent.
equal(a, b): two expressions a and b
if both a and b are leaf nodes and are equivalent
return true
if both a and b have the same ID and the same number of children
in order from left to right, check each pair of corresponding children of a and b for equality
return true if all the subexpressions are equivalent
return false otherwise

ATS code

extern fun equal (a: exp, b: exp): bool

extern fun print_exp (e: exp): void

implement equal (a, b) =
case+ (a, b) of
| (VAR (na), VAR (nb)) => na = nb
| (INT (ia), INT (ib)) => ia = ib
| (CONS (ida, expsa), CONS (idb, expsb)) =>
  (
  if (ida <> idb) then false else let
    fun cmp2 (xs: list0 exp, ys: list0 exp): bool =
      case+ (xs, ys) of
      | (nil0 (), nil0 ()) => true
      | (cons0 (x, xs1), cons0 (y, ys1)) =>
          if equal (x, y) = false then false
          else cmp2 (xs1, ys1)
      | (_, _) => false
  in
    cmp2 (expsa, expsb)
  end
  )
| (_, _) => false
Definition of substitution:
A mapping from variabes to expressions, e.g. {“v”: 3, “xs”: cons0 (1, nil0), ...}.

ATS code

abstype substitution = ptr
typedef subs = substitution

exception conflict of ()
exception notfound of ()

extern fun subs_create (): subs
extern fun subs_add (s: subs, name: string, v: exp): subs  // may raise exception
extern fun subs_merge (s1: subs, s2: subs): subs  // may raise exception
extern fun subs_get (s: subs, n: string): exp // may raise exception

extern fun print_subs (s: subs): void

assume substitution = '(string, exp)  // one possible implementation
Definition of substitute expresion *a* with substitution \(\sigma\):
Replace the variables in an expression with corresponding expression designated in the substitution.

ATS code

extern fun subs_substitute (e: exp, s: subs): exp

Unification

Definition of Unification (not very strict):
Given two expressions a and b, find \(\sigma\) such that \(\sigma(a) = \sigma(b)\)
Algorithm (pattern matching unification): Whether unification can be computed efficiently, or at all, depends on what restrictions are placed on the expressions that may need to be unified). The following algorithm, which we will call pattern matching unification, is guaranteed to terminate quickly (i.e., polynomial time) as long as at least one side of the equation contains no variables. It is guaranteed to quickly find a solution if it exists, as long as all variables occur exactly once.
unify(a, b): two expressions a and b
if both a and b are leaf nodes and are equivalent
return the empty substitution \(\sigma0\)
if a is a variable node representing a variable x
return the substitution {x: b}
if b is a variable node representing a variable x
return the substitution {x: a}
if both a and b have the same ID and the same number of children
in order from left to right, unify each pair of corresponding children of a and b
as long as they do not overlap on any variables, combine the substitutions obtained above
return the combined substitution

ATS code

fun unify (a: exp, b: exp): subs  // may raise exception

Skeleton Code

#define
ATS_PACKNAME "LAB_UNIFICATION"

#include "share/atspre_define.hats"
#include "share/atspre_staload.hats"

#include "share/HATS/atspre_staload_libats_ML.hats"

datatype exp =
| VAR of (string)
| INT of (int)
| CONS of (string (*constructor id*), explst)
where
explst = list0 (exp)


extern fun equal (a: exp, b: exp): bool

implement equal (a, b) =
case+ (a, b) of
| (VAR (na), VAR (nb)) => na = nb
| (INT (ia), INT (ib)) => ia = ib
| (CONS (ida, expsa), CONS (idb, expsb)) =>
  (
  if (ida <> idb) then false else let
    fun cmp2 (xs: list0 exp, ys: list0 exp): bool =
      case+ (xs, ys) of
      | (nil0 (), nil0 ()) => true
      | (cons0 (x, xs1), cons0 (y, ys1)) =>
          if equal (a, b) = false then false
          else cmp2 (xs1, ys1)
      | (_, _) => false
  in
    cmp2 (expsa, expsb)
  end
  )
| (_, _) => false

fun print_exp (e: exp): void =
case+ e of
| VAR (x) => print x
| INT (x) => print x
| CONS (id, xs) => let
  val () = print (id)
  val () = print (" (")
  val () = print_explst (xs)
  val () = print (")")
in
end
and
print_explst (es: list0 exp): void = let
  fun print_explst_tail (es: list0 exp): void =
    case+ es of
    | cons0 (e, es1) => let
      val () = print ", "
      val () = print_exp (e)
    in
      print_explst_tail (es1)
    end
    | nil0 () => ()
in
  case+ es of
  | cons0 (x, es) => let
    val () = print_exp (x)
    val () = print_explst_tail es
  in end
  | nil0 () => ()
end

overload print with print_exp

(* ************** *************** *)

abstype substitution = ptr
typedef subs = substitution

exception conflict of ()
exception notfound of ()

extern fun subs_create (): subs

// may raise exception
extern fun subs_add (xs: subs, name: string, v: exp): subs

// may raise exception
extern fun subs_merge (s1: subs, s2: subs): subs  

// may raise exception
extern fun subs_get (s: subs, n: string): exp

extern fun subs_substitute (e: exp, s: subs): exp

extern fun print_subs (s: subs): void

local
  assume substitution = list0 '(string, exp)
in
  implement subs_create () = nil0 ()

  implement subs_add (xs, name, v) = let
    fun cmp (res: '(string, exp), x: '(string, exp)):<cloref1> '(string, exp) =
      if (res.0 = x.0) then $raise conflict
      else res

    val _ = list0_foldleft<'(string, exp)><'(string, exp)> (xs, '(name, v), cmp)
  in
    cons0 {'(string, exp)} ('(name, v), xs)
  end

  // implement subs_merge (s1, s2) = todo

  // implement subs_get (s: subs, n: string) = todo

  // implement subs_substitute (e, s) = todo

  implement print_subs (s) = let
    fun print_subs_tail (s: subs): void =
      case+ s of
      | cons0 (p, s) => let
        val () = print! (", ", p.0, ": ", p.1)
      in end
      | nil0 () => ()
    val () = print "{"
    val () = case+ s of
      | cons0 (m, s1) => let
        val () = print! (m.0, ": ", m.1)
      in
        print_subs_tail (s1)
      end
      | nil0 () => ()
    val () = print "}"
  in end

end  // end of [local]

// may raise exception
extern fun unify (a: exp, b: exp): subs

// implement unify (a, b) = todo

implement main0 () = let
  // cons1 (y, nil1 ())
  val e1 = CONS ("cons1", cons0 (VAR ("y"),
                          cons0 (CONS ("nil1", nil0 ()),
                          nil0))
           )
  // cons1 (x, cons1 (y, nil1 ()))
  val e2 = CONS ("cons1", cons0 (VAR ("x"), 
                          cons0 (e1,
                          nil0))
           )
  
  // cons1 (2, nil1 ())
  val e3 = CONS ("cons1", cons0 (INT (2),
                          cons0 (CONS ("nil1", nil0 ()),
                          nil0))
           )
  // cons1 (1, cons1 (2, nil1 ()))
  val e4 = CONS ("cons1", cons0 (INT (1), 
                          cons0 (e3,
                          nil0))
           )
  val e5 = VAR ("x")

  val () = println! ("e2 is ", e2)
  val () = println! ("e4 is ", e4)
  val s = unify (e2, e4)
  val () = print "s = "
  val () = print_subs (s)
  val () = println! ()

  val e2' = subs_substitute (e2, s)
  val e4' = subs_substitute (e4, s)
  val () = println! ("s(e2) = ", e2')
  val () = println! ("s(e4) = ", e4')

  val () = println! ()
  val () = println! ()

  val () = println! ("e5 is ", e5)
  val () = println! ("e3 is ", e3)
  val s = unify (e5, e3)
  val () = print "s = "
  val () = print_subs (s)
  val () = println! ()

  val e5' = subs_substitute (e5, s)
  val e3' = subs_substitute (e3, s)
  val () = println! ("s(e5) = ", e5')
  val () = println! ("s(e3) = ", e3')
in
end

unification_skeleton.dats

Solution

unification.dats

Makefile