X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=sandbox.mdwn;h=45b5dfbc9cdd0fd024ead7c7eae29a70cf2df0d8;hp=4a2897507b2a727ee671e79ef1e1261a6eda976c;hb=cf725beaaf55f74fe02a94dd072449b030ae8928;hpb=b27a7a1123dc21df15cdc007667150719f8d456d diff --git a/sandbox.mdwn b/sandbox.mdwn index 4a289750..45b5dfbc 100644 --- a/sandbox.mdwn +++ b/sandbox.mdwn @@ -1,44 +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* -Try some math: -. Okay, that's it! + 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 -# Header + type pred = string + type world = pred -> ent -> bool + type pegcount = int + type poss = world * pegcount * refsys * assignment + type infostate = [poss] -## Subheader +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} -[[ikiwiki/WikiLink]] + 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