code/gsv-jim.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