[[!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.