--- /dev/null
+type Predicate = String
+data Ent = Alice | Bob | Carl deriving (Eq, Show)
+data World = W1 | W2 | Hungry | Full deriving (Eq, Show)
+type Variable = String
+data Term = Constant Ent | Var Variable deriving (Eq, Show)
+data Clause = Pred Predicate Term
+ | Eq Term Term
+ | Conj Clause Clause
+ | Neg Clause
+ | Poss Clause
+ | Ex String Clause
+ deriving (Eq, Show)
+type Assignment = [(Variable, Ent)]
+type Poss = (World, Assignment)
+type Infostate = [Poss]
+
+referent :: Poss -> Term -> Ent
+referent (w,g) (Constant c) = c
+referent (w,(v',a):g) (Var v) = if v == v' then a else referent (w,g) (Var v)
+
+extension :: World -> Predicate -> Ent -> Bool
+extension _ "woman" Alice = True
+extension _ "man" Bob = True
+extension _ "man" Carl = True
+extension Hungry "hungry" Alice = True
+extension _ "enter" Bob = True
+extension _ "enter" Carl = True
+extension _ "sit" Alice = True
+extension _ "sit" Bob = True
+extension W1 "closet" Alice = True
+extension W1 "guilty" Bob = True
+extension W2 "closet" Carl = True
+extension W2 "guilty" Carl = True
+extension _ _ _ = False
+
+update :: Infostate -> Clause -> Infostate
+update s (Pred p t) = [i | i@(w,g) <- s, extension w p (referent i t)]
+update s (Eq t1 t2) = [i | i <- s, referent i t1 == referent i t2]
+update s (Conj c1 c2) = update (update s c1) c2
+update s (Neg c) = [i | i <- s, length (update [i] c) == 0]
+update s (Poss c) = [i | i <- s, length (update s c) > 0]
+update s (Ex v c) =
+ concat [update [(w, (v,a):g) | (w,g) <- s] c | a <- domain]
+
+domain = [Alice, Bob, Carl]
+
+test1 = update [(W1, [])] (Ex "x" (Pred "man" (Var "x")))
+test2 = update [(W1, [])] (Ex "x" (Pred "woman" (Var "x")))
+test3 = update [(W1, [])] (Ex "x" (Ex "y" (Conj (Pred "man" (Var "x"))
+ (Pred "man" (Var "y")))))
+test4 = update [(W1, [])] (Ex "x" (Ex "y" (Eq (Var "x") (Var "y"))))
+test5 = update [(Hungry,[]),(Full,[])] (Neg (Pred "hungry" (Constant Alice)))
+
+test6 = update [(Hungry,[]),(Full,[])]
+ (Conj (Neg (Pred "hungry" (Constant Alice)))
+ (Poss (Pred "hungry" (Constant Alice))))
+
+test7 = update [(Hungry,[]),(Full,[])]
+ (Conj (Poss (Pred "hungry" (Constant Alice)))
+ (Neg (Pred "hungry" (Constant Alice))))
+
+test8 = update [(W1,[("x",Bob)])]
+ (Conj (Ex "x" (Pred "enter" (Var "x")))
+ (Pred "sit" (Var "x")))
+
+test9 = update [(W1,[("x",Bob)])]
+ (Conj (Pred "sit" (Var "x"))
+ (Ex "x" (Pred "enter" (Var "x"))))
+test10 = update [(W1,[]),(W2,[])]
+ (Conj (Ex "x" (Pred "closet" (Var "x")))
+ (Poss (Pred "guilty" (Var "x"))))
+
+test11 = update [(W1,[]),(W2,[])]
+ (Ex "x" (Conj (Pred "closet" (Var "x"))
+ (Poss (Pred "guilty" (Var "x")))))
+
+
and epistemic possibility).
An implementation in OCaml is available [[here|code/gsv.ml]]; consult
-that code for details of syntax, types, and values.
+that code for details of syntax, types, and values. [[An implementation
+in Haskell|code/gsv.hs]] is available as well, if you prefer.
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
variable is assigned a discourse referent distinct from all previous
discourse referents.
-End of digression on pegs.
-
+The addition of pegs tracks an active discussion in the dynamic
+literature around the time of publication of the paper. Groenendijk
+and Stokhof (Two theories of dynamic semantics, 1989) noted that it
+was possible in DPL for information to be "lost".
+
+ 18. (∃x.P(x)) & (∃x.Q(x)) & R(x)
+
+If the two existentials happen to bind the same variable (here, "x"),
+then the second existential occludes the first. That is, at the point
+at which we evalute R(x), all of the assignment functions will be
+mapping the variable "x" to objects that have property Q. The
+information that there exist objects with property P has been lost.
+If you want your dynamic system to be eliminative---or in more general
+terms, if you want the amount of information embodied by an updated
+information state to be monotonically increasing---then this is a
+problem.
+
+A syntactic solution is to require that the variable bound
+by an existential to be chosen fresh.
+
+Vermeulen, Cees FM. "Merging without mystery or: Variables in dynamics
+semantics." Journal of Philosophical Logic 24.4 (1995): 405-450 offers
+a different approach, one based on *referent systems*. GSV's pegs are
+a referent system. In the pegs system, when (18) is processed, the
+information that there is an object that has property P is maintained
+in the information state. Curiously, however, there is still no way
+to refer to that object, at least, not with a variable, since there is
+no variable that is associated with the peg that points to the
+relevant object. So the information is present, but not accessible.
+
+That does not mean that there aren't other expression types that are
+able to latch onto peg. An intriguing suggestion based on an example
+in Vermeulen is that "former" might be able to provide access to a
+hidden peg:
+
+ 19. Someone entered. Someone spoke. The former was a woman.
+
+Presumably we want *the former* to be able to pick out the person who
+entered, whether or not the two existentials bind the same variable or
+not. If we allow "former" to latch onto the second most recently
+established peg, no matter whether there is a variable still pointing
+to that peg, the desired effect is achieved.
+
+But none of this is relevant for any of the explanations or analyses
+provide by the GSV fragment, and it is considerably simpler to see
+what their fragment is about if we leave referent systems out of it.