e971fe93d15b8f09cde4cbc48000b82cb214a569
1 <!-- λ ∃ Λ ∀ ≡ α β γ ρ ω φ ψ Ω ○ μ η δ ζ ξ ⋆ ★ • ∙ ● ⚫ 𝟎 𝟏 𝟐 𝟘 𝟙 𝟚 𝟬 𝟭 𝟮 ⇧ (U+2e17) ¢ -->
3 [[!toc levels=2]]
5 # Doing things with monads
7 ## Extended application: Groenendijk, Stokhof and Veltman's *Coreference and Modality*
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:
12   GSV = GS + V
14 That is, Groenendijk and Stokhof have a well-known theory of dynamic
15 semantics, and Veltman has a well-known theory of epistemic modality,
16 and this fragment brings both of those strands together into a single
17 system.
19 We will be interested in this paper both from a theoretical point of
20 view and from a practical engineering point of view.  On the
21 theoretical level, these scholars are proposing a strategy for
22 managing the connection between variables and the objects they
23 designate in way that is flexible enough to be useful for describing
24 natural language.  The main way they attempt to do this is by
25 inserting an extra level in between the variable and the object:
26 instead of having an assignment function that maps variables directly
27 onto objects, GSV provide *pegs*: variables map onto pegs, and pegs
28 map onto objects.  We'll discuss in considerable detail what pegs
29 allow us to do, since it is highly relevant to one of the main
30 applications of the course, namely, reference and coreference.
32 What are pegs?  The term harks back to a paper by Landman called `Pegs
33 and Alecs'.  There pegs are simply hooks for hanging properties on.
34 Pegs are supposed to be as anonymous as possible.  Think of hanging
35 your coat on a physical peg: you don't care which peg it is, only that
36 there are enough pegs for everyone's coat to hang from.  Likewise, for
37 the pegs of GSV, all that matters is that there are enough of them.
38 (Incidentally, there is nothing in Gronendijk and Stokhof's original
39 DPL paper that corresponds naturally to pegs; but in their Dynamic
40 Montague Grammar paper, pegs serve a purpose similar to discourse
41 referents there, though the connection is not simple.)
43 On an engineering level, the fact that GSV are combining anaphora and
44 bound quantification with epistemic quantification means that they are
45 gluing together related but distinct subsystems into a single
46 fragment.  These subsystems naturally cleave into separate layers in a
47 way that is obscured in the paper.  We will argue in detail that
48 re-engineering GSV using monads will lead to a cleaner system that
49 does all of the same theoretical work.
51 Empirical targets: on the anaphoric side, GSV want to
53 On the epistemic side, GSV aim to account for asymmetries such as
55     It might be raining.  It's not raining.
56     #It's not raining.  It might be raining.
58 ## Basics
60 There are a lot of formal details in the paper in advance of the
61 empirical discussion.  Here are the ones that matter:
63     type var = string
64     type peg = int
65     type refsys = var -> peg
66     type ent = Alice | Bob | Carl
67     type assignment = peg -> ent
69 So in order to get from a variable to an object, we have to compose a
70 refsys `r` with an assignment `g`.  For instance, we might have
71 r (g ("x")) = Alice.
73     type pred = string
74     type world = pred -> ent -> bool
75     type pegcount = int
76     type poss = world * pegcount * refsys * assignment
77     type infostate = [poss]
79 Worlds in general settle all matters of fact in the world.  In
80 particular, they determine the extensions of predicates and relations.
81 In this discussion, we'll (crudely) approximate worlds by making them
82 a function from predicates such as "man" to a function mapping each
83 entity to a boolean.
85 As we'll see, indefinites as a side effect increase the number of pegs
86 by one.  GSV assume that we can determine what integer the next unused
87 peg corresponds to by examining the range of the refsys function.
88 We'll make things easy on ourselves by simply tracking the total
89 number of used pegs in a counter called `pegcount`.
91 So information states track both facts about the world (e.g., which
92 objects count as a man), and facts about the discourse (e.g., how many
93 pegs have been used).
95 The formal language the fragment interprets is Predicate Calculus with
96 equality, existential and universal quantification, and one unary
97 modality (box and diamond, corresponding to epistemic necessity and
98 epistemic possibility).
100 Terms in this language are either individuals such as Alice or Bob, or
101 else variables.  So in general, the referent of a term can depend on a
102 possibility:
104     ref(i, t) = t if t is an individual, and
105                 g(r(t)) if t is a variable, where i = (w,n,r,g)
107 Here are the main clauses for update (their definition 3.1).
109 Following GSV, we'll write `update(s, φ)` (the update of information
110 state `s` with the information in φ) as `s[φ]`.
112     s[P(t)] = {i in s | w(P)(ref(i,t))}
114 So `man(x)` is the set of live possibilities `i = (w,r,g)` in s such that
115 the set of men in `w` given by `w(man)` maps the object referred to by
116 `x`, namely, `r(g("x"))`, to `true`.   That is, update with "man(x)"
117 discards all possibilities in which "x" fails to refer to a man.
119     s[t1 = t2] = {i in s | ref(i,t1) = ref(i,t2)}
121     s[φ and ψ] = s[φ][ψ]
123 When updating with a conjunction, first update with the left conjunct,
124 then update with the right conjunct.
126 Existential quantification requires adding a new peg to the set of
127 discourse referents.
129     s[∃xφ] = {(w, n+1, r[x->n], g[n->a]) | (w,n,r,g) in s and a in ent}[φ]
131 Here's the recipe: for every possibility (w,n,r,g) in s, and for every
132 entity a in the domain of discourse, construct a new possibility with
133 the same world w, an incrementd peg count n+1, and a new r and g
134 adjusted in such a way that the variable x refers to the object a.
136 Note that this recipe does not examine φ.  This means that this
137 analysis treats the formula prefix `∃x` as if it were a meaningful
138 constituent independent of φ.
140 Negation is natural enough:
142     s[neg φ] =  {i | {i}[φ] = {}}
144 If updating φ with the information state that contains only the
145 possibility i returns the empty information state, then not φ is true
146 with respect to i.
148 In GSV, disjunction, the conditional, and the universals are defined
149 in terms of negation and the other connectives.
151 Exercise: assume that there are two entities in the domain of
152 discourse, Alice and Bob.  Assume that Alice is a woman, and Bob is a
153 man.  Show the following computations, where `i = (w,n,r,g)`:
155     1. {i}[∃x.person(x)]
157        = {(w,n+1,r[x->n],g[n->a]),(w,n+1,r[x->n],g[n->b])}[person(x)]
158        = {(w,n+1,r[x->n],g[n->a]),(w,n+1,r[x->n],g[n->b])}
160     2. {i}[∃x.man(x)]
162        = {(w,n+1,r[x->n],g[n->a]),(w,n+1,r[x->n],g[n->b])}[person(x)]
163        = {(w,n+1,r[x->n],g[n->b])}
166     3. {i}[∃x∃y.person(x) and person(y)]
168        = {(w,n+1,r[x->n],g[n->a]),(w,n+1,r[x->n],g[n->b])}[∃y.person(x) and person(y)]
169        = {(w, n+2, r[x->n][y->n+1], g[n->a][n+1->a]),
170           (w, n+2, r[x->n][y->n+1], g[n->a][n+1->b]),
171           (w, n+2, r[x->n][y->n+1], g[n->b][n+1->a]),
172           (w, n+2, r[x->n][y->n+1], g[n->b][n+1->b])
173          }[person(x) and person(y)]
174        = {(w, n+2, r[x->n][y->n+1], g[n->a][n+1->a]),
175           (w, n+2, r[x->n][y->n+1], g[n->a][n+1->b]),
176           (w, n+2, r[x->n][y->n+1], g[n->b][n+1->a]),
177           (w, n+2, r[x->n][y->n+1], g[n->b][n+1->b])
178          }
180     4. {i}[∃x∃y.x=x]
182        = {(w, n+2, r[x->n][y->n+1], g[n->a][n+1->a]),
183           (w, n+2, r[x->n][y->n+1], g[n->a][n+1->b]),
184           (w, n+2, r[x->n][y->n+1], g[n->b][n+1->a]),
185           (w, n+2, r[x->n][y->n+1], g[n->b][n+1->b])
186          }[∃x∃y.x=x]
187        = {(w, n+2, r[x->n][y->n+1], g[n->a][n+1->a]),
188           (w, n+2, r[x->n][y->n+1], g[n->a][n+1->b]),
189           (w, n+2, r[x->n][y->n+1], g[n->b][n+1->a]),
190           (w, n+2, r[x->n][y->n+1], g[n->b][n+1->b])
191          }
193     5. {i}[∃x∃y.x=y]
195        = {(w, n+2, r[x->n][y->n+1], g[n->a][n+1->a]),
196           (w, n+2, r[x->n][y->n+1], g[n->a][n+1->b]),
197           (w, n+2, r[x->n][y->n+1], g[n->b][n+1->a]),
198           (w, n+2, r[x->n][y->n+1], g[n->b][n+1->b])
199          }[∃x∃y.x=y]
200        = {(w, n+2, r[x->n][y->n+1], g[n->a][n+1->a]),
201           (w, n+2, r[x->n][y->n+1], g[n->b][n+1->b])
202          }