/tmp/mosstmp/csu01122/unify.sml
(* CS253 - Introduction to Logic for Computer Science
Assignment3 : Unification
Submitted by: Mohit Bhargava (2001122), Group 1
*)
signature UNIFY =
sig
datatype Term = VAR of string | CONST of string | OPR1 of string * Term | OPR2 of string * Term * Term | OPR3 of string * Term * Term * Term
val unify : Term list -> Term list list
end;
structure UNIFY: UNIFY =
struct
(* datatype Term definition *)
datatype Term = VAR of string | CONST of string | OPR1 of string * Term | OPR2 of string * Term * Term | OPR3 of string * Term * Term * Term;
(********************** DISAGREEMENT SET ************************)
(* fun degree returns the degree of terms - taking degree of CONST as 0 and VAR as 4 *)
fun degree(CONST a) = 0
| degree(OPR1(a,b)) = 1
| degree(OPR2(a,b,c)) = 2
| degree(OPR3(a,b,c,d)) = 3
| degree(VAR a) = 4;
(* fun degsame returns true if degree of the two terms is same else returns false *)
fun degsame([],d) = true
| degsame(l::L,d) = (degree(l)=d) andalso degsame(L,d);
(* fun match returns true if 2 terms are same, else false *)
fun match(OPR1(f,x1),OPR1(g,x2))= (f=g)
| match(OPR2(f,x1,y1),OPR2(g,x2,y2))= (f=g)
| match(OPR3(f,x1,y1,z1),OPR3(g,x2,y2,z2))= (f=g)
| match(VAR(x1),VAR(x2)) = (x1=x2)
| match(CONST(x1),CONST(x2)) = (x1=x2)
| match(x,_)=false;
(* fun child1 lists the first child of all the terms in the list - taking [] when child not present*)
fun child1([]) = []
| child1(OPR1(f,x)::L) = x::child1(L)
| child1(OPR2(f,x,y)::L) = x::child1(L)
| child1(OPR3(f,x,y,z)::L) = x::child1(L)
| child1(x::L) = []@child1(L);
(* fun child2 lists the second child of all the terms in the list - taking [] when child not present*)
fun child2([]) = []
| child2(OPR1(f,x)::L) = []@child2(L)
| child2(OPR2(f,x,y)::L) = y::child2(L)
| child2(OPR3(f,x,y,z)::L) = y::child2(L)
| child2(x::L) = []@child2(L);
(* fun child3 lists the third child of all the terms in the list - taking [] when child not present*)
fun child3([]) = []
| child3(OPR1(f,x)::L) = []@child3(L)
| child3(OPR2(f,x,y)::L) = []@child3(L)
| child3(OPR3(f,x,y,z)::L) = z::child3(L)
| child3(x::L) = []@child3(L);
(* fun ispresent returns true if term is presentin list else false *)
fun ispresent(x,[]) = false
| ispresent (x,y::L) = if (x=y) then true else ispresent(x,L);
(* fun remdups removes duplcates in a list *)
fun remdups1([])=[]
| remdups1(x::nil)= x::nil
| remdups1(x::L)= if(ispresent(x,L)) then remdups1(L)
else (x::(remdups1(L)));
(* fun same returns true if entire list is same and matches the term *)
fun same(t,[]) = true
| same(t,l::L) = (match(t,l)) andalso same(t,L);
(* fun disset determines the disagreement set *)
fun disset([]) = []
| disset(l::L) = if not((degsame(l::L,degree(l))) andalso (same(l,L))) then l::L
else if (not(disset(child1(l::L))=[])) then disset(child1(l::L))
else if (not(disset(child2(l::L))=[])) then disset(child2(l::L))
else disset(child3(l::L));
(************************ SUBSTITUTION *********************)
(* fun disagree picks up a List and returns a boolean to indiacate substitution *)
fun disagree(L) = let
(* fun varsub checks if a varialble is there to be substituted *)
fun varsub(VAR(x),VAR(y)) = not(x=y)
| varsub(VAR(x),CONST(y)) = true
| varsub(VAR(x1),OPR1(f,x2)) = (varsub(VAR(x1),x2))
| varsub(VAR(x1),OPR2(f,x2,y2)) = (varsub(VAR(x1),x2) andalso varsub(VAR(x1),y2))
| varsub(VAR(x1),OPR3(f,x2,y2,z2)) = (varsub(VAR(x1),x2) andalso varsub(VAR(x1),y2) andalso varsub(VAR(x1),z2))
| varsub(x,_) = true
(* fun varList checks for a variable and a list *)
fun varList(x,[]) = true
| varList(x,l::L) = varsub(x,l) andalso varList(x,L)
fun vars([],L) = true
| vars(l::L1,L2) = varList(l,L2) andalso vars(L1,L2)
(* fun pickconst creates a list of constants in a given list *)
fun pickconst([]) = []
| pickconst(CONST(x)::L) = CONST(x)::pickconst(L)
| pickconst(_::L) = pickconst(L)
(* fun pickvar creates a list of variables in a given list *)
fun pickvar([]) = []
| pickvar(VAR(x)::L) = VAR(x)::pickvar(L)
| pickvar(_::L) = pickvar(L)
(* fun pickopr creates a list of operators in a given list *)
fun pickopr([])= []
| pickopr(x::L) = if (degree(x)>0 andalso degree(x)<4) then x::pickopr(L)
else pickopr(L)
in
((length(pickconst(L))<=1) andalso length(pickvar(L))>0) andalso vars(pickvar(L),pickopr(L))
end;
(* fun sub gives the substitution *)
fun sub(L) = let
fun vsub1(VAR(x)::L) = VAR(x)
| vsub1(_::L) = vsub1(L)
fun vsub2(x,l::L) = if not(x=l) then l else vsub2(x,L)
| vsub2(x,_) = x
in
[vsub2(vsub1(L),L),vsub1(L)]
end;
(* fun subs performs substitution *)
fun subs(CONST(x),L)=CONST(x)
| subs(VAR(x),[l1,l2])=if VAR(x)=l2 then l1 else VAR(x)
| subs(OPR1(f,x1),x2)=OPR1(f,subs(x1,x2))
| subs(OPR2(f,x1,y1),x2)=OPR2(f,subs(x1,x2),subs(y1,x2))
| subs(OPR3(f,x1,y1,z1),x2)=OPR3(f,subs(x1,x2),subs(y1,x2),subs(z1,x2))
| subs(x,_) = x;
(* fun subsL performs substitution on a list *)
fun subsL([],s)=[]
| subsL(l::L,s)=subs(l,s)::subsL(L,s);
(****************************MAIN UNIFICATION****************************)
(* determines where unification is not possible *)
fun unify2([])= []
| unify2(L) = let
fun ispresent(x,[]) = false
| ispresent (x,y::L) = if (x=y) then true else ispresent(x,L)
(* to determine if unification is present or not *)
fun notpossibleAt([]) = []
| notpossibleAt([l1,l2]::L) = if(l1= CONST "UnificationNotPossible") then [[l1,l2]] else notpossibleAt(L)
| notpossibleAt(x::L) = notpossibleAt(L)
in
if(ispresent([CONST"UnificationNotPossible"],L))
then notpossibleAt(L) else L
end;
(*checks if possible and then performs unification *)
fun unify1([]) = []
| unify1(l::[])=[]
| unify1(l::L)= let
val L1 = remdups1(disset(l::L))
in
if (disagree(L1))
then sub(L1)::unify1(remdups1(subsL(l::L,sub(L1))))
else [CONST"UnificationNotPossible"::L1]
end;
(* fun getLabel gives 5 lists of consts, vars and the 3 arity operators from a single Term*)
fun getLabel(CONST(x)) = ([x],[],[],[],[])
| getLabel(VAR(x)) = ([],[x],[],[],[])
| getLabel(OPR1(f,x)) = let val (L11,L12,L13,L14,L15) = getLabel(x)
in
(L11,L12,f::L13,L14,L15)
end
| getLabel(OPR2(f,x,y)) = let val (L11,L12,L13,L14,L15) = getLabel(x)
val (L21,L22,L23,L24,L25) = getLabel(y)
in
(L11@L21,L12@L22,L13@L23,f::L14@L24,L15@L25)
end
| getLabel(OPR3(f,x,y,z)) = let val (L11,L12,L13,L14,L15) = getLabel(x)
val (L21,L22,L23,L24,L25) = getLabel(y)
val (L31,L32,L33,L34,L35) = getLabel(z)
in
(L11@L21@L31,L12@L22@L32,L13@L23@L33,L14@L24@L34,f::L15@L25@L35)
end;
(* fun getLabel gives 5 lists of consts, vars and the 3 arity operators from a List of Terms*)
fun splitList([],L1,L2,L3,L4,L5) = (L1,L2,L3,L4,L5)
| splitList(l::L,L1,L2,L3,L4,L5) = let val (LL1,LL2,LL3,LL4,LL5) = getLabel(l)
in
splitList(L,L1@LL1,L2@LL2,L3@LL3,L4@LL4,L5@LL5)
end;
(* to check for illegal expressions *)
fun illegal([]) = true
| illegal(L) =
let
val (L1,L2,L3,L4,L5) = splitList(L,[],[],[],[],[])
val (LL1,LL2,LL3,LL4,LL5) = (remdups1(L1),remdups1(L2),remdups1(L3),remdups1(L4),remdups1(L5))
val M = LL1@LL2@LL3@LL4@LL5
in
length(remdups1(M)) = length(M)
end;
(*main unifier function *)
fun unify(L)= if(not(illegal(L))) then ([[CONST("ILLEGALEXPRESSION")]])
else (unify2(unify1(remdups1(L))));
end;