X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=code%2Fgsv.ml;fp=code%2Fgsv.ml;h=6f4c4166fde833f701b28dbb7dfaf06f569456d3;hp=0000000000000000000000000000000000000000;hb=585323674554a6a414312ef903d753d53912e68e;hpb=2dc2206118459c9657c63bdc5ca31424eafa69be

diff --git a/code/gsv.ml b/code/gsv.ml
new file mode 100644
index 00000000..6f4c4166
--- /dev/null
+++ b/code/gsv.ml
@@ -0,0 +1,94 @@
+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")))))
+