From: Jim Date: Tue, 14 Apr 2015 00:48:39 +0000 (-0400) Subject: update Juli8 to v1.6 and post gsv.ml X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=commitdiff_plain;h=9ef8c8a5c822f05b63ff23c92980a103efc85967;ds=sidebyside update Juli8 to v1.6 and post gsv.ml --- diff --git a/code/Juli8-v1.6.tgz b/code/Juli8-v1.6.tgz new file mode 100644 index 00000000..4df3d091 Binary files /dev/null and b/code/Juli8-v1.6.tgz differ diff --git a/code/gsv.ml b/code/gsv.ml new file mode 100644 index 00000000..abd305f6 --- /dev/null +++ b/code/gsv.ml @@ -0,0 +1,1001 @@ +(* GSV monadically 13 April 2015 *) + +type identifier = char +let any_truths (xs : 'a list) : bool = List.exists ident xs +let all_truths (xs : 'a list) : bool = List.for_all ident xs + +module type SEMANTICS = sig + type noun (* this is whatever monadic type the semantics assigns to noun-sized contents *) + type sent (* this is whatever monadic type the semantics assigns to sentence-sized contents *) + val run : sent -> bool + val dynamic : bool + val extensional : bool + + val getx : noun val gety : noun val getz : noun + (* OCaml will parse ~~~ as a prefix operator, but unfortunately won't let you say + `~~~ predicate subject`; you have to say `~~~ (predicate subject)`. *) + val ( ~~~ ) : sent -> sent + (* OCaml will parse these three as infix operators (yay), but makes them all + left-associative (ehh for >>>) and have the same precedence (boo). *) + val ( &&& ) : sent -> sent -> sent + val ( ||| ) : sent -> sent -> sent + val ( >>> ) : sent -> sent -> sent + (* OCaml parses this with same associativity and precedence as the preceding (boo). *) + val (===) : noun -> noun -> sent + val ann : noun val bill : noun val carol : noun val dave : noun val ella : noun val frank : noun + val male : noun -> sent val female : noun -> sent + val left : noun -> sent + val single : noun -> sent + (* Transitive verbs apply to their direct objs first, subjects second. *) + val marriedto : noun -> noun -> sent + val saw : noun -> noun -> sent + val kisses : noun -> noun -> sent + val loves : noun -> noun -> sent (* here construed extensionally *) + (* Quantifiers may be unimplemented. *) + val some : identifier -> sent -> sent + val every : identifier -> sent -> sent + (* Intensional verbs and operators may be unimplemented. *) + val thinks : sent -> noun -> sent + val maybe : sent -> sent +end + +type world = Actual | Other | Another +let modal_domain = [Actual; Other; Another] + +type entity = Ann | Bill | Carol | Dave | Ella | Frank +let domain = [Ann; Bill; Carol; Dave; Ella; Frank] +let string_of_entity = function + | Ann -> "Ann" + | Bill -> "Bill" + | Carol -> "Carol" + | Dave -> "Dave" + | Ella -> "Ella" + | Frank -> "Frank" +let print_entity ent = print_string (string_of_entity ent) + +module Facts(X : Monad.MONAD) = struct +(* Here are the atomic facts: Ann and Bill are married, also Carol and Dave. + Genders and marital statuses are epistemically necessary. + 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. + In w2, all but Carol left; no one sees anything; all spouses kiss; all men love only Carol and Ella loves the wives. + In w3, only Ann and Bill left; no one sees anything; nobody kisses; Frank loves everyone else. +*) + + let is_male = function Bill | Dave | Frank -> true | _ -> false + let are_married = function (Ann, Bill) | (Bill, Ann) | (Carol, Dave) | (Dave, Carol) -> true | _ -> false + let is_a_wife = function Ann | Carol -> true | _ -> false + + let male xx = X.(map is_male xx) + let female xx = X.(map (not % is_male) xx) + +(* Ella and Frank are single *) + let single xx = X.(map (fun x -> x > Dave) xx) + +(* Actually (in w1), everybody left. In w2, everybody but Carol left. In w3, only Ann and Bill left. *) + let left1 xx = X.(map (fun _ -> true) xx) + let left2 xx = X.(map (fun x -> x <> Carol) xx) + let left3 xx = X.(map (fun x -> x = Ann || x = Bill) xx) + +(* In the sentences, order of application is: TransitiveVerb + Object + Subject. + But we convert to logical order for our operations. *) + +(* Actually, each person saw the people alphabetically before them. In w2 and w3, no one saw anyone. *) + let saw1 yy xx = X.(map2 (fun x y -> x < y) xx yy) + let saw2 yy xx = X.(map2 (fun _ _ -> false) xx yy) + let saw3 = saw2 + +(* Necessarily, Ann and Bill are married to each other; also Carol to Dave. *) + let marriedto yy xx = X.(map2 (curry are_married) xx yy) + +(* Actually, only Carol and Dave kiss. In w2, spouses kiss. In w3, there is no kissing. *) + let kisses1 yy xx = X.(map2 (fun x y -> (x = Carol && y = Dave) || (x = Dave && y = Carol)) xx yy) + let kisses2 yy xx = marriedto xx yy + let kisses3 yy xx = X.(map2 (fun x y -> false) xx yy) + +(* Actually, each husband loves only his wife and Frank also loves the women. + In w2, all the men love Carol and Ella loves the wives. + In w3, Frank loves everyone else. *) + let loves1 yy xx = X.(map2 (fun x y -> (is_male x && are_married(x,y)) || (x = Frank && not (is_male y))) xx yy) + let loves2 yy xx = X.(map2 (fun x y -> (is_male x && y = Carol) || (x = Ella && is_a_wife y)) xx yy) + let loves3 yy xx = X.(map2 (fun x y -> x = Frank && x <> y) xx yy) +end + +module Test(S : SEMANTICS) : sig end = struct + type result = True | False | Fail + let print_result res = match res with True -> print_string "true" | False -> print_string "false" | Fail -> print_string "failure" + + let check name expected expr = + (match (try Some (S.run expr) with Not_found -> None) with + | 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 + | 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 + | 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) +(* + 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 + with Failure "Unimplemented" -> begin print_string "Sentence \""; print_string name; print_endline "\" unimplemented."; true end +*) + + let dynamic res = if S.dynamic then res else Fail + + let truth = S.(male bill) + let falsehood = S.(female bill) + let bool_results = + [ check "true" True truth + ; check "false" False falsehood + ; check "true and true" True S.(truth &&& truth) + ; check "true and false" False S.(truth &&& falsehood) + ; check "false and true" False S.(falsehood &&& truth) + ; check "false and false" False S.(falsehood &&& falsehood) + ; check "true or true" True S.(truth ||| truth) + ; check "true or false" True S.(truth ||| falsehood) + ; check "false or true" True S.(falsehood ||| truth) + ; check "false or false" False S.(falsehood ||| falsehood) + ; check "true >>> true" True S.(truth >>> truth) + ; check "true >>> false" False S.(truth >>> falsehood) + ; check "false >>> true" True S.(falsehood >>> truth) + ; check "false >>> false" True S.(falsehood >>> falsehood) + ] + let () = print_newline(); print_int (List.count not bool_results); print_endline " boolean test(s) failed." + + let results = + [ check "1. Bill is male" True S.(male bill) + ; check "2. Bill is female" False S.(female bill) + ; check "3. Bill isn't female" True S.(~~~ (female bill)) + ; check "4. Carol didn't leave" False S.(~~~ (left carol)) + ; S.extensional || check "5. Maybe Carol didn't leave" True S.(maybe (~~~ (left carol))) + ; S.extensional || check "6. Maybe Ann didn't leave" False S.(maybe (~~~ (left ann))) + + ; check "7. Some x. x is male" True S.(some 'x' (male getx)) + ; check "8. Some x. x isn't female" True S.(some 'x' (~~~ (female getx))) + ; check "9. Some x. x left" True S.(some 'x' (left getx)) + ; check "10. Some x. x didn't leave" False S.(some 'x' (~~~ (left getx))) + ; check "11. Every x. x left" True S.(every 'x' (left getx)) + ; check "12. Every x. x is female" False S.(every 'x' (female getx)) + ; check "13. Every x. x isn't male" False S.(every 'x' (~~~ (male getx))) + ; check "14. (Some x. x is male) and Ann is female" True S.(some 'x' (male getx) &&& female ann) + ; check "15. Some x. (x is male and Ann is female)" True S.(some 'x' (male getx &&& female ann)) + + ; check "16. Some x. (x is male and x is female)" False S.(some 'x' (male getx &&& female getx)) + ; check "17. Some x. (x is male) and Some x. x is female" True S.(some 'x' (male getx) &&& some 'x' (female getx)) + + ; check "18. Some x. (x is male and Some y. y is male)" True S.(some 'x' (male getx &&& some 'y' (male gety))) + ; check "19. Some x. (x is male and Some y. y is female)" True S.(some 'x' (male getx &&& some 'y' (female gety))) + ; check "20. Some x. (x is male and Some y. x is male)" True S.(some 'x' (male getx &&& some 'y' (male getx))) + ; check "21. Some x. (x is male and Some y. x is female)" False S.(some 'x' (male getx &&& some 'y' (female getx))) + ; check "22. Some x. (x is male and Some y. x isn't female)" True S.(some 'x' (male getx &&& some 'y' (~~~ (female getx)))) + ; check "23. Some x. (x is male and Some x. x is female)" True S.(some 'x' (male getx &&& some 'x' (female getx))) + + ; 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)) + ; 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))) + ; 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))) + ; 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))) + ; 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))) + ; 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))) + + ; 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)))) + ; 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))) + ; 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)))) + ; 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))) + ; 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)))) + + ; 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))) + ; 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)))) + ; 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))) + ; 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)))) + + ; check "39. (Some x. male x) and x left" (dynamic True) S.(some 'x' (male getx) &&& left getx) + ; check "40. (Some x. male x) and female x" (dynamic False) S.(some 'x' (male getx) &&& female getx) + ; check "41. (Some x. male x) and Some y. female x" (dynamic False) S.(some 'x' (male getx) &&& some 'y' (female getx)) + ; check "42. (Some x. male x) and Some y. male x" (dynamic True) S.(some 'x' (male getx) &&& some 'y' (male getx)) + ; 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)) + ; 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)) + ; 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))) + ; 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))) + ; 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))) + + ; 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)) + ; 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)) + ; 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) + ; 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) + + ; 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)) + ; 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)) + ; 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)) + ; 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)) + ] + let () = print_newline(); print_int (List.count not results); print_endline " test(s) failed." + +end + + + + + + +module R = Monad.Reader(struct type env = identifier -> entity end) +module S = Monad.State(struct type store = identifier -> entity end) +module S' = Monad.State(struct type store = identifier -> int end) +module R' = Monad.Reader(struct type env = identifier -> int end) + +let env0 = fun _ -> raise Not_found +let lookup (sought : identifier) env = env sought +let lookup_string (sought : identifier) env = try string_of_entity (env sought) with Not_found -> "*" +let print_lookup c env = print_string (lookup_string c env) +let insert (var : identifier) who env = fun sought -> if sought = var then who else env sought + +module Y = Monad.Reader(struct type env = world end) + +module L = Monad.List + +module RY = struct + include R.T(Y) + include Monad.Derive.Reader_dbl(Y)(R.T(Y)) +end +module YR = struct + include Y.T(R) + include Monad.Derive.Reader_dbl(R)(Y.T(R)) +end +module LR = struct + include L.T(R) + include Monad.Derive.Reader(R)(L.T(R)) +end +module LY = struct + include L.T(Y) + include Monad.Derive.Reader(Y)(L.T(Y)) +end +module RL = struct + include R.M(L) + include Monad.Derive.List(L)(R.M(L)) +end +module YL = struct + include Y.M(L) + include Monad.Derive.List(L)(Y.M(L)) +end + +module SY = struct + include S.T(Y) + include Monad.Derive.Reader(Y)(S.T(Y)) +end +module YS = struct + include Y.T(S) + include Monad.Derive.State(S)(Y.T(S)) +end +module LS = struct + include L.T(S) + include Monad.Derive.State(S)(L.T(S)) +end +module LY = struct + include L.T(Y) + include Monad.Derive.Reader(Y)(L.T(Y)) +end +module SL = struct + include S.M(L) + include Monad.Derive.List(L)(S.M(L)) +end +module YL = struct + include Y.M(L) + include Monad.Derive.List(L)(Y.M(L)) +end + +module S'Y = struct + include S'.T(Y) + include Monad.Derive.Reader(Y)(S'.T(Y)) +end +module YS' = struct + include Y.T(S') + include Monad.Derive.State(S')(Y.T(S')) +end +module LS' = struct + include L.T(S') + include Monad.Derive.State(S')(L.T(S')) +end +module S'L = struct + include S'.M(L) + include Monad.Derive.List(L)(S'.M(L)) +end + +module LRY = struct + include L.T(RY) + include Monad.Derive.Reader2(RY)(L.T(RY)) +end +module LYR = struct + include L.T(YR) + include Monad.Derive.Reader2(YR)(L.T(YR)) +end +module RLY = struct + include R.M(LY) + include Monad.Derive.List(LY)(R.M(LY)) + include Monad.Derive.Reader_dbl(LY)(R.M(LY)) +end +module RYL = struct + include R.M(YL) + include Monad.Derive.List(YL)(R.M(YL)) + include Monad.Derive.Reader_dbl(YL)(R.M(YL)) +end +module YLR = struct + include Y.M(LR) + include Monad.Derive.List(LR)(Y.M(LR)) + include Monad.Derive.Reader_dbl(LR)(Y.M(LR)) +end +module YRL = struct + include Y.M(RL) + include Monad.Derive.List(RL)(Y.M(RL)) + include Monad.Derive.Reader_dbl(RL)(Y.M(RL)) +end + +module LSY = struct + include L.T(SY) + include Monad.Derive.Reader(SY)(L.T(SY)) + include Monad.Derive.State(SY)(L.T(SY)) +end +module LYS = struct + include L.T(YS) + include Monad.Derive.Reader(YS)(L.T(YS)) + include Monad.Derive.State(YS)(L.T(YS)) +end +module SLY = struct + include S.M(LY) + include Monad.Derive.List(LY)(S.M(LY)) + include Monad.Derive.Reader(LY)(S.M(LY)) +end +module SYL = struct + include S.M(YL) + include Monad.Derive.List(YL)(S.M(YL)) + include Monad.Derive.Reader(YL)(S.M(YL)) +end +module YLS = struct + include Y.M(LS) + include Monad.Derive.List(LS)(Y.M(LS)) + include Monad.Derive.State(LS)(Y.M(LS)) +end +module YSL = struct + include Y.M(SL) + include Monad.Derive.List(SL)(Y.M(SL)) + include Monad.Derive.State(SL)(Y.M(SL)) +end + +module LS'Y = struct + include L.T(S'Y) + include Monad.Derive.Reader(S'Y)(L.T(S'Y)) + include Monad.Derive.State(S'Y)(L.T(S'Y)) +end +module LYS' = struct + include L.T(YS') + include Monad.Derive.Reader(YS')(L.T(YS')) + include Monad.Derive.State(YS')(L.T(YS')) +end +module S'LY = struct + include S'.M(LY) + include Monad.Derive.List(LY)(S'.M(LY)) + include Monad.Derive.Reader(LY)(S'.M(LY)) +end +module S'YL = struct + include S'.M(YL) + include Monad.Derive.List(YL)(S'.M(YL)) + include Monad.Derive.Reader(YL)(S'.M(YL)) +end +module YLS' = struct + include Y.M(LS') + include Monad.Derive.List(LS')(Y.M(LS')) + include Monad.Derive.State(LS')(Y.M(LS')) +end +module YS'L = struct + include Y.M(S'L) + include Monad.Derive.List(S'L)(Y.M(S'L)) + include Monad.Derive.State(S'L)(Y.M(S'L)) +end + + +module Sem1a = struct + let dynamic = false + let extensional = true + + (* We use monad R, with env = var -> entity. + Types of sentences are env -> bool. *) + module X = R + type noun = entity X.t + type sent = bool X.t + let run (xx : sent) : bool = X.(run xx env0 = true) + let getx = X.(asks (lookup 'x')) + let gety = X.(asks (lookup 'y')) + let getz = X.(asks (lookup 'z')) + let let_ c (xx : noun) (body : sent) = X.(xx >>= fun x -> shift (insert c x) body) + + let (~~~) xx = X.(map not xx) + let (&&&) xx yy = X.(xx >>= fun b' -> if not b' then mid false else yy) + let (|||) xx yy = X.(xx >>= fun b' -> if b' then mid true else yy) + let (>>>) xx yy = X.(xx >>= fun b' -> if not b' then mid true else yy) + + let some c (body : sent) = + let (bbs : bool X.t list) = List.map (fun x -> let_ c X.(mid x) body) domain in + let (bsb : bool list X.t) = X.seq bbs in + let (bb : bool X.t) = X.map (exists ident) bsb in + bb + let every c (body : sent) = + let (bbs : bool X.t list) = List.map (fun x -> let_ c X.(mid x) body) domain in + let (bsb : bool list X.t) = X.seq bbs in + let (bb : bool X.t) = X.map (for_all ident) bsb in + bb + + module F = Facts(X) + 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) + let (===) xx yy = X.(map2 (=) xx yy) + let male = F.male let female = F.female let single = F.single let left = F.left1 + let marriedto = F.marriedto let saw = F.saw1 let kisses = F.kisses1 let loves = F.loves1 + let thinks pp xx = failwith "Unimplemented" + let maybe pp = failwith "Unimplemented" +end (* Sem1a *) + +module Sem1b = struct + let dynamic = false + let extensional = true + + (* We again use monad R, with env = var -> entity. + This variant defines sentence meanings as Kleisli arrows, that is: + type sent = bool -> bool X.t + or equivalently, bool -> (env -> bool). A true sentence takes any bool + input to a boxed version of that input (so truth = mid), and a false + sentence takes any input to mid false. + This more closely parallels the dynamic semantics (though it should not, + just on account of that structural similarity, be itself counted as dynamic). + It also brings the boolean operations closer to monadic primitives. + *) + module X = R + type noun = entity X.t + type sent = bool -> bool X.t + let run (k : sent) : bool = X.(run (k true) env0 = true) + let getx = X.(asks (lookup 'x')) + let gety = X.(asks (lookup 'y')) + let getz = X.(asks (lookup 'z')) + let let_ c (xx : noun) (body : sent) = fun b -> X.(xx >>= fun x -> shift (insert c x) (body b)) + + let (~~~) k = fun b -> X.(if b then map not (k true) else mid false) + let (&&&) k j = X.(k >=> j) + let (|||) k j = ~~~ (~~~ k &&& ~~~ j) + let (>>>) k j = ~~~ k ||| j +(* or + let (|||) xx yy = fun b -> X.(xx b >>= fun b' -> if b' then mid true else yy b) + let (>>>) xx yy = fun b -> X.(xx b >>= fun b' -> if not b' then mid true else yy b) + let (>>>) k j = ~~~ (k &&& ~~~ j) +*) + + let some c (body : sent) = fun b -> + let (bbs : bool X.t list) = List.map (fun x -> let_ c X.(mid x) body b) domain in + let (bsb : bool list X.t) = X.seq bbs in + let (bb : bool X.t) = X.map (exists ident) bsb in + bb + let every c (body : sent) = fun b -> + let (bbs : bool X.t list) = List.map (fun x -> let_ c X.(mid x) body b) domain in + let (bsb : bool list X.t) = X.seq bbs in + let (bb : bool X.t) = X.map (for_all ident) bsb in + bb + + module F = Facts(X) + let to_kleisli xx = fun b -> X.(xx >>= fun b' -> mid (b && b')) + 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) + let (===) xx yy = to_kleisli X.(map2 (=) xx yy) + let male = to_kleisli % F.male let female = to_kleisli % F.female let single = to_kleisli % F.single let left = to_kleisli % F.left1 + 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) + let thinks pp xx = fun b -> failwith "Unimplemented" + let maybe pp = fun b -> failwith "Unimplemented" +end (* Sem1b *) + +module Sem2a = struct + let dynamic = false + let extensional = true + + (* We could use either monad RL or LR, with type env = var -> entity. + Their box type is the same: env -> ['a] + 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. + We use the box type in two ways: first, we use a box(entity) to compute whether a matrix + clause is satisfied by a bound pronoun, where entity ranges over the whole domain. + Second, it is convenient and more consonant with later strategies + to re-use the same monad for sentence types (rather than using a simpler monad + that lacks a List component). Here we will let the types of sentences + be box(bool), that is: env -> [bool]. We will understand the sentence to be true + if there are ANY truths in the resulting list. A list of all falses is treated + the same as an empty list. Sem2c, below, eliminates this artifact by changing + the sentence type to box(unit). Then truths (rel to an env) are [();...] and + falsehoods are []. +*) + module X = LR + type noun = entity X.t + type sent = bool X.t + let run (xx : sent) : bool = X.(any_truths (run xx env0)) + (* lift an 'a list to a single 'a X.t *) + 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 + let getx = X.(asks (lookup 'x')) + let gety = X.(asks (lookup 'y')) + let getz = X.(asks (lookup 'z')) + let let_ c (xx : noun) (body : sent) = X.(xx >>= fun x -> shift (insert c x) body) + + let (~~~) xx = X.(map not xx) + let (&&&) xx yy = X.(xx >>= fun b' -> if not b' then mid false else yy) + let (|||) xx yy = X.(xx >>= fun b' -> if b' then mid true else yy) + let (>>>) xx yy = X.(xx >>= fun b' -> if not b' then mid true else yy) + + (* On this semantics, `some c body` is a list of the boolean outcomes for body for each assignment to c. + That matches our convention for sentence types, where any truth in the list means the sentence is true. + 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. + In later semantics, the duality of `some` and `every` will be restored. + *) + let some c (body : sent) = X.(let_ c (mids domain) body) + 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 *) + + module F = Facts(X) + 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) + let (===) xx yy = X.(map2 (=) xx yy) + let male = F.male let female = F.female let single = F.single let left = F.left1 + let marriedto = F.marriedto let saw = F.saw1 let kisses = F.kisses1 let loves = F.loves1 + let thinks pp xx = failwith "Unimplemented" + let maybe pp = failwith "Unimplemented" +end (* Sem2a *) + +(* Sem2b would convert Sem2a into having sentence meanings be Kleisli arrows, as Sem1b did. + Not here implemented. *) + +(* Variant of Sem2a, which uses [();...] vs [] instead of [true;...] vs (list of all false OR []). *) +module Sem2c = struct + let dynamic = false + let extensional = true + + (* We use monad LR as above, with same env = var -> entity and box type = env -> ['a]. + We again use box(entity) to compute whether matrix clauses are satisfied by + bound pronouns; but now we use box(unit) for the types of sentences. + Truths (rel to an env) are [();...] and falsehood is []. + *) + module X = LR + type noun = entity X.t + type sent = unit X.t + let run (xx : sent) : bool = X.(not (List.is_null (run xx env0))) + (* lift an 'a list to a single 'a X.t *) + 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 + let getx = X.(asks (lookup 'x')) + let gety = X.(asks (lookup 'y')) + let getz = X.(asks (lookup 'z')) + let let_ c (xx : noun) (body : sent) = X.(xx >>= fun x -> shift (insert c x) body) + let to_unit (x : bool) : unit X.t = X.guard x + + let (~~~) xx = X.(list_map (fun xs -> if is_null xs then [()] else []) xx) + let (&&&) xx yy = X.(xx >> yy) + let (|||) xx yy = X.(xx ++ (* ~~~ xx >> *) yy) + let (>>>) xx yy = X.(~~~ xx ++ yy) +(* or + let (>>>) xx yy = X.(~~~ (xx >> ~~~ yy)) +*) + + let some c (body : sent) = X.(let_ c (mids domain) body) + let every c (body : sent) = ~~~ (some c (~~~ body)) + + module F = Facts(X) + 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) + let (===) xx yy = X.(map2 (=) xx yy >>= to_unit) + let male xx = X.(F.male xx >>= to_unit) + let female xx = X.(F.female xx >>= to_unit) + let single xx = X.(F.single xx >>= to_unit) + let left xx = X.(F.left1 xx >>= to_unit) + let marriedto yy xx = X.(F.marriedto yy xx >>= to_unit) + let saw yy xx = X.(F.saw1 yy xx >>= to_unit) + let kisses yy xx = X.(F.kisses1 yy xx >>= to_unit) + let loves yy xx = X.(F.loves1 yy xx >>= to_unit) + let thinks pp xx = failwith "Unimplemented" + let maybe pp = failwith "Unimplemented" +end (* Sem2c *) + +(* Sem2d would convert Sem2c into having sentence meanings be Kleisli arrows, as Sem1b did. + Not here implemented. *) + +(* Add intensionality to 2a *) +module Sem3a = struct + let dynamic = false + let extensional = false + + (* Using monad LRY, with type env = var -> entity. + Box type is env -> world -> ['a] + Types of sentences are env -> world -> [bool]. *) + module X = LRY + type noun = entity X.t + type sent = bool X.t + let run xx = X.(any_truths (run xx env0 Actual)) + (* lift an 'a list to a single 'a X.t *) + 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 + let getx = X.(asks (lookup 'x')) + let gety = X.(asks (lookup 'y')) + let getz = X.(asks (lookup 'z')) + let getw = X.(uask) (* get world from the underlying Y monad *) + (* select an intranstive verb based on the world *) + let select1 f1 f2 f3 xx = X.(getw >>= fun w -> (if w = Actual then f1 else if w = Other then f2 else f3) xx) + (* select a transitive verb based on the world *) + 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) + let let_ c (xx : noun) (body : sent) = X.(xx >>= fun x -> shift (insert c x) body) + let letw world (body : sent) = X.(ushift (fun _ -> world) body) (* shift the "env" of the underlying Y monad *) + + let (~~~) xx = X.(map not xx) + let (&&&) xx yy = X.(xx >>= fun b' -> if not b' then mid false else yy) + let (|||) xx yy = X.(xx >>= fun b' -> if b' then mid true else yy) + let (>>>) xx yy = X.(xx >>= fun b' -> if not b' then mid true else yy) + + let some c (body : sent) = X.(let_ c (mids domain) body) + 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) + + module F = Facts(X) + 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) + let (===) xx yy = X.(map2 (=) xx yy) + let male = F.male let female = F.female let single = F.single + let left xx = select1 F.left1 F.left2 F.left3 xx + let saw yy xx = select2 F.saw1 F.saw2 F.saw3 yy xx + let marriedto = F.marriedto + let kisses yy xx = select2 F.kisses1 F.kisses2 F.kisses3 yy xx + let loves yy xx = select2 F.loves1 F.loves2 F.loves3 yy xx + let thinks pp xx = failwith "Unimplemented" + let maybe (body : sent) : sent = + let (yy : R.env -> Y.env -> bool list) = fun e w -> + let body_int = List.map (fun w' -> any_truths (X.run (letw w' body) e w)) modal_domain in + body_int (* can just use body's intension as the result of `maybe body` *) in + Obj.magic yy +end (* Sem3a *) + +(* Sem3b would convert Sem3a into having sentence meanings be Kleisli arrows, as Sem1b did. + Not here implemented. *) + +(* Add intensionality to 2c *) +module Sem3c = struct + let dynamic = false + let extensional = false + + (* Using monad LRY, with type env = var -> entity. + Box type is env -> world -> ['a] + Types of sentences are env -> world -> [unit]. *) + module X = LRY + type noun = entity X.t + type sent = unit X.t + let run xx = X.(not (List.is_null (run xx env0 Actual))) + (* lift an 'a list to a single 'a X.t *) + 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 + let getx = X.(asks (lookup 'x')) + let gety = X.(asks (lookup 'y')) + let getz = X.(asks (lookup 'z')) + let getw = X.(uask) (* get world from the underlying Y monad *) + (* select an intranstive verb based on the world *) + let select1 f1 f2 f3 xx = X.(getw >>= fun w -> (if w = Actual then f1 else if w = Other then f2 else f3) xx) + (* select a transitive verb based on the world *) + 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) + let let_ c (xx : noun) (body : sent) = X.(xx >>= fun x -> shift (insert c x) body) + let letw world (body : sent) = X.(ushift (fun _ -> world) body) (* shift the "env" of the underlying Y monad *) + let to_unit (x : bool) : unit X.t = X.guard x + + let (~~~) xx = X.(list_map (fun xs -> if is_null xs then [()] else []) xx) + let (&&&) xx yy = X.(xx >> yy) + let (|||) xx yy = X.(xx ++ (* ~~~ xx >> *) yy) + let (>>>) xx yy = X.(~~~ xx ++ yy) +(* or + let (>>>) xx yy = X.(~~~ (xx >> ~~~ yy)) +*) + + let some c (body : sent) = X.(let_ c (mids domain) body) + let every c (body : sent) = ~~~ (some c (~~~ body)) + + module F = Facts(X) + 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) + let (===) xx yy = X.(map2 (=) xx yy >>= to_unit) + let male xx = X.(F.male xx >>= to_unit) + let female xx = X.(F.female xx >>= to_unit) + let single xx = X.(F.single xx >>= to_unit) + let left xx = X.(select1 F.left1 F.left2 F.left3 xx >>= to_unit) + let saw yy xx = X.(select2 F.saw1 F.saw2 F.saw3 yy xx >>= to_unit) + let marriedto yy xx = X.(F.marriedto yy xx >>= to_unit) + let kisses yy xx = X.(select2 F.kisses1 F.kisses2 F.kisses3 yy xx >>= to_unit) + let loves yy xx = X.(select2 F.loves1 F.loves2 F.loves3 yy xx >>= to_unit) + let thinks pp xx = failwith "Unimplemented" + let maybe (body : sent) : sent = + let (yy : R.env -> Y.env -> unit list) = fun e w -> + let body_int = List.map (fun w' -> not @@ List.is_null @@ X.run (letw w' body) e w) modal_domain in + if any_truths body_int then [()] else [] in + Obj.magic yy +end (* Sem3c *) + +(* Sem3d would convert Sem3c into having sentence meanings be Kleisli arrows, as Sem1b did. + Not here implemented. *) + + +(* Dynamic version of Sem2c *) +module Sem5c = struct + let dynamic = true + let extensional = true + + (* This needs to use monad SL, with store = var -> entity + and box type = store -> ['a,store] + Sentence meaning is box(unit). + Later strategies with more complex sentence meanings and stores + may be able to use monad LS, with box type store -> ['a],store + *) + module X = SL + type noun = entity X.t + type sent = unit X.t + let run (xx : sent) : bool = X.(not (List.is_null (run xx env0))) + (* lift an 'a list to a single 'a X.t *) + 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 + let getx = X.(gets (lookup 'x')) + let gety = X.(gets (lookup 'y')) + let getz = X.(gets (lookup 'z')) + let let_ c (xx : noun) (body : sent) = X.(xx >>= fun x -> modify (insert c x) >> body) + let to_unit (x : bool) : unit X.t = X.guard x +(* + 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) +*) + + let (~~~) (xx : sent) : sent = + let yy : S.store -> (unit * S.store) list = fun s -> if List.is_null (X.run xx s) then [(),s] else [] in + Obj.magic yy (* this is an identity function that changes the type of yy to a unit X.t *) + let (&&&) xx yy = X.(xx >> yy) + let (|||) xx yy = ~~~ (~~~ xx &&& ~~~ yy) + let (>>>) xx yy = X.(~~~ (xx >> ~~~ yy)) + +(* + This would propagate effects out of the disjuncts, so that for example after + "Some y. (x = frank and female y) or Some y. married y x" + "y" would be available for anaphor: + let (|||) xx yy = X.(xx ++ (~~~ xx >> yy)) + + This wouldn't propagate effects from antecedent to consequent, so that for example + "(Some y. marriedto y bill) >>> female gety" + has a failed lookup on "y": + let (>>>) xx yy = X.(~~~ xx ++ yy) +*) + + let some c (body : sent) = X.(let_ c (mids domain) body) + let every c (body : sent) = ~~~ (some c (~~~ body)) + + module F = Facts(X) + 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) + let (===) xx yy = X.(map2 (=) xx yy >>= to_unit) + let male xx = X.(F.male xx >>= to_unit) + let female xx = X.(F.female xx >>= to_unit) + let single xx = X.(F.single xx >>= to_unit) + let left xx = X.(F.left1 xx >>= to_unit) + let marriedto yy xx = X.(F.marriedto yy xx >>= to_unit) + let saw yy xx = X.(F.saw1 yy xx >>= to_unit) + let kisses yy xx = X.(F.kisses1 yy xx >>= to_unit) + let loves yy xx = X.(F.loves1 yy xx >>= to_unit) + let thinks pp xx = failwith "Unimplemented" + let maybe pp = failwith "Unimplemented" +end (* Sem5c *) + + +(* Dynamic version of Sem3c / Add intensionality to Sem5c *) +module Sem6c = struct + let dynamic = true + let extensional = false + + (* This needs to use monad SLY, with store = var -> entity + and box type = store -> world -> ['a,store] + Sentence meaning is box(unit). + Later strategies with more complex sentence meanings and stores + may be able to use monad LSY, with box type store -> world -> ['a],store + *) + module X = SLY + type noun = entity X.t + type sent = unit X.t + let run (xx : sent) : bool = X.(not (List.is_null (run xx env0 Actual))) + (* lift an 'a list to a single 'a X.t *) + 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 + let getx = X.(gets (lookup 'x')) + let gety = X.(gets (lookup 'y')) + let getz = X.(gets (lookup 'z')) + let getw = X.(ask) (* get world from the underlying Y monad *) + (* select an intranstive verb based on the world *) + let select1 f1 f2 f3 xx = X.(getw >>= fun w -> (if w = Actual then f1 else if w = Other then f2 else f3) xx) + (* select a transitive verb based on the world *) + 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) + let let_ c (xx : noun) (body : sent) = X.(xx >>= fun x -> modify (insert c x) >> body) + let letw world (body : sent) = X.(shift (fun _ -> world) body) (* shift the "env" of the underlying Y monad *) + let to_unit (x : bool) : unit X.t = X.guard x +(* + 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) +*) + + let (~~~) (xx : sent) : sent = + 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 + Obj.magic yy (* this is an identity function that changes the type of yy to a unit X.t *) + + let (&&&) xx yy = X.(xx >> yy) + let (|||) xx yy = ~~~ (~~~ xx &&& ~~~ yy) + let (>>>) xx yy = X.(~~~ (xx >> ~~~ yy)) + + let some c (body : sent) = X.(let_ c (mids domain) body) + let every c (body : sent) = ~~~ (some c (~~~ body)) + + module F = Facts(X) + 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) + let (===) xx yy = X.(map2 (=) xx yy >>= to_unit) + let male xx = X.(F.male xx >>= to_unit) + let female xx = X.(F.female xx >>= to_unit) + let single xx = X.(F.single xx >>= to_unit) + let left xx = X.(select1 F.left1 F.left2 F.left3 xx >>= to_unit) + let saw yy xx = X.(select2 F.saw1 F.saw2 F.saw3 yy xx >>= to_unit) + let marriedto yy xx = X.(F.marriedto yy xx >>= to_unit) + let kisses yy xx = X.(select2 F.kisses1 F.kisses2 F.kisses3 yy xx >>= to_unit) + let loves yy xx = X.(select2 F.loves1 F.loves2 F.loves3 yy xx >>= to_unit) + let thinks pp xx = failwith "Unimplemented" + let maybe (body : sent) : sent = + let (yy : S.store -> Y.env -> (unit * S.store) list) = fun s w -> + let body_int = List.map (fun w' -> not @@ List.is_null @@ X.run (letw w' body) s w) modal_domain in + if any_truths body_int then [(),s] else [] in + Obj.magic yy +end (* Sem6c *) + +(* 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. + Next we develop some semantics that are closer to their actual presentation. *) + +(* This develops Sem5c using in part the strategies from Sem1b. *) +module Sem5e = struct + let dynamic = true + let extensional = true + + (* Let a topic be sequence of entities introduced into conversation (GSV's pegs -> entities, with pegs construed as positions in the sequence). + Then let store = var -> int (that is, position in the topic) + Then we can use monad LS', with box type = store -> ['a],store + And sentence meanings are Kleisli arrows: topic -> box(topic). The list component + in the type captures indeterminacy in what objects are being discussed (introduced + by quantifiers). Truths (relative to a initial store and topic) result in + non-empty topic lists; falsehoods in empty ones. + *) + type topic = entity list + let topic0 = [] + module X = LS' + type noun = (topic -> entity) X.t + type sent = topic -> topic X.t + let run (k : sent) : bool = X.(not (List.is_null (fst (run (k topic0) env0)))) + (* lift an 'a list to a single 'a X.t *) + 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 + 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) + let getx : noun = X.(gets (lookup 'x') >>= fun n -> mid (get_nth n)) + let gety : noun = X.(gets (lookup 'y') >>= fun n -> mid (get_nth n)) + let getz : noun = X.(gets (lookup 'z') >>= fun n -> mid (get_nth n)) + let let_ c (n : int) (body : sent) : sent = fun top -> X.(modify (insert c n) >> (body top)) +(* + let lookup_string sought env top = try string_of_entity (List.nth top (env sought)) with Not_found -> "*" | List.Short_list -> "#" + let print_lookup sought env top = print_string (lookup_string sought env top) + 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) +*) + + let (~~~) (k : sent) : sent = fun top -> + 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 + Obj.magic yy (* this is an identity function that changes the type of yy to a topic X.t *) + let (&&&) k j = X.(k >=> j) + let (|||) k j = ~~~ (~~~ k &&& ~~~ j) (* TODO how about (k >>> j) >>> j *) + let (>>>) k j = X.(~~~ (k >=> ~~~ j)) + + let some c (body : sent) : sent = fun top -> + let n = length top in + let aux ent = X.(let_ c n body) (List.snoc top ent) in + let domain' = List.map aux domain in + X.join (mids domain') + + let every c (body : sent) = ~~~ (some c (~~~ body)) + +(* TODO + let some c body = X.(mids domain >>= fun x -> modify (insert c x) body >>= guard >> mid x) + 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) +*) + + module F = Facts(X) + let mapply' (ff : noun) (top : topic) : entity X.t = X.(map (fun f -> f top) ff) + let wrap name = X.(mid (const name)) + let wrap1 f xx = fun top -> X.(f (mapply' xx top) >>= fun b -> if b then mid top else mzero) + let wrap2 f xx yy = fun top -> X.(f (mapply' xx top) (mapply' yy top) >>= fun b -> if b then mid top else mzero) + let ann = wrap Ann let bill = wrap Bill let carol = wrap Carol let dave = wrap Dave let ella = wrap Ella let frank = wrap Frank + let (===) (xx : noun) (yy : noun) : sent = wrap2 X.(map2 (=)) xx yy + let male (xx : noun) : sent = wrap1 F.male xx + let female xx = wrap1 F.female xx + let single xx = wrap1 F.single xx + let left xx = wrap1 F.left1 xx + let marriedto yy xx = wrap2 F.marriedto yy xx + let saw yy xx = wrap2 F.saw1 yy xx + let kisses yy xx = wrap2 F.kisses1 yy xx + let loves yy xx = wrap2 F.loves1 yy xx + let thinks pp xx = fun top -> failwith "Unimplemented" + let maybe pp = fun top -> failwith "Unimplemented" +end (* Sem5e *) + +(* Add intensionality to Sem5e *) +module Sem6e = struct + let dynamic = true + let extensional = false + + type topic = entity list + let topic0 = [] + module X = LS'Y + type noun = (topic -> entity) X.t + type sent = topic -> topic X.t + let run (k : sent) : bool = X.(not (List.is_null (fst (run (k topic0) env0 Actual)))) + (* lift an 'a list to a single 'a X.t *) + 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 + 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) + let getx : noun = X.(gets (lookup 'x') >>= fun n -> mid (get_nth n)) + let gety : noun = X.(gets (lookup 'y') >>= fun n -> mid (get_nth n)) + let getz : noun = X.(gets (lookup 'z') >>= fun n -> mid (get_nth n)) + let getw = X.(ask) (* get world from the underlying Y monad *) + (* select an intranstive verb based on the world *) + let select1 f1 f2 f3 xx = X.(getw >>= fun w -> (if w = Actual then f1 else if w = Other then f2 else f3) xx) + (* select a transitive verb based on the world *) + 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) + let let_ c (n : int) (body : sent) : sent = fun top -> X.(modify (insert c n) >> (body top)) + let letw world (body : sent) : sent = fun top -> X.(shift (fun _ -> world) (body top)) (* shift the "env" of the underlying Y monad *) + + let (~~~) (k : sent) : sent = fun top -> + 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 + Obj.magic yy (* this is an identity function that changes the type of yy to a topic X.t *) + let (&&&) k j = X.(k >=> j) + let (|||) k j = ~~~ (~~~ k &&& ~~~ j) + let (>>>) k j = X.(~~~ (k >=> ~~~ j)) + + let some c (body : sent) : sent = fun top -> + let n = length top in + let aux ent = X.(let_ c n body) (List.snoc top ent) in + let domain' = List.map aux domain in + X.join (mids domain') + + let every c (body : sent) = ~~~ (some c (~~~ body)) + + module F = Facts(X) + let mapply' (ff : noun) (top : topic) : entity X.t = X.(map (fun f -> f top) ff) + let wrap name = X.(mid (const name)) + let wrap1 f xx = fun top -> X.(f (mapply' xx top) >>= fun b -> if b then mid top else mzero) + let wrap2 f xx yy = fun top -> X.(f (mapply' xx top) (mapply' yy top) >>= fun b -> if b then mid top else mzero) + let ann = wrap Ann let bill = wrap Bill let carol = wrap Carol let dave = wrap Dave let ella = wrap Ella let frank = wrap Frank + let (===) (xx : noun) (yy : noun) : sent = wrap2 X.(map2 (=)) xx yy + let male (xx : noun) : sent = wrap1 F.male xx + let female xx = wrap1 F.female xx + let single xx = wrap1 F.single xx + let left xx = wrap1 (select1 F.left1 F.left2 F.left3) xx + let marriedto yy xx = wrap2 F.marriedto yy xx + let saw yy xx = wrap2 (select2 F.saw1 F.saw2 F.saw3) yy xx + let kisses yy xx = wrap2 (select2 F.kisses1 F.kisses2 F.kisses3) yy xx + let loves yy xx = wrap2 (select2 F.loves1 F.loves2 F.loves3) yy xx + let thinks pp xx = failwith "Unimplemented" + let maybe (body : sent) : sent = fun top -> + let (yy : S'.store -> Y.env -> topic list * S'.store) = fun s w -> + let body_int = List.map (fun w' -> not @@ List.is_null @@ fst @@ X.run (letw w' body top) s w) modal_domain in + if any_truths body_int then [top],s else [],s in + Obj.magic yy +end (* Sem6e *) + +module TestAll = struct + print_endline "\nTesting Sem1a";; + module T1a = Test(Sem1a);; + print_endline "\nTesting Sem1b";; + module T1b = Test(Sem1b);; + print_endline "\nTesting Sem2a";; + module T2a = Test(Sem2a);; + print_endline "\nTesting Sem2c";; + module T2c = Test(Sem2c);; + print_endline "\nTesting Sem3a";; + module T3a = Test(Sem3a);; + print_endline "\nTesting Sem3c";; + module T3c = Test(Sem3c);; + print_endline "\nTesting Sem5c";; + module T5c = Test(Sem5c);; + print_endline "\nTesting Sem5e";; + module T5e = Test(Sem5e);; + print_endline "\nTesting Sem6c";; + module T6c = Test(Sem6c);; + print_endline "\nTesting Sem6e";; + module T6e = Test(Sem6e);; + print_newline () +end + +(* + One can't test the broken vase case by comparing the _truth_ of any sentences. + The difference is in whether the sentences have meanings that are "supported by" + the same informtation states. Compare in our model: + (i) Someone kissed me. She might have stayed. + and: + (ii) Someone who might have stayed kissed me. + Recall that in our model Ann leaves in every world, but Carol stays in some (non-actual) + world. If my background information settles that I was kissed by either Ann or Carol, + then I'm in a position to assert (i), since after the first clause it's left open + that the referent be either woman. But it doesn't put me in a position to assert (ii), + since that implies I was kissed by Carol. So far as truth-value goes, + if Carol kissed me both sentences are true, and if Ann did then both sentences are false. +*) + diff --git a/index.mdwn b/index.mdwn index 5e1c25da..00082462 100644 --- a/index.mdwn +++ b/index.mdwn @@ -167,7 +167,7 @@ Practical advice for working with OCaml and/or Haskell (will be posted someday); (**Week 9**) Thursday April 2 -> Updated notes on [[Installing and Using the Juli8 Libraries|/juli8]] on Sun 5 April. Continued to fix some bugs and improve the monad transformers. Latest version posted Tuesday evening, 7 April: [[v1.5|/code/Juli8-v1.5.tgz]]. +> Updated notes on [[Installing and Using the Juli8 Libraries|/juli8]] on Sun 5 April. Continued to fix some bugs and improve the monad transformers. Latest version posted Monday evening, 13 April: [[v1.6|/code/Juli8-v1.6.tgz]]. This version is needed to run the GSV.ml code.