--- /dev/null
+<!-- λ ∃ Λ ∀ ≡ α β γ ρ ω φ ψ Ω ○ μ η δ ζ ξ ⋆ ★ • ∙ ● ⚫ 𝟎 𝟏 𝟐 𝟘 𝟙 𝟚 𝟬 𝟭 𝟮 ⇧ (U+2e17) ¢ -->
+
+[[!toc levels=2]]
+
+# Doing things with monads
+
+## Extended application: Groenendijk, Stokhof and Veltman's *Coreference and Modality*
+
+GSV are interested in developing and establishing a reasonable theory
+of discourse update. One way of looking at this paper is like this:
+
+ GSV = GS + V
+
+That is, Groenendijk and Stokhof have a well-known theory of dynamic
+semantics, and Veltman has a well-known theory of epistemic modality,
+and this fragment brings both of those strands together into a single
+system.
+
+We will be interested in this paper both from a theoretical point of
+view and from a practical engineering point of view. On the
+theoretical level, these scholars are proposing a strategy for
+managing the connection between variables and the objects they
+designate in way that is flexible enough to be useful for describing
+natural language. The main way they attempt to do this is by
+inserting an extra level in between the variable and the object:
+instead of having an assignment function that maps variables directly
+onto objects, GSV provide *pegs*: variables map onto pegs, and pegs
+map onto objects. We'll discuss in considerable detail what pegs
+allow us to do, since it is highly relevant to one of the main
+applications of the course, namely, reference and coreference.
+
+What are pegs? The term harks back to a paper by Landman called `Pegs
+and Alecs'. There pegs are simply hooks for hanging properties on.
+Pegs are supposed to be as anonymous as possible. Think of hanging
+your coat on a physical peg: you don't care which peg it is, only that
+there are enough pegs for everyone's coat to hang from. Likewise, for
+the pegs of GSV, all that matters is that there are enough of them.
+(Incidentally, there is nothing in Gronendijk and Stokhof's original
+DPL paper that corresponds naturally to pegs; but in their Dynamic
+Montague Grammar paper, pegs serve a purpose similar to discourse
+referents there, though the connection is not simple.)
+
+On an engineering level, the fact that GSV are combining anaphora and
+bound quantification with epistemic quantification means that they are
+gluing together related but distinct subsystems into a single
+fragment. These subsystems naturally cleave into separate layers in a
+way that is obscured in the paper. We will argue in detail that
+re-engineering GSV using monads will lead to a cleaner system that
+does all of the same theoretical work.
+
+Empirical targets: on the anaphoric side, GSV want to
+
+On the epistemic side, GSV aim to account for asymmetries such as
+
+ It might be raining. It's not raining.
+ #It's not raining. It might be raining.
+
+## Basics
+
+There are a lot of formal details in the paper in advance of the
+empirical discussion. Here are the ones that matter:
+
+ type var = string
+ type peg = int
+ type refsys = var -> peg
+ type ent = Alice | Bob | Carl
+ type assignment = peg -> ent
+
+So in order to get from a variable to an object, we have to compose a
+refsys `r` with an assignment `g`. For instance, we might have
+r (g ("x")) = Alice.
+
+ type pred = string
+ type world = pred -> ent -> bool
+ type pegcount = int
+ type poss = world * pegcount * refsys * assignment
+ type infostate = [poss]
+
+Worlds in general settle all matters of fact in the world. In
+particular, they determine the extensions of predicates and relations.
+In this discussion, we'll (crudely) approximate worlds by making them
+a function from predicates such as "man" to a function mapping each
+entity to a boolean.
+
+As we'll see, indefinites as a side effect increase the number of pegs
+by one. GSV assume that we can determine what integer the next unused
+peg corresponds to by examining the range of the refsys function.
+We'll make things easy on ourselves by simply tracking the total
+number of used pegs in a counter called `pegcount`.
+
+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).
+
+The formal language the fragment interprets is Predicate Calculus with
+equality, existential and universal quantification, and one unary
+modality (box and diamond, corresponding to epistemic necessity and
+epistemic possibility).
+
+Terms in this language are either individuals such as Alice or Bob, or
+else variables. So in general, the referent of a term can depend on a
+possibility:
+
+ ref(i, t) = t if t is an individual, and
+ g(r(t)) if t is a variable, where i = (w,n,r,g)
+
+Here are the main clauses for update (their definition 3.1).
+
+Following GSV, we'll write `update(s, φ)` (the update of information
+state `s` with the information in φ) as `s[φ]`.
+
+ s[P(t)] = {i in s | w(P)(ref(i,t))}
+
+So `man(x)` is the set of live possibilities `i = (w,r,g)` in s such that
+the set of men in `w` given by `w(man)` maps the object referred to by
+`x`, namely, `r(g("x"))`, to `true`. That is, update with "man(x)"
+discards all possibilities in which "x" fails to refer to a man.
+
+ s[t1 = t2] = {i in s | ref(i,t1) = ref(i,t2)}
+
+ s[φ and ψ] = s[φ][ψ]
+
+When updating with a conjunction, first update with the left conjunct,
+then update with the right conjunct.
+
+Existential quantification requires adding a new peg to the set of
+discourse referents.
+
+ s[∃xφ] = {(w, n+1, r[x->n], g[n->a]) | (w,n,r,g) in s and a in ent}[φ]
+
+Here's the recipe: for every possibility (w,n,r,g) in s, and for every
+entity a in the domain of discourse, construct a new possibility with
+the same world w, an incrementd peg count n+1, and a new r and g
+adjusted in such a way that the variable x refers to the object a.
+
+Note that this recipe does not examine φ. This means that this
+analysis treats the formula prefix `∃x` as if it were a meaningful
+constituent independent of φ.
+
+Negation is natural enough:
+
+ s[neg φ] = {i | {i}[φ] = {}}
+
+If updating φ with the information state that contains only the
+possibility i returns the empty information state, then not φ is true
+with respect to i.
+
+In GSV, disjunction, the conditional, and the universals are defined
+in terms of negation and the other connectives.
+
+Exercise: assume that there are two entities in the domain of
+discourse, Alice and Bob. Assume that Alice is a woman, and Bob is a
+man. Show the following computations:
+
+ 1. {}[∃x.person(x)]
+ 2. {}[∃x.man(x)]
+ 3. {}[∃x∃y.person(x) and person(y)]
+ 4. {}[∃x∃y.x=x]
+ 5. {}[∃x∃y.x=y]