some rewrites, not finished
[lambda.git] / sandbox.mdwn
1 <pre>
2 # Doing things with monads
3
4 ## Extended application: Groenendijk, Stokhof and Veltman's *Coreference and Modality*
5
6   GSV = GS + V
7         
8   GS = Dynamic Predicate Logic L&P 1991: dynamic binding, donkey anaphora
9        Dynamic Montague Grammar 1990: generalized quantifiers, discourse referents
10
11   V = epistemic modality
12
13 What are pegs?  A paper by Landman called `Pegs and Alecs'.
14
15     It might be raining.  It's not raining.
16     #It's not raining.  It might be raining.
17
18 ## Two-part assignment functions
19
20     type var = string
21     type peg = int
22     type refsys = var -> peg
23     type ent = Alice | Bob | Carl
24     type assignment = peg -> ent
25
26     type pred = string
27     type world = pred -> ent -> bool
28     type pegcount = int
29     type poss = world * pegcount * refsys * assignment
30     type infostate = [poss]
31
32 So information states track both facts about the world (e.g., which
33 objects count as a man), and facts about the discourse (e.g., how many
34 pegs have been used).
35
36     ref(i, t) = t if t is an individual, and 
37                 g(r(t)) if t is a variable, where i = (w,n,r,g)
38
39     s[P(t)] = {i in s | w(P)(ref(i,t))}
40
41     s[t1 = t2] = {i in s | ref(i,t1) = ref(i,t2)}
42
43     s[φ and ψ] = s[φ][ψ]
44
45     s[∃xφ] = Union {{(w, n+1, r[x->n], g[n->a]) | (w,n,r,g) in s}[φ] | a in ent} 
46
47     s[neg φ] =  {i | {i}[φ] = {}}
48
49     1. {(w,n,r,g)}[∃x.person(x)]
50     2. {(w,n,r,g)}[∃x.man(x)]
51     3. {(w,n,r,g)}[∃x∃y.person(x) and person(y)]
52     4. {(w,n,r,g)}[∃x∃y.x=y]
53
54 ## Order and modality
55
56     s[◊φ] = {i in s | s[φ] ≠ {}}
57
58     1. Alice isn't hungry.  #Alice might be hungry.
59
60       {hungry, full}[Alice isn't hungry][Alice might be hungry]
61     = {full}[Alice might be hungry]
62     = {}
63
64     2. Alice might be hungry.  Alice isn't hungry.
65
66     = {hungry, full}[Alice might be hungry][Alice isn't hungry]
67     = {hungry, full}[Alice isn't hungry]
68     = {full}
69
70 GSV: a single speaker couldn't possibly be in a position to utter (2).
71
72     3. Based on public evidence, Alice might be hungry.  But in fact she's not hungry.
73
74     4. Alice might be hungry.  Alice *is* hungry.
75     5. Alice is hungry.  (So of course) Alice might be hungry.
76
77 consider: update with the prejacent and its negation must both be non-empty.
78
79 ## Order and binding
80
81     6. A man^x entered.  He_x sat.
82     7. He_x sat.  A man^x entered.
83
84     8. {(w,1,r[x->0],g[0->b])}
85
86 This infostate contains a refsys and an assignment that maps the
87 variable x to Bob.  Here are the facts in world w:
88
89     w "enter" a = false
90     w "enter" b = true
91     w "enter" c = true
92
93     w "sit" a = true
94     w "sit" b = true
95     w "sit" c = false
96
97     9. Someone^x entered.  He_x sat.  
98
99          {(w,1,r[x->0],g[0->b])}[∃x.enter(x)][sit(x)]
100
101           -- the existential adds a new peg and assigns it to each
102           -- entity in turn
103
104        = (   {(w,2,r[x->0][x->1],g[0->b][1->a])}[enter(x)]
105           ++ {(w,2,r[x->0][x->1],g[0->b][1->b])}[enter(x)]
106           ++ {(w,2,r[x->0][x->1],g[0->b][1->c])}[enter(x)])[sit(x)]
107
108           -- "enter(x)" filters out the possibility in which x refers
109           -- to Alice, since Alice didn't enter
110
111        = (   {}
112           ++ {(w,2,r[x->0][x->1],g[0->b][1->b])}
113           ++ {(w,2,r[x->0][x->1],g[0->b][1->c])})[sit(x)]
114
115           -- "sit(x)" filters out the possibility in which x refers
116           -- to Carl, since Carl didn't sit
117
118        =  {(w,2,r[x->0][x->1],g[0->b][1->b])}
119
120 existential in effect binds the pronoun in the following clause
121
122     10. He_x sat.  Someone^x entered. 
123
124          {(w,1,r[x->0],g[0->b])}[sit(x)][∃x.enter(x)]
125
126          -- evaluating `sit(x)` rules out nothing, since (coincidentally)
127          -- x refers to Bob, and Bob is a sitter
128
129        = {(w,1,r[x->0],g[0->b])}[∃x.enter(x)]
130
131          -- Just as before, the existential adds a new peg and assigns
132          -- it to each object
133
134        =    {(w,2,r[x->0][x->1],g[0->b][1->a])}[enter(x)]
135          ++ {(w,2,r[x->0][x->1],g[0->b][1->b])}[enter(x)]
136          ++ {(w,2,r[x->0][x->1],g[0->b][1->c])}[enter(x)]
137
138          -- enter(x) eliminates all those possibilities in which x did
139          -- not enter
140
141        = {} ++ {(w,2,r[x->0][x->1],g[0->b][1->b])}
142             ++ {(w,2,r[x->0][x->1],g[0->b][1->c])}
143
144        = {(w,2,r[x->0][x->1],g[0->b][1->b]), 
145           (w,2,r[x->0][x->1],g[0->b][1->c])}
146
147     11. A man^x entered.  He_x sat.  He_x spoke.
148     12. He_x sat.  A man^x entered.  He_x spoke.
149
150 consider: new peg requires object not in the domain of the assignment fn
151
152     13. If a woman entered, she sat.
153
154 ## Interactions of binding with modality
155
156     (∃x.enter(x)) and (sit(x)) ≡ ∃x (enter(x) and sit(x))
157
158 but (∃x.closet(x)) and (◊guilty(x)) ≡/≡ ∃x (closet(x) and ◊guilty(x))
159
160     The Broken Vase:
161     There are three sons, Bob, Carl, and Dave.  
162     One of them broke a vase.  
163     Bob is known to be innocent.  
164     Someone is hiding in the closet.
165
166
167         in closet        guilty 
168         ---------------  ---------------
169     w:  b  false         b  false
170         c  false         c  false
171         d  true          d  true
172
173     w': b  false         b  false
174         c  true          c  false
175         d  false         d  true
176
177 GSV observe that (∃x.closet(x)) and (◊guilty(x)) is true if there is
178 at least one possibility in which a person in the closet is guilty.
179 In this scenario, world w is the verifying world.  It remains possible
180 that there are closet hiders who are not guilty in any world.  Carl
181 fits this bill: he's in the closet in world w', but he is not guilty
182 in any world.
183
184     14. Someone^x is in the closet.  He_x might be guilty.
185
186          {(w,0,r,g), (w',0,r,g}[∃x.closet(x)][◊guilty(x)]
187
188          -- existential introduces new peg
189
190        = (   {(w,1,r[x->0],g[0->b])}[closet(x)]
191           ++ {(w,1,r[x->0],g[0->c])}[closet(x)]
192           ++ {(w,1,r[x->0],g[0->d])}[closet(x)]
193           ++ {(w',1,r[x->0],g[0->b])}[closet(x)]
194           ++ {(w',1,r[x->0],g[0->c])}[closet(x)]
195           ++ {(w',1,r[x->0],g[0->d])}[closet(x)])[◊guilty(x)]
196
197          -- only possibilities in which x is in the closet survive
198
199        = {(w,1,r[x->0],g[0->d]),
200           (w',1,r[x->0],g[0->c])}[◊guilty(x)]
201
202          -- Is there any possibility in which x is guilty?
203          -- yes: for x = Dave, in world w Dave broke the vase
204
205        = {(w,1,r[x->0],g[0->d]),
206           (w',1,r[x->0],g[0->c])}
207
208 Now we consider the second half:
209
210     14. Someone^x is in the closet who_x might be guilty.
211
212          {(w,0,r,g), (w',0,r,g)}[∃x(closet(x) & ◊guilty(x))]
213        
214          -- existential introduces new peg
215
216        =    {(w,1,r[x->0],g[0->b])}[closet(x)][◊guilty(x)]
217          ++ {(w,1,r[x->0],g[0->c])}[closet(x)][◊guilty(x)]
218          ++ {(w,1,r[x->0],g[0->d])}[closet(x)][◊guilty(x)]
219          ++ {(w',1,r[x->0],g[0->b])}[closet(x)][◊guilty(x)]
220          ++ {(w',1,r[x->0],g[0->c])}[closet(x)][◊guilty(x)]
221          ++ {(w',1,r[x->0],g[0->d])}[closet(x)][◊guilty(x)]
222
223           -- filter out possibilities in which x is not in the closet
224           -- and filter out possibilities in which x is not guilty
225           -- the only person who was guilty in the closet was Dave in
226           -- world 1
227
228        = {(w,1,r[x->0],g[0->d])}
229
230 The result is different, and more informative.  
231
232 ## Binding, modality, and identity
233
234 The fragment correctly predicts the following contrast:
235
236     15. Someone^x entered.  He_x might be Bob.  He_x might not be Bob.
237         (∃x.enter(x)) & ◊x=b & ◊not(x=b)
238         -- This discourse requires a possibility in which Bob entered
239         -- and another possibility in which someone who is not Bob entered
240
241     16. Someone^x entered who might be Bob and who might not be Bob.
242         ∃x (enter(x) & ◊x=b & ◊not(x=b))
243         -- This is a contradition: there is no single person who might be Bob
244         -- and who simultaneously might be someone else
245
246 ### Identifiers
247
248 Let α be a term which differs from x.  Then α is an identifier if the
249 following formula is supported by every information state:
250
251     ∀x(◊(x=α) --> (x=α))
252
253 The idea is that α is an identifier just in case there is only one
254 object that it can refer to.  Here is what GSV say:
255
256     A term is an identifier per se if no mattter what the information
257     state is, it cannot fail to decie what the denotation of the term is.
258
259 ## Why have a two-part assignment function?
260
261 In the current system, variables are associated with values in two
262 steps.
263
264     Variables        Pegs         Entities
265     ---------   r    ----    g    --------   
266        x       -->    0     -->      a
267        y       -->    1     -->      b
268        z       -->    2     -->      c
269
270 Here, r is a refsys mapping variables to pegs, and g is an assignment function mapping pegs to entities