X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=sandbox.mdwn;h=45b5dfbc9cdd0fd024ead7c7eae29a70cf2df0d8;hp=a00ad11eda45f6ce2d1815f437bd5c2c2c850f8b;hb=aa3fa8ee79bd50b6371da340227b2144026ae3a7;hpb=c5a278e48f536a3ad2858a1a8a3e7875fc8b6452 diff --git a/sandbox.mdwn b/sandbox.mdwn index a00ad11e..45b5dfbc 100644 --- a/sandbox.mdwn +++ b/sandbox.mdwn @@ -1,42 +1,270 @@ -This is the SandBox, a page anyone can edit to learn how to use the wiki. Here is $some^2 x^{e \pi} + 3y$ math, and $$here_{is} some + more$$. End of math. +
+# Doing things with monads

-Here is [[!img y-combinator.jpg size="200x200" alt="clouds"]]. And rest of paragraph.
+## 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

-----
-[[!inline pages="tagged(foo)" show=0 archive=yes]]
+  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.

-Here's a paragraph.
+## Two-part assignment functions

-Here's another one with *emphasised* text.
+    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).

-> This is a blockquote.
->
-> This is the first level of quoting.
->
-> > This is nested blockquote.
->
-> Back to the first level.
+    ref(i, t) = t if t is an individual, and
+                g(r(t)) if t is a variable, where i = (w,n,r,g)

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

-1. First item.
-1. Another.
-1. And another..
+    s[t1 = t2] = {i in s | ref(i,t1) = ref(i,t2)}

-Bulleted list
+    s[Ï and Ï] = s[Ï][Ï]

-* *item*
-* item
+    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
`