-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.
+<pre>
+# 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:
-<img src="/cgi-bin/mathtex.cgi?x=\frac{-b\pm\sqrt{b^2-4ac}}{2a\pi}">. 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
-<!--
-[[!inline pages="test/* and !*/Discussion" show="3" rootpage="test"]]
--->
+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