1 (* GSV monadically 13 April 2015 *)
5 module type SEMANTICS = sig
6 type noun (* this is whatever monadic type the semantics assigns to noun-sized contents *)
7 type sent (* this is whatever monadic type the semantics assigns to sentence-sized contents *)
10 val extensional : bool
12 val getx : noun val gety : noun val getz : noun
13 (* OCaml will parse ~~~ as a prefix operator, but unfortunately won't let you say
14 `~~~ predicate subject`; you have to say `~~~ (predicate subject)`. *)
15 val ( ~~~ ) : sent -> sent
16 (* OCaml will parse these three as infix operators (yay), but makes them all
17 left-associative (ehh for >>>) and have the same precedence (boo). *)
18 val ( &&& ) : sent -> sent -> sent
19 val ( ||| ) : sent -> sent -> sent
20 val ( >>> ) : sent -> sent -> sent
21 (* OCaml parses this with same associativity and precedence as the preceding (boo). *)
22 val (===) : noun -> noun -> sent
23 val ann : noun val bill : noun val carol : noun val dave : noun val ella : noun val frank : noun
24 val male : noun -> sent val female : noun -> sent
25 val left : noun -> sent
26 val single : noun -> sent
27 (* Transitive verbs apply to their direct objs first, subjects second. *)
28 val marriedto : noun -> noun -> sent
29 val saw : noun -> noun -> sent
30 val kisses : noun -> noun -> sent
31 val loves : noun -> noun -> sent (* here construed extensionally *)
32 (* Quantifiers may be unimplemented. *)
33 val some : identifier -> sent -> sent
34 val every : identifier -> sent -> sent
35 (* Intensional verbs and operators may be unimplemented. *)
36 val thinks : sent -> noun -> sent
37 val maybe : sent -> sent
40 type world = Actual | Second | Third
41 let modal_domain = [Actual; Second; Third]
43 type entity = Ann | Bill | Carol | Dave | Ella | Frank
44 let domain = [Ann; Bill; Carol; Dave; Ella; Frank]
45 let string_of_entity = function
52 let print_entity ent = print_string (string_of_entity ent)
54 let env0 = fun _ -> raise Not_found
55 let lookup (sought : identifier) env = env sought
56 let lookup_string (sought : identifier) env = try string_of_entity (env sought) with Not_found -> "*"
57 let print_lookup c env = print_string (lookup_string c env)
58 let insert (var : identifier) who env = fun sought -> if sought = var then who else env sought
60 let any_truths (xs : 'a list) : bool = List.exists ident xs
61 let all_truths (xs : 'a list) : bool = List.for_all ident xs
63 module Facts(X : Monad.MONAD) = struct
64 (* Here are the atomic facts: Ann and Bill are married, also Carol and Dave.
65 Genders and marital statuses are epistemically necessary.
66 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.
67 In w2, all but Carol left; no one sees anything; all spouses kiss; all men love only Carol and Ella loves the wives.
68 In w3, only Ann and Bill left; no one sees anything; nobody kisses; Frank loves everyone else.
69 So: everyone is either essentially married or essentially single. And Ann and Bill essentially left; others left only contingently.
72 let is_male = function Bill | Dave | Frank -> true | _ -> false
73 let are_married = function (Ann, Bill) | (Bill, Ann) | (Carol, Dave) | (Dave, Carol) -> true | _ -> false
74 let is_a_wife = function Ann | Carol -> true | _ -> false
76 let male xx = X.(map is_male xx)
77 let female xx = X.(map (not % is_male) xx)
79 (* Ella and Frank are single *)
80 let single xx = X.(map (fun x -> x > Dave) xx)
82 (* Actually (in w1), everybody left. In w2, everybody but Carol left. In w3, only Ann and Bill left. *)
83 let left1 xx = X.(map (fun _ -> true) xx)
84 let left2 xx = X.(map (fun x -> x <> Carol) xx)
85 let left3 xx = X.(map (fun x -> x = Ann || x = Bill) xx)
87 (* In the sentences, order of application is: TransitiveVerb + Object + Subject.
88 But we convert to logical order for our operations. *)
90 (* Actually, each person saw the people alphabetically before them. In w2 and w3, no one saw anyone. *)
91 let saw1 yy xx = X.(map2 (fun x y -> x < y) xx yy)
92 let saw2 yy xx = X.(map2 (fun _ _ -> false) xx yy)
95 (* Necessarily, Ann and Bill are married to each other; also Carol to Dave. *)
96 let marriedto yy xx = X.(map2 (curry are_married) xx yy)
98 (* Actually, only Carol and Dave kiss. In w2, spouses kiss. In w3, there is no kissing. *)
99 let kisses1 yy xx = X.(map2 (fun x y -> (x = Carol && y = Dave) || (x = Dave && y = Carol)) xx yy)
100 let kisses2 yy xx = marriedto xx yy
101 let kisses3 yy xx = X.(map2 (fun x y -> false) xx yy)
103 (* Actually, each husband loves only his wife and Frank also loves the women.
104 In w2, all the men love Carol and Ella loves the wives.
105 In w3, Frank loves everyone else. *)
106 let loves1 yy xx = X.(map2 (fun x y -> (is_male x && are_married(x,y)) || (x = Frank && not (is_male y))) xx yy)
107 let loves2 yy xx = X.(map2 (fun x y -> (is_male x && y = Carol) || (x = Ella && is_a_wife y)) xx yy)
108 let loves3 yy xx = X.(map2 (fun x y -> x = Frank && x <> y) xx yy)
111 module Test(S : SEMANTICS) : sig end = struct
112 type result = True | False | Fail
113 let print_result res = match res with True -> print_string "true" | False -> print_string "false" | Fail -> print_string "failure"
115 let check name expected expr =
116 (match (try Some (S.run expr) with Not_found -> None) with
117 | 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
118 | 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
119 | 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)
121 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
122 with Failure "Unimplemented" -> begin print_string "Sentence \""; print_string name; print_endline "\" unimplemented."; true end
125 let dynamic res = if S.dynamic then res else Fail
127 let truth = S.(male bill)
128 let falsehood = S.(female bill)
130 [ check "true" True truth
131 ; check "false" False falsehood
132 ; check "true and true" True S.(truth &&& truth)
133 ; check "true and false" False S.(truth &&& falsehood)
134 ; check "false and true" False S.(falsehood &&& truth)
135 ; check "false and false" False S.(falsehood &&& falsehood)
136 ; check "true or true" True S.(truth ||| truth)
137 ; check "true or false" True S.(truth ||| falsehood)
138 ; check "false or true" True S.(falsehood ||| truth)
139 ; check "false or false" False S.(falsehood ||| falsehood)
140 ; check "true >>> true" True S.(truth >>> truth)
141 ; check "true >>> false" False S.(truth >>> falsehood)
142 ; check "false >>> true" True S.(falsehood >>> truth)
143 ; check "false >>> false" True S.(falsehood >>> falsehood)
145 let () = print_newline(); print_int (List.count not bool_results); print_endline " boolean test(s) failed."
148 [ check "1. Bill is male" True S.(male bill)
149 ; check "2. Bill is female" False S.(female bill)
150 ; check "3. Bill isn't female" True S.(~~~ (female bill))
151 ; check "4. Carol didn't leave" False S.(~~~ (left carol))
152 ; S.extensional || check "5. Maybe Carol didn't leave" True S.(maybe (~~~ (left carol)))
153 ; S.extensional || check "6. Maybe Ann didn't leave" False S.(maybe (~~~ (left ann)))
155 ; check "7. Some x. x is male" True S.(some 'x' (male getx))
156 ; check "8. Some x. x isn't female" True S.(some 'x' (~~~ (female getx)))
157 ; check "9. Some x. x left" True S.(some 'x' (left getx))
158 ; check "10. Some x. x didn't leave" False S.(some 'x' (~~~ (left getx)))
159 ; check "11. Every x. x left" True S.(every 'x' (left getx))
160 ; check "12. Every x. x is female" False S.(every 'x' (female getx))
161 ; check "13. Every x. x isn't male" False S.(every 'x' (~~~ (male getx)))
162 ; check "14. (Some x. x is male) and Ann is female" True S.(some 'x' (male getx) &&& female ann)
163 ; check "15. Some x. (x is male and Ann is female)" True S.(some 'x' (male getx &&& female ann))
165 ; check "16. Some x. (x is male and x is female)" False S.(some 'x' (male getx &&& female getx))
166 ; check "17. Some x. (x is male) and Some x. x is female" True S.(some 'x' (male getx) &&& some 'x' (female getx))
168 ; check "18. Some x. (x is male and Some y. y is male)" True S.(some 'x' (male getx &&& some 'y' (male gety)))
169 ; check "19. Some x. (x is male and Some y. y is female)" True S.(some 'x' (male getx &&& some 'y' (female gety)))
170 ; check "20. Some x. (x is male and Some y. x is male)" True S.(some 'x' (male getx &&& some 'y' (male getx)))
171 ; check "21. Some x. (x is male and Some y. x is female)" False S.(some 'x' (male getx &&& some 'y' (female getx)))
172 ; check "22. Some x. (x is male and Some y. x isn't female)" True S.(some 'x' (male getx &&& some 'y' (~~~ (female getx))))
173 ; check "23. Some x. (x is male and Some x. x is female)" True S.(some 'x' (male getx &&& some 'x' (female getx)))
175 ; 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))
176 ; 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)))
177 ; 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)))
178 ; 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)))
179 ; 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)))
180 ; 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)))
182 ; 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))))
183 ; 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)))
184 ; 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))))
185 ; 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)))
186 ; 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))))
188 ; 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)))
189 ; 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))))
190 ; 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)))
191 ; 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))))
193 ; check "39. (Some x. male x) and x left" (dynamic True) S.(some 'x' (male getx) &&& left getx)
194 ; check "40. (Some x. male x) and female x" (dynamic False) S.(some 'x' (male getx) &&& female getx)
195 ; check "41. (Some x. male x) and Some y. female x" (dynamic False) S.(some 'x' (male getx) &&& some 'y' (female getx))
196 ; check "42. (Some x. male x) and Some y. male x" (dynamic True) S.(some 'x' (male getx) &&& some 'y' (male getx))
197 ; 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))
198 ; 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))
199 ; 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)))
200 ; 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)))
201 ; 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)))
203 ; 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))
204 ; 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))
205 ; 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)
206 ; 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)
208 ; 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))
209 ; 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))
210 ; 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))
211 ; 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))
213 let () = print_newline(); print_int (List.count not results); print_endline " test(s) failed."
217 (* create lots of monads, so that we have them if we need them *)
219 module L = Monad.List
220 module R = Monad.Reader(struct type env = identifier -> entity end)
221 module R' = Monad.Reader(struct type env = identifier -> int end)
222 module Y = Monad.Reader(struct type env = world end)
223 module S = Monad.State(struct type store = identifier -> entity end)
224 module S' = Monad.State(struct type store = identifier -> int end)
228 include Monad.Derive.Reader_dbl(Y)(R.T(Y))
232 include Monad.Derive.Reader_dbl(R)(Y.T(R))
236 include Monad.Derive.Reader(R)(L.T(R))
240 include Monad.Derive.Reader(Y)(L.T(Y))
244 include Monad.Derive.List(L)(R.M(L))
248 include Monad.Derive.List(L)(Y.M(L))
253 include Monad.Derive.Reader(Y)(S.T(Y))
257 include Monad.Derive.State(S)(Y.T(S))
261 include Monad.Derive.State(S)(L.T(S))
265 include Monad.Derive.Reader(Y)(L.T(Y))
269 include Monad.Derive.List(L)(S.M(L))
273 include Monad.Derive.List(L)(Y.M(L))
278 include Monad.Derive.Reader(Y)(S'.T(Y))
282 include Monad.Derive.State(S')(Y.T(S'))
286 include Monad.Derive.State(S')(L.T(S'))
290 include Monad.Derive.List(L)(S'.M(L))
295 include Monad.Derive.Reader2(RY)(L.T(RY))
299 include Monad.Derive.Reader2(YR)(L.T(YR))
303 include Monad.Derive.List(LY)(R.M(LY))
304 include Monad.Derive.Reader_dbl(LY)(R.M(LY))
308 include Monad.Derive.List(YL)(R.M(YL))
309 include Monad.Derive.Reader_dbl(YL)(R.M(YL))
313 include Monad.Derive.List(LR)(Y.M(LR))
314 include Monad.Derive.Reader_dbl(LR)(Y.M(LR))
318 include Monad.Derive.List(RL)(Y.M(RL))
319 include Monad.Derive.Reader_dbl(RL)(Y.M(RL))
324 include Monad.Derive.Reader(SY)(L.T(SY))
325 include Monad.Derive.State(SY)(L.T(SY))
329 include Monad.Derive.Reader(YS)(L.T(YS))
330 include Monad.Derive.State(YS)(L.T(YS))
334 include Monad.Derive.List(LY)(S.M(LY))
335 include Monad.Derive.Reader(LY)(S.M(LY))
339 include Monad.Derive.List(YL)(S.M(YL))
340 include Monad.Derive.Reader(YL)(S.M(YL))
344 include Monad.Derive.List(LS)(Y.M(LS))
345 include Monad.Derive.State(LS)(Y.M(LS))
349 include Monad.Derive.List(SL)(Y.M(SL))
350 include Monad.Derive.State(SL)(Y.M(SL))
355 include Monad.Derive.Reader(S'Y)(L.T(S'Y))
356 include Monad.Derive.State(S'Y)(L.T(S'Y))
360 include Monad.Derive.Reader(YS')(L.T(YS'))
361 include Monad.Derive.State(YS')(L.T(YS'))
365 include Monad.Derive.List(LY)(S'.M(LY))
366 include Monad.Derive.Reader(LY)(S'.M(LY))
370 include Monad.Derive.List(YL)(S'.M(YL))
371 include Monad.Derive.Reader(YL)(S'.M(YL))
375 include Monad.Derive.List(LS')(Y.M(LS'))
376 include Monad.Derive.State(LS')(Y.M(LS'))
380 include Monad.Derive.List(S'L)(Y.M(S'L))
381 include Monad.Derive.State(S'L)(Y.M(S'L))
386 A variety of semantics are provided. Here is the naming scheme:
388 Sem1* is classic semantics with support for variable binding/anaphora.
389 Sem4* would be the dynamic alternative of 1*. (not here provided)
390 You shouldn't be able to implement quantification in these,
391 without bringing in some of the mechanisms of a list/set component.
392 However, Haskell provides those mechanisms in the basic Monad API (as the
393 function Juli8 names `seq`), so we can do quantification without _explicitly_
394 invoking a ListT in our monadic stack.
396 Sem2* adds a List component to the stack to do quantification.
397 Sem5* is the dynamic counterpart.
399 Sem3* adds an (additional) Reader monad for intensionality.
400 Sem6* is the dynamic counterpart.
402 Within that broad organization, here are the sub-patterns:
404 SemNa uses just a bool payload, so sent types are box(bool).
405 SemBb makes sent types the Klesli variant of Na, so sent types are
407 SemNc uses instead a unit payload, which we can do when the monadic
408 stack has a List or Option component; then false will be the monad's
409 mzero, whereas truth will be instances of type box(unit) that aren't
411 SemNd would be the Kleisli variant of Nc, as Nb is the Kleisli variant
413 SemNe (only for dynamic) uses "topics" or sequences of entities being
414 discussed as payloads, so sent types use box(topic). It also incorporates
415 elements of SemNb/d, so that sent types are really topic -> box(topic).
416 SemNf (not yet provided) would remove the List component from the monad
417 stack, in order to properly implement Veltman's "might". Now sent
418 types would be [topic] -> box([topic]).
422 module Sem1a = struct
424 let extensional = true
426 (* We use monad R, with env = var -> entity.
427 Types of sentences are env -> bool. *)
429 type noun = entity X.t
431 let run (xx : sent) : bool = X.(run xx env0 = true)
432 let getx = X.(asks (lookup 'x'))
433 let gety = X.(asks (lookup 'y'))
434 let getz = X.(asks (lookup 'z'))
435 let let_ c (xx : noun) (body : sent) = X.(xx >>= fun x -> shift (insert c x) body)
437 let (~~~) xx = X.(map not xx)
438 let (&&&) xx yy = X.(xx >>= fun b' -> if not b' then mid false else yy)
439 let (|||) xx yy = X.(xx >>= fun b' -> if b' then mid true else yy)
440 let (>>>) xx yy = X.(xx >>= fun b' -> if not b' then mid true else yy)
442 let some c (body : sent) =
443 let (bbs : bool X.t list) = List.map (fun x -> let_ c X.(mid x) body) domain in
444 let (bsb : bool list X.t) = X.seq bbs in
445 let (bb : bool X.t) = X.map (exists ident) bsb in
447 let every c (body : sent) =
448 let (bbs : bool X.t list) = List.map (fun x -> let_ c X.(mid x) body) domain in
449 let (bsb : bool list X.t) = X.seq bbs in
450 let (bb : bool X.t) = X.map (for_all ident) bsb in
454 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)
455 let (===) xx yy = X.(map2 (=) xx yy)
456 let male = F.male let female = F.female let single = F.single let left = F.left1
457 let marriedto = F.marriedto let saw = F.saw1 let kisses = F.kisses1 let loves = F.loves1
458 let thinks pp xx = failwith "Unimplemented"
459 let maybe pp = failwith "Unimplemented"
462 module Sem1b = struct
464 let extensional = true
466 (* We again use monad R, with env = var -> entity.
467 This variant defines sentence meanings as Kleisli arrows, that is:
468 type sent = bool -> bool X.t
469 or equivalently, bool -> (env -> bool). A true sentence takes any bool
470 input to a boxed version of that input (so truth = mid), and a false
471 sentence takes any input to mid false.
472 This more closely parallels the dynamic semantics (though it should not,
473 just on account of that structural similarity, be itself counted as dynamic).
474 It also brings the boolean operations closer to monadic primitives.
477 type noun = entity X.t
478 type sent = bool -> bool X.t
479 let run (k : sent) : bool = X.(run (k true) env0 = true)
480 let getx = X.(asks (lookup 'x'))
481 let gety = X.(asks (lookup 'y'))
482 let getz = X.(asks (lookup 'z'))
483 let let_ c (xx : noun) (body : sent) = fun b -> X.(xx >>= fun x -> shift (insert c x) (body b))
485 let (~~~) k = fun b -> X.(if b then map not (k true) else mid false)
486 let (&&&) k j = X.(k >=> j)
487 let (|||) k j = ~~~ (~~~ k &&& ~~~ j)
488 let (>>>) k j = ~~~ k ||| j
490 let (|||) xx yy = fun b -> X.(xx b >>= fun b' -> if b' then mid true else yy b)
491 let (>>>) xx yy = fun b -> X.(xx b >>= fun b' -> if not b' then mid true else yy b)
492 let (>>>) k j = ~~~ (k &&& ~~~ j)
495 let some c (body : sent) = fun b ->
496 let (bbs : bool X.t list) = List.map (fun x -> let_ c X.(mid x) body b) domain in
497 let (bsb : bool list X.t) = X.seq bbs in
498 let (bb : bool X.t) = X.map (exists ident) bsb in
500 let every c (body : sent) = fun b ->
501 let (bbs : bool X.t list) = List.map (fun x -> let_ c X.(mid x) body b) domain in
502 let (bsb : bool list X.t) = X.seq bbs in
503 let (bb : bool X.t) = X.map (for_all ident) bsb in
507 let to_kleisli xx = fun b -> X.(xx >>= fun b' -> mid (b && b'))
508 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)
509 let (===) xx yy = to_kleisli X.(map2 (=) xx yy)
510 let male = to_kleisli % F.male let female = to_kleisli % F.female let single = to_kleisli % F.single let left = to_kleisli % F.left1
511 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)
512 let thinks pp xx = fun b -> failwith "Unimplemented"
513 let maybe pp = fun b -> failwith "Unimplemented"
516 module Sem2a = struct
518 let extensional = true
520 (* We could use either monad RL or LR, with type env = var -> entity.
521 Their box type is the same: env -> ['a]
522 However, the types of SL and LS differ, and the latter is more suitable for (some of) the dynamic version(s). So to keep things maximally parallel, we'll use LR here.
523 We use the box type in two ways: first, we use a box(entity) to compute whether a matrix
524 clause is satisfied by a bound pronoun, where entity ranges over the whole domain.
525 Second, it is convenient and more consonant with later strategies
526 to re-use the same monad for sentence types (rather than using a simpler monad
527 that lacks a List component). Here we will let the types of sentences
528 be box(bool), that is: env -> [bool]. We will understand the sentence to be true
529 if there are ANY truths in the resulting list. A list of all falses is treated
530 the same as an empty list. Sem2c, below, eliminates this artifact by changing
531 the sentence type to box(unit). Then truths (rel to an env) are [();...] and
535 type noun = entity X.t
537 let run (xx : sent) : bool = X.(any_truths (run xx env0))
538 (* lift an 'a list to a single 'a X.t *)
539 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
540 let getx = X.(asks (lookup 'x'))
541 let gety = X.(asks (lookup 'y'))
542 let getz = X.(asks (lookup 'z'))
543 let let_ c (xx : noun) (body : sent) = X.(xx >>= fun x -> shift (insert c x) body)
545 let (~~~) xx = X.(map not xx)
546 let (&&&) xx yy = X.(xx >>= fun b' -> if not b' then mid false else yy)
547 let (|||) xx yy = X.(xx >>= fun b' -> if b' then mid true else yy)
548 let (>>>) xx yy = X.(xx >>= fun b' -> if not b' then mid true else yy)
550 (* On this semantics, `some c body` is a list of the boolean outcomes for body for each assignment to c.
551 That matches our convention for sentence types, where any truth in the list means the sentence is true.
552 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.
553 In later semantics, the duality of `some` and `every` will be restored.
555 let some c (body : sent) = X.(let_ c (mids domain) body)
556 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 *)
559 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)
560 let (===) xx yy = X.(map2 (=) xx yy)
561 let male = F.male let female = F.female let single = F.single let left = F.left1
562 let marriedto = F.marriedto let saw = F.saw1 let kisses = F.kisses1 let loves = F.loves1
563 let thinks pp xx = failwith "Unimplemented"
564 let maybe pp = failwith "Unimplemented"
567 (* Sem2b would convert Sem2a into having sentence meanings be Kleisli arrows, as Sem1b did.
568 Not here implemented. *)
570 (* Variant of Sem2a, which uses [();...] vs [] instead of [true;...] vs (list of all false OR []). *)
571 module Sem2c = struct
573 let extensional = true
575 (* We use monad LR as above, with same env = var -> entity and box type = env -> ['a].
576 We again use box(entity) to compute whether matrix clauses are satisfied by
577 bound pronouns; but now we use box(unit) for the types of sentences.
578 Truths (rel to an env) are [();...] and falsehood is [].
581 type noun = entity X.t
583 let run (xx : sent) : bool = X.(not (List.is_null (run xx env0)))
584 (* lift an 'a list to a single 'a X.t *)
585 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
586 let getx = X.(asks (lookup 'x'))
587 let gety = X.(asks (lookup 'y'))
588 let getz = X.(asks (lookup 'z'))
589 let let_ c (xx : noun) (body : sent) = X.(xx >>= fun x -> shift (insert c x) body)
590 let to_unit (x : bool) : unit X.t = X.guard x
592 let (~~~) xx = X.(list_map (fun xs -> if is_null xs then [()] else []) xx)
593 let (&&&) xx yy = X.(xx >> yy)
594 let (|||) xx yy = X.(xx ++ (* ~~~ xx >> *) yy)
595 let (>>>) xx yy = X.(~~~ xx ++ yy)
597 let (>>>) xx yy = X.(~~~ (xx >> ~~~ yy))
600 let some c (body : sent) = X.(let_ c (mids domain) body)
601 let every c (body : sent) = ~~~ (some c (~~~ body))
604 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)
605 let (===) xx yy = X.(map2 (=) xx yy >>= to_unit)
606 let male xx = X.(F.male xx >>= to_unit)
607 let female xx = X.(F.female xx >>= to_unit)
608 let single xx = X.(F.single xx >>= to_unit)
609 let left xx = X.(F.left1 xx >>= to_unit)
610 let marriedto yy xx = X.(F.marriedto yy xx >>= to_unit)
611 let saw yy xx = X.(F.saw1 yy xx >>= to_unit)
612 let kisses yy xx = X.(F.kisses1 yy xx >>= to_unit)
613 let loves yy xx = X.(F.loves1 yy xx >>= to_unit)
614 let thinks pp xx = failwith "Unimplemented"
615 let maybe pp = failwith "Unimplemented"
618 (* Sem2d would convert Sem2c into having sentence meanings be Kleisli arrows, as Sem1b did.
619 Not here implemented. *)
621 (* Add intensionality to 2a *)
622 module Sem3a = struct
624 let extensional = false
626 (* Using monad LRY, with type env = var -> entity.
627 Box type is env -> world -> ['a]
628 Types of sentences are env -> world -> [bool]. *)
630 type noun = entity X.t
632 let run xx = X.(any_truths (run xx env0 Actual))
633 (* lift an 'a list to a single 'a X.t *)
634 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
635 let getx = X.(asks (lookup 'x'))
636 let gety = X.(asks (lookup 'y'))
637 let getz = X.(asks (lookup 'z'))
638 let getw = X.(uask) (* get world from the underlying Y monad *)
639 (* select an intranstive verb based on the world *)
640 let select1 f1 f2 f3 xx = X.(getw >>= fun w -> (if w = Actual then f1 else if w = Second then f2 else f3) xx)
641 (* select a transitive verb based on the world *)
642 let select2 f1 f2 f3 yy xx = X.(getw >>= fun w -> (if w = Actual then f1 else if w = Second then f2 else f3) yy xx)
643 let let_ c (xx : noun) (body : sent) = X.(xx >>= fun x -> shift (insert c x) body)
644 let letw world (body : sent) = X.(ushift (fun _ -> world) body) (* shift the "env" of the underlying Y monad *)
646 let (~~~) xx = X.(map not xx)
647 let (&&&) xx yy = X.(xx >>= fun b' -> if not b' then mid false else yy)
648 let (|||) xx yy = X.(xx >>= fun b' -> if b' then mid true else yy)
649 let (>>>) xx yy = X.(xx >>= fun b' -> if not b' then mid true else yy)
651 let some c (body : sent) = X.(let_ c (mids domain) body)
652 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)
655 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)
656 let (===) xx yy = X.(map2 (=) xx yy)
657 let male = F.male let female = F.female let single = F.single
658 let left xx = select1 F.left1 F.left2 F.left3 xx
659 let saw yy xx = select2 F.saw1 F.saw2 F.saw3 yy xx
660 let marriedto = F.marriedto
661 let kisses yy xx = select2 F.kisses1 F.kisses2 F.kisses3 yy xx
662 let loves yy xx = select2 F.loves1 F.loves2 F.loves3 yy xx
663 let thinks pp xx = failwith "Unimplemented"
664 let maybe (body : sent) : sent =
665 let (yy : R.env -> Y.env -> bool list) = fun e w ->
666 let body_int = List.map (fun w' -> any_truths (X.run (letw w' body) e w)) modal_domain in
667 body_int (* can just use body's intension as the result of `maybe body` *) in
671 (* Sem3b would convert Sem3a into having sentence meanings be Kleisli arrows, as Sem1b did.
672 Not here implemented. *)
674 (* Add intensionality to 2c *)
675 module Sem3c = struct
677 let extensional = false
679 (* Using monad LRY, with type env = var -> entity.
680 Box type is env -> world -> ['a]
681 Types of sentences are env -> world -> [unit]. *)
683 type noun = entity X.t
685 let run xx = X.(not (List.is_null (run xx env0 Actual)))
686 (* lift an 'a list to a single 'a X.t *)
687 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
688 let getx = X.(asks (lookup 'x'))
689 let gety = X.(asks (lookup 'y'))
690 let getz = X.(asks (lookup 'z'))
691 let getw = X.(uask) (* get world from the underlying Y monad *)
692 (* select an intranstive verb based on the world *)
693 let select1 f1 f2 f3 xx = X.(getw >>= fun w -> (if w = Actual then f1 else if w = Second then f2 else f3) xx)
694 (* select a transitive verb based on the world *)
695 let select2 f1 f2 f3 yy xx = X.(getw >>= fun w -> (if w = Actual then f1 else if w = Second then f2 else f3) yy xx)
696 let let_ c (xx : noun) (body : sent) = X.(xx >>= fun x -> shift (insert c x) body)
697 let letw world (body : sent) = X.(ushift (fun _ -> world) body) (* shift the "env" of the underlying Y monad *)
698 let to_unit (x : bool) : unit X.t = X.guard x
700 let (~~~) xx = X.(list_map (fun xs -> if is_null xs then [()] else []) xx)
701 let (&&&) xx yy = X.(xx >> yy)
702 let (|||) xx yy = X.(xx ++ (* ~~~ xx >> *) yy)
703 let (>>>) xx yy = X.(~~~ xx ++ yy)
705 let (>>>) xx yy = X.(~~~ (xx >> ~~~ yy))
708 let some c (body : sent) = X.(let_ c (mids domain) body)
709 let every c (body : sent) = ~~~ (some c (~~~ body))
712 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)
713 let (===) xx yy = X.(map2 (=) xx yy >>= to_unit)
714 let male xx = X.(F.male xx >>= to_unit)
715 let female xx = X.(F.female xx >>= to_unit)
716 let single xx = X.(F.single xx >>= to_unit)
717 let left xx = X.(select1 F.left1 F.left2 F.left3 xx >>= to_unit)
718 let saw yy xx = X.(select2 F.saw1 F.saw2 F.saw3 yy xx >>= to_unit)
719 let marriedto yy xx = X.(F.marriedto yy xx >>= to_unit)
720 let kisses yy xx = X.(select2 F.kisses1 F.kisses2 F.kisses3 yy xx >>= to_unit)
721 let loves yy xx = X.(select2 F.loves1 F.loves2 F.loves3 yy xx >>= to_unit)
722 let thinks pp xx = failwith "Unimplemented"
723 let maybe (body : sent) : sent =
724 let (yy : R.env -> Y.env -> unit list) = fun e w ->
725 let body_int = List.map (fun w' -> not @@ List.is_null @@ X.run (letw w' body) e w) modal_domain in
726 if any_truths body_int then [()] else [] in
730 (* Sem3d would convert Sem3c into having sentence meanings be Kleisli arrows, as Sem1b did.
731 Not here implemented. *)
734 (* Dynamic version of Sem2c *)
735 module Sem5c = struct
737 let extensional = true
739 (* This needs to use monad SL, with store = var -> entity
740 and box type = store -> ['a,store]
741 Sentence meaning is box(unit).
742 Later strategies with more complex sentence meanings and stores
743 may be able to use monad LS, with box type store -> ['a],store
746 type noun = entity X.t
748 let run (xx : sent) : bool = X.(not (List.is_null (run xx env0)))
749 (* lift an 'a list to a single 'a X.t *)
750 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
751 let getx = X.(gets (lookup 'x'))
752 let gety = X.(gets (lookup 'y'))
753 let getz = X.(gets (lookup 'z'))
754 let let_ c (xx : noun) (body : sent) = X.(xx >>= fun x -> modify (insert c x) >> body)
755 let to_unit (x : bool) : unit X.t = X.guard x
757 let (~~~) (xx : sent) : sent =
758 let yy : S.store -> (unit * S.store) list = fun s -> if List.is_null (X.run xx s) then [(),s] else [] in
759 Obj.magic yy (* this is an identity function that changes the type of yy to a unit X.t *)
760 let (&&&) xx yy = X.(xx >> yy)
761 let (|||) xx yy = ~~~ (~~~ xx &&& ~~~ yy)
762 let (>>>) xx yy = X.(~~~ (xx &&& ~~~ yy))
765 This would propagate effects out of the disjuncts, so that for example after
766 "Some y. (x = frank and female y) or Some y. married y x"
767 "y" would be available for anaphor:
768 let (|||) xx yy = X.(xx ++ (~~~ xx >> yy))
770 This wouldn't propagate effects from antecedent to consequent, so that for example
771 "(Some y. marriedto y bill) >>> female gety"
772 has a failed lookup on "y":
773 let (>>>) xx yy = X.(~~~ xx ++ yy)
776 let some c (body : sent) = X.(let_ c (mids domain) body)
777 let every c (body : sent) = ~~~ (some c (~~~ body))
780 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)
781 let (===) xx yy = X.(map2 (=) xx yy >>= to_unit)
782 let male xx = X.(F.male xx >>= to_unit)
783 let female xx = X.(F.female xx >>= to_unit)
784 let single xx = X.(F.single xx >>= to_unit)
785 let left xx = X.(F.left1 xx >>= to_unit)
786 let marriedto yy xx = X.(F.marriedto yy xx >>= to_unit)
787 let saw yy xx = X.(F.saw1 yy xx >>= to_unit)
788 let kisses yy xx = X.(F.kisses1 yy xx >>= to_unit)
789 let loves yy xx = X.(F.loves1 yy xx >>= to_unit)
790 let thinks pp xx = failwith "Unimplemented"
791 let maybe pp = failwith "Unimplemented"
795 (* Dynamic version of Sem3c / Add intensionality to Sem5c *)
796 module Sem6c = struct
798 let extensional = false
800 (* This needs to use monad SLY, with store = var -> entity
801 and box type = store -> world -> ['a,store]
802 Sentence meaning is box(unit).
803 Later strategies with more complex sentence meanings and stores
804 may be able to use monad LSY, with box type store -> world -> ['a],store
807 type noun = entity X.t
809 let run (xx : sent) : bool = X.(not (List.is_null (run xx env0 Actual)))
810 (* lift an 'a list to a single 'a X.t *)
811 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
812 let getx = X.(gets (lookup 'x'))
813 let gety = X.(gets (lookup 'y'))
814 let getz = X.(gets (lookup 'z'))
815 let getw = X.(ask) (* get world from the underlying Y monad *)
816 (* select an intranstive verb based on the world *)
817 let select1 f1 f2 f3 xx = X.(getw >>= fun w -> (if w = Actual then f1 else if w = Second then f2 else f3) xx)
818 (* select a transitive verb based on the world *)
819 let select2 f1 f2 f3 yy xx = X.(getw >>= fun w -> (if w = Actual then f1 else if w = Second then f2 else f3) yy xx)
820 let let_ c (xx : noun) (body : sent) = X.(xx >>= fun x -> modify (insert c x) >> body)
821 let letw world (body : sent) = X.(shift (fun _ -> world) body) (* shift the "env" of the underlying Y monad *)
822 let to_unit (x : bool) : unit X.t = X.guard x
824 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)
827 let (~~~) (xx : sent) : sent =
828 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
829 Obj.magic yy (* this is an identity function that changes the type of yy to a unit X.t *)
831 let (&&&) xx yy = X.(xx >> yy)
832 let (|||) xx yy = ~~~ (~~~ xx &&& ~~~ yy)
833 let (>>>) xx yy = X.(~~~ (xx &&& ~~~ yy))
835 let some c (body : sent) = X.(let_ c (mids domain) body)
836 let every c (body : sent) = ~~~ (some c (~~~ body))
839 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)
840 let (===) xx yy = X.(map2 (=) xx yy >>= to_unit)
841 let male xx = X.(F.male xx >>= to_unit)
842 let female xx = X.(F.female xx >>= to_unit)
843 let single xx = X.(F.single xx >>= to_unit)
844 let left xx = X.(select1 F.left1 F.left2 F.left3 xx >>= to_unit)
845 let saw yy xx = X.(select2 F.saw1 F.saw2 F.saw3 yy xx >>= to_unit)
846 let marriedto yy xx = X.(F.marriedto yy xx >>= to_unit)
847 let kisses yy xx = X.(select2 F.kisses1 F.kisses2 F.kisses3 yy xx >>= to_unit)
848 let loves yy xx = X.(select2 F.loves1 F.loves2 F.loves3 yy xx >>= to_unit)
849 let thinks pp xx = failwith "Unimplemented"
850 let maybe (body : sent) : sent =
851 let (yy : S.store -> Y.env -> (unit * S.store) list) = fun s w ->
852 let body_int = List.map (fun w' -> not @@ List.is_null @@ X.run (letw w' body) s w) modal_domain in
853 if any_truths body_int then [(),s] else [] in
857 (* Sem6c seems adequate for much of 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.
858 Next we develop some semantics that are closer to their actual presentation. *)
860 (* This develops Sem5c using in part the Kleisli strategy from Sem1b. *)
861 module Sem5e = struct
863 let extensional = true
865 (* Let a topic be sequence of entities introduced into conversation (GSV's pegs -> entities, with pegs construed as positions in the sequence).
866 Then let store = var -> int (that is, position in the topic)
867 Then we can use monad LS', with box type = store -> ['a],store
868 And sentence meanings are Kleisli arrows: topic -> box(topic). The list component
869 in the type captures indeterminacy in what objects are being discussed (introduced
870 by quantifiers). Truths (relative to a initial store and topic) result in
871 non-empty topic lists; falsehoods in empty ones.
872 Our stores/envs are GSV's refsys r; our topics are their g.
873 Notice that GSV make their "information states" homogenous wrt r; this corresponds
874 to our result type having stores _outside_ the list.
875 GSV's meaning types are [store * topic * world] -> [store * topic * world], but
876 as noted the homogeneity wrt store would permit also:
877 store * [topic * world] -> store * [topic * world].
878 Our meaning types (once we add worlds in 6e, below) will be:
879 topic -> (store -> world -> ([topic] * store))
880 We count a world as eliminated when it results in an empty list of topics.
881 Note that our Sem6e doesn't yet properly handle Veltman's "might"; see remarks below.
883 type topic = entity list
886 type noun = (topic -> entity) X.t
887 type sent = topic -> topic X.t
888 let run (k : sent) : bool = X.(not (List.is_null (fst (run (k topic0) env0))))
889 (* lift an 'a list to a single 'a X.t *)
890 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
891 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)
892 let getx : noun = X.(gets (lookup 'x') >>= fun n -> mid (get_nth n))
893 let gety : noun = X.(gets (lookup 'y') >>= fun n -> mid (get_nth n))
894 let getz : noun = X.(gets (lookup 'z') >>= fun n -> mid (get_nth n))
895 let let_ c (n : int) (body : sent) : sent = fun top -> X.(modify (insert c n) >> (body top))
897 (* All logical operations except &&& and some are "effect islands", with the exception that effects of the antecedent
898 of a conditional are visible in that conditional's consequent. *)
900 let (~~~) (k : sent) : sent = fun top ->
901 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
902 Obj.magic yy (* this is an identity function that changes the type of yy to a topic X.t *)
903 let (&&&) k j = X.(k >=> j)
904 let (|||) k j = ~~~ (~~~ k &&& ~~~ j)
905 let (>>>) k j = X.(~~~ (k >=> ~~~ j))
907 (* This properly handles `some` as GSV do, by only joining the results
908 _after_ updating them on body(extended topic). See GSV pp. 28-9. *)
909 let some c (body : sent) : sent = fun top ->
910 let n = length top in
911 let aux ent = X.(let_ c n body) (List.snoc top ent) in
912 let domain' = List.map aux domain in
913 X.join (mids domain')
915 let every c (body : sent) = ~~~ (some c (~~~ body))
918 let mapply' (ff : noun) (top : topic) : entity X.t = X.(map (fun f -> f top) ff)
919 let wrap name = X.(mid (const name))
920 let wrap1 f xx = fun top -> X.(f (mapply' xx top) >>= fun b -> if b then mid top else mzero)
921 let wrap2 f xx yy = fun top -> X.(f (mapply' xx top) (mapply' yy top) >>= fun b -> if b then mid top else mzero)
922 let ann = wrap Ann let bill = wrap Bill let carol = wrap Carol let dave = wrap Dave let ella = wrap Ella let frank = wrap Frank
923 let (===) (xx : noun) (yy : noun) : sent = wrap2 X.(map2 (=)) xx yy
924 let male (xx : noun) : sent = wrap1 F.male xx
925 let female xx = wrap1 F.female xx
926 let single xx = wrap1 F.single xx
927 let left xx = wrap1 F.left1 xx
928 let marriedto yy xx = wrap2 F.marriedto yy xx
929 let saw yy xx = wrap2 F.saw1 yy xx
930 let kisses yy xx = wrap2 F.kisses1 yy xx
931 let loves yy xx = wrap2 F.loves1 yy xx
932 let thinks pp xx = fun top -> failwith "Unimplemented"
933 let maybe pp = fun top -> failwith "Unimplemented"
936 (* Add intensionality to Sem5e. See comments there. *)
937 module Sem6e = struct
939 let extensional = false
941 type topic = entity list
944 type noun = (topic -> entity) X.t
945 type sent = topic -> topic X.t
946 let run (k : sent) : bool = X.(not (List.is_null (fst (run (k topic0) env0 Actual))))
947 (* lift an 'a list to a single 'a X.t *)
948 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
949 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)
950 let getx : noun = X.(gets (lookup 'x') >>= fun n -> mid (get_nth n))
951 let gety : noun = X.(gets (lookup 'y') >>= fun n -> mid (get_nth n))
952 let getz : noun = X.(gets (lookup 'z') >>= fun n -> mid (get_nth n))
953 let getw = X.(ask) (* get world from the underlying Y monad *)
954 (* select an intranstive verb based on the world *)
955 let select1 f1 f2 f3 xx = X.(getw >>= fun w -> (if w = Actual then f1 else if w = Second then f2 else f3) xx)
956 (* select a transitive verb based on the world *)
957 let select2 f1 f2 f3 yy xx = X.(getw >>= fun w -> (if w = Actual then f1 else if w = Second then f2 else f3) yy xx)
958 let let_ c (n : int) (body : sent) : sent = fun top -> X.(modify (insert c n) >> (body top))
959 let letw world (body : sent) : sent = fun top -> X.(shift (fun _ -> world) (body top)) (* shift the "env" of the underlying Y monad *)
962 let lookup_string sought env top = try string_of_entity (List.nth top (env sought)) with Not_found -> "*" | List.Short_list -> "#"
963 let print_lookup sought env top = print_string (lookup_string sought env top)
964 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)
965 (* variant of run that uses a non-empty initial topic list, and displays entire result, not just whether it's true *)
966 let run' (k : sent) ?(w=Actual) (tops : topic list) =
967 let n = List.length (List.head tops) in
968 let env = match n with
969 | 1 -> insert 'x' 0 env0
970 | 2 -> insert 'x' 0 (insert 'y' 1 env0)
971 | 3 -> insert 'x' 0 (insert 'y' 1 (insert 'z' 2 env0))
972 | _ -> failwith ("can't run' topics of length " ^ string_of_int n) in
973 assert(for_all (fun top -> List.length top = n) tops);
974 X.(run (mids tops >>= k) env w)
976 let (~~~) (k : sent) : sent = fun top ->
977 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
978 Obj.magic yy (* this is an identity function that changes the type of yy to a topic X.t *)
979 let (&&&) k j = X.(k >=> j)
980 let (|||) k j = ~~~ (~~~ k &&& ~~~ j)
981 let (>>>) k j = X.(~~~ (k >=> ~~~ j))
983 let some c (body : sent) : sent = fun top ->
984 let n = length top in
985 let aux ent = X.(let_ c n body) (List.snoc top ent) in
986 let domain' = List.map aux domain in
987 X.join (mids domain')
989 let every c (body : sent) = ~~~ (some c (~~~ body))
992 let mapply' (ff : noun) (top : topic) : entity X.t = X.(map (fun f -> f top) ff)
993 let wrap name = X.(mid (const name))
994 let wrap1 f xx = fun top -> X.(f (mapply' xx top) >>= fun b -> if b then mid top else mzero)
995 let wrap2 f xx yy = fun top -> X.(f (mapply' xx top) (mapply' yy top) >>= fun b -> if b then mid top else mzero)
996 let ann = wrap Ann let bill = wrap Bill let carol = wrap Carol let dave = wrap Dave let ella = wrap Ella let frank = wrap Frank
997 let (===) (xx : noun) (yy : noun) : sent = wrap2 X.(map2 (=)) xx yy
998 let male (xx : noun) : sent = wrap1 F.male xx
999 let female xx = wrap1 F.female xx
1000 let single xx = wrap1 F.single xx
1001 let left xx = wrap1 (select1 F.left1 F.left2 F.left3) xx
1002 let marriedto yy xx = wrap2 F.marriedto yy xx
1003 let saw yy xx = wrap2 (select2 F.saw1 F.saw2 F.saw3) yy xx
1004 let kisses yy xx = wrap2 (select2 F.kisses1 F.kisses2 F.kisses3) yy xx
1005 let loves yy xx = wrap2 (select2 F.loves1 F.loves2 F.loves3) yy xx
1006 let thinks pp xx = failwith "Unimplemented"
1007 let maybe (body : sent) : sent = fun top ->
1008 let (yy : S'.store -> Y.env -> topic list * S'.store) = fun s w ->
1009 let body_int = List.map (fun w' -> not @@ List.is_null @@ fst @@ X.run (letw w' body top) s w) modal_domain in
1010 if any_truths body_int then [top],s else [],s in
1012 (* This implementation of `maybe` doesn't yet exactly capture Veltman's "might". It isn't a holistic filter:
1013 it examines topics one-by-one and will eliminate any where they (considered in isolation) make body impossible.
1014 Hence, if some of the possible referents for x are essentially not-body, and others are possibly-body, after
1015 updating on _this_ implementation of `maybe body`, we'll be left with only the latter. On Veltman's semantics,
1016 otoh, we'd be left with the whole original information state.
1017 To capture Veltman's semantics properly, we'd need to remove the List component from our monad stack, and use
1018 [topic] as our payloads, so that sent types would then be: [topic] -> S'Y([topic]). All of the operations except
1019 for `maybe` would then have to emulate the operations of the List monad by hand (manually performing catmap etc).
1020 But `maybe` could examine the [topic] as a whole and decide whether to return box(it) or box([]).
1025 module TestAll = struct
1026 print_endline "\nTesting Sem1a";;
1027 module T1a = Test(Sem1a);;
1028 print_endline "\nTesting Sem1b";;
1029 module T1b = Test(Sem1b);;
1030 print_endline "\nTesting Sem2a";;
1031 module T2a = Test(Sem2a);;
1032 print_endline "\nTesting Sem2c";;
1033 module T2c = Test(Sem2c);;
1034 print_endline "\nTesting Sem3a";;
1035 module T3a = Test(Sem3a);;
1036 print_endline "\nTesting Sem3c";;
1037 module T3c = Test(Sem3c);;
1038 print_endline "\nTesting Sem5c";;
1039 module T5c = Test(Sem5c);;
1040 print_endline "\nTesting Sem5e";;
1041 module T5e = Test(Sem5e);;
1042 print_endline "\nTesting Sem6c";;
1043 module T6c = Test(Sem6c);;
1044 print_endline "\nTesting Sem6e";;
1045 module T6e = Test(Sem6e);;
1050 One can't test the broken vase case by comparing the _truth_ of any sentences.
1051 The difference is in whether the sentences have meanings that are "supported by"
1052 the same informtation states. Compare in our model:
1053 (i) Someone kissed me. She might have stayed.
1055 (ii) Someone who might have stayed kissed me.
1056 Recall that in our model Ann leaves in every world, but Carol stays in some (non-actual)
1057 world. If my background information settles that I was kissed by either Ann or Carol,
1058 then I'm in a position to assert (i), since after the first clause it's left open
1059 that the referent be either woman. But it doesn't put me in a position to assert (ii),
1060 since that implies I was kissed by Carol. So far as truth-value goes,
1061 if Carol kissed me both sentences are true, and if Ann did then both sentences are false.
1063 # let module S = Sem6e in let wife xx = S.(female xx &&& ~~~ (single xx)) in let may_stay xx = S.(maybe (~~~ (left xx))) in ...
1064 # let xx = S.(wife getx) in S.(run_ xx [[Ann];[Carol];[Ella]]);;
1065 - : entity list list * S'Y.store = ([[Ann]; [Carol]], <fun>)
1066 # let xx = S.(may_stay getx) in S.(run_ xx [[Ann];[Carol];[Ella]]);;
1067 - : entity list list * S'Y.store = ([[Carol]; [Ella]], <fun>)
1068 # let xx = S.(some 'y' (gety === getx)) in S.(run_ xx [[Ann];[Carol];[Ella]]);;
1069 - : entity list list * S'Y.store = ([[Ann; Ann]; [Carol; Carol]; [Ella; Ella]], <fun>)
1070 # let xx = S.(some 'y' (gety === getx &&& may_stay gety)) in S.(run_ xx [[Ann];[Carol];[Ella]]);;
1071 - : entity list list * S'Y.store = ([[Carol; Carol]; [Ella; Ella]], <fun>)
1072 # let xx = S.(some 'y' (gety === getx) &&& may_stay gety) in S.(run_ xx [[Ann];[Carol];[Ella]]);;
1073 - : entity list list * S'Y.store = ([[Carol; Carol]; [Ella; Ella]], <fun>)