name change

[lambda.git] / code / gsv2.ml

diff --git a/code/gsv2.ml b/code/gsv2.ml
index c8f039f..7f2775a 100644 (file)
--- 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
 
 
 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.
    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).
 
    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
    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.
    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 *)
 
   let maybe pp = fun b -> failwith "Unimplemented"
 end (* Sem1b *)
 

-module Sem2a = struct
+module Sem3a = struct

   let dynamic = false
   let extensional = true
 
   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
      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 [].
 *)
      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"
   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. *)
 
    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
 
   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"
   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 *)
    Not here implemented. *)
 
 (* Add intensionality to 2a *)

-module Sem3a = struct
+module Sem4a = struct

   let dynamic = false
   let extensional = false
 
   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
       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 *)
    Not here implemented. *)
 
 (* Add intensionality to 2c *)

-module Sem3c = struct
+module Sem4c = struct

   let dynamic = false
   let extensional = false
 
   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
       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. *)
 
 
    Not here implemented. *)
 
 

-(* Dynamic version of Sem2c *)
-module Sem5c = struct
+(* Dynamic version of Sem3c *)
+module Sem7c = struct

   let dynamic = true
   let extensional = true
 
   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"
   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
 
   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
       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. *)
 
    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
 
   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.
      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 = []
   *)
   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"
   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
 
   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([]).
      [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);;
 
 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 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
 
   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.
     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>)

 *)
 *)

+