# 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"

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

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

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

## Bibliography¶

 [wikiunification] http://en.wikipedia.org/wiki/Unification_%28computer_science%29