[[!toc levels=2]]
-# Doing things with monads
-
-## Extended application: Groenendijk, Stokhof and Veltman's *Coreference and Modality*
+## Doing things with monads (an 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, where
+> GSV = GS + V, where
- GS = Dynamic theories of binding of Groenendijk and Stokhof, e.g.,
- Dynamic Predicate Logic L&P 1991: dynamic binding, donkey anaphora
- Dynamic Montague Grammar 1990: generalized quantifiers and
- discourse referents
-
- V = a dynamic theory of epistemic modality, e.g.,
- Veltman, Frank. "Data semantics."
- In Truth, Interpretation and Information, Foris, Dordrecht
- (1984): 43-63, or
- Veltman, Frank. "Defaults in update semantics." Journal of
- philosophical logic 25.3 (1996): 221-261.
+> GS = Dynamic theories of binding of Groenendijk and Stokhof, e.g.,
+> Dynamic Predicate Logic L&P 1991: dynamic binding, donkey anaphora
+> Dynamic Montague Grammar 1990: generalized quantifiers and
+> discourse referents
+
+> V = a dynamic theory of epistemic modality, e.g.,
+> Veltman, Frank. "Data semantics."
+> In Truth, Interpretation and Information, Foris, Dordrecht
+> (1984): 43-63, or
+> Veltman, Frank. "Defaults in update semantics." Journal of
+> philosophical logic 25.3 (1996): 221-261.
That is, Groenendijk and Stokhof have a well-known theory of dynamic
semantics, and Veltman has a well-known theory of epistemic modality,
with equality, existential and universal quantification, and one unary
modality, interpreted as epistemic possibility.
-An implementation in OCaml is available [[here|code/gsv.ml]]; consult
+An implementation in OCaml is available [[here|/code/gsv.ml]]; consult
that code for details of syntax, types, and values. [[An implementation
-in Haskell|code/gsv.hs]] is available as well, if you prefer.
+in Haskell|/code/gsv.hs]] is available as well, if you prefer.
+
+(We've also written [[a fuller and separate implementation|/code/gsv2.ml]] using the OCaml Juli8 Monad libraries. This fuller implementation
+demonstrates a graduated collection of semantics, so that you can see how we start from a monadic implementation
+of classic variable binding, and step by step approach the system presented by GSV. In the fullness of time, these
+two bodies of code will be merged. But for the time being, we just present them both for your edification.)
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
1. {(w,g)}[∃x.man(x)]
- = {(w,g[n->a])}[man(x)] ++ {(w,g[n->b])}[man(x)]
- ++ {(w,g[n->c])}[man(x)]
- = {} ++ {(w,g[n->b])} ++ {(w,g[n->c])}
- = {(w,g[n->a]),(w,g[n->b]),(w,g[n->c])}
+ = {(w,g[x->a])}[man(x)] ++ {(w,g[x->b])}[man(x)]
+ ++ {(w,g[x->c])}[man(x)]
+ = {} ++ {(w,g[x->b])} ++ {(w,g[x->c])}
+ = {(w,g[x->a]),(w,g[x->b]),(w,g[x->c])}
-- Bob and Carl are men
2. {(w,g)}[∃x.woman(x)]
3. {(w,g)}[∃x∃y.man(x) and man(y)]
- 4. {(w,n,r,g)}[∃x∃y.x=y]
+ 4. {(w,g)}[∃x∃y.x=y]
Running the [[code|code/gsv.ml]] gives the answers.
--------------- ---------------
w: a true a false
b false b true
- c true c false
+ c false c false
w': a false a false
b false b false
-- existential introduces new peg
- = ( {(w,g[x->a])}[closet(x)]
- ++ {(w,g[x->b])}[closet(x)]
- ++ {(w,g[x->c])}[closet(x)]
- ++ {(w',g[x->a])}[closet(x)]
- ++ {(w',g[x->b])}[closet(x)]
- ++ {(w',g[x->c])}[closet(x)])[◊guilty(x)]
+ = ( {(w,g[x->a]), (w',g[x->a])}[closet(x)]
+ ++ {(w,g[x->b]), (w',g[x->b])}[closet(x)]
+ ++ {(w,g[x->c]), (w',g[x->c])}[closet(x)]
+ )[◊guilty(x)]
-- only possibilities in which x is in the closet survive
-- the first update
{(w,g), (w',g)}[∃x(closet(x) & ◊guilty(x))]
- = {(w,g[x->a])}[closet(x)][◊guilty(x)]
- ++ {(w,g[x->b])}[closet(x)][◊guilty(x)]
- ++ {(w,g[x->c])}[closet(x)][◊guilty(x)]
- ++ {(w',g[x->a])}[closet(x)][◊guilty(x)]
- ++ {(w',g[x->b])}[closet(x)][◊guilty(x)]
- ++ {(w',g[x->c])}[closet(x)][◊guilty(x)]
+ = {(w,g[x->a]), (w',g[x->a])}[closet(x)][◊guilty(x)]
+ ++ {(w,g[x->b]), (w',g[x->b])}[closet(x)][◊guilty(x)]
+ ++ {(w,g[x->c]), (w',g[x->c])}[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
= {(w',g[x->c])}
-The result is different. Fewer possibilities remain. We have one of
-the possible worlds (w is ruled out), and we have ruled out possible
-discourses (x cannot refer to Alice). So the second formula is more
-informative.
+The result is different. Fewer possibilities remain. We have
+eliminated one of the possible worlds (w is ruled out), and we have
+eliminated one of the possible discourses (x cannot refer to Alice).
+So the second formula is more informative.
One of main conclusions of GSV is that in the presence of modality,
the hallmark of dynamic treatments--that existentials bind outside of