--- /dev/null
+(* GSV monadically 13 April 2015 *)
+
+type identifier = char
+let any_truths (xs : 'a list) : bool = List.exists ident xs
+let all_truths (xs : 'a list) : bool = List.for_all ident xs
+
+module type SEMANTICS = sig
+ type noun (* this is whatever monadic type the semantics assigns to noun-sized contents *)
+ type sent (* this is whatever monadic type the semantics assigns to sentence-sized contents *)
+ val run : sent -> bool
+ val dynamic : bool
+ val extensional : bool
+
+ val getx : noun val gety : noun val getz : noun
+ (* OCaml will parse ~~~ as a prefix operator, but unfortunately won't let you say
+ `~~~ predicate subject`; you have to say `~~~ (predicate subject)`. *)
+ val ( ~~~ ) : sent -> sent
+ (* OCaml will parse these three as infix operators (yay), but makes them all
+ left-associative (ehh for >>>) and have the same precedence (boo). *)
+ val ( &&& ) : sent -> sent -> sent
+ val ( ||| ) : sent -> sent -> sent
+ val ( >>> ) : sent -> sent -> sent
+ (* OCaml parses this with same associativity and precedence as the preceding (boo). *)
+ val (===) : noun -> noun -> sent
+ val ann : noun val bill : noun val carol : noun val dave : noun val ella : noun val frank : noun
+ val male : noun -> sent val female : noun -> sent
+ val left : noun -> sent
+ val single : noun -> sent
+ (* Transitive verbs apply to their direct objs first, subjects second. *)
+ val marriedto : noun -> noun -> sent
+ val saw : noun -> noun -> sent
+ val kisses : noun -> noun -> sent
+ val loves : noun -> noun -> sent (* here construed extensionally *)
+ (* Quantifiers may be unimplemented. *)
+ val some : identifier -> sent -> sent
+ val every : identifier -> sent -> sent
+ (* Intensional verbs and operators may be unimplemented. *)
+ val thinks : sent -> noun -> sent
+ val maybe : sent -> sent
+end
+
+type world = Actual | Other | Another
+let modal_domain = [Actual; Other; Another]
+
+type entity = Ann | Bill | Carol | Dave | Ella | Frank
+let domain = [Ann; Bill; Carol; Dave; Ella; Frank]
+let string_of_entity = function
+ | Ann -> "Ann"
+ | Bill -> "Bill"
+ | Carol -> "Carol"
+ | Dave -> "Dave"
+ | Ella -> "Ella"
+ | Frank -> "Frank"
+let print_entity ent = print_string (string_of_entity ent)
+
+module Facts(X : Monad.MONAD) = struct
+(* Here are the atomic facts: Ann and Bill are married, also Carol and Dave.
+ Genders and marital statuses are epistemically necessary.
+ In the actual world (w1), everyone left; people look leftwards (Carol sees Bill and Ann, etc.); Carol and Dave kiss; husbands love only their wives and Frank loves all the women.
+ In w2, all but Carol left; no one sees anything; all spouses kiss; all men love only Carol and Ella loves the wives.
+ In w3, only Ann and Bill left; no one sees anything; nobody kisses; Frank loves everyone else.
+*)
+
+ let is_male = function Bill | Dave | Frank -> true | _ -> false
+ let are_married = function (Ann, Bill) | (Bill, Ann) | (Carol, Dave) | (Dave, Carol) -> true | _ -> false
+ let is_a_wife = function Ann | Carol -> true | _ -> false
+
+ let male xx = X.(map is_male xx)
+ let female xx = X.(map (not % is_male) xx)
+
+(* Ella and Frank are single *)
+ let single xx = X.(map (fun x -> x > Dave) xx)
+
+(* Actually (in w1), everybody left. In w2, everybody but Carol left. In w3, only Ann and Bill left. *)
+ let left1 xx = X.(map (fun _ -> true) xx)
+ let left2 xx = X.(map (fun x -> x <> Carol) xx)
+ let left3 xx = X.(map (fun x -> x = Ann || x = Bill) xx)
+
+(* In the sentences, order of application is: TransitiveVerb + Object + Subject.
+ But we convert to logical order for our operations. *)
+
+(* Actually, each person saw the people alphabetically before them. In w2 and w3, no one saw anyone. *)
+ let saw1 yy xx = X.(map2 (fun x y -> x < y) xx yy)
+ let saw2 yy xx = X.(map2 (fun _ _ -> false) xx yy)
+ let saw3 = saw2
+
+(* Necessarily, Ann and Bill are married to each other; also Carol to Dave. *)
+ let marriedto yy xx = X.(map2 (curry are_married) xx yy)
+
+(* Actually, only Carol and Dave kiss. In w2, spouses kiss. In w3, there is no kissing. *)
+ let kisses1 yy xx = X.(map2 (fun x y -> (x = Carol && y = Dave) || (x = Dave && y = Carol)) xx yy)
+ let kisses2 yy xx = marriedto xx yy
+ let kisses3 yy xx = X.(map2 (fun x y -> false) xx yy)
+
+(* Actually, each husband loves only his wife and Frank also loves the women.
+ In w2, all the men love Carol and Ella loves the wives.
+ In w3, Frank loves everyone else. *)
+ let loves1 yy xx = X.(map2 (fun x y -> (is_male x && are_married(x,y)) || (x = Frank && not (is_male y))) xx yy)
+ let loves2 yy xx = X.(map2 (fun x y -> (is_male x && y = Carol) || (x = Ella && is_a_wife y)) xx yy)
+ let loves3 yy xx = X.(map2 (fun x y -> x = Frank && x <> y) xx yy)
+end
+
+module Test(S : SEMANTICS) : sig end = struct
+ type result = True | False | Fail
+ let print_result res = match res with True -> print_string "true" | False -> print_string "false" | Fail -> print_string "failure"
+
+ let check name expected expr =
+ (match (try Some (S.run expr) with Not_found -> None) with
+ | Some true -> if expected = True then true else begin print_string "Sentence \""; print_string name; print_string "\" failed: got true but expected "; print_result expected; print_newline (); false end
+ | Some false -> if expected = False then true else begin print_string "Sentence \""; print_string name; print_string "\" failed: got false but expected "; print_result expected; print_newline (); false end
+ | None -> if expected = Fail then true else begin print_string "Sentence \""; print_string name; print_string "\" failed: got failure but expected "; print_result expected; print_newline (); false end)
+(*
+ with List.Short_list -> begin print_string "Sentence \""; print_string name; print_string "\" failed: got Short_list but expected "; print_result expected; print_newline (); false end
+ with Failure "Unimplemented" -> begin print_string "Sentence \""; print_string name; print_endline "\" unimplemented."; true end
+*)
+
+ let dynamic res = if S.dynamic then res else Fail
+
+ let truth = S.(male bill)
+ let falsehood = S.(female bill)
+ let bool_results =
+ [ check "true" True truth
+ ; check "false" False falsehood
+ ; check "true and true" True S.(truth &&& truth)
+ ; check "true and false" False S.(truth &&& falsehood)
+ ; check "false and true" False S.(falsehood &&& truth)
+ ; check "false and false" False S.(falsehood &&& falsehood)
+ ; check "true or true" True S.(truth ||| truth)
+ ; check "true or false" True S.(truth ||| falsehood)
+ ; check "false or true" True S.(falsehood ||| truth)
+ ; check "false or false" False S.(falsehood ||| falsehood)
+ ; check "true >>> true" True S.(truth >>> truth)
+ ; check "true >>> false" False S.(truth >>> falsehood)
+ ; check "false >>> true" True S.(falsehood >>> truth)
+ ; check "false >>> false" True S.(falsehood >>> falsehood)
+ ]
+ let () = print_newline(); print_int (List.count not bool_results); print_endline " boolean test(s) failed."
+
+ let results =
+ [ check "1. Bill is male" True S.(male bill)
+ ; check "2. Bill is female" False S.(female bill)
+ ; check "3. Bill isn't female" True S.(~~~ (female bill))
+ ; check "4. Carol didn't leave" False S.(~~~ (left carol))
+ ; S.extensional || check "5. Maybe Carol didn't leave" True S.(maybe (~~~ (left carol)))
+ ; S.extensional || check "6. Maybe Ann didn't leave" False S.(maybe (~~~ (left ann)))
+
+ ; check "7. Some x. x is male" True S.(some 'x' (male getx))
+ ; check "8. Some x. x isn't female" True S.(some 'x' (~~~ (female getx)))
+ ; check "9. Some x. x left" True S.(some 'x' (left getx))
+ ; check "10. Some x. x didn't leave" False S.(some 'x' (~~~ (left getx)))
+ ; check "11. Every x. x left" True S.(every 'x' (left getx))
+ ; check "12. Every x. x is female" False S.(every 'x' (female getx))
+ ; check "13. Every x. x isn't male" False S.(every 'x' (~~~ (male getx)))
+ ; check "14. (Some x. x is male) and Ann is female" True S.(some 'x' (male getx) &&& female ann)
+ ; check "15. Some x. (x is male and Ann is female)" True S.(some 'x' (male getx &&& female ann))
+
+ ; check "16. Some x. (x is male and x is female)" False S.(some 'x' (male getx &&& female getx))
+ ; check "17. Some x. (x is male) and Some x. x is female" True S.(some 'x' (male getx) &&& some 'x' (female getx))
+
+ ; check "18. Some x. (x is male and Some y. y is male)" True S.(some 'x' (male getx &&& some 'y' (male gety)))
+ ; check "19. Some x. (x is male and Some y. y is female)" True S.(some 'x' (male getx &&& some 'y' (female gety)))
+ ; check "20. Some x. (x is male and Some y. x is male)" True S.(some 'x' (male getx &&& some 'y' (male getx)))
+ ; check "21. Some x. (x is male and Some y. x is female)" False S.(some 'x' (male getx &&& some 'y' (female getx)))
+ ; check "22. Some x. (x is male and Some y. x isn't female)" True S.(some 'x' (male getx &&& some 'y' (~~~ (female getx))))
+ ; check "23. Some x. (x is male and Some x. x is female)" True S.(some 'x' (male getx &&& some 'x' (female getx)))
+
+ ; check "24. Some x. (x is male) and Some y. (y is female and Bill is male)" True S.(some 'x' (male getx) &&& some 'y' (male gety &&& male bill))
+ ; check "25. Some x. (x is male and Some y. (y is female and Bill is male))" True S.(some 'x' (male getx &&& some 'y' (female gety &&& male bill)))
+ ; check "26. Some x. (x is male and Some y. (y is male and Bill is male))" True S.(some 'x' (male getx &&& some 'y' (male gety &&& male bill)))
+ ; check "27. Some x. (x is male and Some y. (x is female and Bill is male))" False S.(some 'x' (male getx &&& some 'y' (female getx &&& male bill)))
+ ; check "28. Some x. (x is male and Some y. (x isn't female and Bill is male))" True S.(some 'x' (male getx &&& some 'y' (~~~ (female getx) &&& male bill)))
+ ; check "29. Some x. (x is male and Some y. (x is male and Bill is male))" True S.(some 'x' (male getx &&& some 'y' (male getx &&& male bill)))
+
+ ; check "30. Some x. (x is male and Some y. (y is female and x isn't female))" True S.(some 'x' (male getx &&& some 'y' (female gety &&& ~~~ (female getx))))
+ ; check "31. Some x. (x is male and Some y. (y is female and x is single))" True S.(some 'x' (male getx &&& some 'y' (female gety &&& single getx)))
+ ; check "32. Some x. (x is male and Some y. (y is female and x isn't single))" True S.(some 'x' (male getx &&& some 'y' (female gety &&& ~~~ (single getx))))
+ ; check "33. Some x. (x is male and Some y. (y is male and x is single))" True S.(some 'x' (male getx &&& some 'y' (male gety &&& single getx)))
+ ; check "34. Some x. (x is male and Some y. (y is male and x isn't single))" True S.(some 'x' (male getx &&& some 'y' (male gety &&& ~~~ (single getx))))
+
+ ; check "35. Some x. (x is male and Some y. (x is female and x is single))" False S.(some 'x' (male getx &&& some 'y' (female getx &&& single getx)))
+ ; check "36. Some x. (x is male and Some y. (x is female and x isn't single))" False S.(some 'x' (male getx &&& some 'y' (female getx &&& ~~~ (single getx))))
+ ; check "37. Some x. (x is male and Some y. (x is male and x is single))" True S.(some 'x' (male getx &&& some 'y' (male getx &&& single getx)))
+ ; check "38. Some x. (x is male and Some y. (x is male and x isn't single))" True S.(some 'x' (male getx &&& some 'y' (male getx &&& ~~~ (single getx))))
+
+ ; check "39. (Some x. male x) and x left" (dynamic True) S.(some 'x' (male getx) &&& left getx)
+ ; check "40. (Some x. male x) and female x" (dynamic False) S.(some 'x' (male getx) &&& female getx)
+ ; check "41. (Some x. male x) and Some y. female x" (dynamic False) S.(some 'x' (male getx) &&& some 'y' (female getx))
+ ; check "42. (Some x. male x) and Some y. male x" (dynamic True) S.(some 'x' (male getx) &&& some 'y' (male getx))
+ ; check "43. (Some x. male x) and Some y. (female x and male Bill)" (dynamic False) S.(some 'x' (male getx) &&& some 'y' (female getx &&& male bill))
+ ; check "44. (Some x. male x) and Some y. (male x and male Bill)" (dynamic True) S.(some 'x' (male getx) &&& some 'y' (male getx &&& male bill))
+ ; check "45. (Some x. male x) and Some y. (female y and x isn't single)" (dynamic True) S.(some 'x' (male getx) &&& some 'y' (female gety &&& ~~~ (single getx)))
+ ; check "46. (Some x. male x) and Some y. (female x and x isn't single)" (dynamic False) S.(some 'x' (male getx) &&& some 'y' (female getx &&& ~~~ (single getx)))
+ ; check "47. (Some x. male x) and Some y. (male x and x isn't single)" (dynamic True) S.(some 'x' (male getx) &&& some 'y' (male getx &&& ~~~ (single getx)))
+
+ ; check "48. Every x. (male x and (Some y. married y x) -> loves y x)" (dynamic True) S.(every 'x' (male getx &&& some 'y' (marriedto gety getx) >>> loves gety getx))
+ ; check "49. Every x. (male x and (Some y. married y x) -> kisses y x)" (dynamic False) S.(every 'x' (male getx &&& some 'y' (marriedto gety getx) >>> kisses gety getx))
+ ; check "50. (Some x. (male x and Some y. married y x)) -> loves y x" (dynamic True) S.(some 'x' (male getx &&& some 'y' (marriedto gety getx)) >>> loves gety getx)
+ ; check "51. (Some x. (male x and Some y. married y x)) -> kisses y x" (dynamic False) S.(some 'x' (male getx &&& some 'y' (marriedto gety getx)) >>> kisses gety getx)
+
+ ; check "52. Every x. (male x and Some y. (female y and (x = frank or married y x)) -> loves y x)" (dynamic True) S.(every 'x' (male getx &&& some 'y' (female gety &&& (getx === frank ||| marriedto gety getx)) >>> loves gety getx))
+ ; check "53. Every x. (male x and (x = frank or Some y. married y x) -> loves y x)" (dynamic Fail) S.(every 'x' (male getx &&& (getx === frank ||| some 'y' (marriedto gety getx)) >>> loves gety getx))
+ ; check "54. Every x. (male x and (Some y. (x = frank and female y) or Some y. married y x) -> loves y x)" (dynamic Fail) S.(every 'x' (male getx &&& (some 'y' (getx === frank &&& female gety) ||| some 'y' (marriedto gety getx)) >>> loves gety getx))
+ ; check "55. Every x. (male x and ((x = frank and Some y. female y) or Some y. married y x) -> loves y x)" (dynamic Fail) S.(every 'x' (male getx &&& ((getx === frank &&& some 'y' (female gety)) ||| some 'y' (marriedto gety getx)) >>> loves gety getx))
+ ]
+ let () = print_newline(); print_int (List.count not results); print_endline " test(s) failed."
+
+end
+
+
+
+
+
+
+module R = Monad.Reader(struct type env = identifier -> entity end)
+module S = Monad.State(struct type store = identifier -> entity end)
+module S' = Monad.State(struct type store = identifier -> int end)
+module R' = Monad.Reader(struct type env = identifier -> int end)
+
+let env0 = fun _ -> raise Not_found
+let lookup (sought : identifier) env = env sought
+let lookup_string (sought : identifier) env = try string_of_entity (env sought) with Not_found -> "*"
+let print_lookup c env = print_string (lookup_string c env)
+let insert (var : identifier) who env = fun sought -> if sought = var then who else env sought
+
+module Y = Monad.Reader(struct type env = world end)
+
+module L = Monad.List
+
+module RY = struct
+ include R.T(Y)
+ include Monad.Derive.Reader_dbl(Y)(R.T(Y))
+end
+module YR = struct
+ include Y.T(R)
+ include Monad.Derive.Reader_dbl(R)(Y.T(R))
+end
+module LR = struct
+ include L.T(R)
+ include Monad.Derive.Reader(R)(L.T(R))
+end
+module LY = struct
+ include L.T(Y)
+ include Monad.Derive.Reader(Y)(L.T(Y))
+end
+module RL = struct
+ include R.M(L)
+ include Monad.Derive.List(L)(R.M(L))
+end
+module YL = struct
+ include Y.M(L)
+ include Monad.Derive.List(L)(Y.M(L))
+end
+
+module SY = struct
+ include S.T(Y)
+ include Monad.Derive.Reader(Y)(S.T(Y))
+end
+module YS = struct
+ include Y.T(S)
+ include Monad.Derive.State(S)(Y.T(S))
+end
+module LS = struct
+ include L.T(S)
+ include Monad.Derive.State(S)(L.T(S))
+end
+module LY = struct
+ include L.T(Y)
+ include Monad.Derive.Reader(Y)(L.T(Y))
+end
+module SL = struct
+ include S.M(L)
+ include Monad.Derive.List(L)(S.M(L))
+end
+module YL = struct
+ include Y.M(L)
+ include Monad.Derive.List(L)(Y.M(L))
+end
+
+module S'Y = struct
+ include S'.T(Y)
+ include Monad.Derive.Reader(Y)(S'.T(Y))
+end
+module YS' = struct
+ include Y.T(S')
+ include Monad.Derive.State(S')(Y.T(S'))
+end
+module LS' = struct
+ include L.T(S')
+ include Monad.Derive.State(S')(L.T(S'))
+end
+module S'L = struct
+ include S'.M(L)
+ include Monad.Derive.List(L)(S'.M(L))
+end
+
+module LRY = struct
+ include L.T(RY)
+ include Monad.Derive.Reader2(RY)(L.T(RY))
+end
+module LYR = struct
+ include L.T(YR)
+ include Monad.Derive.Reader2(YR)(L.T(YR))
+end
+module RLY = struct
+ include R.M(LY)
+ include Monad.Derive.List(LY)(R.M(LY))
+ include Monad.Derive.Reader_dbl(LY)(R.M(LY))
+end
+module RYL = struct
+ include R.M(YL)
+ include Monad.Derive.List(YL)(R.M(YL))
+ include Monad.Derive.Reader_dbl(YL)(R.M(YL))
+end
+module YLR = struct
+ include Y.M(LR)
+ include Monad.Derive.List(LR)(Y.M(LR))
+ include Monad.Derive.Reader_dbl(LR)(Y.M(LR))
+end
+module YRL = struct
+ include Y.M(RL)
+ include Monad.Derive.List(RL)(Y.M(RL))
+ include Monad.Derive.Reader_dbl(RL)(Y.M(RL))
+end
+
+module LSY = struct
+ include L.T(SY)
+ include Monad.Derive.Reader(SY)(L.T(SY))
+ include Monad.Derive.State(SY)(L.T(SY))
+end
+module LYS = struct
+ include L.T(YS)
+ include Monad.Derive.Reader(YS)(L.T(YS))
+ include Monad.Derive.State(YS)(L.T(YS))
+end
+module SLY = struct
+ include S.M(LY)
+ include Monad.Derive.List(LY)(S.M(LY))
+ include Monad.Derive.Reader(LY)(S.M(LY))
+end
+module SYL = struct
+ include S.M(YL)
+ include Monad.Derive.List(YL)(S.M(YL))
+ include Monad.Derive.Reader(YL)(S.M(YL))
+end
+module YLS = struct
+ include Y.M(LS)
+ include Monad.Derive.List(LS)(Y.M(LS))
+ include Monad.Derive.State(LS)(Y.M(LS))
+end
+module YSL = struct
+ include Y.M(SL)
+ include Monad.Derive.List(SL)(Y.M(SL))
+ include Monad.Derive.State(SL)(Y.M(SL))
+end
+
+module LS'Y = struct
+ include L.T(S'Y)
+ include Monad.Derive.Reader(S'Y)(L.T(S'Y))
+ include Monad.Derive.State(S'Y)(L.T(S'Y))
+end
+module LYS' = struct
+ include L.T(YS')
+ include Monad.Derive.Reader(YS')(L.T(YS'))
+ include Monad.Derive.State(YS')(L.T(YS'))
+end
+module S'LY = struct
+ include S'.M(LY)
+ include Monad.Derive.List(LY)(S'.M(LY))
+ include Monad.Derive.Reader(LY)(S'.M(LY))
+end
+module S'YL = struct
+ include S'.M(YL)
+ include Monad.Derive.List(YL)(S'.M(YL))
+ include Monad.Derive.Reader(YL)(S'.M(YL))
+end
+module YLS' = struct
+ include Y.M(LS')
+ include Monad.Derive.List(LS')(Y.M(LS'))
+ include Monad.Derive.State(LS')(Y.M(LS'))
+end
+module YS'L = struct
+ include Y.M(S'L)
+ include Monad.Derive.List(S'L)(Y.M(S'L))
+ include Monad.Derive.State(S'L)(Y.M(S'L))
+end
+
+
+module Sem1a = struct
+ let dynamic = false
+ let extensional = true
+
+ (* We use monad R, with env = var -> entity.
+ Types of sentences are env -> bool. *)
+ module X = R
+ type noun = entity X.t
+ type sent = bool X.t
+ let run (xx : sent) : bool = X.(run xx env0 = true)
+ let getx = X.(asks (lookup 'x'))
+ let gety = X.(asks (lookup 'y'))
+ let getz = X.(asks (lookup 'z'))
+ let let_ c (xx : noun) (body : sent) = X.(xx >>= fun x -> shift (insert c x) body)
+
+ let (~~~) xx = X.(map not xx)
+ let (&&&) xx yy = X.(xx >>= fun b' -> if not b' then mid false else yy)
+ let (|||) xx yy = X.(xx >>= fun b' -> if b' then mid true else yy)
+ let (>>>) xx yy = X.(xx >>= fun b' -> if not b' then mid true else yy)
+
+ let some c (body : sent) =
+ let (bbs : bool X.t list) = List.map (fun x -> let_ c X.(mid x) body) domain in
+ let (bsb : bool list X.t) = X.seq bbs in
+ let (bb : bool X.t) = X.map (exists ident) bsb in
+ bb
+ let every c (body : sent) =
+ let (bbs : bool X.t list) = List.map (fun x -> let_ c X.(mid x) body) domain in
+ let (bsb : bool list X.t) = X.seq bbs in
+ let (bb : bool X.t) = X.map (for_all ident) bsb in
+ bb
+
+ module F = Facts(X)
+ let ann = X.(mid Ann) let bill = X.(mid Bill) let carol = X.(mid Carol) let dave = X.(mid Dave) let ella = X.(mid Ella) let frank = X.(mid Frank)
+ let (===) xx yy = X.(map2 (=) xx yy)
+ let male = F.male let female = F.female let single = F.single let left = F.left1
+ let marriedto = F.marriedto let saw = F.saw1 let kisses = F.kisses1 let loves = F.loves1
+ let thinks pp xx = failwith "Unimplemented"
+ let maybe pp = failwith "Unimplemented"
+end (* Sem1a *)
+
+module Sem1b = struct
+ let dynamic = false
+ let extensional = true
+
+ (* We again use monad R, with env = var -> entity.
+ This variant defines sentence meanings as Kleisli arrows, that is:
+ type sent = bool -> bool X.t
+ or equivalently, bool -> (env -> bool). A true sentence takes any bool
+ input to a boxed version of that input (so truth = mid), and a false
+ sentence takes any input to mid false.
+ This more closely parallels the dynamic semantics (though it should not,
+ just on account of that structural similarity, be itself counted as dynamic).
+ It also brings the boolean operations closer to monadic primitives.
+ *)
+ module X = R
+ type noun = entity X.t
+ type sent = bool -> bool X.t
+ let run (k : sent) : bool = X.(run (k true) env0 = true)
+ let getx = X.(asks (lookup 'x'))
+ let gety = X.(asks (lookup 'y'))
+ let getz = X.(asks (lookup 'z'))
+ let let_ c (xx : noun) (body : sent) = fun b -> X.(xx >>= fun x -> shift (insert c x) (body b))
+
+ let (~~~) k = fun b -> X.(if b then map not (k true) else mid false)
+ let (&&&) k j = X.(k >=> j)
+ let (|||) k j = ~~~ (~~~ k &&& ~~~ j)
+ let (>>>) k j = ~~~ k ||| j
+(* or
+ let (|||) xx yy = fun b -> X.(xx b >>= fun b' -> if b' then mid true else yy b)
+ let (>>>) xx yy = fun b -> X.(xx b >>= fun b' -> if not b' then mid true else yy b)
+ let (>>>) k j = ~~~ (k &&& ~~~ j)
+*)
+
+ let some c (body : sent) = fun b ->
+ let (bbs : bool X.t list) = List.map (fun x -> let_ c X.(mid x) body b) domain in
+ let (bsb : bool list X.t) = X.seq bbs in
+ let (bb : bool X.t) = X.map (exists ident) bsb in
+ bb
+ let every c (body : sent) = fun b ->
+ let (bbs : bool X.t list) = List.map (fun x -> let_ c X.(mid x) body b) domain in
+ let (bsb : bool list X.t) = X.seq bbs in
+ let (bb : bool X.t) = X.map (for_all ident) bsb in
+ bb
+
+ module F = Facts(X)
+ let to_kleisli xx = fun b -> X.(xx >>= fun b' -> mid (b && b'))
+ let ann = X.(mid Ann) let bill = X.(mid Bill) let carol = X.(mid Carol) let dave = X.(mid Dave) let ella = X.(mid Ella) let frank = X.(mid Frank)
+ let (===) xx yy = to_kleisli X.(map2 (=) xx yy)
+ let male = to_kleisli % F.male let female = to_kleisli % F.female let single = to_kleisli % F.single let left = to_kleisli % F.left1
+ let marriedto yy xx = to_kleisli (F.marriedto yy xx) let saw yy xx = to_kleisli (F.saw1 yy xx) let kisses yy xx = to_kleisli (F.kisses1 yy xx) let loves yy xx = to_kleisli (F.loves1 yy xx)
+ let thinks pp xx = fun b -> failwith "Unimplemented"
+ let maybe pp = fun b -> failwith "Unimplemented"
+end (* Sem1b *)
+
+module Sem2a = struct
+ let dynamic = false
+ let extensional = true
+
+ (* We could use either monad RL or LR, with type env = var -> entity.
+ Their box type is the same: env -> ['a]
+ However, the types of SL and LS differ, and the latter is more suitable for the dynamic version. So to keep things maximally parallel, we'll use LR here.
+ We use the box type in two ways: first, we use a box(entity) to compute whether a matrix
+ clause is satisfied by a bound pronoun, where entity ranges over the whole domain.
+ Second, it is convenient and more consonant with later strategies
+ to re-use the same monad for sentence types (rather than using a simpler monad
+ that lacks a List component). Here we will let the types of sentences
+ be box(bool), that is: env -> [bool]. We will understand the sentence to be true
+ if there are ANY truths in the resulting list. A list of all falses is treated
+ the same as an empty list. Sem2c, below, eliminates this artifact by changing
+ the sentence type to box(unit). Then truths (rel to an env) are [();...] and
+ falsehoods are [].
+*)
+ module X = LR
+ type noun = entity X.t
+ type sent = bool X.t
+ let run (xx : sent) : bool = X.(any_truths (run xx env0))
+ (* lift an 'a list to a single 'a X.t *)
+ let mids (xs : 'a list) : 'a X.t = let rec aux xx = function [] -> xx | x::xs -> aux X.(xx ++ mid x) xs in aux X.mzero xs
+ let getx = X.(asks (lookup 'x'))
+ let gety = X.(asks (lookup 'y'))
+ let getz = X.(asks (lookup 'z'))
+ let let_ c (xx : noun) (body : sent) = X.(xx >>= fun x -> shift (insert c x) body)
+
+ let (~~~) xx = X.(map not xx)
+ let (&&&) xx yy = X.(xx >>= fun b' -> if not b' then mid false else yy)
+ let (|||) xx yy = X.(xx >>= fun b' -> if b' then mid true else yy)
+ let (>>>) xx yy = X.(xx >>= fun b' -> if not b' then mid true else yy)
+
+ (* On this semantics, `some c body` is a list of the boolean outcomes for body for each assignment to c.
+ That matches our convention for sentence types, where any truth in the list means the sentence is true.
+ However, we can't then define `every c body === ~~~ (some c (~~~ body))`, because it's only when the rhs is entirely true that the lhs should be true.
+ In later semantics, the duality of `some` and `every` will be restored.
+ *)
+ let some c (body : sent) = X.(let_ c (mids domain) body)
+ let every c body = X.(let xx = let_ c (mids domain) body in list_map (fun xs -> if all_truths xs then xs else []) xx) (* could alternatively return [true] instead of xs *)
+
+ module F = Facts(X)
+ let ann = X.(mid Ann) let bill = X.(mid Bill) let carol = X.(mid Carol) let dave = X.(mid Dave) let ella = X.(mid Ella) let frank = X.(mid Frank)
+ let (===) xx yy = X.(map2 (=) xx yy)
+ let male = F.male let female = F.female let single = F.single let left = F.left1
+ let marriedto = F.marriedto let saw = F.saw1 let kisses = F.kisses1 let loves = F.loves1
+ let thinks pp xx = failwith "Unimplemented"
+ let maybe pp = failwith "Unimplemented"
+end (* Sem2a *)
+
+(* Sem2b would convert Sem2a into having sentence meanings be Kleisli arrows, as Sem1b did.
+ Not here implemented. *)
+
+(* Variant of Sem2a, which uses [();...] vs [] instead of [true;...] vs (list of all false OR []). *)
+module Sem2c = struct
+ let dynamic = false
+ let extensional = true
+
+ (* We use monad LR as above, with same env = var -> entity and box type = env -> ['a].
+ We again use box(entity) to compute whether matrix clauses are satisfied by
+ bound pronouns; but now we use box(unit) for the types of sentences.
+ Truths (rel to an env) are [();...] and falsehood is [].
+ *)
+ module X = LR
+ type noun = entity X.t
+ type sent = unit X.t
+ let run (xx : sent) : bool = X.(not (List.is_null (run xx env0)))
+ (* lift an 'a list to a single 'a X.t *)
+ let mids (xs : 'a list) : 'a X.t = let rec aux xx = function [] -> xx | x::xs -> aux X.(xx ++ mid x) xs in aux X.mzero xs
+ let getx = X.(asks (lookup 'x'))
+ let gety = X.(asks (lookup 'y'))
+ let getz = X.(asks (lookup 'z'))
+ let let_ c (xx : noun) (body : sent) = X.(xx >>= fun x -> shift (insert c x) body)
+ let to_unit (x : bool) : unit X.t = X.guard x
+
+ let (~~~) xx = X.(list_map (fun xs -> if is_null xs then [()] else []) xx)
+ let (&&&) xx yy = X.(xx >> yy)
+ let (|||) xx yy = X.(xx ++ (* ~~~ xx >> *) yy)
+ let (>>>) xx yy = X.(~~~ xx ++ yy)
+(* or
+ let (>>>) xx yy = X.(~~~ (xx >> ~~~ yy))
+*)
+
+ let some c (body : sent) = X.(let_ c (mids domain) body)
+ let every c (body : sent) = ~~~ (some c (~~~ body))
+
+ module F = Facts(X)
+ let ann = X.(mid Ann) let bill = X.(mid Bill) let carol = X.(mid Carol) let dave = X.(mid Dave) let ella = X.(mid Ella) let frank = X.(mid Frank)
+ let (===) xx yy = X.(map2 (=) xx yy >>= to_unit)
+ let male xx = X.(F.male xx >>= to_unit)
+ let female xx = X.(F.female xx >>= to_unit)
+ let single xx = X.(F.single xx >>= to_unit)
+ let left xx = X.(F.left1 xx >>= to_unit)
+ let marriedto yy xx = X.(F.marriedto yy xx >>= to_unit)
+ let saw yy xx = X.(F.saw1 yy xx >>= to_unit)
+ let kisses yy xx = X.(F.kisses1 yy xx >>= to_unit)
+ let loves yy xx = X.(F.loves1 yy xx >>= to_unit)
+ let thinks pp xx = failwith "Unimplemented"
+ let maybe pp = failwith "Unimplemented"
+end (* Sem2c *)
+
+(* Sem2d would convert Sem2c into having sentence meanings be Kleisli arrows, as Sem1b did.
+ Not here implemented. *)
+
+(* Add intensionality to 2a *)
+module Sem3a = struct
+ let dynamic = false
+ let extensional = false
+
+ (* Using monad LRY, with type env = var -> entity.
+ Box type is env -> world -> ['a]
+ Types of sentences are env -> world -> [bool]. *)
+ module X = LRY
+ type noun = entity X.t
+ type sent = bool X.t
+ let run xx = X.(any_truths (run xx env0 Actual))
+ (* lift an 'a list to a single 'a X.t *)
+ let mids (xs : 'a list) : 'a X.t = let rec aux xx = function [] -> xx | x::xs -> aux X.(xx ++ mid x) xs in aux X.mzero xs
+ let getx = X.(asks (lookup 'x'))
+ let gety = X.(asks (lookup 'y'))
+ let getz = X.(asks (lookup 'z'))
+ let getw = X.(uask) (* get world from the underlying Y monad *)
+ (* select an intranstive verb based on the world *)
+ let select1 f1 f2 f3 xx = X.(getw >>= fun w -> (if w = Actual then f1 else if w = Other then f2 else f3) xx)
+ (* select a transitive verb based on the world *)
+ let select2 f1 f2 f3 yy xx = X.(getw >>= fun w -> (if w = Actual then f1 else if w = Other then f2 else f3) yy xx)
+ let let_ c (xx : noun) (body : sent) = X.(xx >>= fun x -> shift (insert c x) body)
+ let letw world (body : sent) = X.(ushift (fun _ -> world) body) (* shift the "env" of the underlying Y monad *)
+
+ let (~~~) xx = X.(map not xx)
+ let (&&&) xx yy = X.(xx >>= fun b' -> if not b' then mid false else yy)
+ let (|||) xx yy = X.(xx >>= fun b' -> if b' then mid true else yy)
+ let (>>>) xx yy = X.(xx >>= fun b' -> if not b' then mid true else yy)
+
+ let some c (body : sent) = X.(let_ c (mids domain) body)
+ let every c (body : sent) = X.(let xx = let_ c (mids domain) body in list_map (fun xs -> if all_truths xs then xs else []) xx)
+
+ module F = Facts(X)
+ let ann = X.(mid Ann) let bill = X.(mid Bill) let carol = X.(mid Carol) let dave = X.(mid Dave) let ella = X.(mid Ella) let frank = X.(mid Frank)
+ let (===) xx yy = X.(map2 (=) xx yy)
+ let male = F.male let female = F.female let single = F.single
+ let left xx = select1 F.left1 F.left2 F.left3 xx
+ let saw yy xx = select2 F.saw1 F.saw2 F.saw3 yy xx
+ let marriedto = F.marriedto
+ let kisses yy xx = select2 F.kisses1 F.kisses2 F.kisses3 yy xx
+ let loves yy xx = select2 F.loves1 F.loves2 F.loves3 yy xx
+ let thinks pp xx = failwith "Unimplemented"
+ let maybe (body : sent) : sent =
+ let (yy : R.env -> Y.env -> bool list) = fun e w ->
+ let body_int = List.map (fun w' -> any_truths (X.run (letw w' body) e w)) modal_domain in
+ body_int (* can just use body's intension as the result of `maybe body` *) in
+ Obj.magic yy
+end (* Sem3a *)
+
+(* Sem3b would convert Sem3a into having sentence meanings be Kleisli arrows, as Sem1b did.
+ Not here implemented. *)
+
+(* Add intensionality to 2c *)
+module Sem3c = struct
+ let dynamic = false
+ let extensional = false
+
+ (* Using monad LRY, with type env = var -> entity.
+ Box type is env -> world -> ['a]
+ Types of sentences are env -> world -> [unit]. *)
+ module X = LRY
+ type noun = entity X.t
+ type sent = unit X.t
+ let run xx = X.(not (List.is_null (run xx env0 Actual)))
+ (* lift an 'a list to a single 'a X.t *)
+ let mids (xs : 'a list) : 'a X.t = let rec aux xx = function [] -> xx | x::xs -> aux X.(xx ++ mid x) xs in aux X.mzero xs
+ let getx = X.(asks (lookup 'x'))
+ let gety = X.(asks (lookup 'y'))
+ let getz = X.(asks (lookup 'z'))
+ let getw = X.(uask) (* get world from the underlying Y monad *)
+ (* select an intranstive verb based on the world *)
+ let select1 f1 f2 f3 xx = X.(getw >>= fun w -> (if w = Actual then f1 else if w = Other then f2 else f3) xx)
+ (* select a transitive verb based on the world *)
+ let select2 f1 f2 f3 yy xx = X.(getw >>= fun w -> (if w = Actual then f1 else if w = Other then f2 else f3) yy xx)
+ let let_ c (xx : noun) (body : sent) = X.(xx >>= fun x -> shift (insert c x) body)
+ let letw world (body : sent) = X.(ushift (fun _ -> world) body) (* shift the "env" of the underlying Y monad *)
+ let to_unit (x : bool) : unit X.t = X.guard x
+
+ let (~~~) xx = X.(list_map (fun xs -> if is_null xs then [()] else []) xx)
+ let (&&&) xx yy = X.(xx >> yy)
+ let (|||) xx yy = X.(xx ++ (* ~~~ xx >> *) yy)
+ let (>>>) xx yy = X.(~~~ xx ++ yy)
+(* or
+ let (>>>) xx yy = X.(~~~ (xx >> ~~~ yy))
+*)
+
+ let some c (body : sent) = X.(let_ c (mids domain) body)
+ let every c (body : sent) = ~~~ (some c (~~~ body))
+
+ module F = Facts(X)
+ let ann = X.(mid Ann) let bill = X.(mid Bill) let carol = X.(mid Carol) let dave = X.(mid Dave) let ella = X.(mid Ella) let frank = X.(mid Frank)
+ let (===) xx yy = X.(map2 (=) xx yy >>= to_unit)
+ let male xx = X.(F.male xx >>= to_unit)
+ let female xx = X.(F.female xx >>= to_unit)
+ let single xx = X.(F.single xx >>= to_unit)
+ let left xx = X.(select1 F.left1 F.left2 F.left3 xx >>= to_unit)
+ let saw yy xx = X.(select2 F.saw1 F.saw2 F.saw3 yy xx >>= to_unit)
+ let marriedto yy xx = X.(F.marriedto yy xx >>= to_unit)
+ let kisses yy xx = X.(select2 F.kisses1 F.kisses2 F.kisses3 yy xx >>= to_unit)
+ let loves yy xx = X.(select2 F.loves1 F.loves2 F.loves3 yy xx >>= to_unit)
+ let thinks pp xx = failwith "Unimplemented"
+ let maybe (body : sent) : sent =
+ let (yy : R.env -> Y.env -> unit list) = fun e w ->
+ let body_int = List.map (fun w' -> not @@ List.is_null @@ X.run (letw w' body) e w) modal_domain in
+ if any_truths body_int then [()] else [] in
+ Obj.magic yy
+end (* Sem3c *)
+
+(* Sem3d would convert Sem3c into having sentence meanings be Kleisli arrows, as Sem1b did.
+ Not here implemented. *)
+
+
+(* Dynamic version of Sem2c *)
+module Sem5c = struct
+ let dynamic = true
+ let extensional = true
+
+ (* This needs to use monad SL, with store = var -> entity
+ and box type = store -> ['a,store]
+ Sentence meaning is box(unit).
+ Later strategies with more complex sentence meanings and stores
+ may be able to use monad LS, with box type store -> ['a],store
+ *)
+ module X = SL
+ type noun = entity X.t
+ type sent = unit X.t
+ let run (xx : sent) : bool = X.(not (List.is_null (run xx env0)))
+ (* lift an 'a list to a single 'a X.t *)
+ let mids (xs : 'a list) : 'a X.t = let rec aux xx = function [] -> xx | x::xs -> aux X.(xx ++ mid x) xs in aux X.mzero xs
+ let getx = X.(gets (lookup 'x'))
+ let gety = X.(gets (lookup 'y'))
+ let getz = X.(gets (lookup 'z'))
+ let let_ c (xx : noun) (body : sent) = X.(xx >>= fun x -> modify (insert c x) >> body)
+ let to_unit (x : bool) : unit X.t = X.guard x
+(*
+ let peek msg () = X.(get >>= fun s -> begin print_string msg; print_string ": x="; print_lookup 'x' s; print_string ", y="; print_lookup 'y' s; print_string ", z="; print_lookup 'z' s; print_newline (); mid () end)
+*)
+
+ let (~~~) (xx : sent) : sent =
+ let yy : S.store -> (unit * S.store) list = fun s -> if List.is_null (X.run xx s) then [(),s] else [] in
+ Obj.magic yy (* this is an identity function that changes the type of yy to a unit X.t *)
+ let (&&&) xx yy = X.(xx >> yy)
+ let (|||) xx yy = ~~~ (~~~ xx &&& ~~~ yy)
+ let (>>>) xx yy = X.(~~~ (xx >> ~~~ yy))
+
+(*
+ This would propagate effects out of the disjuncts, so that for example after
+ "Some y. (x = frank and female y) or Some y. married y x"
+ "y" would be available for anaphor:
+ let (|||) xx yy = X.(xx ++ (~~~ xx >> yy))
+
+ This wouldn't propagate effects from antecedent to consequent, so that for example
+ "(Some y. marriedto y bill) >>> female gety"
+ has a failed lookup on "y":
+ let (>>>) xx yy = X.(~~~ xx ++ yy)
+*)
+
+ let some c (body : sent) = X.(let_ c (mids domain) body)
+ let every c (body : sent) = ~~~ (some c (~~~ body))
+
+ module F = Facts(X)
+ let ann = X.(mid Ann) let bill = X.(mid Bill) let carol = X.(mid Carol) let dave = X.(mid Dave) let ella = X.(mid Ella) let frank = X.(mid Frank)
+ let (===) xx yy = X.(map2 (=) xx yy >>= to_unit)
+ let male xx = X.(F.male xx >>= to_unit)
+ let female xx = X.(F.female xx >>= to_unit)
+ let single xx = X.(F.single xx >>= to_unit)
+ let left xx = X.(F.left1 xx >>= to_unit)
+ let marriedto yy xx = X.(F.marriedto yy xx >>= to_unit)
+ let saw yy xx = X.(F.saw1 yy xx >>= to_unit)
+ let kisses yy xx = X.(F.kisses1 yy xx >>= to_unit)
+ let loves yy xx = X.(F.loves1 yy xx >>= to_unit)
+ let thinks pp xx = failwith "Unimplemented"
+ let maybe pp = failwith "Unimplemented"
+end (* Sem5c *)
+
+
+(* Dynamic version of Sem3c / Add intensionality to Sem5c *)
+module Sem6c = struct
+ let dynamic = true
+ let extensional = false
+
+ (* This needs to use monad SLY, with store = var -> entity
+ and box type = store -> world -> ['a,store]
+ Sentence meaning is box(unit).
+ Later strategies with more complex sentence meanings and stores
+ may be able to use monad LSY, with box type store -> world -> ['a],store
+ *)
+ module X = SLY
+ type noun = entity X.t
+ type sent = unit X.t
+ let run (xx : sent) : bool = X.(not (List.is_null (run xx env0 Actual)))
+ (* lift an 'a list to a single 'a X.t *)
+ let mids (xs : 'a list) : 'a X.t = let rec aux xx = function [] -> xx | x::xs -> aux X.(xx ++ mid x) xs in aux X.mzero xs
+ let getx = X.(gets (lookup 'x'))
+ let gety = X.(gets (lookup 'y'))
+ let getz = X.(gets (lookup 'z'))
+ let getw = X.(ask) (* get world from the underlying Y monad *)
+ (* select an intranstive verb based on the world *)
+ let select1 f1 f2 f3 xx = X.(getw >>= fun w -> (if w = Actual then f1 else if w = Other then f2 else f3) xx)
+ (* select a transitive verb based on the world *)
+ let select2 f1 f2 f3 yy xx = X.(getw >>= fun w -> (if w = Actual then f1 else if w = Other then f2 else f3) yy xx)
+ let let_ c (xx : noun) (body : sent) = X.(xx >>= fun x -> modify (insert c x) >> body)
+ let letw world (body : sent) = X.(shift (fun _ -> world) body) (* shift the "env" of the underlying Y monad *)
+ let to_unit (x : bool) : unit X.t = X.guard x
+(*
+ let peek msg () = X.(get >>= fun s -> begin print_string msg; print_string ": x="; print_lookup 'x' s; print_string ", y="; print_lookup 'y' s; print_string ", z="; print_lookup 'z' s; print_newline (); mid () end)
+*)
+
+ let (~~~) (xx : sent) : sent =
+ let yy : S.store -> Y.env -> (unit * S.store) list = fun s w -> if List.is_null (X.run xx s w) then [(),s] else [] in
+ Obj.magic yy (* this is an identity function that changes the type of yy to a unit X.t *)
+
+ let (&&&) xx yy = X.(xx >> yy)
+ let (|||) xx yy = ~~~ (~~~ xx &&& ~~~ yy)
+ let (>>>) xx yy = X.(~~~ (xx >> ~~~ yy))
+
+ let some c (body : sent) = X.(let_ c (mids domain) body)
+ let every c (body : sent) = ~~~ (some c (~~~ body))
+
+ module F = Facts(X)
+ let ann = X.(mid Ann) let bill = X.(mid Bill) let carol = X.(mid Carol) let dave = X.(mid Dave) let ella = X.(mid Ella) let frank = X.(mid Frank)
+ let (===) xx yy = X.(map2 (=) xx yy >>= to_unit)
+ let male xx = X.(F.male xx >>= to_unit)
+ let female xx = X.(F.female xx >>= to_unit)
+ let single xx = X.(F.single xx >>= to_unit)
+ let left xx = X.(select1 F.left1 F.left2 F.left3 xx >>= to_unit)
+ let saw yy xx = X.(select2 F.saw1 F.saw2 F.saw3 yy xx >>= to_unit)
+ let marriedto yy xx = X.(F.marriedto yy xx >>= to_unit)
+ let kisses yy xx = X.(select2 F.kisses1 F.kisses2 F.kisses3 yy xx >>= to_unit)
+ let loves yy xx = X.(select2 F.loves1 F.loves2 F.loves3 yy xx >>= to_unit)
+ let thinks pp xx = failwith "Unimplemented"
+ let maybe (body : sent) : sent =
+ let (yy : S.store -> Y.env -> (unit * S.store) list) = fun s w ->
+ let body_int = List.map (fun w' -> not @@ List.is_null @@ X.run (letw w' body) s w) modal_domain in
+ if any_truths body_int then [(),s] else [] in
+ Obj.magic yy
+end (* Sem6c *)
+
+(* Sem6c seems adequate for the phenomena GSV are examining, and is substantially simpler than their own semantics. Sem6c doesn't have their "pegs" and complex two-stage function from vars to referents.
+ Next we develop some semantics that are closer to their actual presentation. *)
+
+(* This develops Sem5c using in part the strategies from Sem1b. *)
+module Sem5e = struct
+ let dynamic = true
+ let extensional = true
+
+ (* Let a topic be sequence of entities introduced into conversation (GSV's pegs -> entities, with pegs construed as positions in the sequence).
+ Then let store = var -> int (that is, position in the topic)
+ Then we can use monad LS', with box type = store -> ['a],store
+ And sentence meanings are Kleisli arrows: topic -> box(topic). The list component
+ in the type captures indeterminacy in what objects are being discussed (introduced
+ by quantifiers). Truths (relative to a initial store and topic) result in
+ non-empty topic lists; falsehoods in empty ones.
+ *)
+ type topic = entity list
+ let topic0 = []
+ module X = LS'
+ type noun = (topic -> entity) X.t
+ type sent = topic -> topic X.t
+ let run (k : sent) : bool = X.(not (List.is_null (fst (run (k topic0) env0))))
+ (* lift an 'a list to a single 'a X.t *)
+ let mids (xs : 'a list) : 'a X.t = let rec aux xx = function [] -> xx | x::xs -> aux X.(xx ++ mid x) xs in aux X.mzero xs
+ let get_nth n topic = try List.nth topic n with List.Short_list -> failwith ("can't get item "^string_of_int n^" of "^List.string_of_list string_of_entity topic)
+ let getx : noun = X.(gets (lookup 'x') >>= fun n -> mid (get_nth n))
+ let gety : noun = X.(gets (lookup 'y') >>= fun n -> mid (get_nth n))
+ let getz : noun = X.(gets (lookup 'z') >>= fun n -> mid (get_nth n))
+ let let_ c (n : int) (body : sent) : sent = fun top -> X.(modify (insert c n) >> (body top))
+(*
+ let lookup_string sought env top = try string_of_entity (List.nth top (env sought)) with Not_found -> "*" | List.Short_list -> "#"
+ let print_lookup sought env top = print_string (lookup_string sought env top)
+ let peek msg top = X.(get >>= fun s -> begin print_string msg; print_string ": x="; print_lookup 'x' s top; print_string ", y="; print_lookup 'y' s top; print_string ", z="; print_lookup 'z' s top; print_newline (); mid top end)
+*)
+
+ let (~~~) (k : sent) : sent = fun top ->
+ let yy : S'.store -> topic list * S'.store = fun s -> if List.is_null (fst (X.run (k top) s)) then ([top],s) else ([],s) in
+ Obj.magic yy (* this is an identity function that changes the type of yy to a topic X.t *)
+ let (&&&) k j = X.(k >=> j)
+ let (|||) k j = ~~~ (~~~ k &&& ~~~ j) (* TODO how about (k >>> j) >>> j *)
+ let (>>>) k j = X.(~~~ (k >=> ~~~ j))
+
+ let some c (body : sent) : sent = fun top ->
+ let n = length top in
+ let aux ent = X.(let_ c n body) (List.snoc top ent) in
+ let domain' = List.map aux domain in
+ X.join (mids domain')
+
+ let every c (body : sent) = ~~~ (some c (~~~ body))
+
+(* TODO
+ let some c body = X.(mids domain >>= fun x -> modify (insert c x) body >>= guard >> mid x)
+ let every c body = X.(let xx = let_ c (mids domain) body in list_map (fun xs -> if all_truths xs then xs else []) xx)
+*)
+
+ module F = Facts(X)
+ let mapply' (ff : noun) (top : topic) : entity X.t = X.(map (fun f -> f top) ff)
+ let wrap name = X.(mid (const name))
+ let wrap1 f xx = fun top -> X.(f (mapply' xx top) >>= fun b -> if b then mid top else mzero)
+ let wrap2 f xx yy = fun top -> X.(f (mapply' xx top) (mapply' yy top) >>= fun b -> if b then mid top else mzero)
+ let ann = wrap Ann let bill = wrap Bill let carol = wrap Carol let dave = wrap Dave let ella = wrap Ella let frank = wrap Frank
+ let (===) (xx : noun) (yy : noun) : sent = wrap2 X.(map2 (=)) xx yy
+ let male (xx : noun) : sent = wrap1 F.male xx
+ let female xx = wrap1 F.female xx
+ let single xx = wrap1 F.single xx
+ let left xx = wrap1 F.left1 xx
+ let marriedto yy xx = wrap2 F.marriedto yy xx
+ let saw yy xx = wrap2 F.saw1 yy xx
+ let kisses yy xx = wrap2 F.kisses1 yy xx
+ let loves yy xx = wrap2 F.loves1 yy xx
+ let thinks pp xx = fun top -> failwith "Unimplemented"
+ let maybe pp = fun top -> failwith "Unimplemented"
+end (* Sem5e *)
+
+(* Add intensionality to Sem5e *)
+module Sem6e = struct
+ let dynamic = true
+ let extensional = false
+
+ type topic = entity list
+ let topic0 = []
+ module X = LS'Y
+ type noun = (topic -> entity) X.t
+ type sent = topic -> topic X.t
+ let run (k : sent) : bool = X.(not (List.is_null (fst (run (k topic0) env0 Actual))))
+ (* lift an 'a list to a single 'a X.t *)
+ let mids (xs : 'a list) : 'a X.t = let rec aux xx = function [] -> xx | x::xs -> aux X.(xx ++ mid x) xs in aux X.mzero xs
+ let get_nth n topic = try List.nth topic n with List.Short_list -> failwith ("can't get item "^string_of_int n^" of "^List.string_of_list string_of_entity topic)
+ let getx : noun = X.(gets (lookup 'x') >>= fun n -> mid (get_nth n))
+ let gety : noun = X.(gets (lookup 'y') >>= fun n -> mid (get_nth n))
+ let getz : noun = X.(gets (lookup 'z') >>= fun n -> mid (get_nth n))
+ let getw = X.(ask) (* get world from the underlying Y monad *)
+ (* select an intranstive verb based on the world *)
+ let select1 f1 f2 f3 xx = X.(getw >>= fun w -> (if w = Actual then f1 else if w = Other then f2 else f3) xx)
+ (* select a transitive verb based on the world *)
+ let select2 f1 f2 f3 yy xx = X.(getw >>= fun w -> (if w = Actual then f1 else if w = Other then f2 else f3) yy xx)
+ let let_ c (n : int) (body : sent) : sent = fun top -> X.(modify (insert c n) >> (body top))
+ let letw world (body : sent) : sent = fun top -> X.(shift (fun _ -> world) (body top)) (* shift the "env" of the underlying Y monad *)
+
+ let (~~~) (k : sent) : sent = fun top ->
+ let yy : S'.store -> Y.env -> topic list * S'.store = fun s w -> if List.is_null (fst (X.run (k top) s w)) then ([top],s) else ([],s) in
+ Obj.magic yy (* this is an identity function that changes the type of yy to a topic X.t *)
+ let (&&&) k j = X.(k >=> j)
+ let (|||) k j = ~~~ (~~~ k &&& ~~~ j)
+ let (>>>) k j = X.(~~~ (k >=> ~~~ j))
+
+ let some c (body : sent) : sent = fun top ->
+ let n = length top in
+ let aux ent = X.(let_ c n body) (List.snoc top ent) in
+ let domain' = List.map aux domain in
+ X.join (mids domain')
+
+ let every c (body : sent) = ~~~ (some c (~~~ body))
+
+ module F = Facts(X)
+ let mapply' (ff : noun) (top : topic) : entity X.t = X.(map (fun f -> f top) ff)
+ let wrap name = X.(mid (const name))
+ let wrap1 f xx = fun top -> X.(f (mapply' xx top) >>= fun b -> if b then mid top else mzero)
+ let wrap2 f xx yy = fun top -> X.(f (mapply' xx top) (mapply' yy top) >>= fun b -> if b then mid top else mzero)
+ let ann = wrap Ann let bill = wrap Bill let carol = wrap Carol let dave = wrap Dave let ella = wrap Ella let frank = wrap Frank
+ let (===) (xx : noun) (yy : noun) : sent = wrap2 X.(map2 (=)) xx yy
+ let male (xx : noun) : sent = wrap1 F.male xx
+ let female xx = wrap1 F.female xx
+ let single xx = wrap1 F.single xx
+ let left xx = wrap1 (select1 F.left1 F.left2 F.left3) xx
+ let marriedto yy xx = wrap2 F.marriedto yy xx
+ let saw yy xx = wrap2 (select2 F.saw1 F.saw2 F.saw3) yy xx
+ let kisses yy xx = wrap2 (select2 F.kisses1 F.kisses2 F.kisses3) yy xx
+ let loves yy xx = wrap2 (select2 F.loves1 F.loves2 F.loves3) yy xx
+ let thinks pp xx = failwith "Unimplemented"
+ let maybe (body : sent) : sent = fun top ->
+ let (yy : S'.store -> Y.env -> topic list * S'.store) = fun s w ->
+ let body_int = List.map (fun w' -> not @@ List.is_null @@ fst @@ X.run (letw w' body top) s w) modal_domain in
+ if any_truths body_int then [top],s else [],s in
+ Obj.magic yy
+end (* Sem6e *)
+
+module TestAll = struct
+ print_endline "\nTesting Sem1a";;
+ module T1a = Test(Sem1a);;
+ print_endline "\nTesting Sem1b";;
+ module T1b = Test(Sem1b);;
+ print_endline "\nTesting Sem2a";;
+ module T2a = Test(Sem2a);;
+ print_endline "\nTesting Sem2c";;
+ module T2c = Test(Sem2c);;
+ print_endline "\nTesting Sem3a";;
+ module T3a = Test(Sem3a);;
+ print_endline "\nTesting Sem3c";;
+ module T3c = Test(Sem3c);;
+ print_endline "\nTesting Sem5c";;
+ module T5c = Test(Sem5c);;
+ print_endline "\nTesting Sem5e";;
+ module T5e = Test(Sem5e);;
+ print_endline "\nTesting Sem6c";;
+ module T6c = Test(Sem6c);;
+ print_endline "\nTesting Sem6e";;
+ module T6e = Test(Sem6e);;
+ print_newline ()
+end
+
+(*
+ One can't test the broken vase case by comparing the _truth_ of any sentences.
+ The difference is in whether the sentences have meanings that are "supported by"
+ the same informtation states. Compare in our model:
+ (i) Someone kissed me. She might have stayed.
+ and:
+ (ii) Someone who might have stayed kissed me.
+ Recall that in our model Ann leaves in every world, but Carol stays in some (non-actual)
+ world. If my background information settles that I was kissed by either Ann or Carol,
+ then I'm in a position to assert (i), since after the first clause it's left open
+ that the referent be either woman. But it doesn't put me in a position to assert (ii),
+ since that implies I was kissed by Carol. So far as truth-value goes,
+ if Carol kissed me both sentences are true, and if Ann did then both sentences are false.
+*)
+