X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=code%2Fgsv2.ml;h=7f2775a7994dcc23e3e516b81523e17f638b7ca5;hp=c8f039f19d04f3546842fd4712095cca35fb72f3;hb=ad14f269d489cc9a2ea9e522e2da37a42cfd46b3;hpb=32ce1118599528c2f407d7fba1f14a658f918e94

diff --git a/code/gsv2.ml b/code/gsv2.ml
index c8f039f1..7f2775a7 100644
--- a/code/gsv2.ml
+++ b/code/gsv2.ml
@@ -1,4 +1,4 @@
-(* GSV monadically 13 April 2015 *)
+(* GSV monadically 15 April 2015 *)
 
 type identifier = char
 
@@ -386,23 +386,29 @@ end
    A variety of semantics are provided. Here is the naming scheme:
    
    Sem1* is classic semantics with support for variable binding/anaphora.
-   Sem4* would be the dynamic alternative of 1*. (not here provided)
-   You shouldn't be able to implement quantification in these,
-   without bringing in some of the mechanisms of a list/set component.
-   However, Haskell provides those mechanisms in the basic Monad API (as the
-   function Juli8 names `seq`), so we can do quantification without _explicitly_
-   invoking a ListT in our monadic stack.
+   Sem5* would be the dynamic alternative of 1*. (not here provided, but
+   discussed in comments.)
+   You can't implement quantification in these,
+   except by bringing in some of the mechanisms of a list/set component.
+   (You'll create a box([entity]) and convert it to a box([bool]),
+   then convert the latter to box(bool).)
+   However, Haskell already provides the needed mechanisms in the basic Monad API (as the
+   function Juli8 names `seq`), so we can do quantification without _explicitly
+   invoking_ a ListT in our monadic stack.
 
-   Sem2* adds a List component to the stack to do quantification.
-   Sem5* is the dynamic counterpart.
+   Sem2* and Sem 6* would be the intensionalized versions of those.
+   (Not here provided, but Sem6* is discussed in comments.)
 
-   Sem3* adds an (additional) Reader monad for intensionality.
-   Sem6* is the dynamic counterpart.
+   Sem3* adds a List component to the stack to do quantification.
+   Sem7* is the dynamic counterpart.
+
+   Sem4* adds an (additional) Reader monad for intensionality.
+   Sem8* is the dynamic counterpart.
 
    Within that broad organization, here are the sub-patterns:
 
    SemNa uses just a bool payload, so sent types are box(bool).
-   SemBb makes sent types the Klesli variant of Na, so sent types are
+   SemNb makes sent types the Klesli variant of Na, so sent types are
    bool -> box(bool).
    SemNc uses instead a unit payload, which we can do when the monadic
    stack has a List or Option component; then false will be the monad's
@@ -410,12 +416,9 @@ end
    mzero.
    SemNd would be the Kleisli variant of Nc, as Nb is the Kleisli variant
    of Na.
-   SemNe (only for dynamic) uses "topics" or sequences of entities being
-   discussed as payloads, so sent types use box(topic). It also incorporates
-   elements of SemNb/d, so that sent types are really topic -> box(topic).
-   SemNf (not yet provided) would remove the List component from the monad
-   stack, in order to properly implement Veltman's "might". Now sent
-   types would be [topic] -> box([topic]).
+   SemNe (only for dynamic) would use "topics" or sequences of entities being discussed
+   as payloads, so sent types are box(topic). What we really provide
+   here is the Kleisli variation of this (SemNf), so sent types = topic -> box(topic).
 *)
  
 
@@ -513,7 +516,7 @@ module Sem1b = struct
   let maybe pp = fun b -> failwith "Unimplemented"
 end (* Sem1b *)
 
-module Sem2a = struct
+module Sem3a = struct
   let dynamic = false
   let extensional = true
 
@@ -527,7 +530,7 @@ module Sem2a = struct
      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 same as an empty list. Sem3c, below, eliminates this artifact by changing
      the sentence type to box(unit). Then truths (rel to an env) are [();...] and
      falsehoods are [].
 *)
@@ -562,13 +565,13 @@ module Sem2a = struct
   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 *)
+end (* Sem3a *)
 
