open List type predicate = string type ent = Alice | Bob | Carl type world = W1 | W2 | Hungry | Full type variable = string type term = Constant of ent | Var of variable type clause = Pred of predicate * term | Eq of term * term | Conj of clause * clause | Neg of clause | Poss of clause | Ex of string * clause type assignment = (variable * ent) list type poss = world * assignment type infostate = poss list let rec referent (i:poss) (t:term):ent = match (i,t) with (i, Constant e) -> e | ((w,(v',a)::g), Var v) -> if 0 == compare v v' then a else referent (w,g) t (* warning: no error checking *) let extension (w:world) (p:predicate) (e:ent) = match (w,p,e) with _, "woman", Alice -> true | _, "man", Bob -> true | _, "man", Carl -> true | Hungry, "hungry", Alice -> true | _, "enter", Bob -> true | _, "enter", Carl -> true | _, "sit", Alice -> true | _, "sit", Bob -> true | W1, "closet", Alice -> true | W1, "guilty", Bob -> true | W2, "closet", Carl -> true | W2, "guilty", Carl -> true | _,_,_ -> false let domain = [Alice; Bob; Carl] let rec update (s:infostate) (c:clause) = match c with Pred (p,t) -> filter (fun (w,g) -> extension w p (referent (w,g) t)) s | Eq (t1, t2) -> filter (fun i -> (referent i t1) == (referent i t2)) s | Conj (c1, c2) -> update (update s c1) c2 | Neg c -> filter (fun i -> update [i] c == []) s | Poss c -> filter (fun i -> update s c != []) s | Ex (v,c) -> concat (map (fun (a:ent) -> update (map (fun (w,g) -> (w,(v,a)::g)) s) c) domain) (* Basic examples *) let test1 = update [(W1,[])] (Ex ("x", (Pred ("man", Var "x")))) let test2 = update [(W1,[])] (Ex ("x", (Pred ("woman", Var "x")))) let test3 = update [(W1,[])] (Ex ("x", (Ex ("y", (Conj (Pred ("man", (Var "x")), Pred ("man", (Var "y")))))))) let test4 = update [(W1,[])] (Ex ("x", (Ex ("y", (Eq (Var "x", Var "y")))))) (* Alice isn't hungry. *) let test5 = update [(Hungry,[]);(Full,[])] (Neg (Pred ("hungry", Constant Alice))) (* Alice isn't hungry. Alice might be hungry. *) let test6 = update [(Hungry,[]);(Full,[])] (Conj (Neg (Pred ("hungry", Constant Alice)), Poss (Pred ("hungry", Constant Alice)))) (* Alice might be hungry. Alice isn't hungry. *) let test7 = update [(Hungry,[]);(Full,[])] (Conj (Poss (Pred ("hungry", Constant Alice)), Neg (Pred ("hungry", Constant Alice)))) (* Someone^x entered. He_x sat. *) let test8 = update [(W1,[("x",Bob)])] (Conj (Ex ("x", Pred ("enter", Var "x")), Pred ("sit", Var "x"))) (* He_x sat. Someone^x entered. *) let test9 = update [(W1,[("x",Bob)])] (Conj (Pred ("sit", Var "x"), Ex ("x", Pred ("enter", Var "x")))) (* Someone^x is in the closet. He_x might be guilty. *) let test10 = update [(W1,[]);(W2,[])] (Conj (Ex ("x", Pred ("closet", Var "x")), Poss (Pred ("guilty", Var "x")))) (* Someone^x is in the closet who_x might be guilty. *) let test11 = update [(W1,[]);(W2,[])] (Ex ("x", Conj (Pred ("closet", Var "x"), Poss (Pred ("guilty", Var "x")))))