1 (* GSV monadically 13 April 2015 *)
4 let any_truths (xs : 'a list) : bool = List.exists ident xs
5 let all_truths (xs : 'a list) : bool = List.for_all ident xs
7 module type SEMANTICS = sig
8 type noun (* this is whatever monadic type the semantics assigns to noun-sized contents *)
9 type sent (* this is whatever monadic type the semantics assigns to sentence-sized contents *)
10 val run : sent -> bool
12 val extensional : bool
14 val getx : noun val gety : noun val getz : noun
15 (* OCaml will parse ~~~ as a prefix operator, but unfortunately won't let you say
16 `~~~ predicate subject`; you have to say `~~~ (predicate subject)`. *)
17 val ( ~~~ ) : sent -> sent
18 (* OCaml will parse these three as infix operators (yay), but makes them all
19 left-associative (ehh for >>>) and have the same precedence (boo). *)
20 val ( &&& ) : sent -> sent -> sent
21 val ( ||| ) : sent -> sent -> sent
22 val ( >>> ) : sent -> sent -> sent
23 (* OCaml parses this with same associativity and precedence as the preceding (boo). *)
24 val (===) : noun -> noun -> sent
25 val ann : noun val bill : noun val carol : noun val dave : noun val ella : noun val frank : noun
26 val male : noun -> sent val female : noun -> sent
27 val left : noun -> sent
28 val single : noun -> sent
29 (* Transitive verbs apply to their direct objs first, subjects second. *)
30 val marriedto : noun -> noun -> sent
31 val saw : noun -> noun -> sent
32 val kisses : noun -> noun -> sent
33 val loves : noun -> noun -> sent (* here construed extensionally *)
34 (* Quantifiers may be unimplemented. *)
35 val some : identifier -> sent -> sent
36 val every : identifier -> sent -> sent
37 (* Intensional verbs and operators may be unimplemented. *)
38 val thinks : sent -> noun -> sent
39 val maybe : sent -> sent
42 type world = Actual | Other | Another
43 let modal_domain = [Actual; Other; Another]
45 type entity = Ann | Bill | Carol | Dave | Ella | Frank
46 let domain = [Ann; Bill; Carol; Dave; Ella; Frank]
47 let string_of_entity = function
54 let print_entity ent = print_string (string_of_entity ent)
56 module Facts(X : Monad.MONAD) = struct
57 (* Here are the atomic facts: Ann and Bill are married, also Carol and Dave.
58 Genders and marital statuses are epistemically necessary.
59 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.
60 In w2, all but Carol left; no one sees anything; all spouses kiss; all men love only Carol and Ella loves the wives.
61 In w3, only Ann and Bill left; no one sees anything; nobody kisses; Frank loves everyone else.
64 let is_male = function Bill | Dave | Frank -> true | _ -> false
65 let are_married = function (Ann, Bill) | (Bill, Ann) | (Carol, Dave) | (Dave, Carol) -> true | _ -> false
66 let is_a_wife = function Ann | Carol -> true | _ -> false
68 let male xx = X.(map is_male xx)
69 let female xx = X.(map (not % is_male) xx)
71 (* Ella and Frank are single *)
72 let single xx = X.(map (fun x -> x > Dave) xx)
74 (* Actually (in w1), everybody left. In w2, everybody but Carol left. In w3, only Ann and Bill left. *)
75 let left1 xx = X.(map (fun _ -> true) xx)
76 let left2 xx = X.(map (fun x -> x <> Carol) xx)
77 let left3 xx = X.(map (fun x -> x = Ann || x = Bill) xx)
79 (* In the sentences, order of application is: TransitiveVerb + Object + Subject.
80 But we convert to logical order for our operations. *)
82 (* Actually, each person saw the people alphabetically before them. In w2 and w3, no one saw anyone. *)
83 let saw1 yy xx = X.(map2 (fun x y -> x < y) xx yy)
84 let saw2 yy xx = X.(map2 (fun _ _ -> false) xx yy)
87 (* Necessarily, Ann and Bill are married to each other; also Carol to Dave. *)
88 let marriedto yy xx = X.(map2 (curry are_married) xx yy)
90 (* Actually, only Carol and Dave kiss. In w2, spouses kiss. In w3, there is no kissing. *)
91 let kisses1 yy xx = X.(map2 (fun x y -> (x = Carol && y = Dave) || (x = Dave && y = Carol)) xx yy)
92 let kisses2 yy xx = marriedto xx yy
93 let kisses3 yy xx = X.(map2 (fun x y -> false) xx yy)
95 (* Actually, each husband loves only his wife and Frank also loves the women.
96 In w2, all the men love Carol and Ella loves the wives.
97 In w3, Frank loves everyone else. *)
98 let loves1 yy xx = X.(map2 (fun x y -> (is_male x && are_married(x,y)) || (x = Frank && not (is_male y))) xx yy)
99 let loves2 yy xx = X.(map2 (fun x y -> (is_male x && y = Carol) || (x = Ella && is_a_wife y)) xx yy)
100 let loves3 yy xx = X.(map2 (fun x y -> x = Frank && x <> y) xx yy)
103 module Test(S : SEMANTICS) : sig end = struct
104 type result = True | False | Fail
105 let print_result res = match res with True -> print_string "true" | False -> print_string "false" | Fail -> print_string "failure"
107 let check name expected expr =
108 (match (try Some (S.run expr) with Not_found -> None) with
109 | 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
110 | 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
111 | 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)
113 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
114 with Failure "Unimplemented" -> begin print_string "Sentence \""; print_string name; print_endline "\" unimplemented."; true end
117 let dynamic res = if S.dynamic then res else Fail
119 let truth = S.(male bill)
120 let falsehood = S.(female bill)
122 [ check "true" True truth
123 ; check "false" False falsehood
124 ; check "true and true" True S.(truth &&& truth)
125 ; check "true and false" False S.(truth &&& falsehood)
126 ; check "false and true" False S.(falsehood &&& truth)
127 ; check "false and false" False S.(falsehood &&& falsehood)
128 ; check "true or true" True S.(truth ||| truth)
129 ; check "true or false" True S.(truth ||| falsehood)
130 ; check "false or true" True S.(falsehood ||| truth)
131 ; check "false or false" False S.(falsehood ||| falsehood)
132 ; check "true >>> true" True S.(truth >>> truth)
133 ; check "true >>> false" False S.(truth >>> falsehood)
134 ; check "false >>> true" True S.(falsehood >>> truth)
135 ; check "false >>> false" True S.(falsehood >>> falsehood)
137 let () = print_newline(); print_int (List.count not bool_results); print_endline " boolean test(s) failed."
140 [ check "1. Bill is male" True S.(male bill)
141 ; check "2. Bill is female" False S.(female bill)
142 ; check "3. Bill isn't female" True S.(~~~ (female bill))
143 ; check "4. Carol didn't leave" False S.(~~~ (left carol))
144 ; S.extensional || check "5. Maybe Carol didn't leave" True S.(maybe (~~~ (left carol)))
145 ; S.extensional || check "6. Maybe Ann didn't leave" False S.(maybe (~~~ (left ann)))
147 ; check "7. Some x. x is male" True S.(some 'x' (male getx))
148 ; check "8. Some x. x isn't female" True S.(some 'x' (~~~ (female getx)))
149 ; check "9. Some x. x left" True S.(some 'x' (left getx))
150 ; check "10. Some x. x didn't leave" False S.(some 'x' (~~~ (left getx)))
151 ; check "11. Every x. x left" True S.(every 'x' (left getx))
152 ; check "12. Every x. x is female" False S.(every 'x' (female getx))
153 ; check "13. Every x. x isn't male" False S.(every 'x' (~~~ (male getx)))
154 ; check "14. (Some x. x is male) and Ann is female" True S.(some 'x' (male getx) &&& female ann)
155 ; check "15. Some x. (x is male and Ann is female)" True S.(some 'x' (male getx &&& female ann))
157 ; check "16. Some x. (x is male and x is female)" False S.(some 'x' (male getx &&& female getx))
158 ; check "17. Some x. (x is male) and Some x. x is female" True S.(some 'x' (male getx) &&& some 'x' (female getx))
160 ; check "18. Some x. (x is male and Some y. y is male)" True S.(some 'x' (male getx &&& some 'y' (male gety)))
161 ; check "19. Some x. (x is male and Some y. y is female)" True S.(some 'x' (male getx &&& some 'y' (female gety)))
162 ; check "20. Some x. (x is male and Some y. x is male)" True S.(some 'x' (male getx &&& some 'y' (male getx)))
163 ; check "21. Some x. (x is male and Some y. x is female)" False S.(some 'x' (male getx &&& some 'y' (female getx)))
164 ; check "22. Some x. (x is male and Some y. x isn't female)" True S.(some 'x' (male getx &&& some 'y' (~~~ (female getx))))
165 ; check "23. Some x. (x is male and Some x. x is female)" True S.(some 'x' (male getx &&& some 'x' (female getx)))
167 ; 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))
168 ; 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)))
169 ; 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)))
170 ; 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)))
171 ; 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)))
172 ; 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)))
174 ; 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))))
175 ; 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)))
176 ; 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))))
177 ; 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)))
178 ; 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))))
180 ; 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)))
181 ; 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))))
182 ; 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)))
183 ; 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))))
185 ; check "39. (Some x. male x) and x left" (dynamic True) S.(some 'x' (male getx) &&& left getx)
186 ; check "40. (Some x. male x) and female x" (dynamic False) S.(some 'x' (male getx) &&& female getx)
187 ; check "41. (Some x. male x) and Some y. female x" (dynamic False) S.(some 'x' (male getx) &&& some 'y' (female getx))
188 ; check "42. (Some x. male x) and Some y. male x" (dynamic True) S.(some 'x' (male getx) &&& some 'y' (male getx))
189 ; 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))
190 ; 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))
191 ; 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)))
192 ; 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)))
193 ; 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)))
195 ; 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))
196 ; 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))
197 ; 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)
198 ; 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)
200 ; 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))
201 ; 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))
202 ; 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))
203 ; 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))
205 let () = print_newline(); print_int (List.count not results); print_endline " test(s) failed."
214 module R = Monad.Reader(struct type env = identifier -> entity end)
215 module S = Monad.State(struct type store = identifier -> entity end)
216 module S' = Monad.State(struct type store = identifier -> int end)
217 module R' = Monad.Reader(struct type env = identifier -> int end)
219 let env0 = fun _ -> raise Not_found
220 let lookup (sought : identifier) env = env sought
221 let lookup_string (sought : identifier) env = try string_of_entity (env sought) with Not_found -> "*"
222 let print_lookup c env = print_string (lookup_string c env)
223 let insert (var : identifier) who env = fun sought -> if sought = var then who else env sought
225 module Y = Monad.Reader(struct type env = world end)
227 module L = Monad.List
231 include Monad.Derive.Reader_dbl(Y)(R.T(Y))
235 include Monad.Derive.Reader_dbl(R)(Y.T(R))
239 include Monad.Derive.Reader(R)(L.T(R))
243 include Monad.Derive.Reader(Y)(L.T(Y))
247 include Monad.Derive.List(L)(R.M(L))
251 include Monad.Derive.List(L)(Y.M(L))
256 include Monad.Derive.Reader(Y)(S.T(Y))
260 include Monad.Derive.State(S)(Y.T(S))
264 include Monad.Derive.State(S)(L.T(S))
268 include Monad.Derive.Reader(Y)(L.T(Y))
272 include Monad.Derive.List(L)(S.M(L))
276 include Monad.Derive.List(L)(Y.M(L))
281 include Monad.Derive.Reader(Y)(S'.T(Y))
285 include Monad.Derive.State(S')(Y.T(S'))
289 include Monad.Derive.State(S')(L.T(S'))
293 include Monad.Derive.List(L)(S'.M(L))
298 include Monad.Derive.Reader2(RY)(L.T(RY))
302 include Monad.Derive.Reader2(YR)(L.T(YR))
306 include Monad.Derive.List(LY)(R.M(LY))
307 include Monad.Derive.Reader_dbl(LY)(R.M(LY))
311 include Monad.Derive.List(YL)(R.M(YL))
312 include Monad.Derive.Reader_dbl(YL)(R.M(YL))
316 include Monad.Derive.List(LR)(Y.M(LR))
317 include Monad.Derive.Reader_dbl(LR)(Y.M(LR))
321 include Monad.Derive.List(RL)(Y.M(RL))
322 include Monad.Derive.Reader_dbl(RL)(Y.M(RL))
327 include Monad.Derive.Reader(SY)(L.T(SY))
328 include Monad.Derive.State(SY)(L.T(SY))
332 include Monad.Derive.Reader(YS)(L.T(YS))
333 include Monad.Derive.State(YS)(L.T(YS))
337 include Monad.Derive.List(LY)(S.M(LY))
338 include Monad.Derive.Reader(LY)(S.M(LY))
342 include Monad.Derive.List(YL)(S.M(YL))
343 include Monad.Derive.Reader(YL)(S.M(YL))
347 include Monad.Derive.List(LS)(Y.M(LS))
348 include Monad.Derive.State(LS)(Y.M(LS))
352 include Monad.Derive.List(SL)(Y.M(SL))
353 include Monad.Derive.State(SL)(Y.M(SL))
358 include Monad.Derive.Reader(S'Y)(L.T(S'Y))
359 include Monad.Derive.State(S'Y)(L.T(S'Y))
363 include Monad.Derive.Reader(YS')(L.T(YS'))
364 include Monad.Derive.State(YS')(L.T(YS'))
368 include Monad.Derive.List(LY)(S'.M(LY))
369 include Monad.Derive.Reader(LY)(S'.M(LY))
373 include Monad.Derive.List(YL)(S'.M(YL))
374 include Monad.Derive.Reader(YL)(S'.M(YL))
378 include Monad.Derive.List(LS')(Y.M(LS'))
379 include Monad.Derive.State(LS')(Y.M(LS'))
383 include Monad.Derive.List(S'L)(Y.M(S'L))
384 include Monad.Derive.State(S'L)(Y.M(S'L))
388 module Sem1a = struct
390 let extensional = true
392 (* We use monad R, with env = var -> entity.
393 Types of sentences are env -> bool. *)
395 type noun = entity X.t
397 let run (xx : sent) : bool = X.(run xx env0 = true)
398 let getx = X.(asks (lookup 'x'))
399 let gety = X.(asks (lookup 'y'))
400 let getz = X.(asks (lookup 'z'))
401 let let_ c (xx : noun) (body : sent) = X.(xx >>= fun x -> shift (insert c x) body)
403 let (~~~) xx = X.(map not xx)
404 let (&&&) xx yy = X.(xx >>= fun b' -> if not b' then mid false else yy)
405 let (|||) xx yy = X.(xx >>= fun b' -> if b' then mid true else yy)
406 let (>>>) xx yy = X.(xx >>= fun b' -> if not b' then mid true else yy)
408 let some c (body : sent) =
409 let (bbs : bool X.t list) = List.map (fun x -> let_ c X.(mid x) body) domain in
410 let (bsb : bool list X.t) = X.seq bbs in
411 let (bb : bool X.t) = X.map (exists ident) bsb in
413 let every c (body : sent) =
414 let (bbs : bool X.t list) = List.map (fun x -> let_ c X.(mid x) body) domain in
415 let (bsb : bool list X.t) = X.seq bbs in
416 let (bb : bool X.t) = X.map (for_all ident) bsb in
420 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)
421 let (===) xx yy = X.(map2 (=) xx yy)
422 let male = F.male let female = F.female let single = F.single let left = F.left1
423 let marriedto = F.marriedto let saw = F.saw1 let kisses = F.kisses1 let loves = F.loves1
424 let thinks pp xx = failwith "Unimplemented"
425 let maybe pp = failwith "Unimplemented"
428 module Sem1b = struct
430 let extensional = true
432 (* We again use monad R, with env = var -> entity.
433 This variant defines sentence meanings as Kleisli arrows, that is:
434 type sent = bool -> bool X.t
435 or equivalently, bool -> (env -> bool). A true sentence takes any bool
436 input to a boxed version of that input (so truth = mid), and a false
437 sentence takes any input to mid false.
438 This more closely parallels the dynamic semantics (though it should not,
439 just on account of that structural similarity, be itself counted as dynamic).
440 It also brings the boolean operations closer to monadic primitives.
443 type noun = entity X.t
444 type sent = bool -> bool X.t
445 let run (k : sent) : bool = X.(run (k true) env0 = true)
446 let getx = X.(asks (lookup 'x'))
447 let gety = X.(asks (lookup 'y'))
448 let getz = X.(asks (lookup 'z'))
449 let let_ c (xx : noun) (body : sent) = fun b -> X.(xx >>= fun x -> shift (insert c x) (body b))
451 let (~~~) k = fun b -> X.(if b then map not (k true) else mid false)
452 let (&&&) k j = X.(k >=> j)
453 let (|||) k j = ~~~ (~~~ k &&& ~~~ j)
454 let (>>>) k j = ~~~ k ||| j
456 let (|||) xx yy = fun b -> X.(xx b >>= fun b' -> if b' then mid true else yy b)
457 let (>>>) xx yy = fun b -> X.(xx b >>= fun b' -> if not b' then mid true else yy b)
458 let (>>>) k j = ~~~ (k &&& ~~~ j)
461 let some c (body : sent) = fun b ->
462 let (bbs : bool X.t list) = List.map (fun x -> let_ c X.(mid x) body b) domain in
463 let (bsb : bool list X.t) = X.seq bbs in
464 let (bb : bool X.t) = X.map (exists ident) bsb in
466 let every c (body : sent) = fun b ->
467 let (bbs : bool X.t list) = List.map (fun x -> let_ c X.(mid x) body b) domain in
468 let (bsb : bool list X.t) = X.seq bbs in
469 let (bb : bool X.t) = X.map (for_all ident) bsb in
473 let to_kleisli xx = fun b -> X.(xx >>= fun b' -> mid (b && b'))
474 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)
475 let (===) xx yy = to_kleisli X.(map2 (=) xx yy)
476 let male = to_kleisli % F.male let female = to_kleisli % F.female let single = to_kleisli % F.single let left = to_kleisli % F.left1
477 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)
478 let thinks pp xx = fun b -> failwith "Unimplemented"
479 let maybe pp = fun b -> failwith "Unimplemented"
482 module Sem2a = struct
484 let extensional = true
486 (* We could use either monad RL or LR, with type env = var -> entity.
487 Their box type is the same: env -> ['a]
488 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.
489 We use the box type in two ways: first, we use a box(entity) to compute whether a matrix
490 clause is satisfied by a bound pronoun, where entity ranges over the whole domain.
491 Second, it is convenient and more consonant with later strategies
492 to re-use the same monad for sentence types (rather than using a simpler monad
493 that lacks a List component). Here we will let the types of sentences
494 be box(bool), that is: env -> [bool]. We will understand the sentence to be true
495 if there are ANY truths in the resulting list. A list of all falses is treated
496 the same as an empty list. Sem2c, below, eliminates this artifact by changing
497 the sentence type to box(unit). Then truths (rel to an env) are [();...] and
501 type noun = entity X.t
503 let run (xx : sent) : bool = X.(any_truths (run xx env0))
504 (* lift an 'a list to a single 'a X.t *)
505 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
506 let getx = X.(asks (lookup 'x'))
507 let gety = X.(asks (lookup 'y'))
508 let getz = X.(asks (lookup 'z'))
509 let let_ c (xx : noun) (body : sent) = X.(xx >>= fun x -> shift (insert c x) body)
511 let (~~~) xx = X.(map not xx)
512 let (&&&) xx yy = X.(xx >>= fun b' -> if not b' then mid false else yy)
513 let (|||) xx yy = X.(xx >>= fun b' -> if b' then mid true else yy)
514 let (>>>) xx yy = X.(xx >>= fun b' -> if not b' then mid true else yy)
516 (* On this semantics, `some c body` is a list of the boolean outcomes for body for each assignment to c.
517 That matches our convention for sentence types, where any truth in the list means the sentence is true.
518 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.
519 In later semantics, the duality of `some` and `every` will be restored.
521 let some c (body : sent) = X.(let_ c (mids domain) body)
522 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 *)
525 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)
526 let (===) xx yy = X.(map2 (=) xx yy)
527 let male = F.male let female = F.female let single = F.single let left = F.left1
528 let marriedto = F.marriedto let saw = F.saw1 let kisses = F.kisses1 let loves = F.loves1
529 let thinks pp xx = failwith "Unimplemented"
530 let maybe pp = failwith "Unimplemented"
533 (* Sem2b would convert Sem2a into having sentence meanings be Kleisli arrows, as Sem1b did.
534 Not here implemented. *)
536 (* Variant of Sem2a, which uses [();...] vs [] instead of [true;...] vs (list of all false OR []). *)
537 module Sem2c = struct
539 let extensional = true
541 (* We use monad LR as above, with same env = var -> entity and box type = env -> ['a].
542 We again use box(entity) to compute whether matrix clauses are satisfied by
543 bound pronouns; but now we use box(unit) for the types of sentences.
544 Truths (rel to an env) are [();...] and falsehood is [].
547 type noun = entity X.t
549 let run (xx : sent) : bool = X.(not (List.is_null (run xx env0)))
550 (* lift an 'a list to a single 'a X.t *)
551 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
552 let getx = X.(asks (lookup 'x'))
553 let gety = X.(asks (lookup 'y'))
554 let getz = X.(asks (lookup 'z'))
555 let let_ c (xx : noun) (body : sent) = X.(xx >>= fun x -> shift (insert c x) body)
556 let to_unit (x : bool) : unit X.t = X.guard x
558 let (~~~) xx = X.(list_map (fun xs -> if is_null xs then [()] else []) xx)
559 let (&&&) xx yy = X.(xx >> yy)
560 let (|||) xx yy = X.(xx ++ (* ~~~ xx >> *) yy)
561 let (>>>) xx yy = X.(~~~ xx ++ yy)
563 let (>>>) xx yy = X.(~~~ (xx >> ~~~ yy))
566 let some c (body : sent) = X.(let_ c (mids domain) body)
567 let every c (body : sent) = ~~~ (some c (~~~ body))
570 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)
571 let (===) xx yy = X.(map2 (=) xx yy >>= to_unit)
572 let male xx = X.(F.male xx >>= to_unit)
573 let female xx = X.(F.female xx >>= to_unit)
574 let single xx = X.(F.single xx >>= to_unit)
575 let left xx = X.(F.left1 xx >>= to_unit)
576 let marriedto yy xx = X.(F.marriedto yy xx >>= to_unit)
577 let saw yy xx = X.(F.saw1 yy xx >>= to_unit)
578 let kisses yy xx = X.(F.kisses1 yy xx >>= to_unit)
579 let loves yy xx = X.(F.loves1 yy xx >>= to_unit)
580 let thinks pp xx = failwith "Unimplemented"
581 let maybe pp = failwith "Unimplemented"
584 (* Sem2d would convert Sem2c into having sentence meanings be Kleisli arrows, as Sem1b did.
585 Not here implemented. *)
587 (* Add intensionality to 2a *)
588 module Sem3a = struct
590 let extensional = false
592 (* Using monad LRY, with type env = var -> entity.
593 Box type is env -> world -> ['a]
594 Types of sentences are env -> world -> [bool]. *)
596 type noun = entity X.t
598 let run xx = X.(any_truths (run xx env0 Actual))
599 (* lift an 'a list to a single 'a X.t *)
600 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
601 let getx = X.(asks (lookup 'x'))
602 let gety = X.(asks (lookup 'y'))
603 let getz = X.(asks (lookup 'z'))
604 let getw = X.(uask) (* get world from the underlying Y monad *)
605 (* select an intranstive verb based on the world *)
606 let select1 f1 f2 f3 xx = X.(getw >>= fun w -> (if w = Actual then f1 else if w = Other then f2 else f3) xx)
607 (* select a transitive verb based on the world *)
608 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)
609 let let_ c (xx : noun) (body : sent) = X.(xx >>= fun x -> shift (insert c x) body)
610 let letw world (body : sent) = X.(ushift (fun _ -> world) body) (* shift the "env" of the underlying Y monad *)
612 let (~~~) xx = X.(map not xx)
613 let (&&&) xx yy = X.(xx >>= fun b' -> if not b' then mid false else yy)
614 let (|||) xx yy = X.(xx >>= fun b' -> if b' then mid true else yy)
615 let (>>>) xx yy = X.(xx >>= fun b' -> if not b' then mid true else yy)
617 let some c (body : sent) = X.(let_ c (mids domain) body)
618 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)
621 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)
622 let (===) xx yy = X.(map2 (=) xx yy)
623 let male = F.male let female = F.female let single = F.single
624 let left xx = select1 F.left1 F.left2 F.left3 xx
625 let saw yy xx = select2 F.saw1 F.saw2 F.saw3 yy xx
626 let marriedto = F.marriedto
627 let kisses yy xx = select2 F.kisses1 F.kisses2 F.kisses3 yy xx
628 let loves yy xx = select2 F.loves1 F.loves2 F.loves3 yy xx
629 let thinks pp xx = failwith "Unimplemented"
630 let maybe (body : sent) : sent =
631 let (yy : R.env -> Y.env -> bool list) = fun e w ->
632 let body_int = List.map (fun w' -> any_truths (X.run (letw w' body) e w)) modal_domain in
633 body_int (* can just use body's intension as the result of `maybe body` *) in
637 (* Sem3b would convert Sem3a into having sentence meanings be Kleisli arrows, as Sem1b did.
638 Not here implemented. *)
640 (* Add intensionality to 2c *)
641 module Sem3c = struct
643 let extensional = false
645 (* Using monad LRY, with type env = var -> entity.
646 Box type is env -> world -> ['a]
647 Types of sentences are env -> world -> [unit]. *)
649 type noun = entity X.t
651 let run xx = X.(not (List.is_null (run xx env0 Actual)))
652 (* lift an 'a list to a single 'a X.t *)
653 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
654 let getx = X.(asks (lookup 'x'))
655 let gety = X.(asks (lookup 'y'))
656 let getz = X.(asks (lookup 'z'))
657 let getw = X.(uask) (* get world from the underlying Y monad *)
658 (* select an intranstive verb based on the world *)
659 let select1 f1 f2 f3 xx = X.(getw >>= fun w -> (if w = Actual then f1 else if w = Other then f2 else f3) xx)
660 (* select a transitive verb based on the world *)
661 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)
662 let let_ c (xx : noun) (body : sent) = X.(xx >>= fun x -> shift (insert c x) body)
663 let letw world (body : sent) = X.(ushift (fun _ -> world) body) (* shift the "env" of the underlying Y monad *)
664 let to_unit (x : bool) : unit X.t = X.guard x
666 let (~~~) xx = X.(list_map (fun xs -> if is_null xs then [()] else []) xx)
667 let (&&&) xx yy = X.(xx >> yy)
668 let (|||) xx yy = X.(xx ++ (* ~~~ xx >> *) yy)
669 let (>>>) xx yy = X.(~~~ xx ++ yy)
671 let (>>>) xx yy = X.(~~~ (xx >> ~~~ yy))
674 let some c (body : sent) = X.(let_ c (mids domain) body)
675 let every c (body : sent) = ~~~ (some c (~~~ body))
678 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)
679 let (===) xx yy = X.(map2 (=) xx yy >>= to_unit)
680 let male xx = X.(F.male xx >>= to_unit)
681 let female xx = X.(F.female xx >>= to_unit)
682 let single xx = X.(F.single xx >>= to_unit)
683 let left xx = X.(select1 F.left1 F.left2 F.left3 xx >>= to_unit)
684 let saw yy xx = X.(select2 F.saw1 F.saw2 F.saw3 yy xx >>= to_unit)
685 let marriedto yy xx = X.(F.marriedto yy xx >>= to_unit)
686 let kisses yy xx = X.(select2 F.kisses1 F.kisses2 F.kisses3 yy xx >>= to_unit)
687 let loves yy xx = X.(select2 F.loves1 F.loves2 F.loves3 yy xx >>= to_unit)
688 let thinks pp xx = failwith "Unimplemented"
689 let maybe (body : sent) : sent =
690 let (yy : R.env -> Y.env -> unit list) = fun e w ->
691 let body_int = List.map (fun w' -> not @@ List.is_null @@ X.run (letw w' body) e w) modal_domain in
692 if any_truths body_int then [()] else [] in
696 (* Sem3d would convert Sem3c into having sentence meanings be Kleisli arrows, as Sem1b did.
697 Not here implemented. *)
700 (* Dynamic version of Sem2c *)
701 module Sem5c = struct
703 let extensional = true
705 (* This needs to use monad SL, with store = var -> entity
706 and box type = store -> ['a,store]
707 Sentence meaning is box(unit).
708 Later strategies with more complex sentence meanings and stores
709 may be able to use monad LS, with box type store -> ['a],store
712 type noun = entity X.t
714 let run (xx : sent) : bool = X.(not (List.is_null (run xx env0)))
715 (* lift an 'a list to a single 'a X.t *)
716 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
717 let getx = X.(gets (lookup 'x'))
718 let gety = X.(gets (lookup 'y'))
719 let getz = X.(gets (lookup 'z'))
720 let let_ c (xx : noun) (body : sent) = X.(xx >>= fun x -> modify (insert c x) >> body)
721 let to_unit (x : bool) : unit X.t = X.guard x
723 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)
726 let (~~~) (xx : sent) : sent =
727 let yy : S.store -> (unit * S.store) list = fun s -> if List.is_null (X.run xx s) then [(),s] else [] in
728 Obj.magic yy (* this is an identity function that changes the type of yy to a unit X.t *)
729 let (&&&) xx yy = X.(xx >> yy)
730 let (|||) xx yy = ~~~ (~~~ xx &&& ~~~ yy)
731 let (>>>) xx yy = X.(~~~ (xx >> ~~~ yy))
734 This would propagate effects out of the disjuncts, so that for example after
735 "Some y. (x = frank and female y) or Some y. married y x"
736 "y" would be available for anaphor:
737 let (|||) xx yy = X.(xx ++ (~~~ xx >> yy))
739 This wouldn't propagate effects from antecedent to consequent, so that for example
740 "(Some y. marriedto y bill) >>> female gety"
741 has a failed lookup on "y":
742 let (>>>) xx yy = X.(~~~ xx ++ yy)
745 let some c (body : sent) = X.(let_ c (mids domain) body)
746 let every c (body : sent) = ~~~ (some c (~~~ body))
749 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)
750 let (===) xx yy = X.(map2 (=) xx yy >>= to_unit)
751 let male xx = X.(F.male xx >>= to_unit)
752 let female xx = X.(F.female xx >>= to_unit)
753 let single xx = X.(F.single xx >>= to_unit)
754 let left xx = X.(F.left1 xx >>= to_unit)
755 let marriedto yy xx = X.(F.marriedto yy xx >>= to_unit)
756 let saw yy xx = X.(F.saw1 yy xx >>= to_unit)
757 let kisses yy xx = X.(F.kisses1 yy xx >>= to_unit)
758 let loves yy xx = X.(F.loves1 yy xx >>= to_unit)
759 let thinks pp xx = failwith "Unimplemented"
760 let maybe pp = failwith "Unimplemented"
764 (* Dynamic version of Sem3c / Add intensionality to Sem5c *)
765 module Sem6c = struct
767 let extensional = false
769 (* This needs to use monad SLY, with store = var -> entity
770 and box type = store -> world -> ['a,store]
771 Sentence meaning is box(unit).
772 Later strategies with more complex sentence meanings and stores
773 may be able to use monad LSY, with box type store -> world -> ['a],store
776 type noun = entity X.t
778 let run (xx : sent) : bool = X.(not (List.is_null (run xx env0 Actual)))
779 (* lift an 'a list to a single 'a X.t *)
780 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
781 let getx = X.(gets (lookup 'x'))
782 let gety = X.(gets (lookup 'y'))
783 let getz = X.(gets (lookup 'z'))
784 let getw = X.(ask) (* get world from the underlying Y monad *)
785 (* select an intranstive verb based on the world *)
786 let select1 f1 f2 f3 xx = X.(getw >>= fun w -> (if w = Actual then f1 else if w = Other then f2 else f3) xx)
787 (* select a transitive verb based on the world *)
788 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)
789 let let_ c (xx : noun) (body : sent) = X.(xx >>= fun x -> modify (insert c x) >> body)
790 let letw world (body : sent) = X.(shift (fun _ -> world) body) (* shift the "env" of the underlying Y monad *)
791 let to_unit (x : bool) : unit X.t = X.guard x
793 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)
796 let (~~~) (xx : sent) : sent =
797 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
798 Obj.magic yy (* this is an identity function that changes the type of yy to a unit X.t *)
800 let (&&&) xx yy = X.(xx >> yy)
801 let (|||) xx yy = ~~~ (~~~ xx &&& ~~~ yy)
802 let (>>>) xx yy = X.(~~~ (xx >> ~~~ yy))
804 let some c (body : sent) = X.(let_ c (mids domain) body)
805 let every c (body : sent) = ~~~ (some c (~~~ body))
808 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)
809 let (===) xx yy = X.(map2 (=) xx yy >>= to_unit)
810 let male xx = X.(F.male xx >>= to_unit)
811 let female xx = X.(F.female xx >>= to_unit)
812 let single xx = X.(F.single xx >>= to_unit)
813 let left xx = X.(select1 F.left1 F.left2 F.left3 xx >>= to_unit)
814 let saw yy xx = X.(select2 F.saw1 F.saw2 F.saw3 yy xx >>= to_unit)
815 let marriedto yy xx = X.(F.marriedto yy xx >>= to_unit)
816 let kisses yy xx = X.(select2 F.kisses1 F.kisses2 F.kisses3 yy xx >>= to_unit)
817 let loves yy xx = X.(select2 F.loves1 F.loves2 F.loves3 yy xx >>= to_unit)
818 let thinks pp xx = failwith "Unimplemented"
819 let maybe (body : sent) : sent =
820 let (yy : S.store -> Y.env -> (unit * S.store) list) = fun s w ->
821 let body_int = List.map (fun w' -> not @@ List.is_null @@ X.run (letw w' body) s w) modal_domain in
822 if any_truths body_int then [(),s] else [] in
826 (* 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.
827 Next we develop some semantics that are closer to their actual presentation. *)
829 (* This develops Sem5c using in part the strategies from Sem1b. *)
830 module Sem5e = struct
832 let extensional = true
834 (* Let a topic be sequence of entities introduced into conversation (GSV's pegs -> entities, with pegs construed as positions in the sequence).
835 Then let store = var -> int (that is, position in the topic)
836 Then we can use monad LS', with box type = store -> ['a],store
837 And sentence meanings are Kleisli arrows: topic -> box(topic). The list component
838 in the type captures indeterminacy in what objects are being discussed (introduced
839 by quantifiers). Truths (relative to a initial store and topic) result in
840 non-empty topic lists; falsehoods in empty ones.
842 type topic = entity list
845 type noun = (topic -> entity) X.t
846 type sent = topic -> topic X.t
847 let run (k : sent) : bool = X.(not (List.is_null (fst (run (k topic0) env0))))
848 (* lift an 'a list to a single 'a X.t *)
849 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
850 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)
851 let getx : noun = X.(gets (lookup 'x') >>= fun n -> mid (get_nth n))
852 let gety : noun = X.(gets (lookup 'y') >>= fun n -> mid (get_nth n))
853 let getz : noun = X.(gets (lookup 'z') >>= fun n -> mid (get_nth n))
854 let let_ c (n : int) (body : sent) : sent = fun top -> X.(modify (insert c n) >> (body top))
856 let lookup_string sought env top = try string_of_entity (List.nth top (env sought)) with Not_found -> "*" | List.Short_list -> "#"
857 let print_lookup sought env top = print_string (lookup_string sought env top)
858 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)
861 let (~~~) (k : sent) : sent = fun top ->
862 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
863 Obj.magic yy (* this is an identity function that changes the type of yy to a topic X.t *)
864 let (&&&) k j = X.(k >=> j)
865 let (|||) k j = ~~~ (~~~ k &&& ~~~ j) (* TODO how about (k >>> j) >>> j *)
866 let (>>>) k j = X.(~~~ (k >=> ~~~ j))
868 let some c (body : sent) : sent = fun top ->
869 let n = length top in
870 let aux ent = X.(let_ c n body) (List.snoc top ent) in
871 let domain' = List.map aux domain in
872 X.join (mids domain')
874 let every c (body : sent) = ~~~ (some c (~~~ body))
877 let some c body = X.(mids domain >>= fun x -> modify (insert c x) body >>= guard >> mid x)
878 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)
882 let mapply' (ff : noun) (top : topic) : entity X.t = X.(map (fun f -> f top) ff)
883 let wrap name = X.(mid (const name))
884 let wrap1 f xx = fun top -> X.(f (mapply' xx top) >>= fun b -> if b then mid top else mzero)
885 let wrap2 f xx yy = fun top -> X.(f (mapply' xx top) (mapply' yy top) >>= fun b -> if b then mid top else mzero)
886 let ann = wrap Ann let bill = wrap Bill let carol = wrap Carol let dave = wrap Dave let ella = wrap Ella let frank = wrap Frank
887 let (===) (xx : noun) (yy : noun) : sent = wrap2 X.(map2 (=)) xx yy
888 let male (xx : noun) : sent = wrap1 F.male xx
889 let female xx = wrap1 F.female xx
890 let single xx = wrap1 F.single xx
891 let left xx = wrap1 F.left1 xx
892 let marriedto yy xx = wrap2 F.marriedto yy xx
893 let saw yy xx = wrap2 F.saw1 yy xx
894 let kisses yy xx = wrap2 F.kisses1 yy xx
895 let loves yy xx = wrap2 F.loves1 yy xx
896 let thinks pp xx = fun top -> failwith "Unimplemented"
897 let maybe pp = fun top -> failwith "Unimplemented"
900 (* Add intensionality to Sem5e *)
901 module Sem6e = struct
903 let extensional = false
905 type topic = entity list
908 type noun = (topic -> entity) X.t
909 type sent = topic -> topic X.t
910 let run (k : sent) : bool = X.(not (List.is_null (fst (run (k topic0) env0 Actual))))
911 (* lift an 'a list to a single 'a X.t *)
912 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
913 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)
914 let getx : noun = X.(gets (lookup 'x') >>= fun n -> mid (get_nth n))
915 let gety : noun = X.(gets (lookup 'y') >>= fun n -> mid (get_nth n))
916 let getz : noun = X.(gets (lookup 'z') >>= fun n -> mid (get_nth n))
917 let getw = X.(ask) (* get world from the underlying Y monad *)
918 (* select an intranstive verb based on the world *)
919 let select1 f1 f2 f3 xx = X.(getw >>= fun w -> (if w = Actual then f1 else if w = Other then f2 else f3) xx)
920 (* select a transitive verb based on the world *)
921 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)
922 let let_ c (n : int) (body : sent) : sent = fun top -> X.(modify (insert c n) >> (body top))
923 let letw world (body : sent) : sent = fun top -> X.(shift (fun _ -> world) (body top)) (* shift the "env" of the underlying Y monad *)
925 let (~~~) (k : sent) : sent = fun top ->
926 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
927 Obj.magic yy (* this is an identity function that changes the type of yy to a topic X.t *)
928 let (&&&) k j = X.(k >=> j)
929 let (|||) k j = ~~~ (~~~ k &&& ~~~ j)
930 let (>>>) k j = X.(~~~ (k >=> ~~~ j))
932 let some c (body : sent) : sent = fun top ->
933 let n = length top in
934 let aux ent = X.(let_ c n body) (List.snoc top ent) in
935 let domain' = List.map aux domain in
936 X.join (mids domain')
938 let every c (body : sent) = ~~~ (some c (~~~ body))
941 let mapply' (ff : noun) (top : topic) : entity X.t = X.(map (fun f -> f top) ff)
942 let wrap name = X.(mid (const name))
943 let wrap1 f xx = fun top -> X.(f (mapply' xx top) >>= fun b -> if b then mid top else mzero)
944 let wrap2 f xx yy = fun top -> X.(f (mapply' xx top) (mapply' yy top) >>= fun b -> if b then mid top else mzero)
945 let ann = wrap Ann let bill = wrap Bill let carol = wrap Carol let dave = wrap Dave let ella = wrap Ella let frank = wrap Frank
946 let (===) (xx : noun) (yy : noun) : sent = wrap2 X.(map2 (=)) xx yy
947 let male (xx : noun) : sent = wrap1 F.male xx
948 let female xx = wrap1 F.female xx
949 let single xx = wrap1 F.single xx
950 let left xx = wrap1 (select1 F.left1 F.left2 F.left3) xx
951 let marriedto yy xx = wrap2 F.marriedto yy xx
952 let saw yy xx = wrap2 (select2 F.saw1 F.saw2 F.saw3) yy xx
953 let kisses yy xx = wrap2 (select2 F.kisses1 F.kisses2 F.kisses3) yy xx
954 let loves yy xx = wrap2 (select2 F.loves1 F.loves2 F.loves3) yy xx
955 let thinks pp xx = failwith "Unimplemented"
956 let maybe (body : sent) : sent = fun top ->
957 let (yy : S'.store -> Y.env -> topic list * S'.store) = fun s w ->
958 let body_int = List.map (fun w' -> not @@ List.is_null @@ fst @@ X.run (letw w' body top) s w) modal_domain in
959 if any_truths body_int then [top],s else [],s in
963 module TestAll = struct
964 print_endline "\nTesting Sem1a";;
965 module T1a = Test(Sem1a);;
966 print_endline "\nTesting Sem1b";;
967 module T1b = Test(Sem1b);;
968 print_endline "\nTesting Sem2a";;
969 module T2a = Test(Sem2a);;
970 print_endline "\nTesting Sem2c";;
971 module T2c = Test(Sem2c);;
972 print_endline "\nTesting Sem3a";;
973 module T3a = Test(Sem3a);;
974 print_endline "\nTesting Sem3c";;
975 module T3c = Test(Sem3c);;
976 print_endline "\nTesting Sem5c";;
977 module T5c = Test(Sem5c);;
978 print_endline "\nTesting Sem5e";;
979 module T5e = Test(Sem5e);;
980 print_endline "\nTesting Sem6c";;
981 module T6c = Test(Sem6c);;
982 print_endline "\nTesting Sem6e";;
983 module T6e = Test(Sem6e);;
988 One can't test the broken vase case by comparing the _truth_ of any sentences.
989 The difference is in whether the sentences have meanings that are "supported by"
990 the same informtation states. Compare in our model:
991 (i) Someone kissed me. She might have stayed.
993 (ii) Someone who might have stayed kissed me.
994 Recall that in our model Ann leaves in every world, but Carol stays in some (non-actual)
995 world. If my background information settles that I was kissed by either Ann or Carol,
996 then I'm in a position to assert (i), since after the first clause it's left open
997 that the referent be either woman. But it doesn't put me in a position to assert (ii),
998 since that implies I was kissed by Carol. So far as truth-value goes,
999 if Carol kissed me both sentences are true, and if Ann did then both sentences are false.