-(* Sem2b would convert Sem2a into having sentence meanings be Kleisli arrows, as Sem1b did.
+(* Sem3b would convert Sem3a 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
+(* Variant of Sem3a, which uses [();...] vs [] instead of [true;...] vs (list of all false OR []). *)
+module Sem3c = struct
   let dynamic = false
   let extensional = true
 
@@ -613,13 +616,13 @@ module Sem2c = struct
   let loves yy xx = X.(F.loves1 yy xx >>= to_unit)
   let thinks pp xx = failwith "Unimplemented"
   let maybe pp = failwith "Unimplemented"
-end (* Sem2c *)
+end (* Sem3c *)
 
-(* Sem2d would convert Sem2c into having sentence meanings be Kleisli arrows, as Sem1b did.
+(* Sem3d would convert Sem3c into having sentence meanings be Kleisli arrows, as Sem1b did.
    Not here implemented. *)
 
 (* Add intensionality to 2a *)
-module Sem3a = struct
+module Sem4a = struct
   let dynamic = false
   let extensional = false
 
@@ -666,13 +669,13 @@ module Sem3a = struct
       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 *)
+end (* Sem4a *)
 
-(* Sem3b would convert Sem3a into having sentence meanings be Kleisli arrows, as Sem1b did.
+(* Sem4b would convert Sem4a into having sentence meanings be Kleisli arrows, as Sem1b did.
    Not here implemented. *)
 
 (* Add intensionality to 2c *)
-module Sem3c = struct
+module Sem4c = struct
   let dynamic = false
   let extensional = false
 
@@ -725,14 +728,14 @@ module Sem3c = struct
       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 *)
+end (* Sem4c *)
 
-(* Sem3d would convert Sem3c into having sentence meanings be Kleisli arrows, as Sem1b did.
+(* Sem4d would convert Sem4c into having sentence meanings be Kleisli arrows, as Sem1b did.
    Not here implemented. *)
 
 
-(* Dynamic version of Sem2c *)
-module Sem5c = struct
+(* Dynamic version of Sem3c *)
+module Sem7c = struct
   let dynamic = true
   let extensional = true
 
@@ -789,11 +792,11 @@ module Sem5c = struct
   let loves yy xx = X.(F.loves1 yy xx >>= to_unit)
   let thinks pp xx = failwith "Unimplemented"
   let maybe pp = failwith "Unimplemented"
-end (* Sem5c *)
+end (* Sem7c *)
 
 
-(* Dynamic version of Sem3c / Add intensionality to Sem5c *)
-module Sem6c = struct
+(* Dynamic version of Sem4c / Add intensionality to Sem7c *)
+module Sem8c = struct
   let dynamic = true
   let extensional = false
 
@@ -852,13 +855,13 @@ module Sem6c = struct
       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 *)
+end (* Sem8c *)
 
-(* Sem6c seems adequate for much of the phenomena GSV are examining, and is substantially simpler than their own semantics. Sem6c doesn't have their "pegs" and complex two-stage function from vars to referents.
+(* Sem8c seems adequate for much of the phenomena GSV are examining, and is substantially simpler than their own semantics. Sem8c doesn't have their "pegs" and complex two-stage function from vars to referents.
    Next we develop some semantics that are closer to their actual presentation. *)
 
-(* This develops Sem5c using in part the Kleisli strategy from Sem1b. *)
-module Sem5e = struct
+(* This develops Sem7c using in part the Kleisli strategy from Sem1b. *)
+module Sem7f = struct
   let dynamic = true
   let extensional = true
 
@@ -878,7 +881,7 @@ module Sem5e = struct
      Our meaning types (once we add worlds in 6e, below) will be:
        topic -> (store -> world -> ([topic] * store))
      We count a world as eliminated when it results in an empty list of topics.
-     Note that our Sem6e doesn't yet properly handle Veltman's "might"; see remarks below.
+     Note that our Sem8f doesn't yet properly handle Veltman's "might"; see remarks below.
   *)
   type topic = entity list
   let topic0 = []
@@ -931,10 +934,10 @@ module Sem5e = struct
   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 *)
+end (* Sem7f *)
 
-(* Add intensionality to Sem5e. See comments there. *)
-module Sem6e = struct
+(* Add intensionality to Sem7f. See comments there. *)
+module Sem8f = struct
   let dynamic = true
   let extensional = false
 
@@ -1018,31 +1021,53 @@ module Sem6e = struct
      [topic] as our payloads, so that sent types would then be: [topic] -> S'Y([topic]). All of the operations except
      for `maybe` would then have to emulate the operations of the List monad by hand (manually performing catmap etc).
      But `maybe` could examine the [topic] as a whole and decide whether to return box(it) or box([]).
+     This would be to go back to the Sem5/Sem6 choices of monads (without list), and to implement the handling of lists
+     by hand, as we did in the Sem1/Sem2 strategies.
+
+     Additionally, we haven't tried here to handle non-rigid noun-types. That's why we can have sent types be:
+         topic (or [topic]) -> store -> world -> ([topic], store)
+     the input topic doesn't depend on what the world is. GSV's types are suited to handle non-rigid noun types,
+     since they are instead using an analogue of (world * topic) -> store -> ([world,topic], store). We could follow suit,
+     removing the Reader monad implementing Intensionality from our stack and implementing that by hand, too. Another
+     strategy would be to continue using a Reader monad but not by merging it into our main monad stack, instead using
+     values of _that_ box type as _payloads for_ our main box type. This echoes a question raised by Dylan in seminar:
+     why must we combine the monads only by way of "stacking them" into a single monad? As Jim said in seminar, it's not
+     obvious one must do so, it just seems most natural. The strategy being evisaged now would at least in part follow
+     Dylan's suggestion. We'd let our sentence types then be:
+         intensionality_box([topic]) -> state_plus_intensionality_box(intensionality_box([topic]))
+       = intensionality_box([topic]) -> store -> world -> (intensionality_box([topic]) * store)
+     In that case, I think we could once again merge the list component into the intensionality_box type, getting:
+         intens_list_box(topic) -> state_intens_box(intens_list_box(topic))
+       = intens_list_box(topic) -> store -> world -> (intens_list_box(topic) * store)
+       = (world -> [topic]) -> store -> world -> ((world -> [topic]) * store)
+     That looks like a pretty complicated type, and might not seem an improvement over GSV's own system. But its advantage is that
+     the implementation of its operations would so closely parallel the other semantic strategies illustrated above.
+     Testifying to the "modularity" of monads, which we have been recommending as one of their prominent virtues.
   *)
 
