1 (* GSV monadically 15 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 Sem5* would be the dynamic alternative of 1*. (not here provided, but
390 discussed in comments.)
391 You can't implement quantification in these,
392 except by bringing in some of the mechanisms of a list/set component.
393 (You'll create a box([entity]) and convert it to a box([bool]),
394 then convert the latter to box(bool).)
395 However, Haskell already provides the needed mechanisms in the basic Monad API (as the
396 function Juli8 names `seq`), so we can do quantification without _explicitly
397 invoking_ a ListT in our monadic stack.
399 Sem2* and Sem 6* would be the intensionalized versions of those.
400 (Not here provided, but Sem6* is discussed in comments.)
402 Sem3* adds a List component to the stack to do quantification.
403 Sem7* is the dynamic counterpart.
405 Sem4* adds an (additional) Reader monad for intensionality.
406 Sem8* is the dynamic counterpart.
408 Within that broad organization, here are the sub-patterns:
410 SemNa uses just a bool payload, so sent types are box(bool).
411 SemNb makes sent types the Klesli variant of Na, so sent types are
413 SemNc uses instead a unit payload, which we can do when the monadic
414 stack has a List or Option component; then false will be the monad's
415 mzero, whereas truth will be instances of type box(unit) that aren't
417 SemNd would be the Kleisli variant of Nc, as Nb is the Kleisli variant
419 SemNe (only for dynamic) would use "topics" or sequences of entities being discussed
420 as payloads, so sent types are box(topic). What we really provide
421 here is the Kleisli variation of this (SemNf), so sent types = topic -> box(topic).
425 module Sem1a = struct
427 let extensional = true
429 (* We use monad R, with env = var -> entity.
430 Types of sentences are env -> bool. *)
432 type noun = entity X.t
434 let run (xx : sent) : bool = X.(run xx env0 = true)
435 let getx = X.(asks (lookup 'x'))
436 let gety = X.(asks (lookup 'y'))
437 let getz = X.(asks (lookup 'z'))
438 let let_ c (xx : noun) (body : sent) = X.(xx >>= fun x -> shift (insert c x) body)
440 let (~~~) xx = X.(map not xx)
441 let (&&&) xx yy = X.(xx >>= fun b' -> if not b' then mid false else yy)
442 let (|||) xx yy = X.(xx >>= fun b' -> if b' then mid true else yy)
443 let (>>>) xx yy = X.(xx >>= fun b' -> if not b' then mid true else yy)
445 let some c (body : sent) =
446 let (bbs : bool X.t list) = List.map (fun x -> let_ c X.(mid x) body) domain in
447 let (bsb : bool list X.t) = X.seq bbs in
448 let (bb : bool X.t) = X.map (exists ident) bsb in
450 let every c (body : sent) =
451 let (bbs : bool X.t list) = List.map (fun x -> let_ c X.(mid x) body) domain in
452 let (bsb : bool list X.t) = X.seq bbs in
453 let (bb : bool X.t) = X.map (for_all ident) bsb in
457 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)
458 let (===) xx yy = X.(map2 (=) xx yy)
459 let male = F.male let female = F.female let single = F.single let left = F.left1
460 let marriedto = F.marriedto let saw = F.saw1 let kisses = F.kisses1 let loves = F.loves1
461 let thinks pp xx = failwith "Unimplemented"
462 let maybe pp = failwith "Unimplemented"
465 module Sem1b = struct
467 let extensional = true
469 (* We again use monad R, with env = var -> entity.
470 This variant defines sentence meanings as Kleisli arrows, that is:
471 type sent = bool -> bool X.t
472 or equivalently, bool -> (env -> bool). A true sentence takes any bool
473 input to a boxed version of that input (so truth = mid), and a false
474 sentence takes any input to mid false.
475 This more closely parallels the dynamic semantics (though it should not,
476 just on account of that structural similarity, be itself counted as dynamic).
477 It also brings the boolean operations closer to monadic primitives.
480 type noun = entity X.t
481 type sent = bool -> bool X.t
482 let run (k : sent) : bool = X.(run (k true) env0 = true)
483 let getx = X.(asks (lookup 'x'))
484 let gety = X.(asks (lookup 'y'))
485 let getz = X.(asks (lookup 'z'))
486 let let_ c (xx : noun) (body : sent) = fun b -> X.(xx >>= fun x -> shift (insert c x) (body b))
488 let (~~~) k = fun b -> X.(if b then map not (k true) else mid false)
489 let (&&&) k j = X.(k >=> j)
490 let (|||) k j = ~~~ (~~~ k &&& ~~~ j)
491 let (>>>) k j = ~~~ k ||| j
493 let (|||) xx yy = fun b -> X.(xx b >>= fun b' -> if b' then mid true else yy b)
494 let (>>>) xx yy = fun b -> X.(xx b >>= fun b' -> if not b' then mid true else yy b)
495 let (>>>) k j = ~~~ (k &&& ~~~ j)
498 let some c (body : sent) = fun b ->
499 let (bbs : bool X.t list) = List.map (fun x -> let_ c X.(mid x) body b) domain in
500 let (bsb : bool list X.t) = X.seq bbs in
501 let (bb : bool X.t) = X.map (exists ident) bsb in
503 let every c (body : sent) = fun b ->
504 let (bbs : bool X.t list) = List.map (fun x -> let_ c X.(mid x) body b) domain in
505 let (bsb : bool list X.t) = X.seq bbs in
506 let (bb : bool X.t) = X.map (for_all ident) bsb in
510 let to_kleisli xx = fun b -> X.(xx >>= fun b' -> mid (b && b'))
511 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)
512 let (===) xx yy = to_kleisli X.(map2 (=) xx yy)
513 let male = to_kleisli % F.male let female = to_kleisli % F.female let single = to_kleisli % F.single let left = to_kleisli % F.left1
514 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)
515 let thinks pp xx = fun b -> failwith "Unimplemented"
516 let maybe pp = fun b -> failwith "Unimplemented"
519 module Sem3a = struct
521 let extensional = true
523 (* We could use either monad RL or LR, with type env = var -> entity.
524 Their box type is the same: env -> ['a]
525 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.
526 We use the box type in two ways: first, we use a box(entity) to compute whether a matrix
527 clause is satisfied by a bound pronoun, where entity ranges over the whole domain.
528 Second, it is convenient and more consonant with later strategies
529 to re-use the same monad for sentence types (rather than using a simpler monad
530 that lacks a List component). Here we will let the types of sentences
531 be box(bool), that is: env -> [bool]. We will understand the sentence to be true
532 if there are ANY truths in the resulting list. A list of all falses is treated
533 the same as an empty list. Sem3c, below, eliminates this artifact by changing
534 the sentence type to box(unit). Then truths (rel to an env) are [();...] and
538 type noun = entity X.t
540 let run (xx : sent) : bool = X.(any_truths (run xx env0))
541 (* lift an 'a list to a single 'a X.t *)
542 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
543 let getx = X.(asks (lookup 'x'))
544 let gety = X.(asks (lookup 'y'))
545 let getz = X.(asks (lookup 'z'))
546 let let_ c (xx : noun) (body : sent) = X.(xx >>= fun x -> shift (insert c x) body)
548 let (~~~) xx = X.(map not xx)
549 let (&&&) xx yy = X.(xx >>= fun b' -> if not b' then mid false else yy)
550 let (|||) xx yy = X.(xx >>= fun b' -> if b' then mid true else yy)
551 let (>>>) xx yy = X.(xx >>= fun b' -> if not b' then mid true else yy)
553 (* On this semantics, `some c body` is a list of the boolean outcomes for body for each assignment to c.
554 That matches our convention for sentence types, where any truth in the list means the sentence is true.
555 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.
556 In later semantics, the duality of `some` and `every` will be restored.
558 let some c (body : sent) = X.(let_ c (mids domain) body)
559 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 *)
562 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)
563 let (===) xx yy = X.(map2 (=) xx yy)
564 let male = F.male let female = F.female let single = F.single let left = F.left1
565 let marriedto = F.marriedto let saw = F.saw1 let kisses = F.kisses1 let loves = F.loves1
566 let thinks pp xx = failwith "Unimplemented"
567 let maybe pp = failwith "Unimplemented"
570 (* Sem3b would convert Sem3a into having sentence meanings be Kleisli arrows, as Sem1b did.
571 Not here implemented. *)
573 (* Variant of Sem3a, which uses [();...] vs [] instead of [true;...] vs (list of all false OR []). *)
574 module Sem3c = struct
576 let extensional = true
578 (* We use monad LR as above, with same env = var -> entity and box type = env -> ['a].
579 We again use box(entity) to compute whether matrix clauses are satisfied by
580 bound pronouns; but now we use box(unit) for the types of sentences.
581 Truths (rel to an env) are [();...] and falsehood is [].
584 type noun = entity X.t
586 let run (xx : sent) : bool = X.(not (List.is_null (run xx env0)))
587 (* lift an 'a list to a single 'a X.t *)
588 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
589 let getx = X.(asks (lookup 'x'))
590 let gety = X.(asks (lookup 'y'))
591 let getz = X.(asks (lookup 'z'))
592 let let_ c (xx : noun) (body : sent) = X.(xx >>= fun x -> shift (insert c x) body)
593 let to_unit (x : bool) : unit X.t = X.guard x
595 let (~~~) xx = X.(list_map (fun xs -> if is_null xs then [()] else []) xx)
596 let (&&&) xx yy = X.(xx >> yy)
597 let (|||) xx yy = X.(xx ++ (* ~~~ xx >> *) yy)
598 let (>>>) xx yy = X.(~~~ xx ++ yy)
600 let (>>>) xx yy = X.(~~~ (xx >> ~~~ yy))
603 let some c (body : sent) = X.(let_ c (mids domain) body)
604 let every c (body : sent) = ~~~ (some c (~~~ body))
607 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)
608 let (===) xx yy = X.(map2 (=) xx yy >>= to_unit)
609 let male xx = X.(F.male xx >>= to_unit)
610 let female xx = X.(F.female xx >>= to_unit)
611 let single xx = X.(F.single xx >>= to_unit)
612 let left xx = X.(F.left1 xx >>= to_unit)
613 let marriedto yy xx = X.(F.marriedto yy xx >>= to_unit)
614 let saw yy xx = X.(F.saw1 yy xx >>= to_unit)
615 let kisses yy xx = X.(F.kisses1 yy xx >>= to_unit)
616 let loves yy xx = X.(F.loves1 yy xx >>= to_unit)
617 let thinks pp xx = failwith "Unimplemented"
618 let maybe pp = failwith "Unimplemented"
621 (* Sem3d would convert Sem3c into having sentence meanings be Kleisli arrows, as Sem1b did.
622 Not here implemented. *)
624 (* Add intensionality to 2a *)
625 module Sem4a = struct
627 let extensional = false
629 (* Using monad LRY, with type env = var -> entity.
630 Box type is env -> world -> ['a]
631 Types of sentences are env -> world -> [bool]. *)
633 type noun = entity X.t
635 let run xx = X.(any_truths (run xx env0 Actual))
636 (* lift an 'a list to a single 'a X.t *)
637 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
638 let getx = X.(asks (lookup 'x'))
639 let gety = X.(asks (lookup 'y'))
640 let getz = X.(asks (lookup 'z'))
641 let getw = X.(uask) (* get world from the underlying Y monad *)
642 (* select an intranstive verb based on the world *)
643 let select1 f1 f2 f3 xx = X.(getw >>= fun w -> (if w = Actual then f1 else if w = Second then f2 else f3) xx)
644 (* select a transitive verb based on the world *)
645 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)
646 let let_ c (xx : noun) (body : sent) = X.(xx >>= fun x -> shift (insert c x) body)
647 let letw world (body : sent) = X.(ushift (fun _ -> world) body) (* shift the "env" of the underlying Y monad *)
649 let (~~~) xx = X.(map not xx)
650 let (&&&) xx yy = X.(xx >>= fun b' -> if not b' then mid false else yy)
651 let (|||) xx yy = X.(xx >>= fun b' -> if b' then mid true else yy)
652 let (>>>) xx yy = X.(xx >>= fun b' -> if not b' then mid true else yy)
654 let some c (body : sent) = X.(let_ c (mids domain) body)
655 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)
658 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)
659 let (===) xx yy = X.(map2 (=) xx yy)
660 let male = F.male let female = F.female let single = F.single
661 let left xx = select1 F.left1 F.left2 F.left3 xx
662 let saw yy xx = select2 F.saw1 F.saw2 F.saw3 yy xx
663 let marriedto = F.marriedto
664 let kisses yy xx = select2 F.kisses1 F.kisses2 F.kisses3 yy xx
665 let loves yy xx = select2 F.loves1 F.loves2 F.loves3 yy xx
666 let thinks pp xx = failwith "Unimplemented"
667 let maybe (body : sent) : sent =
668 let (yy : R.env -> Y.env -> bool list) = fun e w ->
669 let body_int = List.map (fun w' -> any_truths (X.run (letw w' body) e w)) modal_domain in
670 body_int (* can just use body's intension as the result of `maybe body` *) in
674 (* Sem4b would convert Sem4a into having sentence meanings be Kleisli arrows, as Sem1b did.
675 Not here implemented. *)
677 (* Add intensionality to 2c *)
678 module Sem4c = struct
680 let extensional = false
682 (* Using monad LRY, with type env = var -> entity.
683 Box type is env -> world -> ['a]
684 Types of sentences are env -> world -> [unit]. *)
686 type noun = entity X.t
688 let run xx = X.(not (List.is_null (run xx env0 Actual)))
689 (* lift an 'a list to a single 'a X.t *)
690 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
691 let getx = X.(asks (lookup 'x'))
692 let gety = X.(asks (lookup 'y'))
693 let getz = X.(asks (lookup 'z'))
694 let getw = X.(uask) (* get world from the underlying Y monad *)
695 (* select an intranstive verb based on the world *)
696 let select1 f1 f2 f3 xx = X.(getw >>= fun w -> (if w = Actual then f1 else if w = Second then f2 else f3) xx)
697 (* select a transitive verb based on the world *)
698 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)
699 let let_ c (xx : noun) (body : sent) = X.(xx >>= fun x -> shift (insert c x) body)
700 let letw world (body : sent) = X.(ushift (fun _ -> world) body) (* shift the "env" of the underlying Y monad *)
701 let to_unit (x : bool) : unit X.t = X.guard x
703 let (~~~) xx = X.(list_map (fun xs -> if is_null xs then [()] else []) xx)
704 let (&&&) xx yy = X.(xx >> yy)
705 let (|||) xx yy = X.(xx ++ (* ~~~ xx >> *) yy)
706 let (>>>) xx yy = X.(~~~ xx ++ yy)
708 let (>>>) xx yy = X.(~~~ (xx >> ~~~ yy))
711 let some c (body : sent) = X.(let_ c (mids domain) body)
712 let every c (body : sent) = ~~~ (some c (~~~ body))
715 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)
716 let (===) xx yy = X.(map2 (=) xx yy >>= to_unit)
717 let male xx = X.(F.male xx >>= to_unit)
718 let female xx = X.(F.female xx >>= to_unit)
719 let single xx = X.(F.single xx >>= to_unit)
720 let left xx = X.(select1 F.left1 F.left2 F.left3 xx >>= to_unit)
721 let saw yy xx = X.(select2 F.saw1 F.saw2 F.saw3 yy xx >>= to_unit)
722 let marriedto yy xx = X.(F.marriedto yy xx >>= to_unit)
723 let kisses yy xx = X.(select2 F.kisses1 F.kisses2 F.kisses3 yy xx >>= to_unit)
724 let loves yy xx = X.(select2 F.loves1 F.loves2 F.loves3 yy xx >>= to_unit)
725 let thinks pp xx = failwith "Unimplemented"
726 let maybe (body : sent) : sent =
727 let (yy : R.env -> Y.env -> unit list) = fun e w ->
728 let body_int = List.map (fun w' -> not @@ List.is_null @@ X.run (letw w' body) e w) modal_domain in
729 if any_truths body_int then [()] else [] in
733 (* Sem4d would convert Sem4c into having sentence meanings be Kleisli arrows, as Sem1b did.
734 Not here implemented. *)
737 (* Dynamic version of Sem3c *)
738 module Sem7c = struct
740 let extensional = true
742 (* This needs to use monad SL, with store = var -> entity
743 and box type = store -> ['a,store]
744 Sentence meaning is box(unit).
745 Later strategies with more complex sentence meanings and stores
746 may be able to use monad LS, with box type store -> ['a],store
749 type noun = entity X.t
751 let run (xx : sent) : bool = X.(not (List.is_null (run xx env0)))
752 (* lift an 'a list to a single 'a X.t *)
753 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
754 let getx = X.(gets (lookup 'x'))
755 let gety = X.(gets (lookup 'y'))
756 let getz = X.(gets (lookup 'z'))
757 let let_ c (xx : noun) (body : sent) = X.(xx >>= fun x -> modify (insert c x) >> body)
758 let to_unit (x : bool) : unit X.t = X.guard x
760 let (~~~) (xx : sent) : sent =
761 let yy : S.store -> (unit * S.store) list = fun s -> if List.is_null (X.run xx s) then [(),s] else [] in
762 Obj.magic yy (* this is an identity function that changes the type of yy to a unit X.t *)
763 let (&&&) xx yy = X.(xx >> yy)
764 let (|||) xx yy = ~~~ (~~~ xx &&& ~~~ yy)
765 let (>>>) xx yy = X.(~~~ (xx &&& ~~~ yy))
768 This would propagate effects out of the disjuncts, so that for example after
769 "Some y. (x = frank and female y) or Some y. married y x"
770 "y" would be available for anaphor:
771 let (|||) xx yy = X.(xx ++ (~~~ xx >> yy))
773 This wouldn't propagate effects from antecedent to consequent, so that for example
774 "(Some y. marriedto y bill) >>> female gety"
775 has a failed lookup on "y":
776 let (>>>) xx yy = X.(~~~ xx ++ yy)
779 let some c (body : sent) = X.(let_ c (mids domain) body)
780 let every c (body : sent) = ~~~ (some c (~~~ body))
783 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)
784 let (===) xx yy = X.(map2 (=) xx yy >>= to_unit)
785 let male xx = X.(F.male xx >>= to_unit)
786 let female xx = X.(F.female xx >>= to_unit)
787 let single xx = X.(F.single xx >>= to_unit)
788 let left xx = X.(F.left1 xx >>= to_unit)
789 let marriedto yy xx = X.(F.marriedto yy xx >>= to_unit)
790 let saw yy xx = X.(F.saw1 yy xx >>= to_unit)
791 let kisses yy xx = X.(F.kisses1 yy xx >>= to_unit)
792 let loves yy xx = X.(F.loves1 yy xx >>= to_unit)
793 let thinks pp xx = failwith "Unimplemented"
794 let maybe pp = failwith "Unimplemented"
798 (* Dynamic version of Sem4c / Add intensionality to Sem7c *)
799 module Sem8c = struct
801 let extensional = false
803 (* This needs to use monad SLY, with store = var -> entity
804 and box type = store -> world -> ['a,store]
805 Sentence meaning is box(unit).
806 Later strategies with more complex sentence meanings and stores
807 may be able to use monad LSY, with box type store -> world -> ['a],store
810 type noun = entity X.t
812 let run (xx : sent) : bool = X.(not (List.is_null (run xx env0 Actual)))
813 (* lift an 'a list to a single 'a X.t *)
814 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
815 let getx = X.(gets (lookup 'x'))
816 let gety = X.(gets (lookup 'y'))
817 let getz = X.(gets (lookup 'z'))
818 let getw = X.(ask) (* get world from the underlying Y monad *)
819 (* select an intranstive verb based on the world *)
820 let select1 f1 f2 f3 xx = X.(getw >>= fun w -> (if w = Actual then f1 else if w = Second then f2 else f3) xx)
821 (* select a transitive verb based on the world *)
822 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)
823 let let_ c (xx : noun) (body : sent) = X.(xx >>= fun x -> modify (insert c x) >> body)
824 let letw world (body : sent) = X.(shift (fun _ -> world) body) (* shift the "env" of the underlying Y monad *)
825 let to_unit (x : bool) : unit X.t = X.guard x
827 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)
830 let (~~~) (xx : sent) : sent =
831 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
832 Obj.magic yy (* this is an identity function that changes the type of yy to a unit X.t *)
834 let (&&&) xx yy = X.(xx >> yy)
835 let (|||) xx yy = ~~~ (~~~ xx &&& ~~~ yy)
836 let (>>>) xx yy = X.(~~~ (xx &&& ~~~ yy))
838 let some c (body : sent) = X.(let_ c (mids domain) body)
839 let every c (body : sent) = ~~~ (some c (~~~ body))
842 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)
843 let (===) xx yy = X.(map2 (=) xx yy >>= to_unit)
844 let male xx = X.(F.male xx >>= to_unit)
845 let female xx = X.(F.female xx >>= to_unit)
846 let single xx = X.(F.single xx >>= to_unit)
847 let left xx = X.(select1 F.left1 F.left2 F.left3 xx >>= to_unit)
848 let saw yy xx = X.(select2 F.saw1 F.saw2 F.saw3 yy xx >>= to_unit)
849 let marriedto yy xx = X.(F.marriedto yy xx >>= to_unit)
850 let kisses yy xx = X.(select2 F.kisses1 F.kisses2 F.kisses3 yy xx >>= to_unit)
851 let loves yy xx = X.(select2 F.loves1 F.loves2 F.loves3 yy xx >>= to_unit)
852 let thinks pp xx = failwith "Unimplemented"
853 let maybe (body : sent) : sent =
854 let (yy : S.store -> Y.env -> (unit * S.store) list) = fun s w ->
855 let body_int = List.map (fun w' -> not @@ List.is_null @@ X.run (letw w' body) s w) modal_domain in
856 if any_truths body_int then [(),s] else [] in
860 (* Sem8c seems adequate for much of the phenomena GSV are examining, and is substantially simpler than their own semantics. Sem8c doesn't have their "pegs" and complex two-stage function from vars to referents.
861 Next we develop some semantics that are closer to their actual presentation. *)
863 (* This develops Sem7c using in part the Kleisli strategy from Sem1b. *)
864 module Sem7f = struct
866 let extensional = true
868 (* Let a topic be sequence of entities introduced into conversation (GSV's pegs -> entities, with pegs construed as positions in the sequence).
869 Then let store = var -> int (that is, position in the topic)
870 Then we can use monad LS', with box type = store -> ['a],store
871 And sentence meanings are Kleisli arrows: topic -> box(topic). The list component
872 in the type captures indeterminacy in what objects are being discussed (introduced
873 by quantifiers). Truths (relative to a initial store and topic) result in
874 non-empty topic lists; falsehoods in empty ones.
875 Our stores/envs are GSV's refsys r; our topics are their g.
876 Notice that GSV make their "information states" homogenous wrt r; this corresponds
877 to our result type having stores _outside_ the list.
878 GSV's meaning types are [store * topic * world] -> [store * topic * world], but
879 as noted the homogeneity wrt store would permit also:
880 store * [topic * world] -> store * [topic * world].
881 Our meaning types (once we add worlds in 6e, below) will be:
882 topic -> (store -> world -> ([topic] * store))
883 We count a world as eliminated when it results in an empty list of topics.
884 Note that our Sem8f doesn't yet properly handle Veltman's "might"; see remarks below.
886 type topic = entity list
889 type noun = (topic -> entity) X.t
890 type sent = topic -> topic X.t
891 let run (k : sent) : bool = X.(not (List.is_null (fst (run (k topic0) env0))))
892 (* lift an 'a list to a single 'a X.t *)
893 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
894 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)
895 let getx : noun = X.(gets (lookup 'x') >>= fun n -> mid (get_nth n))
896 let gety : noun = X.(gets (lookup 'y') >>= fun n -> mid (get_nth n))
897 let getz : noun = X.(gets (lookup 'z') >>= fun n -> mid (get_nth n))
898 let let_ c (n : int) (body : sent) : sent = fun top -> X.(modify (insert c n) >> (body top))
900 (* All logical operations except &&& and some are "effect islands", with the exception that effects of the antecedent
901 of a conditional are visible in that conditional's consequent. *)
903 let (~~~) (k : sent) : sent = fun top ->
904 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
905 Obj.magic yy (* this is an identity function that changes the type of yy to a topic X.t *)
906 let (&&&) k j = X.(k >=> j)
907 let (|||) k j = ~~~ (~~~ k &&& ~~~ j)
908 let (>>>) k j = X.(~~~ (k >=> ~~~ j))
910 (* This properly handles `some` as GSV do, by only joining the results
911 _after_ updating them on body(extended topic). See GSV pp. 28-9. *)
912 let some c (body : sent) : sent = fun top ->
913 let n = length top in
914 let aux ent = X.(let_ c n body) (List.snoc top ent) in
915 let domain' = List.map aux domain in
916 X.join (mids domain')
918 let every c (body : sent) = ~~~ (some c (~~~ body))
921 let mapply' (ff : noun) (top : topic) : entity X.t = X.(map (fun f -> f top) ff)
922 let wrap name = X.(mid (const name))
923 let wrap1 f xx = fun top -> X.(f (mapply' xx top) >>= fun b -> if b then mid top else mzero)
924 let wrap2 f xx yy = fun top -> X.(f (mapply' xx top) (mapply' yy top) >>= fun b -> if b then mid top else mzero)
925 let ann = wrap Ann let bill = wrap Bill let carol = wrap Carol let dave = wrap Dave let ella = wrap Ella let frank = wrap Frank
926 let (===) (xx : noun) (yy : noun) : sent = wrap2 X.(map2 (=)) xx yy
927 let male (xx : noun) : sent = wrap1 F.male xx
928 let female xx = wrap1 F.female xx
929 let single xx = wrap1 F.single xx
930 let left xx = wrap1 F.left1 xx
931 let marriedto yy xx = wrap2 F.marriedto yy xx
932 let saw yy xx = wrap2 F.saw1 yy xx
933 let kisses yy xx = wrap2 F.kisses1 yy xx
934 let loves yy xx = wrap2 F.loves1 yy xx
935 let thinks pp xx = fun top -> failwith "Unimplemented"
936 let maybe pp = fun top -> failwith "Unimplemented"
939 (* Add intensionality to Sem7f. See comments there. *)
940 module Sem8f = struct
942 let extensional = false
944 type topic = entity list
947 type noun = (topic -> entity) X.t
948 type sent = topic -> topic X.t
949 let run (k : sent) : bool = X.(not (List.is_null (fst (run (k topic0) env0 Actual))))
950 (* lift an 'a list to a single 'a X.t *)
951 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
952 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)
953 let getx : noun = X.(gets (lookup 'x') >>= fun n -> mid (get_nth n))
954 let gety : noun = X.(gets (lookup 'y') >>= fun n -> mid (get_nth n))
955 let getz : noun = X.(gets (lookup 'z') >>= fun n -> mid (get_nth n))
956 let getw = X.(ask) (* get world from the underlying Y monad *)
957 (* select an intranstive verb based on the world *)
958 let select1 f1 f2 f3 xx = X.(getw >>= fun w -> (if w = Actual then f1 else if w = Second then f2 else f3) xx)
959 (* select a transitive verb based on the world *)
960 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)
961 let let_ c (n : int) (body : sent) : sent = fun top -> X.(modify (insert c n) >> (body top))
962 let letw world (body : sent) : sent = fun top -> X.(shift (fun _ -> world) (body top)) (* shift the "env" of the underlying Y monad *)
965 let lookup_string sought env top = try string_of_entity (List.nth top (env sought)) with Not_found -> "*" | List.Short_list -> "#"
966 let print_lookup sought env top = print_string (lookup_string sought env top)
967 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)
968 (* variant of run that uses a non-empty initial topic list, and displays entire result, not just whether it's true *)
969 let run' (k : sent) ?(w=Actual) (tops : topic list) =
970 let n = List.length (List.head tops) in
971 let env = match n with
972 | 1 -> insert 'x' 0 env0
973 | 2 -> insert 'x' 0 (insert 'y' 1 env0)
974 | 3 -> insert 'x' 0 (insert 'y' 1 (insert 'z' 2 env0))
975 | _ -> failwith ("can't run' topics of length " ^ string_of_int n) in
976 assert(for_all (fun top -> List.length top = n) tops);
977 X.(run (mids tops >>= k) env w)
979 let (~~~) (k : sent) : sent = fun top ->
980 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
981 Obj.magic yy (* this is an identity function that changes the type of yy to a topic X.t *)
982 let (&&&) k j = X.(k >=> j)
983 let (|||) k j = ~~~ (~~~ k &&& ~~~ j)
984 let (>>>) k j = X.(~~~ (k >=> ~~~ j))
986 let some c (body : sent) : sent = fun top ->
987 let n = length top in
988 let aux ent = X.(let_ c n body) (List.snoc top ent) in
989 let domain' = List.map aux domain in
990 X.join (mids domain')
992 let every c (body : sent) = ~~~ (some c (~~~ body))
995 let mapply' (ff : noun) (top : topic) : entity X.t = X.(map (fun f -> f top) ff)
996 let wrap name = X.(mid (const name))
997 let wrap1 f xx = fun top -> X.(f (mapply' xx top) >>= fun b -> if b then mid top else mzero)
998 let wrap2 f xx yy = fun top -> X.(f (mapply' xx top) (mapply' yy top) >>= fun b -> if b then mid top else mzero)
999 let ann = wrap Ann let bill = wrap Bill let carol = wrap Carol let dave = wrap Dave let ella = wrap Ella let frank = wrap Frank
1000 let (===) (xx : noun) (yy : noun) : sent = wrap2 X.(map2 (=)) xx yy
1001 let male (xx : noun) : sent = wrap1 F.male xx
1002 let female xx = wrap1 F.female xx
1003 let single xx = wrap1 F.single xx
1004 let left xx = wrap1 (select1 F.left1 F.left2 F.left3) xx
1005 let marriedto yy xx = wrap2 F.marriedto yy xx
1006 let saw yy xx = wrap2 (select2 F.saw1 F.saw2 F.saw3) yy xx
1007 let kisses yy xx = wrap2 (select2 F.kisses1 F.kisses2 F.kisses3) yy xx
1008 let loves yy xx = wrap2 (select2 F.loves1 F.loves2 F.loves3) yy xx
1009 let thinks pp xx = failwith "Unimplemented"
1010 let maybe (body : sent) : sent = fun top ->
1011 let (yy : S'.store -> Y.env -> topic list * S'.store) = fun s w ->
1012 let body_int = List.map (fun w' -> not @@ List.is_null @@ fst @@ X.run (letw w' body top) s w) modal_domain in
1013 if any_truths body_int then [top],s else [],s in
1015 (* This implementation of `maybe` doesn't yet exactly capture Veltman's "might". It isn't a holistic filter:
1016 it examines topics one-by-one and will eliminate any where they (considered in isolation) make body impossible.
1017 Hence, if some of the possible referents for x are essentially not-body, and others are possibly-body, after
1018 updating on _this_ implementation of `maybe body`, we'll be left with only the latter. On Veltman's semantics,
1019 otoh, we'd be left with the whole original information state.
1020 To capture Veltman's semantics properly, we'd need to remove the List component from our monad stack, and use
1021 [topic] as our payloads, so that sent types would then be: [topic] -> S'Y([topic]). All of the operations except
1022 for `maybe` would then have to emulate the operations of the List monad by hand (manually performing catmap etc).
1023 But `maybe` could examine the [topic] as a whole and decide whether to return box(it) or box([]).
1024 This would be to go back to the Sem5/Sem6 choices of monads (without list), and to implement the handling of lists
1025 by hand, as we did in the Sem1/Sem2 strategies.
1027 Additionally, we haven't tried here to handle non-rigid noun-types. That's why we can have sent types be:
1028 topic (or [topic]) -> store -> world -> ([topic], store)
1029 the input topic doesn't depend on what the world is. GSV's types are suited to handle non-rigid noun types,
1030 since they are instead using an analogue of (world * topic) -> store -> ([world,topic], store). We could follow suit,
1031 removing the Reader monad implementing Intensionality from our stack and implementing that by hand, too. Another
1032 strategy would be to continue using a Reader monad but not by merging it into our main monad stack, instead using
1033 values of _that_ box type as _payloads for_ our main box type. This echoes a question raised by Dylan in seminar:
1034 why must we combine the monads only by way of "stacking them" into a single monad? As Jim said in seminar, it's not
1035 obvious one must do so, it just seems most natural. The strategy being evisaged now would at least in part follow
1036 Dylan's suggestion. We'd let our sentence types then be:
1037 intensionality_box([topic]) -> state_plus_intensionality_box(intensionality_box([topic]))
1038 = intensionality_box([topic]) -> store -> world -> (intensionality_box([topic]) * store)
1039 In that case, I think we could once again merge the list component into the intensionality_box type, getting:
1040 intens_list_box(topic) -> state_intens_box(intens_list_box(topic))
1041 = intens_list_box(topic) -> store -> world -> (intens_list_box(topic) * store)
1042 = (world -> [topic]) -> store -> world -> ((world -> [topic]) * store)
1043 That looks like a pretty complicated type, and might not seem an improvement over GSV's own system. But its advantage is that
1044 the implementation of its operations would so closely parallel the other semantic strategies illustrated above.
1045 Testifying to the "modularity" of monads, which we have been recommending as one of their prominent virtues.
1050 module TestAll = struct
1051 print_endline "\nTesting Sem1a";;
1052 module T1a = Test(Sem1a);;
1053 print_endline "\nTesting Sem1b";;
1054 module T1b = Test(Sem1b);;
1055 print_endline "\nTesting Sem3a";;
1056 module T3a = Test(Sem3a);;
1057 print_endline "\nTesting Sem3c";;
1058 module T3c = Test(Sem3c);;
1059 print_endline "\nTesting Sem4a";;
1060 module T4a = Test(Sem4a);;
1061 print_endline "\nTesting Sem4c";;
1062 module T4c = Test(Sem4c);;
1063 print_endline "\nTesting Sem7c";;
1064 module T7c = Test(Sem7c);;
1065 print_endline "\nTesting Sem7f";;
1066 module T7f = Test(Sem7f);;
1067 print_endline "\nTesting Sem8c";;
1068 module T8c = Test(Sem8c);;
1069 print_endline "\nTesting Sem8f";;
1070 module T8f = Test(Sem8f);;
1075 One can't test the broken vase case by comparing the _truth_ of any sentences.
1076 The difference is in whether the sentences have meanings that are "supported by"
1077 the same informtation states. Compare in our model:
1078 (i) Someone kissed me. She might have stayed.
1080 (ii) Someone who might have stayed kissed me.
1081 Recall that in our model Ann leaves in every world, but Carol stays in some (non-actual)
1082 world. If my background information settles that I was kissed by either Ann or Carol,
1083 then I'm in a position to assert (i), since after the first clause it's left open
1084 that the referent be either woman. But it doesn't put me in a position to assert (ii),
1085 since that implies I was kissed by Carol. So far as truth-value goes,
1086 if Carol kissed me both sentences are true, and if Ann did then both sentences are false.