From: jim
Date: Tue, 14 Apr 2015 01:00:06 +0000 (0400)
Subject: add note about gsv2.ml
XGitUrl: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=commitdiff_plain;h=c722a15a22df75a41522a245e49eddc73902a60a
add note about gsv2.ml

diff git a/topics/week10_gsv.mdwn b/topics/week10_gsv.mdwn
index 4ff29764..96786ca3 100644
 a/topics/week10_gsv.mdwn
+++ b/topics/week10_gsv.mdwn
@@ 2,26 +2,24 @@
[[!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): 4363, or
 Veltman, Frank. "Defaults in update semantics." Journal of
 philosophical logic 25.3 (1996): 221261.
+> 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): 4363, or
+> Veltman, Frank. "Defaults in update semantics." Journal of
+> philosophical logic 25.3 (1996): 221261.
That is, Groenendijk and Stokhof have a wellknown theory of dynamic
semantics, and Veltman has a wellknown theory of epistemic modality,
@@ 52,9 +50,14 @@ The formal language the fragment interprets is the Predicate Calculus
with equality, existential and universal quantification, and one unary
modality, interpreted as epistemic possibility.
An implementation in OCaml is available [[herecode/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 Haskellcode/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