-(* 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.
-*)
+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")))))