X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?a=blobdiff_plain;ds=inline;f=sandbox.mdwn;h=45b5dfbc9cdd0fd024ead7c7eae29a70cf2df0d8;hb=f73d7704650f26f1ad4663abf5a811961ce143cf;hp=ddb43d2cc65e804d021fd8ec91585e592893c83b;hpb=cf87edfd9d4cb5026287b39b190797ef72237f19;p=lambda.git diff --git a/sandbox.mdwn b/sandbox.mdwn index ddb43d2c..45b5dfbc 100644 --- a/sandbox.mdwn +++ b/sandbox.mdwn @@ -1,32 +1,270 @@ -This is the SandBox, a page anyone can edit to learn how to use the wiki. +
+# Doing things with monads ----- +## Extended application: Groenendijk, Stokhof and Veltman's *Coreference and Modality* -Here's a paragraph. α β + GSV = GS + V + + GS = Dynamic Predicate Logic L&P 1991: dynamic binding, donkey anaphora + Dynamic Montague Grammar 1990: generalized quantifiers, discourse referents -Here's _another_ **one** with *emphasised* text. + V = epistemic modality -# Header +What are pegs? A paper by Landman called `Pegs and Alecs'. -## Subheader + It might be raining. It's not raining. + #It's not raining. It might be raining. -> This is a blockquote. -> -> This is the first level of quoting. -> -> > This is nested blockquote. -> -> Back to the first level. +## Two-part assignment functions -Numbered list + type var = string + type peg = int + type refsys = var -> peg + type ent = Alice | Bob | Carl + type assignment = peg -> ent -1. First item. -1. Another. -1. And another.. + type pred = string + type world = pred -> ent -> bool + type pegcount = int + type poss = world * pegcount * refsys * assignment + type infostate = [poss] -Bulleted list +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). -* *item* -* item + ref(i, t) = t if t is an individual, and + g(r(t)) if t is a variable, where i = (w,n,r,g) -[[ikiwiki/WikiLink]] + 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