code/gsv.ml

   1 open List
   2
   3 type predicate = string
   4 type ent = Alice | Bob | Carl
   5 type world = W1 | W2 | Hungry | Full
   6 type variable = string
   7 type term = Constant of ent | Var of variable
   8 type clause =   Pred of predicate * term
   9               | Eq of term * term
  10               | Conj of clause * clause
  11               | Neg of clause
  12               | Poss of clause
  13               | Ex of string * clause
  14 type assignment = (variable * ent) list
  15 type poss = world * assignment
  16 type infostate = poss list
  17
  18 let rec referent (i:poss) (t:term):ent = match (i,t) with
  19     (i, Constant e) -> e
  20   | ((w,(v',a)::g), Var v) -> if 0 == compare v v' then a else referent (w,g) t
  21   (* warning: no error checking *)
  22
  23 let extension (w:world) (p:predicate) (e:ent) = match (w,p,e) with
  24     _, "woman", Alice -> true
  25   | _, "man", Bob -> true
  26   | _, "man", Carl -> true
  27   | Hungry, "hungry", Alice -> true
  28   | _, "enter", Bob -> true
  29   | _, "enter", Carl -> true
  30   | _, "sit", Alice -> true
  31   | _, "sit", Bob -> true
  32   | W1, "closet", Alice -> true
  33   | W1, "guilty", Bob -> true
  34   | W2, "closet", Carl -> true
  35   | W2, "guilty", Carl -> true
  36   | _,_,_ -> false
  37
  38 let domain = [Alice; Bob; Carl]
  39
  40 let rec update (s:infostate) (c:clause) = match c with
  41     Pred (p,t) -> filter (fun (w,g) -> extension w p (referent (w,g) t)) s
  42   | Eq (t1, t2) -> filter (fun i -> (referent i t1) == (referent i t2)) s
  43   | Conj (c1, c2) -> update (update s c1) c2
  44   | Neg c -> filter (fun i -> update [i] c == []) s
  45   | Poss c -> filter (fun i -> update s c != []) s
  46   | Ex (v,c) -> concat (map (fun (a:ent) ->
  47                                update (map (fun (w,g) -> (w,(v,a)::g)) s) c)
  48                             domain)
  49
  50 (* Basic examples *)
  51 let test1 = update [(W1,[])] (Ex ("x", (Pred ("man", Var "x"))))
  52
  53 let test2 = update [(W1,[])] (Ex ("x", (Pred ("woman", Var "x"))))
  54
  55 let test3 = update [(W1,[])]
  56                    (Ex ("x", (Ex ("y", (Conj (Pred ("man", (Var "x")),
  57                                               Pred ("man", (Var "y"))))))))
  58 let test4 = update [(W1,[])] (Ex ("x", (Ex ("y", (Eq (Var "x", Var "y"))))))
  59
  60
  61 (* Alice isn't hungry. *)
  62 let test5 = update [(Hungry,[]);(Full,[])]
  63                    (Neg (Pred ("hungry", Constant Alice)))
  64
  65 (* Alice isn't hungry.  Alice might be hungry. *)
  66 let test6 = update [(Hungry,[]);(Full,[])]
  67                    (Conj (Neg (Pred ("hungry", Constant Alice)),
  68                           Poss (Pred ("hungry", Constant Alice))))
  69
  70 (* Alice might be hungry.  Alice isn't hungry. *)
  71 let test7 = update [(Hungry,[]);(Full,[])]
  72                    (Conj (Poss (Pred ("hungry", Constant Alice)),
  73                           Neg (Pred ("hungry", Constant Alice))))
  74
  75 (* Someone^x entered.  He_x sat. *)
  76 let test8 = update [(W1,[("x",Bob)])]
  77                    (Conj (Ex ("x", Pred ("enter", Var "x")),
  78                           Pred ("sit", Var "x")))
  79
  80 (* He_x sat.  Someone^x entered. *)
  81 let test9 = update [(W1,[("x",Bob)])]
  82                    (Conj (Pred ("sit", Var "x"),
  83                           Ex ("x", Pred ("enter", Var "x"))))
  84
  85 (* Someone^x is in the closet.  He_x might be guilty. *)
  86 let test10 = update [(W1,[]);(W2,[])]
  87                     (Conj (Ex ("x", Pred ("closet", Var "x")),
  88                            Poss (Pred ("guilty", Var "x"))))
  89
  90 (* Someone^x is in the closet who_x might be guilty. *)
  91 let test11 = update [(W1,[]);(W2,[])]
  92                     (Ex ("x", Conj (Pred ("closet", Var "x"),
  93                                     Poss (Pred ("guilty", Var "x")))))
  94