(no commit message)
[lambda.git] / topics / _week10_gsv.mdwn
1 <!-- λ ◊ ≠ ∃ Λ ∀ ≡ α β γ ρ ω φ ψ Ω ○ μ η δ ζ ξ ⋆ ★ • ∙ ● ⚫ 𝟎 𝟏 𝟐 𝟘 𝟙 𝟚 𝟬 𝟭 𝟮 ⇧ (U+2e17) ¢ -->
2
3 [[!toc levels=2]]
4
5 # Doing things with monads
6
7 ## Extended application: Groenendijk, Stokhof and Veltman's *Coreference and Modality*
8
9 GSV are interested in developing and establishing a reasonable theory
10 of discourse update.  One way of looking at this paper is like this:
11
12   GSV = GS + V, where
13         
14   GS = Dynamic theories of binding of Groenendijk and Stokhof, e.g.,
15        Dynamic Predicate Logic L&P 1991: dynamic binding, donkey anaphora
16        Dynamic Montague Grammar 1990: generalized quantifiers, discourse referents
17
18   V = a dynamic theory of epistemic modality, e.g., 
19       Veltman, Frank. "Data semantics." 
20       In Truth, Interpretation and Information, Foris, Dordrecht (1984): 43-63.
21
22 That is, Groenendijk and Stokhof have a well-known theory of dynamic
23 semantics, and Veltman has a well-known theory of epistemic modality,
24 and this fragment brings both of those strands together into a single
25 system.  
26
27 We will be interested in this paper both from a theoretical point of
28 view and from a practical engineering point of view.  On the
29 theoretical level, these scholars are proposing a strategy for
30 managing the connection between variables and the objects they
31 designate in way that is flexible enough to be useful for describing
32 natural language.  
33
34 ## Basics of GSV's fragment
35
36 The fragment in this paper is unusually elegant.  We'll present it on
37 its own terms, with the exception that we will not use pegs.  See the
38 digression below concerning pegs for an explanation.  After presenting
39 the paper, we'll re-engineering the fragment using explicit monads.
40
41 In this fragment, points of evaluation are not just worlds, but a pair
42 of a world and an assginment function.  This is familiar from Heim's
43 1983 File Change Semantics.  We'll follow GSV and call a
44 world-assignment pair a "possibility".  Then a context is a set (an
45 "information state") is a set of possiblities.  Infostates
46 simultaneously track both information about the world (which possible
47 worlds are live possibilities?) as well as information about the
48 discourse (which objects to the variables refer to?).
49
50 Worlds in general settle all matters of fact in the world.  In
51 particular, they determine the extensions of predicates and relations.
52
53 The formal language the fragment interprets is Predicate Calculus with
54 equality, existential and universal quantification, along with one
55 unary modality (box and diamond, corresponding to epistemic necessity
56 and epistemic possibility).
57
58 An implementation in OCaml is available [[here|code/gsv.ml]]; consult
59 that code for details of syntax, types, and values.
60
61 Terms in this language are either individuals such as Alice or Bob, or
62 else variables.  So in general, the referent of a term can depend on a
63 possibility:
64
65     ref(i, t) = t if t is an individual, and 
66                 g(t) if t is a variable, where i = (w,g)
67
68 Here are the main clauses for update (their definition 3.1).  
69
70 Following GSV, we'll write `update(s, φ)` (the update of information
71 state `s` with the information in φ) as `s[φ]`.
72
73     s[P(t)] = {i in s | w(P)(ref(i,t))}
74
75 So `man(x)` is the set of live possibilities `i = (w,g)` in s such that
76 the set of men in `w` given by `w(man)` maps the object referred to by
77 `x`, namely, `g("x")`, to `true`.   That is, update with "man(x)"
78 discards all possibilities in which "x" fails to refer to a man.
79
80     s[t1 = t2] = {i in s | ref(i,t1) == ref(i,t2)}
81
82     s[φ and ψ] = s[φ][ψ]
83
84 When updating with a conjunction, first update with the left conjunct,
85 then update with the right conjunct.
86
87 Existential quantification is somewhat intricate.
88
89     s[∃xφ] = Union {{(w, g[x->a]) | (w,g) in s}[φ] | a in ent} 
90
91 Here's the recipe: given a starting infostate s, choose an object a
92 from the domain of discourse.  Construct a modified infostate s' by
93 adjusting the assignment function of each possibility so as to map the variable x to a.
94 Then update s' with φ.  Finally, take the union over the results of
95 doing this for every object a in the domain of discourse.
96
97 Negation is natural enough:
98
99     s[neg φ] =  {i | {i}[φ] = {}}
100
101 If updating φ with the information state that contains only the
102 possibility i returns the empty information state, then not φ is true
103 with respect to i.
104
105 In GSV, disjunction, the conditional, and the universals are defined
106 in terms of negation and the other connectives (see fact 3.2).
107
108 Exercise: assume that there are three entities in the domain of
109 discourse, Alice, Bob, and Carl.  Assume that Alice is a woman, and
110 Bob and Carl are men.
111
112 Compute the following:
113
114     1. {(w,g)}[∃x.man(x)]
115
116        = {(w,g[n->a])}[man(x)] ++ {(w,g[n->b])}[man(x)] 
117                                ++ {(w,g[n->c])}[man(x)] 
118        = {} ++ {(w,g[n->b])} ++ {(w,g[n->c])}
119        = {(w,g[n->a]),(w,g[n->b]),(w,g[n->c])}
120        -- Bob and Carl are men
121
122     2. {(w,g)}[∃x.woman(x)]
123     3. {(w,g)}[∃x∃y.man(x) and man(y)]
124     4. {(w,n,r,g)}[∃x∃y.x=y]
125
126 Running the [[code|code/gsv.ml]] gives the answers.
127
128
129 ## Order and modality
130
131 The final remaining update rule concerns modality:
132
133     s[◊φ] = {i in s | s[φ] ≠ {}}
134
135 This is a peculiar rule: a possibility `i` will survive update just in
136 case something is true of the information state `s` as a whole.  That
137 means that either every `i` in `s` will survive, or none of them will.
138 The criterion is that updating `s` with the information in the
139 prejacent φ does not produce the contradictory information state
140 (i.e., `{}`).
141
142 So let's explore what this means.  GSV offer a contrast between two
143 discourses that differ only in the order in which the updates occur.
144 The fact that the predictions of the fragment differ depending on
145 order shows that the system is order-sensitive.
146
147     1. Alice isn't hungry.  #Alice might be hungry.
148
149 According to GSV, the combination of these sentences in this order is
150 `inconsistent', and they mark the second sentence with the star of
151 ungrammaticality.  We'll say instead that the discourse is
152 gramamtical, leave the exact way to think about its intuitive status
153 up for grabs.  What is important for our purposes is to get clear on
154 how the fragment behaves with respect to these sentences.
155
156 We'll start with an infostate containing two possibilities.  In one
157 possibility, Alice is hungry (call this possibility "hungry"); in the
158 other, she is not (call it "full").
159
160       {hungry, full}[Alice isn't hungry][Alice might be hungry]
161     = {full}[Alice might be hungry]
162     = {}
163
164 As usual in dynamic theories, a sequence of sentences is treated as if
165 the sentence were conjoined.  This is the same thing as updating with
166 the first sentence, then updating with the second sentence.
167 Update with *Alice isn't hungry* eliminates the possibility in which
168 Alice is hungry, leaving only the possibility in which she is full.
169 Subsequent update with *Alice might be hungry* depends on the result
170 of updating with the prejacent, *Alice is hungry*.  Let's do that side
171 calculation:
172
173       {full}[Alice is hungry]
174     = {}
175
176 Because the only possibility in the information state is one in which
177 Alice is not hungry, update with *Alice is hungry* results in an empty
178 information state.  That means that update with *Alice might be
179 hungry* will also be empty, as indicated above.
180
181 In order for update with *Alice might be hungry* to be non-empty,
182 there must be at least one possibility in the input state in which
183 Alice is hungry.  That is what epistemic might means in this fragment:
184 the prejacent must be possible.  But update with *Alice isn't hungry*
185 eliminates all possibilities in which Alice is hungry.  So the
186 prediction of the fragment is that update with the sequence in (1)
187 will always produce an empty information state.
188
189 In contrast, consider the sentences in the opposite order:
190
191     2. Alice might be hungry.  Alice isn't hungry.
192
193 We'll start with the same two possibilities.
194
195     = {hungry, full}[Alice might be hungry][Alice isn't hungry]
196     = {hungry, full}[Alice isn't hungry]
197     = {full}
198
199 GSV comment that a single speaker couldn't possibly be in a position
200 to utter the discourse in (2).  The reason is that in order for the
201 speaker to appropriately assert that Alice isn't hungry, that speaker
202 would have to possess knowledge (or sufficient justification,
203 depending on your theory of the norms for assertion) that Alice isn't
204 hungry.  But if they know that Alice isn't hungry, they couldn't
205 appropriately assert *Alice might be hungry*, based on the predictions
206 of the fragment.  
207
208 Another view is that it can be acceptable to assert a sentence if it
209 is supported by the information in the common ground.  So if the
210 speaker assumes that as far as the listener knows, Alice might be
211 hungry, they can utter the discourse in (2).  Here's a variant that
212 makes this thought more vivid:
213
214     3. Based on public evidence, Alice might be hungry.  
215        But in fact I have private knowledge that she's not hungry.
216
217 The main point to appreciate here is that the update behavior of the
218 discourses depends on the order in which the updates due to the
219 individual sentence occur.  
220
221 Note, incidentally, that there is an asymmetry in the fragment
222 concerning negation.
223
224     4. Alice might be hungry.  Alice *is* hungry.
225     5. Alice is hungry.  (So of course) Alice might be hungry.
226
227 Both of these discourses lead to the same update effect: all and only
228 those possibilites in which Alice is hungry survive.  You might think
229 that asserting *might* requires that the prejacent be not only
230 possible, but undecided.  If you like this idea, you can easily write
231 an update rule for the diamond on which update with the prejacent and
232 its negation must both be non-empty.
233
234 ## Order and binding
235
236 The GSV fragment differs from the DPL and the DMG dynamic semantics in
237 important details.  Nevertheless, it says something highly similar to
238 DPL about anaphora, binding, quantificational binding, and donkey
239 anaphora (at least, when modality is absent, as we'll discuss below).
240
241 In particular, continuing the theme of order-based asymmetries,
242
243     6. A man^x entered.  He_x sat.
244     7. He_x sat.  A man^x entered.
245
246 These discourses differ only in the order of the sentences.  Yet the
247 first allows for coreference between the indefinite and the pronoun,
248 where the second discourse does not.  In order to demonstrate, we'll
249 need an information state whose refsys is defined for at least one
250 variable.
251
252     8. {(w,g[x->b])}
253
254 This infostate contains a refsys and an assignment that maps the
255 variable x to Bob.  Here are the facts in world w:
256
257     extension w "enter" a = false
258     extension w "enter" b = true
259     extension w "enter" c = true
260
261     extension w "sit" a = true
262     extension w "sit" b = true
263     extension w "sit" c = false
264
265 We can now consider the discourses in (6) and (7) (after magically
266 converting them to the Predicate Calculus):
267
268     9. Someone^x entered.  He_x sat.  
269
270          {(w,g[x->b])}[∃x.enter(x)][sit(x)]
271
272        = (   {(w,g[x->b][x->a])}[enter(x)]
273           ++ {(w,g[x->b][x->b])}[enter(x)]
274           ++ {(w,g[x->b][x->c])}[enter(x)])[sit(x)]
275
276           -- "enter(x)" filters out the possibility in which x refers
277           -- to Alice, since Alice didn't enter
278
279        = (   {}
280           ++ {(w,g[x->b][x->b])}
281           ++ {(w,g[x->b][x->c])})[sit(x)]
282
283           -- "sit(x)" filters out the possibility in which x refers
284           -- to Carl, since Carl didn't sit
285
286        =  {(w,g[x->b][x->b])}
287
288 One of the key facts here is that even though the existential has
289 scope only over the first sentence, in effect it binds the pronoun in
290 the following clause.  This is characteristic of dynamic theories in
291 the style of Groenendijk and Stokhof, including DPL and DMG. 
292
293 The outcome is different if the order of the sentences is reversed.
294
295     10. He_x sat.  Someone^x entered. 
296
297          {(w,g[x->b])}[sit(x)][∃x.enter(x)]
298
299          -- evaluating `sit(x)` rules out nothing, since (coincidentally)
300          -- x refers to Bob, and Bob is a sitter
301
302        = {(w,g[x->b])}[∃x.enter(x)]
303
304          -- Just as before, the existential adds a new peg and assigns
305          -- it to each object
306
307        =    {(w,g[x->b][x->a])}[enter(x)]
308          ++ {(w,g[x->b][x->b])}[enter(x)]
309          ++ {(w,g[x->b][x->c])}[enter(x)]
310
311          -- enter(x) eliminates all those possibilities in which x did
312          -- not enter
313
314        = {} ++ {(w,g[x->b][x->b])}
315             ++ {(w,g[x->b][x->c])}
316
317        = {(w,g[x->b][x->b]), (w,g[x->b][x->c])}
318
319 The result is different than before.  Before, there was only one
320 possibility: that x refered to the only person who both entered and
321 sat.  Here, there remain two possibilities: that x refers to Bob, or
322 that x refers to Carl.  This makes predictions about the
323 interpretation of continuations of the dialogs:
324
325     11. A man^x entered.  He_x sat.  He_x spoke.
326     12. He_x sat.  A man^x entered.  He_x spoke.
327
328 The construal of (11) as marked entails that the person who spoke also
329 entered and sat.  The construal of (12) guarantees only that the
330 person who spoke also entered.  There is no guarantee that the person
331 who spoke sat.  
332
333 Intuitively, there is a strong impression in (12) that the person who
334 entered and spoke not only should not be identified as the person who
335 sat, he should be different from the person who sat.  Some dynamic
336 systems, such as Heim's File Change Semantics, guarantee non-identity.
337 That is not guaranteed by the GSV fragment.  If you wanted to add this
338 as a refinement to the fragment, you could require that the
339 existential only considers object in the domain that are not in the
340 range of the starting assignment function.
341
342 As usual with dynamic semantics, a point of pride is the ability to
343 give a good account of donkey anaphora, as in
344
345     13. If a woman entered, she sat.
346
347 See the paper for details.
348
349 ## Interactions of binding with modality
350
351 At this point, we have a fragment that handles modality, and that
352 handles indefinites and pronouns.  It it only interesting to combine
353 these two elements if they interact in non-trivial ways.  This is
354 exactly what GSV argue.
355
356 The discussion of indefinites in the previous section established the
357 following dynamic equivalence:
358
359     (∃x.enter(x)) and (sit(x)) ≡ ∃x (enter(x) and sit(x))
360
361 In words, existentials take effective scope over subsequent clauses.
362
363 The presence of modal possibility, however, disrupts this
364 generalization.  GSV illustrate this with the following story.
365
366     The Broken Vase:
367     There are three children: Alice, Bob, and Carl.
368     One of them broke a vase.  
369     Alice is known to be innocent.  
370     Someone is hiding in the closet.
371
372     (∃x.closet(x)) and (◊guilty(x)) ≡/≡ ∃x (closet(x) and ◊guilty(x))
373
374 To see this, we'll start with the left hand side.  We'll need at least
375 two worlds.
376
377         in closet        guilty 
378         ---------------  ---------------
379     w:  a  true          a  false
380         b  false         b  true
381         c  true          c  false
382
383     w': a  false         a  false
384         b  false         b  false
385         c  true          c  true
386
387 GSV say that (∃x.closet(x)) and (◊guilty(x)) is true if there is at
388 least one possibility in which a person in the closet is guilty.  In
389 this scenario, world w' is the verifying world: Carl is in the closet,
390 and he's guilty.  It remains possible that there are closet hiders who
391 are not guilty in any world.  Alice fits this bill: she's in the
392 closet in world w', but she is not guilty in any world.
393
394 Let's see how this works out in detail.
395
396     14. Someone^x is in the closet.  He_x might be guilty.
397
398          {(w,g), (w',g}[∃x.closet(x)][◊guilty(x)]
399
400          -- existential introduces new peg
401
402        = (   {(w,g[x->a])}[closet(x)]
403           ++ {(w,g[x->b])}[closet(x)]
404           ++ {(w,g[x->c])}[closet(x)]
405           ++ {(w',g[x->a])}[closet(x)]
406           ++ {(w',g[x->b])}[closet(x)]
407           ++ {(w',g[x->c])}[closet(x)])[◊guilty(x)]
408
409          -- only possibilities in which x is in the closet survive
410          -- the first update
411
412        = {(w,g[x->a]), (w',g[x->c])}[◊guilty(x)]
413
414          -- Is there any possibility in which x is guilty?
415          -- yes: for x = Carl, in world w' Carl broke the vase
416          -- that's enough for the possiblity modal to allow the entire
417          -- infostate to pass through unmodified.
418
419        = {(w,g[x->a]),(w',g[x->c])}
420
421 Now we consider the second half:
422
423     15. Someone^x is in the closet who_x might be guilty.
424
425          {(w,g), (w',g)}[∃x(closet(x) & ◊guilty(x))]
426        
427        =    {(w,g[x->a])}[closet(x)][◊guilty(x)]
428          ++ {(w,g[x->b])}[closet(x)][◊guilty(x)]
429          ++ {(w,g[x->c])}[closet(x)][◊guilty(x)]
430          ++ {(w',g[x->a])}[closet(x)][◊guilty(x)]
431          ++ {(w',g[x->b])}[closet(x)][◊guilty(x)]
432          ++ {(w',g[x->c])}[closet(x)][◊guilty(x)]
433
434           -- filter out possibilities in which x is not in the closet
435           -- and filter out possibilities in which x is not guilty
436           -- the only person who was guilty in the closet was Carl in
437           -- world w'
438
439        = {(w',g[x->c])}
440
441 The result is different.  Fewer possibilities remain.
442 We have elminated both possible worlds and possible discourses.
443 So the second formula is more informative.
444
445 As we discovered in class, there is considerable work to be done to
446 decide which expressions in natural language (if any) are capable of
447 expressing which of the two translations into the GSV fragment.  We
448 can certainly grasp the truth conditions, but that is not the same
449 thing as discovering that there are natural language sentences that
450 express one or the other or both.
451
452
453 ## Binding, modality, and identity
454
455 The fragment correctly predicts the following contrast:
456
457     16. Someone^x entered.  He_x might be Bob.  He_x might not be Bob.
458         (∃x.enter(x)) & ◊x=b & ◊not(x=b)
459         -- This discourse requires a possibility in which Bob entered
460         -- and another possibility in which someone who is not Bob entered
461
462     17. Someone^x entered who might be Bob and who might not be Bob.
463         ∃x (enter(x) & ◊x=b & ◊not(x=b))
464         -- This is a contradition: there is no single person who might be Bob
465         -- and who simultaneously might be someone else
466
467 These formulas are expressing extensional, de-reish intuitions.  If we
468 add individual concepts to the fragment, the ability to express
469 fancier claims would come along.
470
471 ## GSV's "Identifiers"
472
473 Let α be a term which differs from x.  Then α is an identifier if the
474 following formula is supported by every information state:
475
476     ∀x(◊(x=α) --> (x=α))
477
478 The idea is that α is an identifier just in case there is only one
479 object that it can refer to.  Here is what GSV say:
480
481     A term is an identifier per se if no mattter what the information
482     state is, it cannot fail to decie what the denotation of the term is.
483
484 ## Digression on pegs
485
486 One of the more salient aspects of the technical part of the paper is
487 that GSV insert an extra level in between the variable and the object:
488 instead of having an assignment function that maps variables directly
489 onto objects, GSV provide *pegs*: variables map onto pegs, and pegs
490 map onto objects.  It happens that pegs play no role in the paper
491 whatsoever.  We'll demonstrate this by providing a faithful
492 implementation of the paper that does not use pegs at all.
493
494 Nevertheless, it makes sense to pause here to discuss pegs briefly,
495 since this technique is highly relevant to one of the main
496 applications of the course, namely, reference and coreference.
497
498 What are pegs?  The term harks back to a 1986 paper by Fred Landman
499 called `Pegs and Alecs'.  Pegs are simply hooks for hanging properties
500 on.  Pegs are supposed to be as anonymous as possible.  Think of
501 hanging your coat on a physical peg: you don't care which peg it is,
502 only that there are enough pegs for everyone's coat to hang from.
503 Likewise, for the pegs of GSV, all that matters is that there are
504 enough of them.  (Incidentally, there is nothing in Gronendijk and
505 Stokhof's original DPL paper that corresponds naturally to pegs; but
506 in their Dynamic Montague Grammar paper, pegs serve a purpose similar
507 to discourse referents there, though the connection is not simple.)
508
509 Pegs can be highly useful for exploring puzzles of reference and
510 coreference.
511
512     Standard assignment function    System with Pegs (drefs)
513     ----------------------------    ------------------------
514      Variable      Object           Var      Peg      Object
515     ---------      -------          ---      ---      ------
516         x     -->    a               x   -->  0   -->   a
517         y     -/                     y   -/   
518         z     -->    b               z   -->  1   -->   a
519
520 A standard assignment function can map two different variables onto
521 the same object.  In the diagram, x and y are both mapped onto the
522 object a.  With discourse referents in view, we can have two different
523 flavors of coreference.  Just as with ordinary assignment functions,
524 variables can be mapped onto pegs (discourse referents) that are in
525 turn mapped onto the same object.  In the diagram, x is mapped onto
526 the peg 0, which in turn is mapped onto the object a, and z is mapped
527 onto a discourse referent that is mapped onto a.  On a deeper level,
528 we can suppose that y is mapped onto the same discourse referent as
529 x.  With a system like this, we are free to reassign the discourse
530 referent associated with z to a different object, in which case x and
531 z will no longer refer to the same object.  But there is no way to
532 change the object associated with x without necessarily changing the
533 object associated with y.  They are coreferent in a deeper, less
534 accidental sense.  
535
536 GSV could make use of this expressive power.  But they don't.  In
537 fact, their system is careful designed to guarantee that every
538 variable is assigned a discourse referent distinct from all previous
539 discourse referents.
540
541 End of digression on pegs.
542