abd305f69573dbd4c7e0485734d06147b662a0ce
[lambda.git] / code / gsv.ml
1 (* GSV monadically 13 April 2015 *)
2
3 type identifier = char
4 let any_truths (xs : 'a list) : bool = List.exists ident xs
5 let all_truths (xs : 'a list) : bool = List.for_all ident xs
6
7 module type SEMANTICS = sig
8   type noun (* this is whatever monadic type the semantics assigns to noun-sized contents *)
9   type sent (* this is whatever monadic type the semantics assigns to sentence-sized contents *)
10   val run : sent -> bool
11   val dynamic : bool
12   val extensional : bool
13
14   val getx : noun  val gety : noun  val getz : noun
15   (* OCaml will parse ~~~ as a prefix operator, but unfortunately won't let you say
16      `~~~ predicate subject`; you have to say `~~~ (predicate subject)`. *)
17   val ( ~~~ ) : sent -> sent
18   (* OCaml will parse these three as infix operators (yay), but makes them all
19      left-associative (ehh for >>>) and have the same precedence (boo). *)
20   val ( &&& ) : sent -> sent -> sent
21   val ( ||| ) : sent -> sent -> sent
22   val ( >>> ) : sent -> sent -> sent
23   (* OCaml parses this with same associativity and precedence as the preceding (boo). *)
24   val (===) : noun -> noun -> sent
25   val ann : noun  val bill : noun  val carol : noun  val dave : noun  val ella : noun  val frank : noun
26   val male : noun -> sent  val female : noun -> sent
27   val left : noun -> sent
28   val single : noun -> sent
29   (* Transitive verbs apply to their direct objs first, subjects second. *)
30   val marriedto : noun -> noun -> sent
31   val saw : noun -> noun -> sent
32   val kisses : noun -> noun -> sent
33   val loves : noun -> noun -> sent   (* here construed extensionally *)
34   (* Quantifiers may be unimplemented. *)
35   val some : identifier -> sent -> sent
36   val every : identifier -> sent -> sent
37   (* Intensional verbs and operators may be unimplemented. *)
38   val thinks : sent -> noun -> sent
39   val maybe : sent -> sent
40 end
41
42 type world = Actual | Other | Another
43 let modal_domain = [Actual; Other; Another]
44
45 type entity = Ann | Bill | Carol | Dave | Ella | Frank
46 let domain = [Ann; Bill; Carol; Dave; Ella; Frank]
47 let string_of_entity = function
48   | Ann -> "Ann"
49   | Bill -> "Bill"
50   | Carol -> "Carol"
51   | Dave -> "Dave"
52   | Ella -> "Ella"
53   | Frank -> "Frank"
54 let print_entity ent = print_string (string_of_entity ent)
55
56 module Facts(X : Monad.MONAD) = struct
57 (* Here are the atomic facts: Ann and Bill are married, also Carol and Dave.
58    Genders and marital statuses are epistemically necessary.
59    In the actual world (w1), everyone left; people look leftwards (Carol sees Bill and Ann, etc.); Carol and Dave kiss; husbands love only their wives and Frank loves all the women.
60    In w2, all but Carol left; no one sees anything; all spouses kiss; all men love only Carol and Ella loves the wives.
61    In w3, only Ann and Bill left; no one sees anything; nobody kisses; Frank loves everyone else.
62 *)
63
64   let is_male = function Bill | Dave | Frank -> true | _ -> false
65   let are_married = function (Ann, Bill) | (Bill, Ann) | (Carol, Dave) | (Dave, Carol) -> true | _ -> false
66   let is_a_wife = function Ann | Carol -> true | _ -> false
67   
68   let male xx = X.(map is_male xx)
69   let female xx = X.(map (not % is_male) xx)
70
71 (* Ella and Frank are single *)
72   let single xx = X.(map (fun x -> x > Dave) xx)
73
74 (* Actually (in w1), everybody left. In w2, everybody but Carol left. In w3, only Ann and Bill left. *)
75   let left1 xx = X.(map (fun _ -> true) xx)
76   let left2 xx = X.(map (fun x -> x <> Carol) xx)
77   let left3 xx = X.(map (fun x -> x = Ann || x = Bill) xx)
78   
79 (* In the sentences, order of application is: TransitiveVerb + Object + Subject.
80    But we convert to logical order for our operations. *)
81
82 (* Actually, each person saw the people alphabetically before them. In w2 and w3, no one saw anyone. *)
83   let saw1 yy xx = X.(map2 (fun x y -> x < y) xx yy)
84   let saw2 yy xx = X.(map2 (fun _ _ -> false) xx yy)
85   let saw3 = saw2
86   
87 (* Necessarily, Ann and Bill are married to each other; also Carol to Dave. *)
88   let marriedto yy xx = X.(map2 (curry are_married) xx yy)
89
90 (* Actually, only Carol and Dave kiss. In w2, spouses kiss. In w3, there is no kissing. *)
91   let kisses1 yy xx = X.(map2 (fun x y -> (x = Carol && y = Dave) || (x = Dave && y = Carol)) xx yy)
92   let kisses2 yy xx = marriedto xx yy
93   let kisses3 yy xx = X.(map2 (fun x y -> false) xx yy)
94   
95 (* Actually, each husband loves only his wife and Frank also loves the women.
96    In w2, all the men love Carol and Ella loves the wives.
97    In w3, Frank loves everyone else. *)
98   let loves1 yy xx = X.(map2 (fun x y -> (is_male x && are_married(x,y)) || (x = Frank && not (is_male y))) xx yy)
99   let loves2 yy xx = X.(map2 (fun x y -> (is_male x && y = Carol) || (x = Ella && is_a_wife y)) xx yy)
100   let loves3 yy xx = X.(map2 (fun x y -> x = Frank && x <> y) xx yy)
101 end
102
103 module Test(S : SEMANTICS) : sig end = struct
104   type result = True | False | Fail
105   let print_result res = match res with True -> print_string "true" | False -> print_string "false" | Fail -> print_string "failure"
106
107   let check name expected expr =
108     (match (try Some (S.run expr) with Not_found -> None) with
109       | Some true -> if expected = True then true else begin print_string "Sentence \""; print_string name; print_string "\" failed: got true but expected "; print_result expected; print_newline (); false end
110       | Some false -> if expected = False then true else begin print_string "Sentence \""; print_string name; print_string "\" failed: got false but expected "; print_result expected; print_newline (); false end
111       | None -> if expected = Fail then true else begin print_string "Sentence \""; print_string name; print_string "\" failed: got failure but expected "; print_result expected; print_newline (); false end)
112 (*
113     with List.Short_list -> begin print_string "Sentence \""; print_string name; print_string "\" failed: got Short_list but expected "; print_result expected; print_newline (); false end
114     with Failure "Unimplemented" -> begin print_string "Sentence \""; print_string name; print_endline "\" unimplemented."; true end
115 *)
116
117   let dynamic res = if S.dynamic then res else Fail
118
119   let truth = S.(male bill)
120   let falsehood = S.(female bill)
121   let bool_results =
122   [ check "true" True truth
123   ; check "false" False falsehood
124   ; check "true and true" True S.(truth &&& truth)
125   ; check "true and false" False S.(truth &&& falsehood)
126   ; check "false and true" False S.(falsehood &&& truth)
127   ; check "false and false" False S.(falsehood &&& falsehood)
128   ; check "true or true" True S.(truth ||| truth)
129   ; check "true or false" True S.(truth ||| falsehood)
130   ; check "false or true" True S.(falsehood ||| truth)
131   ; check "false or false" False S.(falsehood ||| falsehood)
132   ; check "true >>> true" True S.(truth >>> truth)
133   ; check "true >>> false" False S.(truth >>> falsehood)
134   ; check "false >>> true" True S.(falsehood >>> truth)
135   ; check "false >>> false" True S.(falsehood >>> falsehood)
136   ]
137   let () = print_newline(); print_int (List.count not bool_results); print_endline " boolean test(s) failed."
138
139   let results =
140   [ check "1. Bill is male" True S.(male bill)
141   ; check "2. Bill is female" False S.(female bill)
142   ; check "3. Bill isn't female" True S.(~~~ (female bill))
143   ; check "4. Carol didn't leave" False S.(~~~ (left carol))
144   ; S.extensional || check "5. Maybe Carol didn't leave" True S.(maybe (~~~ (left carol)))
145   ; S.extensional || check "6. Maybe Ann didn't leave" False S.(maybe (~~~ (left ann)))
146
147   ; check "7. Some x. x is male" True S.(some 'x' (male getx))
148   ; check "8. Some x. x isn't female" True S.(some 'x' (~~~ (female getx)))
149   ; check "9. Some x. x left" True S.(some 'x' (left getx))
150   ; check "10. Some x. x didn't leave" False S.(some 'x' (~~~ (left getx)))
151   ; check "11. Every x. x left" True S.(every 'x' (left getx))
152   ; check "12. Every x. x is female" False S.(every 'x' (female getx))
153   ; check "13. Every x. x isn't male" False S.(every 'x' (~~~ (male getx)))
154   ; check "14. (Some x. x is male) and Ann is female" True S.(some 'x' (male getx) &&& female ann)
155   ; check "15. Some x. (x is male and Ann is female)" True S.(some 'x' (male getx &&& female ann))
156
157   ; check "16. Some x. (x is male and x is female)" False S.(some 'x' (male getx &&& female getx))
158   ; check "17. Some x. (x is male) and Some x. x is female" True S.(some 'x' (male getx) &&& some 'x' (female getx))
159
160   ; check "18. Some x. (x is male and Some y. y is male)" True S.(some 'x' (male getx &&& some 'y' (male gety)))
161   ; check "19. Some x. (x is male and Some y. y is female)" True S.(some 'x' (male getx &&& some 'y' (female gety)))
162   ; check "20. Some x. (x is male and Some y. x is male)" True S.(some 'x' (male getx &&& some 'y' (male getx)))
163   ; check "21. Some x. (x is male and Some y. x is female)" False S.(some 'x' (male getx &&& some 'y' (female getx)))
164   ; check "22. Some x. (x is male and Some y. x isn't female)" True S.(some 'x' (male getx &&& some 'y' (~~~ (female getx))))
165   ; check "23. Some x. (x is male and Some x. x is female)" True S.(some 'x' (male getx &&& some 'x' (female getx)))
166
167   ; check "24. Some x. (x is male) and Some y. (y is female and Bill is male)" True S.(some 'x' (male getx) &&& some 'y' (male gety &&& male bill))
168   ; check "25. Some x. (x is male and Some y. (y is female and Bill is male))" True S.(some 'x' (male getx &&& some 'y' (female gety &&& male bill)))
169   ; check "26. Some x. (x is male and Some y. (y is male and Bill is male))" True S.(some 'x' (male getx &&& some 'y' (male gety &&& male bill)))
170   ; check "27. Some x. (x is male and Some y. (x is female and Bill is male))" False S.(some 'x' (male getx &&& some 'y' (female getx &&& male bill)))
171   ; check "28. Some x. (x is male and Some y. (x isn't female and Bill is male))" True S.(some 'x' (male getx &&& some 'y' (~~~ (female getx) &&& male bill)))
172   ; check "29. Some x. (x is male and Some y. (x is male and Bill is male))" True S.(some 'x' (male getx &&& some 'y' (male getx &&& male bill)))
173
174   ; check "30. Some x. (x is male and Some y. (y is female and x isn't female))" True S.(some 'x' (male getx &&& some 'y' (female gety &&& ~~~ (female getx))))
175   ; check "31. Some x. (x is male and Some y. (y is female and x is single))" True S.(some 'x' (male getx &&& some 'y' (female gety &&& single getx)))
176   ; check "32. Some x. (x is male and Some y. (y is female and x isn't single))" True S.(some 'x' (male getx &&& some 'y' (female gety &&& ~~~ (single getx))))
177   ; check "33. Some x. (x is male and Some y. (y is male and x is single))" True S.(some 'x' (male getx &&& some 'y' (male gety &&& single getx)))
178   ; check "34. Some x. (x is male and Some y. (y is male and x isn't single))" True S.(some 'x' (male getx &&& some 'y' (male gety &&& ~~~ (single getx))))
179
180   ; check "35. Some x. (x is male and Some y. (x is female and x is single))" False S.(some 'x' (male getx &&& some 'y' (female getx &&& single getx)))
181   ; check "36. Some x. (x is male and Some y. (x is female and x isn't single))" False S.(some 'x' (male getx &&& some 'y' (female getx &&& ~~~ (single getx))))
182   ; check "37. Some x. (x is male and Some y. (x is male and x is single))" True S.(some 'x' (male getx &&& some 'y' (male getx &&& single getx)))
183   ; check "38. Some x. (x is male and Some y. (x is male and x isn't single))" True S.(some 'x' (male getx &&& some 'y' (male getx &&& ~~~ (single getx))))
184   
185   ; check "39. (Some x. male x) and x left" (dynamic True) S.(some 'x' (male getx) &&& left getx)
186   ; check "40. (Some x. male x) and female x" (dynamic False) S.(some 'x' (male getx) &&& female getx)
187   ; check "41. (Some x. male x) and Some y. female x" (dynamic False) S.(some 'x' (male getx) &&& some 'y' (female getx))
188   ; check "42. (Some x. male x) and Some y. male x" (dynamic True) S.(some 'x' (male getx) &&& some 'y' (male getx))
189   ; check "43. (Some x. male x) and Some y. (female x and male Bill)" (dynamic False) S.(some 'x' (male getx) &&& some 'y' (female getx &&& male bill))
190   ; check "44. (Some x. male x) and Some y. (male x and male Bill)" (dynamic True) S.(some 'x' (male getx) &&& some 'y' (male getx &&& male bill))
191   ; check "45. (Some x. male x) and Some y. (female y and x isn't single)" (dynamic True) S.(some 'x' (male getx) &&& some 'y' (female gety &&& ~~~ (single getx)))
192   ; check "46. (Some x. male x) and Some y. (female x and x isn't single)" (dynamic False) S.(some 'x' (male getx) &&& some 'y' (female getx &&& ~~~ (single getx)))
193   ; check "47. (Some x. male x) and Some y. (male x and x isn't single)" (dynamic True) S.(some 'x' (male getx) &&& some 'y' (male getx &&& ~~~ (single getx)))
194
195   ; check "48. Every x. (male x and (Some y. married y x) -> loves y x)" (dynamic True) S.(every 'x' (male getx &&& some 'y' (marriedto gety getx) >>> loves gety getx))
196   ; check "49. Every x. (male x and (Some y. married y x) -> kisses y x)" (dynamic False) S.(every 'x' (male getx &&& some 'y' (marriedto gety getx) >>> kisses gety getx))
197   ; check "50. (Some x. (male x and Some y. married y x)) -> loves y x" (dynamic True) S.(some 'x' (male getx &&& some 'y' (marriedto gety getx)) >>> loves gety getx)
198   ; check "51. (Some x. (male x and Some y. married y x)) -> kisses y x" (dynamic False) S.(some 'x' (male getx &&& some 'y' (marriedto gety getx)) >>> kisses gety getx)
199
200   ; check "52. Every x. (male x and Some y. (female y and (x = frank or married y x)) -> loves y x)" (dynamic True) S.(every 'x' (male getx &&& some 'y' (female gety &&& (getx === frank ||| marriedto gety getx)) >>> loves gety getx))
201   ; check "53. Every x. (male x and (x = frank or Some y. married y x) -> loves y x)" (dynamic Fail) S.(every 'x' (male getx &&& (getx === frank ||| some 'y' (marriedto gety getx)) >>> loves gety getx))
202   ; check "54. Every x. (male x and (Some y. (x = frank and female y) or Some y. married y x) -> loves y x)" (dynamic Fail) S.(every 'x' (male getx &&& (some 'y' (getx === frank &&& female gety) ||| some 'y' (marriedto gety getx)) >>> loves gety getx))
203   ; check "55. Every x. (male x and ((x = frank and Some y. female y) or Some y. married y x) -> loves y x)" (dynamic Fail) S.(every 'x' (male getx &&& ((getx === frank &&& some 'y' (female gety)) ||| some 'y' (marriedto gety getx)) >>> loves gety getx))
204   ]
205   let () = print_newline(); print_int (List.count not results); print_endline " test(s) failed."
206
207 end
208
209
210
211
212
213
214 module R = Monad.Reader(struct type env = identifier -> entity end)
215 module S = Monad.State(struct type store = identifier -> entity end)
216 module S' = Monad.State(struct type store = identifier -> int end)
217 module R' = Monad.Reader(struct type env = identifier -> int end)
218
219 let env0 = fun _ -> raise Not_found
220 let lookup (sought : identifier) env = env sought
221 let lookup_string (sought : identifier) env = try string_of_entity (env sought) with Not_found -> "*"
222 let print_lookup c env = print_string (lookup_string c env)
223 let insert (var : identifier) who env = fun sought -> if sought = var then who else env sought
224
225 module Y = Monad.Reader(struct type env = world end)
226
227 module L = Monad.List
228
229 module RY = struct
230   include R.T(Y)
231   include Monad.Derive.Reader_dbl(Y)(R.T(Y))
232 end
233 module YR = struct
234   include Y.T(R)
235   include Monad.Derive.Reader_dbl(R)(Y.T(R))
236 end
237 module LR = struct
238   include L.T(R)
239   include Monad.Derive.Reader(R)(L.T(R))
240 end
241 module LY = struct
242   include L.T(Y)
243   include Monad.Derive.Reader(Y)(L.T(Y))
244 end
245 module RL = struct
246   include R.M(L)
247   include Monad.Derive.List(L)(R.M(L))
248 end
249 module YL = struct
250   include Y.M(L)
251   include Monad.Derive.List(L)(Y.M(L))
252 end
253
254 module SY = struct
255   include S.T(Y)
256   include Monad.Derive.Reader(Y)(S.T(Y))
257 end
258 module YS = struct
259   include Y.T(S)
260   include Monad.Derive.State(S)(Y.T(S))
261 end
262 module LS = struct
263   include L.T(S)
264   include Monad.Derive.State(S)(L.T(S))
265 end
266 module LY = struct
267   include L.T(Y)
268   include Monad.Derive.Reader(Y)(L.T(Y))
269 end
270 module SL = struct
271   include S.M(L)
272   include Monad.Derive.List(L)(S.M(L))
273 end
274 module YL = struct
275   include Y.M(L)
276   include Monad.Derive.List(L)(Y.M(L))
277 end
278
279 module S'Y = struct
280   include S'.T(Y)
281   include Monad.Derive.Reader(Y)(S'.T(Y))
282 end
283 module YS' = struct
284   include Y.T(S')
285   include Monad.Derive.State(S')(Y.T(S'))
286 end
287 module LS' = struct
288   include L.T(S')
289   include Monad.Derive.State(S')(L.T(S'))
290 end
291 module S'L = struct
292   include S'.M(L)
293   include Monad.Derive.List(L)(S'.M(L))
294 end
295
296 module LRY = struct
297   include L.T(RY)
298   include Monad.Derive.Reader2(RY)(L.T(RY))
299 end
300 module LYR = struct
301   include L.T(YR)
302   include Monad.Derive.Reader2(YR)(L.T(YR))
303 end
304 module RLY = struct
305   include R.M(LY)
306   include Monad.Derive.List(LY)(R.M(LY))
307   include Monad.Derive.Reader_dbl(LY)(R.M(LY))
308 end
309 module RYL = struct
310   include R.M(YL)
311   include Monad.Derive.List(YL)(R.M(YL))
312   include Monad.Derive.Reader_dbl(YL)(R.M(YL))
313 end
314 module YLR = struct
315   include Y.M(LR)
316   include Monad.Derive.List(LR)(Y.M(LR))
317   include Monad.Derive.Reader_dbl(LR)(Y.M(LR))
318 end
319 module YRL = struct
320   include Y.M(RL)
321   include Monad.Derive.List(RL)(Y.M(RL))
322   include Monad.Derive.Reader_dbl(RL)(Y.M(RL))
323 end
324
325 module LSY = struct
326   include L.T(SY)
327   include Monad.Derive.Reader(SY)(L.T(SY))
328   include Monad.Derive.State(SY)(L.T(SY))
329 end
330 module LYS = struct
331   include L.T(YS)
332   include Monad.Derive.Reader(YS)(L.T(YS))
333   include Monad.Derive.State(YS)(L.T(YS))
334 end
335 module SLY = struct
336   include S.M(LY)
337   include Monad.Derive.List(LY)(S.M(LY))
338   include Monad.Derive.Reader(LY)(S.M(LY))
339 end
340 module SYL = struct
341   include S.M(YL)
342   include Monad.Derive.List(YL)(S.M(YL))
343   include Monad.Derive.Reader(YL)(S.M(YL))
344 end
345 module YLS = struct
346   include Y.M(LS)
347   include Monad.Derive.List(LS)(Y.M(LS))
348   include Monad.Derive.State(LS)(Y.M(LS))
349 end
350 module YSL = struct
351   include Y.M(SL)
352   include Monad.Derive.List(SL)(Y.M(SL))
353   include Monad.Derive.State(SL)(Y.M(SL))
354 end
355
356 module LS'Y = struct
357   include L.T(S'Y)
358   include Monad.Derive.Reader(S'Y)(L.T(S'Y))
359   include Monad.Derive.State(S'Y)(L.T(S'Y))
360 end
361 module LYS' = struct
362   include L.T(YS')
363   include Monad.Derive.Reader(YS')(L.T(YS'))
364   include Monad.Derive.State(YS')(L.T(YS'))
365 end
366 module S'LY = struct
367   include S'.M(LY)
368   include Monad.Derive.List(LY)(S'.M(LY))
369   include Monad.Derive.Reader(LY)(S'.M(LY))
370 end
371 module S'YL = struct
372   include S'.M(YL)
373   include Monad.Derive.List(YL)(S'.M(YL))
374   include Monad.Derive.Reader(YL)(S'.M(YL))
375 end
376 module YLS' = struct
377   include Y.M(LS')
378   include Monad.Derive.List(LS')(Y.M(LS'))
379   include Monad.Derive.State(LS')(Y.M(LS'))
380 end
381 module YS'L = struct
382   include Y.M(S'L)
383   include Monad.Derive.List(S'L)(Y.M(S'L))
384   include Monad.Derive.State(S'L)(Y.M(S'L))
385 end
386
387
388 module Sem1a = struct
389   let dynamic = false
390   let extensional = true
391
392   (* We use monad R, with env = var -> entity.
393      Types of sentences are env -> bool. *)
394   module X = R
395   type noun = entity X.t
396   type sent = bool X.t
397   let run (xx : sent) : bool = X.(run xx env0 = true)
398   let getx = X.(asks (lookup 'x'))
399   let gety = X.(asks (lookup 'y'))
400   let getz = X.(asks (lookup 'z'))
401   let let_ c (xx : noun) (body : sent) = X.(xx >>= fun x -> shift (insert c x) body)
402
403   let (~~~) xx = X.(map not xx)
404   let (&&&) xx yy = X.(xx >>= fun b' -> if not b' then mid false else yy)
405   let (|||) xx yy = X.(xx >>= fun b' -> if b' then mid true else yy)
406   let (>>>) xx yy = X.(xx >>= fun b' -> if not b' then mid true else yy)
407
408   let some c (body : sent) =
409     let (bbs : bool X.t list) = List.map (fun x -> let_ c X.(mid x) body) domain in
410     let (bsb : bool list X.t) = X.seq bbs in
411     let (bb : bool X.t) = X.map (exists ident) bsb in
412     bb
413   let every c (body : sent) =
414     let (bbs : bool X.t list) = List.map (fun x -> let_ c X.(mid x) body) domain in
415     let (bsb : bool list X.t) = X.seq bbs in
416     let (bb : bool X.t) = X.map (for_all ident) bsb in
417     bb
418
419   module F = Facts(X)
420   let ann = X.(mid Ann) let bill = X.(mid Bill) let carol = X.(mid Carol) let dave = X.(mid Dave) let ella = X.(mid Ella) let frank = X.(mid Frank)
421   let (===) xx yy = X.(map2 (=) xx yy)
422   let male = F.male let female = F.female let single = F.single let left = F.left1
423   let marriedto = F.marriedto let saw = F.saw1 let kisses = F.kisses1 let loves = F.loves1
424   let thinks pp xx = failwith "Unimplemented"
425   let maybe pp = failwith "Unimplemented"
426 end (* Sem1a *)
427
428 module Sem1b = struct
429   let dynamic = false
430   let extensional = true
431
432   (* We again use monad R, with env = var -> entity.
433      This variant defines sentence meanings as Kleisli arrows, that is:
434        type sent = bool -> bool X.t
435      or equivalently, bool -> (env -> bool). A true sentence takes any bool
436      input to a boxed version of that input (so truth = mid), and a false
437      sentence takes any input to mid false.
438      This more closely parallels the dynamic semantics (though it should not,
439      just on account of that structural similarity, be itself counted as dynamic).
440      It also brings the boolean operations closer to monadic primitives.
441   *)
442   module X = R
443   type noun = entity X.t
444   type sent = bool -> bool X.t
445   let run (k : sent) : bool = X.(run (k true) env0 = true)
446   let getx = X.(asks (lookup 'x'))
447   let gety = X.(asks (lookup 'y'))
448   let getz = X.(asks (lookup 'z'))
449   let let_ c (xx : noun) (body : sent) = fun b -> X.(xx >>= fun x -> shift (insert c x) (body b))
450
451   let (~~~) k = fun b -> X.(if b then map not (k true) else mid false)
452   let (&&&) k j = X.(k >=> j)
453   let (|||) k j = ~~~ (~~~ k &&& ~~~ j)
454   let (>>>) k j = ~~~ k ||| j
455 (* or
456   let (|||) xx yy = fun b -> X.(xx b >>= fun b' -> if b' then mid true else yy b)
457   let (>>>) xx yy = fun b -> X.(xx b >>= fun b' -> if not b' then mid true else yy b)
458   let (>>>) k j = ~~~ (k &&& ~~~ j)
459 *)
460
461   let some c (body : sent) = fun b ->
462     let (bbs : bool X.t list) = List.map (fun x -> let_ c X.(mid x) body b) domain in
463     let (bsb : bool list X.t) = X.seq bbs in
464     let (bb : bool X.t) = X.map (exists ident) bsb in
465     bb
466   let every c (body : sent) = fun b ->
467     let (bbs : bool X.t list) = List.map (fun x -> let_ c X.(mid x) body b) domain in
468     let (bsb : bool list X.t) = X.seq bbs in
469     let (bb : bool X.t) = X.map (for_all ident) bsb in
470     bb
471
472   module F = Facts(X)
473   let to_kleisli xx = fun b -> X.(xx >>= fun b' -> mid (b && b'))
474   let ann = X.(mid Ann) let bill = X.(mid Bill) let carol = X.(mid Carol) let dave = X.(mid Dave) let ella = X.(mid Ella) let frank = X.(mid Frank)
475   let (===) xx yy = to_kleisli X.(map2 (=) xx yy)
476   let male = to_kleisli % F.male let female = to_kleisli % F.female let single = to_kleisli % F.single let left = to_kleisli % F.left1
477   let marriedto yy xx = to_kleisli (F.marriedto yy xx) let saw yy xx = to_kleisli (F.saw1 yy xx) let kisses yy xx = to_kleisli (F.kisses1 yy xx) let loves yy xx = to_kleisli (F.loves1 yy xx)
478   let thinks pp xx = fun b -> failwith "Unimplemented"
479   let maybe pp = fun b -> failwith "Unimplemented"
480 end (* Sem1b *)
481
482 module Sem2a = struct
483   let dynamic = false
484   let extensional = true
485
486   (* We could use either monad RL or LR, with type env = var -> entity.
487      Their box type is the same: env -> ['a]
488      However, the types of SL and LS differ, and the latter is more suitable for the dynamic version. So to keep things maximally parallel, we'll use LR here.
489      We use the box type in two ways: first, we use a box(entity) to compute whether a matrix
490      clause is satisfied by a bound pronoun, where entity ranges over the whole domain.
491      Second, it is convenient and more consonant with later strategies
492      to re-use the same monad for sentence types (rather than using a simpler monad
493      that lacks a List component). Here we will let the types of sentences
494      be box(bool), that is: env -> [bool]. We will understand the sentence to be true
495      if there are ANY truths in the resulting list. A list of all falses is treated
496      the same as an empty list. Sem2c, below, eliminates this artifact by changing
497      the sentence type to box(unit). Then truths (rel to an env) are [();...] and
498      falsehoods are [].
499 *)
500   module X = LR
501   type noun = entity X.t
502   type sent = bool X.t
503   let run (xx : sent) : bool = X.(any_truths (run xx env0))
504   (* lift an 'a list to a single 'a X.t *)
505   let mids (xs : 'a list) : 'a X.t = let rec aux xx = function [] -> xx | x::xs -> aux X.(xx ++ mid x) xs in aux X.mzero xs
506   let getx = X.(asks (lookup 'x'))
507   let gety = X.(asks (lookup 'y'))
508   let getz = X.(asks (lookup 'z'))
509   let let_ c (xx : noun) (body : sent) = X.(xx >>= fun x -> shift (insert c x) body)
510
511   let (~~~) xx = X.(map not xx)
512   let (&&&) xx yy = X.(xx >>= fun b' -> if not b' then mid false else yy)
513   let (|||) xx yy = X.(xx >>= fun b' -> if b' then mid true else yy)
514   let (>>>) xx yy = X.(xx >>= fun b' -> if not b' then mid true else yy)
515
516   (* On this semantics, `some c body` is a list of the boolean outcomes for body for each assignment to c.
517      That matches our convention for sentence types, where any truth in the list means the sentence is true.
518      However, we can't then define `every c body === ~~~ (some c (~~~ body))`, because it's only when the rhs is entirely true that the lhs should be true.
519      In later semantics, the duality of `some` and `every` will be restored.
520   *)
521   let some c (body : sent) = X.(let_ c (mids domain) body)
522   let every c body = X.(let xx = let_ c (mids domain) body in list_map (fun xs -> if all_truths xs then xs else []) xx) (* could alternatively return [true] instead of xs *)
523
524   module F = Facts(X)
525   let ann = X.(mid Ann) let bill = X.(mid Bill) let carol = X.(mid Carol) let dave = X.(mid Dave) let ella = X.(mid Ella) let frank = X.(mid Frank)
526   let (===) xx yy = X.(map2 (=) xx yy)
527   let male = F.male let female = F.female let single = F.single let left = F.left1
528   let marriedto = F.marriedto let saw = F.saw1 let kisses = F.kisses1 let loves = F.loves1
529   let thinks pp xx = failwith "Unimplemented"
530   let maybe pp = failwith "Unimplemented"
531 end (* Sem2a *)
532
533 (* Sem2b would convert Sem2a into having sentence meanings be Kleisli arrows, as Sem1b did.
534    Not here implemented. *)
535
536 (* Variant of Sem2a, which uses [();...] vs [] instead of [true;...] vs (list of all false OR []). *)
537 module Sem2c = struct
538   let dynamic = false
539   let extensional = true
540
541   (* We use monad LR as above, with same env = var -> entity and box type = env -> ['a].
542      We again use box(entity) to compute whether matrix clauses are satisfied by
543      bound pronouns; but now we use box(unit) for the types of sentences.
544      Truths (rel to an env) are [();...] and falsehood is [].
545   *)
546   module X = LR
547   type noun = entity X.t
548   type sent = unit X.t
549   let run (xx : sent) : bool = X.(not (List.is_null (run xx env0)))
550   (* lift an 'a list to a single 'a X.t *)
551   let mids (xs : 'a list) : 'a X.t = let rec aux xx = function [] -> xx | x::xs -> aux X.(xx ++ mid x) xs in aux X.mzero xs
552   let getx = X.(asks (lookup 'x'))
553   let gety = X.(asks (lookup 'y'))
554   let getz = X.(asks (lookup 'z'))
555   let let_ c (xx : noun) (body : sent) = X.(xx >>= fun x -> shift (insert c x) body)
556   let to_unit (x : bool) : unit X.t = X.guard x
557
558   let (~~~) xx = X.(list_map (fun xs -> if is_null xs then [()] else []) xx)
559   let (&&&) xx yy = X.(xx >> yy)
560   let (|||) xx yy = X.(xx ++ (* ~~~ xx >> *) yy)
561   let (>>>) xx yy = X.(~~~ xx ++ yy)
562 (* or
563   let (>>>) xx yy = X.(~~~ (xx >> ~~~ yy))
564 *)
565
566   let some c (body : sent) = X.(let_ c (mids domain) body)
567   let every c (body : sent) = ~~~ (some c (~~~ body))
568
569   module F = Facts(X)
570   let ann = X.(mid Ann) let bill = X.(mid Bill) let carol = X.(mid Carol) let dave = X.(mid Dave) let ella = X.(mid Ella) let frank = X.(mid Frank)
571   let (===) xx yy = X.(map2 (=) xx yy >>= to_unit)
572   let male xx = X.(F.male xx >>= to_unit)
573   let female xx = X.(F.female xx >>= to_unit)
574   let single xx = X.(F.single xx >>= to_unit)
575   let left xx = X.(F.left1 xx >>= to_unit)
576   let marriedto yy xx = X.(F.marriedto yy xx >>= to_unit)
577   let saw yy xx = X.(F.saw1 yy xx >>= to_unit)
578   let kisses yy xx = X.(F.kisses1 yy xx >>= to_unit)
579   let loves yy xx = X.(F.loves1 yy xx >>= to_unit)
580   let thinks pp xx = failwith "Unimplemented"
581   let maybe pp = failwith "Unimplemented"
582 end (* Sem2c *)
583
584 (* Sem2d would convert Sem2c into having sentence meanings be Kleisli arrows, as Sem1b did.
585    Not here implemented. *)
586
587 (* Add intensionality to 2a *)
588 module Sem3a = struct
589   let dynamic = false
590   let extensional = false
591
592   (* Using monad LRY, with type env = var -> entity.
593      Box type is env -> world -> ['a]
594      Types of sentences are env -> world -> [bool]. *)
595   module X = LRY
596   type noun = entity X.t
597   type sent = bool X.t
598   let run xx = X.(any_truths (run xx env0 Actual))
599   (* lift an 'a list to a single 'a X.t *)
600   let mids (xs : 'a list) : 'a X.t = let rec aux xx = function [] -> xx | x::xs -> aux X.(xx ++ mid x) xs in aux X.mzero xs
601   let getx = X.(asks (lookup 'x'))
602   let gety = X.(asks (lookup 'y'))
603   let getz = X.(asks (lookup 'z'))
604   let getw = X.(uask) (* get world from the underlying Y monad *)
605   (* select an intranstive verb based on the world *)
606   let select1 f1 f2 f3 xx = X.(getw >>= fun w -> (if w = Actual then f1 else if w = Other then f2 else f3) xx)
607   (* select a transitive verb based on the world *)
608   let select2 f1 f2 f3 yy xx = X.(getw >>= fun w -> (if w = Actual then f1 else if w = Other then f2 else f3) yy xx)
609   let let_ c (xx : noun) (body : sent) = X.(xx >>= fun x -> shift (insert c x) body)
610   let letw world (body : sent) = X.(ushift (fun _ -> world) body) (* shift the "env" of the underlying Y monad *)
611
612   let (~~~) xx = X.(map not xx)
613   let (&&&) xx yy = X.(xx >>= fun b' -> if not b' then mid false else yy)
614   let (|||) xx yy = X.(xx >>= fun b' -> if b' then mid true else yy)
615   let (>>>) xx yy = X.(xx >>= fun b' -> if not b' then mid true else yy)
616
617   let some c (body : sent) = X.(let_ c (mids domain) body)
618   let every c (body : sent) = X.(let xx = let_ c (mids domain) body in list_map (fun xs -> if all_truths xs then xs else []) xx)
619
620   module F = Facts(X)
621   let ann = X.(mid Ann) let bill = X.(mid Bill) let carol = X.(mid Carol) let dave = X.(mid Dave) let ella = X.(mid Ella) let frank = X.(mid Frank)
622   let (===) xx yy = X.(map2 (=) xx yy)
623   let male = F.male let female = F.female let single = F.single
624   let left xx = select1 F.left1 F.left2 F.left3 xx
625   let saw yy xx = select2 F.saw1 F.saw2 F.saw3 yy xx
626   let marriedto = F.marriedto
627   let kisses yy xx = select2 F.kisses1 F.kisses2 F.kisses3 yy xx
628   let loves yy xx = select2 F.loves1 F.loves2 F.loves3 yy xx
629   let thinks pp xx = failwith "Unimplemented"
630   let maybe (body : sent) : sent =
631     let (yy : R.env -> Y.env -> bool list) = fun e w ->
632       let body_int = List.map (fun w' -> any_truths (X.run (letw w' body) e w)) modal_domain in
633       body_int (* can just use body's intension as the result of `maybe body` *) in
634     Obj.magic yy
635 end (* Sem3a *)
636
637 (* Sem3b would convert Sem3a into having sentence meanings be Kleisli arrows, as Sem1b did.
638    Not here implemented. *)
639
640 (* Add intensionality to 2c *)
641 module Sem3c = struct
642   let dynamic = false
643   let extensional = false
644
645   (* Using monad LRY, with type env = var -> entity.
646      Box type is env -> world -> ['a]
647      Types of sentences are env -> world -> [unit]. *)
648   module X = LRY
649   type noun = entity X.t
650   type sent = unit X.t
651   let run xx = X.(not (List.is_null (run xx env0 Actual)))
652   (* lift an 'a list to a single 'a X.t *)
653   let mids (xs : 'a list) : 'a X.t = let rec aux xx = function [] -> xx | x::xs -> aux X.(xx ++ mid x) xs in aux X.mzero xs
654   let getx = X.(asks (lookup 'x'))
655   let gety = X.(asks (lookup 'y'))
656   let getz = X.(asks (lookup 'z'))
657   let getw = X.(uask) (* get world from the underlying Y monad *)
658   (* select an intranstive verb based on the world *)
659   let select1 f1 f2 f3 xx = X.(getw >>= fun w -> (if w = Actual then f1 else if w = Other then f2 else f3) xx)
660   (* select a transitive verb based on the world *)
661   let select2 f1 f2 f3 yy xx = X.(getw >>= fun w -> (if w = Actual then f1 else if w = Other then f2 else f3) yy xx)
662   let let_ c (xx : noun) (body : sent) = X.(xx >>= fun x -> shift (insert c x) body)
663   let letw world (body : sent) = X.(ushift (fun _ -> world) body) (* shift the "env" of the underlying Y monad *)
664   let to_unit (x : bool) : unit X.t = X.guard x
665
666   let (~~~) xx = X.(list_map (fun xs -> if is_null xs then [()] else []) xx)
667   let (&&&) xx yy = X.(xx >> yy)
668   let (|||) xx yy = X.(xx ++ (* ~~~ xx >> *) yy)
669   let (>>>) xx yy = X.(~~~ xx ++ yy)
670 (* or
671   let (>>>) xx yy = X.(~~~ (xx >> ~~~ yy))
672 *)
673
674   let some c (body : sent) = X.(let_ c (mids domain) body)
675   let every c (body : sent) = ~~~ (some c (~~~ body))
676
677   module F = Facts(X)
678   let ann = X.(mid Ann) let bill = X.(mid Bill) let carol = X.(mid Carol) let dave = X.(mid Dave) let ella = X.(mid Ella) let frank = X.(mid Frank)
679   let (===) xx yy = X.(map2 (=) xx yy >>= to_unit)
680   let male xx = X.(F.male xx >>= to_unit)
681   let female xx = X.(F.female xx >>= to_unit)
682   let single xx = X.(F.single xx >>= to_unit)
683   let left xx = X.(select1 F.left1 F.left2 F.left3 xx >>= to_unit)
684   let saw yy xx = X.(select2 F.saw1 F.saw2 F.saw3 yy xx >>= to_unit)
685   let marriedto yy xx = X.(F.marriedto yy xx >>= to_unit)
686   let kisses yy xx = X.(select2 F.kisses1 F.kisses2 F.kisses3 yy xx >>= to_unit)
687   let loves yy xx = X.(select2 F.loves1 F.loves2 F.loves3 yy xx >>= to_unit)
688   let thinks pp xx = failwith "Unimplemented"
689   let maybe (body : sent) : sent =
690     let (yy : R.env -> Y.env -> unit list) = fun e w ->
691       let body_int = List.map (fun w' -> not @@ List.is_null @@ X.run (letw w' body) e w) modal_domain in
692       if any_truths body_int then [()] else [] in
693     Obj.magic yy
694 end (* Sem3c *)
695
696 (* Sem3d would convert Sem3c into having sentence meanings be Kleisli arrows, as Sem1b did.
697    Not here implemented. *)
698
699
700 (* Dynamic version of Sem2c *)
701 module Sem5c = struct
702   let dynamic = true
703   let extensional = true
704
705   (* This needs to use monad SL, with store = var -> entity
706      and box type = store -> ['a,store]
707      Sentence meaning is box(unit).
708      Later strategies with more complex sentence meanings and stores
709      may be able to use monad LS, with box type store -> ['a],store
710   *)
711   module X = SL
712   type noun = entity X.t
713   type sent = unit X.t
714   let run (xx : sent) : bool = X.(not (List.is_null (run xx env0)))
715   (* lift an 'a list to a single 'a X.t *)
716   let mids (xs : 'a list) : 'a X.t = let rec aux xx = function [] -> xx | x::xs -> aux X.(xx ++ mid x) xs in aux X.mzero xs
717   let getx = X.(gets (lookup 'x'))
718   let gety = X.(gets (lookup 'y'))
719   let getz = X.(gets (lookup 'z'))
720   let let_ c (xx : noun) (body : sent) = X.(xx >>= fun x -> modify (insert c x) >> body)
721   let to_unit (x : bool) : unit X.t = X.guard x
722 (*
723   let peek msg () = X.(get >>= fun s -> begin print_string msg; print_string ": x="; print_lookup 'x' s; print_string ", y="; print_lookup 'y' s; print_string ", z="; print_lookup 'z' s; print_newline (); mid () end)
724 *)
725
726   let (~~~) (xx : sent) : sent =
727     let yy : S.store -> (unit * S.store) list = fun s -> if List.is_null (X.run xx s) then [(),s] else [] in
728     Obj.magic yy  (* this is an identity function that changes the type of yy to a unit X.t *)
729   let (&&&) xx yy = X.(xx >> yy)
730   let (|||) xx yy = ~~~ (~~~ xx &&& ~~~ yy)
731   let (>>>) xx yy = X.(~~~ (xx >> ~~~ yy))
732
733 (*
734     This would propagate effects out of the disjuncts, so that for example after
735       "Some y. (x = frank and female y) or Some y. married y x"
736     "y" would be available for anaphor:
737       let (|||) xx yy = X.(xx ++ (~~~ xx >> yy))
738
739     This wouldn't propagate effects from antecedent to consequent, so that for example
740       "(Some y. marriedto y bill) >>> female gety"
741     has a failed lookup on "y":
742       let (>>>) xx yy = X.(~~~ xx ++ yy)
743 *)
744
745   let some c (body : sent) = X.(let_ c (mids domain) body)
746   let every c (body : sent) = ~~~ (some c (~~~ body))
747
748   module F = Facts(X)
749   let ann = X.(mid Ann) let bill = X.(mid Bill) let carol = X.(mid Carol) let dave = X.(mid Dave) let ella = X.(mid Ella) let frank = X.(mid Frank)
750   let (===) xx yy = X.(map2 (=) xx yy >>= to_unit)
751   let male xx = X.(F.male xx >>= to_unit)
752   let female xx = X.(F.female xx >>= to_unit)
753   let single xx = X.(F.single xx >>= to_unit)
754   let left xx = X.(F.left1 xx >>= to_unit)
755   let marriedto yy xx = X.(F.marriedto yy xx >>= to_unit)
756   let saw yy xx = X.(F.saw1 yy xx >>= to_unit)
757   let kisses yy xx = X.(F.kisses1 yy xx >>= to_unit)
758   let loves yy xx = X.(F.loves1 yy xx >>= to_unit)
759   let thinks pp xx = failwith "Unimplemented"
760   let maybe pp = failwith "Unimplemented"
761 end (* Sem5c *)
762
763
764 (* Dynamic version of Sem3c / Add intensionality to Sem5c *)
765 module Sem6c = struct
766   let dynamic = true
767   let extensional = false
768
769   (* This needs to use monad SLY, with store = var -> entity
770      and box type = store -> world -> ['a,store]
771      Sentence meaning is box(unit).
772      Later strategies with more complex sentence meanings and stores
773      may be able to use monad LSY, with box type store -> world -> ['a],store
774   *)
775   module X = SLY
776   type noun = entity X.t
777   type sent = unit X.t
778   let run (xx : sent) : bool = X.(not (List.is_null (run xx env0 Actual)))
779   (* lift an 'a list to a single 'a X.t *)
780   let mids (xs : 'a list) : 'a X.t = let rec aux xx = function [] -> xx | x::xs -> aux X.(xx ++ mid x) xs in aux X.mzero xs
781   let getx = X.(gets (lookup 'x'))
782   let gety = X.(gets (lookup 'y'))
783   let getz = X.(gets (lookup 'z'))
784   let getw = X.(ask) (* get world from the underlying Y monad *)
785   (* select an intranstive verb based on the world *)
786   let select1 f1 f2 f3 xx = X.(getw >>= fun w -> (if w = Actual then f1 else if w = Other then f2 else f3) xx)
787   (* select a transitive verb based on the world *)
788   let select2 f1 f2 f3 yy xx = X.(getw >>= fun w -> (if w = Actual then f1 else if w = Other then f2 else f3) yy xx)
789   let let_ c (xx : noun) (body : sent) = X.(xx >>= fun x -> modify (insert c x) >> body)
790   let letw world (body : sent) = X.(shift (fun _ -> world) body) (* shift the "env" of the underlying Y monad *)
791   let to_unit (x : bool) : unit X.t = X.guard x
792 (*
793   let peek msg () = X.(get >>= fun s -> begin print_string msg; print_string ": x="; print_lookup 'x' s; print_string ", y="; print_lookup 'y' s; print_string ", z="; print_lookup 'z' s; print_newline (); mid () end)
794 *)
795
796   let (~~~) (xx : sent) : sent =
797     let yy : S.store -> Y.env -> (unit * S.store) list = fun s w -> if List.is_null (X.run xx s w) then [(),s] else [] in
798     Obj.magic yy  (* this is an identity function that changes the type of yy to a unit X.t *)
799
800   let (&&&) xx yy = X.(xx >> yy)
801   let (|||) xx yy = ~~~ (~~~ xx &&& ~~~ yy)
802   let (>>>) xx yy = X.(~~~ (xx >> ~~~ yy))
803
804   let some c (body : sent) = X.(let_ c (mids domain) body)
805   let every c (body : sent) = ~~~ (some c (~~~ body))
806
807   module F = Facts(X)
808   let ann = X.(mid Ann) let bill = X.(mid Bill) let carol = X.(mid Carol) let dave = X.(mid Dave) let ella = X.(mid Ella) let frank = X.(mid Frank)
809   let (===) xx yy = X.(map2 (=) xx yy >>= to_unit)
810   let male xx = X.(F.male xx >>= to_unit)
811   let female xx = X.(F.female xx >>= to_unit)
812   let single xx = X.(F.single xx >>= to_unit)
813   let left xx = X.(select1 F.left1 F.left2 F.left3 xx >>= to_unit)
814   let saw yy xx = X.(select2 F.saw1 F.saw2 F.saw3 yy xx >>= to_unit)
815   let marriedto yy xx = X.(F.marriedto yy xx >>= to_unit)
816   let kisses yy xx = X.(select2 F.kisses1 F.kisses2 F.kisses3 yy xx >>= to_unit)
817   let loves yy xx = X.(select2 F.loves1 F.loves2 F.loves3 yy xx >>= to_unit)
818   let thinks pp xx = failwith "Unimplemented"
819   let maybe (body : sent) : sent =
820     let (yy : S.store -> Y.env -> (unit * S.store) list) = fun s w ->
821       let body_int = List.map (fun w' -> not @@ List.is_null @@ X.run (letw w' body) s w) modal_domain in
822       if any_truths body_int then [(),s] else [] in
823     Obj.magic yy
824 end (* Sem6c *)
825
826 (* Sem6c seems adequate for the phenomena GSV are examining, and is substantially simpler than their own semantics. Sem6c doesn't have their "pegs" and complex two-stage function from vars to referents.
827    Next we develop some semantics that are closer to their actual presentation. *)
828
829 (* This develops Sem5c using in part the strategies from Sem1b. *)
830 module Sem5e = struct
831   let dynamic = true
832   let extensional = true
833
834   (* Let a topic be sequence of entities introduced into conversation (GSV's pegs -> entities, with pegs construed as positions in the sequence).
835      Then let store = var -> int (that is, position in the topic)
836      Then we can use monad LS', with box type = store -> ['a],store
837      And sentence meanings are Kleisli arrows: topic -> box(topic). The list component
838      in the type captures indeterminacy in what objects are being discussed (introduced
839      by quantifiers). Truths (relative to a initial store and topic) result in
840      non-empty topic lists; falsehoods in empty ones.
841   *)
842   type topic = entity list
843   let topic0 = []
844   module X = LS'
845   type noun = (topic -> entity) X.t
846   type sent = topic -> topic X.t
847   let run (k : sent) : bool = X.(not (List.is_null (fst (run (k topic0) env0))))
848   (* lift an 'a list to a single 'a X.t *)
849   let mids (xs : 'a list) : 'a X.t = let rec aux xx = function [] -> xx | x::xs -> aux X.(xx ++ mid x) xs in aux X.mzero xs
850   let get_nth n topic = try List.nth topic n with List.Short_list -> failwith ("can't get item "^string_of_int n^" of "^List.string_of_list string_of_entity topic)
851   let getx : noun = X.(gets (lookup 'x') >>= fun n -> mid (get_nth n))
852   let gety : noun = X.(gets (lookup 'y') >>= fun n -> mid (get_nth n))
853   let getz : noun = X.(gets (lookup 'z') >>= fun n -> mid (get_nth n))
854   let let_ c (n : int) (body : sent) : sent = fun top -> X.(modify (insert c n) >> (body top))
855 (*
856   let lookup_string sought env top = try string_of_entity (List.nth top (env sought)) with Not_found -> "*" | List.Short_list -> "#"
857   let print_lookup sought env top = print_string (lookup_string sought env top)
858   let peek msg top = X.(get >>= fun s -> begin print_string msg; print_string ": x="; print_lookup 'x' s top; print_string ", y="; print_lookup 'y' s top; print_string ", z="; print_lookup 'z' s top; print_newline (); mid top end)
859 *)
860
861   let (~~~) (k : sent) : sent = fun top ->
862     let yy : S'.store -> topic list * S'.store = fun s -> if List.is_null (fst (X.run (k top) s)) then ([top],s) else ([],s) in
863     Obj.magic yy  (* this is an identity function that changes the type of yy to a topic X.t *)
864   let (&&&) k j = X.(k >=> j)
865   let (|||) k j = ~~~ (~~~ k &&& ~~~ j) (* TODO how about (k >>> j) >>> j *)
866   let (>>>) k j = X.(~~~ (k >=> ~~~ j))
867
868   let some c (body : sent) : sent = fun top ->
869     let n = length top in
870     let aux ent = X.(let_ c n body) (List.snoc top ent) in
871     let domain' = List.map aux domain in
872     X.join (mids domain')
873
874   let every c (body : sent) = ~~~ (some c (~~~ body))
875
876 (* TODO
877   let some c body = X.(mids domain >>= fun x -> modify (insert c x) body >>= guard >> mid x)
878   let every c body = X.(let xx = let_ c (mids domain) body in list_map (fun xs -> if all_truths xs then xs else []) xx)
879 *)
880
881   module F = Facts(X)
882   let mapply' (ff : noun) (top : topic) : entity X.t = X.(map (fun f -> f top) ff)
883   let wrap name = X.(mid (const name))
884   let wrap1 f xx = fun top -> X.(f (mapply' xx top) >>= fun b -> if b then mid top else mzero)
885   let wrap2 f xx yy = fun top -> X.(f (mapply' xx top) (mapply' yy top) >>= fun b -> if b then mid top else mzero)
886   let ann = wrap Ann let bill = wrap Bill let carol = wrap Carol let dave = wrap Dave let ella = wrap Ella let frank = wrap Frank
887   let (===) (xx : noun) (yy : noun) : sent = wrap2 X.(map2 (=)) xx yy
888   let male (xx : noun) : sent = wrap1 F.male xx
889   let female xx = wrap1 F.female xx
890   let single xx = wrap1 F.single xx
891   let left xx = wrap1 F.left1 xx
892   let marriedto yy xx = wrap2 F.marriedto yy xx
893   let saw yy xx = wrap2 F.saw1 yy xx
894   let kisses yy xx = wrap2 F.kisses1 yy xx
895   let loves yy xx = wrap2 F.loves1 yy xx
896   let thinks pp xx = fun top -> failwith "Unimplemented"
897   let maybe pp = fun top -> failwith "Unimplemented"
898 end (* Sem5e *)
899
900 (* Add intensionality to Sem5e *)
901 module Sem6e = struct
902   let dynamic = true
903   let extensional = false
904
905   type topic = entity list
906   let topic0 = []
907   module X = LS'Y
908   type noun = (topic -> entity) X.t
909   type sent = topic -> topic X.t
910   let run (k : sent) : bool = X.(not (List.is_null (fst (run (k topic0) env0 Actual))))
911   (* lift an 'a list to a single 'a X.t *)
912   let mids (xs : 'a list) : 'a X.t = let rec aux xx = function [] -> xx | x::xs -> aux X.(xx ++ mid x) xs in aux X.mzero xs
913   let get_nth n topic = try List.nth topic n with List.Short_list -> failwith ("can't get item "^string_of_int n^" of "^List.string_of_list string_of_entity topic)
914   let getx : noun = X.(gets (lookup 'x') >>= fun n -> mid (get_nth n))
915   let gety : noun = X.(gets (lookup 'y') >>= fun n -> mid (get_nth n))
916   let getz : noun = X.(gets (lookup 'z') >>= fun n -> mid (get_nth n))
917   let getw = X.(ask) (* get world from the underlying Y monad *)
918   (* select an intranstive verb based on the world *)
919   let select1 f1 f2 f3 xx = X.(getw >>= fun w -> (if w = Actual then f1 else if w = Other then f2 else f3) xx)
920   (* select a transitive verb based on the world *)
921   let select2 f1 f2 f3 yy xx = X.(getw >>= fun w -> (if w = Actual then f1 else if w = Other then f2 else f3) yy xx)
922   let let_ c (n : int) (body : sent) : sent = fun top -> X.(modify (insert c n) >> (body top))
923   let letw world (body : sent) : sent = fun top -> X.(shift (fun _ -> world) (body top)) (* shift the "env" of the underlying Y monad *)
924
925   let (~~~) (k : sent) : sent = fun top ->
926     let yy : S'.store -> Y.env -> topic list * S'.store = fun s w -> if List.is_null (fst (X.run (k top) s w)) then ([top],s) else ([],s) in
927     Obj.magic yy  (* this is an identity function that changes the type of yy to a topic X.t *)
928   let (&&&) k j = X.(k >=> j)
929   let (|||) k j = ~~~ (~~~ k &&& ~~~ j)
930   let (>>>) k j = X.(~~~ (k >=> ~~~ j))
931
932   let some c (body : sent) : sent = fun top ->
933     let n = length top in
934     let aux ent = X.(let_ c n body) (List.snoc top ent) in
935     let domain' = List.map aux domain in
936     X.join (mids domain')
937
938   let every c (body : sent) = ~~~ (some c (~~~ body))
939
940   module F = Facts(X)
941   let mapply' (ff : noun) (top : topic) : entity X.t = X.(map (fun f -> f top) ff)
942   let wrap name = X.(mid (const name))
943   let wrap1 f xx = fun top -> X.(f (mapply' xx top) >>= fun b -> if b then mid top else mzero)
944   let wrap2 f xx yy = fun top -> X.(f (mapply' xx top) (mapply' yy top) >>= fun b -> if b then mid top else mzero)
945   let ann = wrap Ann let bill = wrap Bill let carol = wrap Carol let dave = wrap Dave let ella = wrap Ella let frank = wrap Frank
946   let (===) (xx : noun) (yy : noun) : sent = wrap2 X.(map2 (=)) xx yy
947   let male (xx : noun) : sent = wrap1 F.male xx
948   let female xx = wrap1 F.female xx
949   let single xx = wrap1 F.single xx
950   let left xx = wrap1 (select1 F.left1 F.left2 F.left3) xx
951   let marriedto yy xx = wrap2 F.marriedto yy xx
952   let saw yy xx = wrap2 (select2 F.saw1 F.saw2 F.saw3) yy xx
953   let kisses yy xx = wrap2 (select2 F.kisses1 F.kisses2 F.kisses3) yy xx
954   let loves yy xx = wrap2 (select2 F.loves1 F.loves2 F.loves3) yy xx
955   let thinks pp xx = failwith "Unimplemented"
956   let maybe (body : sent) : sent = fun top ->
957     let (yy : S'.store -> Y.env -> topic list * S'.store) = fun s w ->
958       let body_int = List.map (fun w' -> not @@ List.is_null @@ fst @@ X.run (letw w' body top) s w) modal_domain in
959       if any_truths body_int then [top],s else [],s in
960     Obj.magic yy
961 end (* Sem6e *)
962
963 module TestAll = struct
964   print_endline "\nTesting Sem1a";;
965   module T1a = Test(Sem1a);;
966   print_endline "\nTesting Sem1b";;
967   module T1b = Test(Sem1b);;
968   print_endline "\nTesting Sem2a";;
969   module T2a = Test(Sem2a);;
970   print_endline "\nTesting Sem2c";;
971   module T2c = Test(Sem2c);;
972   print_endline "\nTesting Sem3a";;
973   module T3a = Test(Sem3a);;
974   print_endline "\nTesting Sem3c";;
975   module T3c = Test(Sem3c);;
976   print_endline "\nTesting Sem5c";;
977   module T5c = Test(Sem5c);;
978   print_endline "\nTesting Sem5e";;
979   module T5e = Test(Sem5e);;
980   print_endline "\nTesting Sem6c";;
981   module T6c = Test(Sem6c);;
982   print_endline "\nTesting Sem6e";;
983   module T6e = Test(Sem6e);;
984   print_newline ()
985 end
986
987 (*
988     One can't test the broken vase case by comparing the _truth_ of any sentences.
989     The difference is in whether the sentences have meanings that are "supported by"
990     the same informtation states. Compare in our model:
991       (i) Someone kissed me. She might have stayed.
992     and:
993       (ii) Someone who might have stayed kissed me.
994     Recall that in our model Ann leaves in every world, but Carol stays in some (non-actual)
995     world. If my background information settles that I was kissed by either Ann or Carol,
996     then I'm in a position to assert (i), since after the first clause it's left open
997     that the referent be either woman. But it doesn't put me in a position to assert (ii),
998     since that implies I was kissed by Carol. So far as truth-value goes,
999     if Carol kissed me both sentences are true, and if Ann did then both sentences are false.
1000 *)
1001