-end (* Sem6e *)
+end (* Sem8f *)
 
 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_endline "\nTesting Sem4a";;
+  module T4a = Test(Sem4a);;
+  print_endline "\nTesting Sem4c";;
+  module T4c = Test(Sem4c);;
+  print_endline "\nTesting Sem7c";;
+  module T7c = Test(Sem7c);;
+  print_endline "\nTesting Sem7f";;
+  module T7f = Test(Sem7f);;
+  print_endline "\nTesting Sem8c";;
+  module T8c = Test(Sem8c);;
+  print_endline "\nTesting Sem8f";;
+  module T8f = Test(Sem8f);;
   print_newline ()
 end
 
@@ -1059,16 +1084,5 @@ end
     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.
-
-# let module S = Sem6e in let wife xx = S.(female xx &&& ~~~ (single xx)) in let may_stay xx = S.(maybe (~~~ (left xx))) in ...
-# let xx = S.(wife getx) in S.(run_ xx [[Ann];[Carol];[Ella]]);;
-- : entity list list * S'Y.store = ([[Ann]; [Carol]], <fun>)
-# let xx = S.(may_stay getx) in S.(run_ xx [[Ann];[Carol];[Ella]]);;
-- : entity list list * S'Y.store = ([[Carol]; [Ella]], <fun>)
-# let xx = S.(some 'y' (gety === getx)) in S.(run_ xx [[Ann];[Carol];[Ella]]);;
-- : entity list list * S'Y.store = ([[Ann; Ann]; [Carol; Carol]; [Ella; Ella]], <fun>)
-# let xx = S.(some 'y' (gety === getx &&& may_stay gety)) in S.(run_ xx [[Ann];[Carol];[Ella]]);;
-- : entity list list * S'Y.store = ([[Carol; Carol]; [Ella; Ella]], <fun>)
-# let xx = S.(some 'y' (gety === getx) &&& may_stay gety) in S.(run_ xx [[Ann];[Carol];[Ella]]);;
-- : entity list list * S'Y.store = ([[Carol; Carol]; [Ella; Ella]], <fun>)
 *)
+