# Doing things with monads

## Extended application: Groenendijk, Stokhof and Veltman's *Coreference and Modality*

  GSV = GS + V
        
  GS = Dynamic Predicate Logic L&P 1991: dynamic binding, donkey anaphora
       Dynamic Montague Grammar 1990: generalized quantifiers, discourse referents

  V = epistemic modality

What are pegs?  A paper by Landman called `Pegs and Alecs'.

    It might be raining.  It's not raining.
    #It's not raining.  It might be raining.

## Two-part assignment functions

    type var = string
    type peg = int
    type refsys = var -> peg
    type ent = Alice | Bob | Carl
    type assignment = peg -> ent

    type pred = string
    type world = pred -> ent -> bool
    type pegcount = int
    type poss = world * pegcount * refsys * assignment
    type infostate = [poss]

So information states track both facts about the world (e.g., which
objects count as a man), and facts about the discourse (e.g., how many
pegs have been used).

    ref(i, t) = t if t is an individual, and 
                g(r(t)) if t is a variable, where i = (w,n,r,g)

    s[P(t)] = {i in s | w(P)(ref(i,t))}

    s[t1 = t2] = {i in s | ref(i,t1) = ref(i,t2)}

    s[φ and ψ] = s[φ][ψ]

    s[∃xφ] = Union {{(w, n+1, r[x->n], g[n->a]) | (w,n,r,g) in s}[φ] | a in ent} 

    s[neg φ] =  {i | {i}[φ] = {}}

    1. {(w,n,r,g)}[∃x.person(x)]
    2. {(w,n,r,g)}[∃x.man(x)]
    3. {(w,n,r,g)}[∃x∃y.person(x) and person(y)]
    4. {(w,n,r,g)}[∃x∃y.x=y]

## Order and modality

    s[◊φ] = {i in s | s[φ] ≠ {}}

    1. Alice isn't hungry.  #Alice might be hungry.

      {hungry, full}[Alice isn't hungry][Alice might be hungry]
    = {full}[Alice might be hungry]
    = {}

    2. Alice might be hungry.  Alice isn't hungry.

    = {hungry, full}[Alice might be hungry][Alice isn't hungry]
    = {hungry, full}[Alice isn't hungry]
    = {full}

GSV: a single speaker couldn't possibly be in a position to utter (2).

    3. Based on public evidence, Alice might be hungry.  But in fact she's not hungry.

    4. Alice might be hungry.  Alice *is* hungry.
    5. Alice is hungry.  (So of course) Alice might be hungry.

consider: update with the prejacent and its negation must both be non-empty.

## Order and binding

    6. A man^x entered.  He_x sat.
    7. He_x sat.  A man^x entered.

    8. {(w,1,r[x->0],g[0->b])}

This infostate contains a refsys and an assignment that maps the
variable x to Bob.  Here are the facts in world w:

    w "enter" a = false
    w "enter" b = true
    w "enter" c = true

    w "sit" a = true
    w "sit" b = true
    w "sit" c = false

    9. Someone^x entered.  He_x sat.  

         {(w,1,r[x->0],g[0->b])}[∃x.enter(x)][sit(x)]

          -- the existential adds a new peg and assigns it to each
          -- entity in turn

       = (   {(w,2,r[x->0][x->1],g[0->b][1->a])}[enter(x)]
          ++ {(w,2,r[x->0][x->1],g[0->b][1->b])}[enter(x)]
          ++ {(w,2,r[x->0][x->1],g[0->b][1->c])}[enter(x)])[sit(x)]

          -- "enter(x)" filters out the possibility in which x refers
          -- to Alice, since Alice didn't enter

       = (   {}
          ++ {(w,2,r[x->0][x->1],g[0->b][1->b])}
          ++ {(w,2,r[x->0][x->1],g[0->b][1->c])})[sit(x)]

          -- "sit(x)" filters out the possibility in which x refers
          -- to Carl, since Carl didn't sit

       =  {(w,2,r[x->0][x->1],g[0->b][1->b])}

existential in effect binds the pronoun in the following clause

    10. He_x sat.  Someone^x entered. 

         {(w,1,r[x->0],g[0->b])}[sit(x)][∃x.enter(x)]

         -- evaluating `sit(x)` rules out nothing, since (coincidentally)
         -- x refers to Bob, and Bob is a sitter

       = {(w,1,r[x->0],g[0->b])}[∃x.enter(x)]

         -- Just as before, the existential adds a new peg and assigns
         -- it to each object

       =    {(w,2,r[x->0][x->1],g[0->b][1->a])}[enter(x)]
         ++ {(w,2,r[x->0][x->1],g[0->b][1->b])}[enter(x)]
         ++ {(w,2,r[x->0][x->1],g[0->b][1->c])}[enter(x)]

         -- enter(x) eliminates all those possibilities in which x did
         -- not enter

       = {} ++ {(w,2,r[x->0][x->1],g[0->b][1->b])}
            ++ {(w,2,r[x->0][x->1],g[0->b][1->c])}

       = {(w,2,r[x->0][x->1],g[0->b][1->b]), 
          (w,2,r[x->0][x->1],g[0->b][1->c])}

    11. A man^x entered.  He_x sat.  He_x spoke.
    12. He_x sat.  A man^x entered.  He_x spoke.

consider: new peg requires object not in the domain of the assignment fn

    13. If a woman entered, she sat.

## Interactions of binding with modality

    (∃x.enter(x)) and (sit(x)) ≡ ∃x (enter(x) and sit(x))

but (∃x.closet(x)) and (◊guilty(x)) ≡/≡ ∃x (closet(x) and ◊guilty(x))

    The Broken Vase:
    There are three sons, Bob, Carl, and Dave.  
    One of them broke a vase.  
    Bob is known to be innocent.  
    Someone is hiding in the closet.


        in closet        guilty 
        ---------------  ---------------
    w:  b  false         b  false
        c  false         c  false
        d  true          d  true

    w': b  false         b  false
        c  true          c  false
        d  false         d  true

GSV observe that (∃x.closet(x)) and (◊guilty(x)) is true if there is
at least one possibility in which a person in the closet is guilty.
In this scenario, world w is the verifying world.  It remains possible
that there are closet hiders who are not guilty in any world.  Carl
fits this bill: he's in the closet in world w', but he is not guilty
in any world.

    14. Someone^x is in the closet.  He_x might be guilty.

         {(w,0,r,g), (w',0,r,g}[∃x.closet(x)][◊guilty(x)]

         -- existential introduces new peg

       = (   {(w,1,r[x->0],g[0->b])}[closet(x)]
          ++ {(w,1,r[x->0],g[0->c])}[closet(x)]
          ++ {(w,1,r[x->0],g[0->d])}[closet(x)]
          ++ {(w',1,r[x->0],g[0->b])}[closet(x)]
          ++ {(w',1,r[x->0],g[0->c])}[closet(x)]
          ++ {(w',1,r[x->0],g[0->d])}[closet(x)])[◊guilty(x)]

         -- only possibilities in which x is in the closet survive

       = {(w,1,r[x->0],g[0->d]),
          (w',1,r[x->0],g[0->c])}[◊guilty(x)]

         -- Is there any possibility in which x is guilty?
         -- yes: for x = Dave, in world w Dave broke the vase

       = {(w,1,r[x->0],g[0->d]),
          (w',1,r[x->0],g[0->c])}

Now we consider the second half:

    14. Someone^x is in the closet who_x might be guilty.

         {(w,0,r,g), (w',0,r,g)}[∃x(closet(x) & ◊guilty(x))]
       
         -- existential introduces new peg

       =    {(w,1,r[x->0],g[0->b])}[closet(x)][◊guilty(x)]
         ++ {(w,1,r[x->0],g[0->c])}[closet(x)][◊guilty(x)]
         ++ {(w,1,r[x->0],g[0->d])}[closet(x)][◊guilty(x)]
         ++ {(w',1,r[x->0],g[0->b])}[closet(x)][◊guilty(x)]
         ++ {(w',1,r[x->0],g[0->c])}[closet(x)][◊guilty(x)]
         ++ {(w',1,r[x->0],g[0->d])}[closet(x)][◊guilty(x)]

          -- filter out possibilities in which x is not in the closet
          -- and filter out possibilities in which x is not guilty
          -- the only person who was guilty in the closet was Dave in
          -- world 1

       = {(w,1,r[x->0],g[0->d])}

The result is different, and more informative.  

## Binding, modality, and identity

The fragment correctly predicts the following contrast:

    15. Someone^x entered.  He_x might be Bob.  He_x might not be Bob.
        (∃x.enter(x)) & ◊x=b & ◊not(x=b)
        -- This discourse requires a possibility in which Bob entered
        -- and another possibility in which someone who is not Bob entered

    16. Someone^x entered who might be Bob and who might not be Bob.
        ∃x (enter(x) & ◊x=b & ◊not(x=b))
        -- This is a contradition: there is no single person who might be Bob
        -- and who simultaneously might be someone else

### Identifiers

Let α be a term which differs from x.  Then α is an identifier if the
following formula is supported by every information state:

    ∀x(◊(x=α) --> (x=α))

The idea is that α is an identifier just in case there is only one
object that it can refer to.  Here is what GSV say:

    A term is an identifier per se if no mattter what the information
    state is, it cannot fail to decie what the denotation of the term is.

## Why have a two-part assignment function?

In the current system, variables are associated with values in two
steps.

    Variables        Pegs         Entities
    ---------   r    ----    g    --------   
       x       -->    0     -->      a
       y       -->    1     -->      b
       z       -->    2     -->      c

Here, r is a refsys mapping variables to pegs, and g is an assignment function mapping pegs to entities