Docs / Studies / Studies.Muskens1996
Combining Montague semantics and discourse representation
Muskens, R. (1996). Linguistics and Philosophy, 19(2), 143–186
Muskens treats the boxes of discourse representation theory as relations between states, so
that word meanings combine by function application and sequencing as in Montague semantics.
This file gives his lexicon over the register structures of
Semantics/Dynamic/RegisterStructure.lean and computes the meanings of his example sentences.
Implementation notes
Static predicates are sets, so an atomic condition is a preimage. A dynamic predicate takes the
value function of a referent rather than its register, and names, pronouns and traces mean
Function.eval δ for their referent δ. Conjunction at every category is the product of the
update monoid lifted pointwise, so conjoined verb phrases and noun phrases multiply with *.
TODO
- Muskens's box language with sequencing, its translation into first-order logic, and his
propositions about that translation. The one relating properness to closed formulas needs the
free variables of
DRS.toFormula, which mathlib does not yet compute forrelabelandiExs.
References
- Muskens 1996, Combining Montague semantics and discourse representation
- Kamp & Reyle 1993, From Discourse to Logic formalized
The lexicon
A common noun or intransitive verb translates as the test of its predicate, as in
farmer ↝ λv[|farmer v] and stink ↝ λv[|stinks v].
- ofStatic P v = DynamicSemantics.Update.test (v ⁻¹' P)
Built from
Used by everyNarrow, reassignment
A transitive verb takes its object noun phrase, as in love ↝ λQλv(Q(λv'[|v loves v'])).
- ofStatic₂ P Q v = Q fun (v' : S → E) => DynamicSemantics.Update.test {i : S | (v i, v' i) ∈ P}
Built from ,
Used by everyNarrow, reassignment
A name translates as the lift of the constant referent that AX4 gives it, as in
Maryⁿ ↝ λP.P(Mary).
- name x = Function.eval (Function.const S x)
Built from
Used by reassignment
The indefinite, aⁿ ↝ λP'λP([uₙ|]; P'(uₙ); P(uₙ)).
- indef u P' P = SetRel.comp (DynamicSemantics.Update.randomAssign u) (SetRel.comp (P' (DynamicSemantics.RegisterStructure.val u)) (P (DynamicSemantics.RegisterStructure.val u)))
Built from ,
Used by everyNarrow, reassignment
The universal, everyⁿ ↝ λP'λP[|([uₙ|]; P'(uₙ)) ⇒ P(uₙ)].
The definition is too large to print here; read it in the source.
Built from ,
Used by everyNarrow
The negative determiner, noⁿ ↝ λP'λP[|not([uₙ|]; P'(uₙ); P(uₙ))].
The definition is too large to print here; read it in the source.
Built from ,
Auxiliary negation, doesn't ↝ λPλQ[|not Q(P)].
- doesnt P Q = DynamicSemantics.Update.test (Q P).neg
Built from ,
The conditional, if ↝ λpq[|p ⇒ q].
- ifThen p q = DynamicSemantics.Update.test (p.impl q)
The paper's derivations
"A¹ man adores a² woman. She₂ abhors him₁." ((9); its first sentence is tree (39)).
{R : Type u_1} {S : Type u_2} {E : Type u_3} [DynamicSemantics.RegisterStructure R S E] (u₁ u₂ : R) (man woman : Set E) (adores abhors : SetRel E E) :
The definition is too large to print here; read it in the source.
Used by text_eq_box, dom_text
The text reduces by merging to the box (20).
{R : Type u_1} {S : Type u_2} {E : Type u_3} [DynamicSemantics.RegisterStructure R S E] {u₁ u₂ : R} [DecidableEq R] (h : u₁ ≠ u₂) (man woman : Set E) (adores abhors : SetRel E E) :
text u₁ u₂ man woman adores abhors = DynamicSemantics.Update.box {u₁, u₂} (DynamicSemantics.RegisterStructure.val u₁ ⁻¹' man ∩ (DynamicSemantics.RegisterStructure.val u₂ ⁻¹' woman ∩ {i : S | (DynamicSemantics.RegisterStructure.val u₁ i, DynamicSemantics.RegisterStructure.val u₂ i) ∈ adores}) ∩ {i : S | (DynamicSemantics.RegisterStructure.val u₂ i, DynamicSemantics.RegisterStructure.val u₁ i) ∈ abhors})
Built from
The truth conditions (24) of the text.
{R : Type u_1} {S : Type u_2} {E : Type u_3} [DynamicSemantics.RegisterStructure R S E] {u₁ u₂ : R} (h : u₁ ≠ u₂) (man woman : Set E) (adores abhors : SetRel E E) :
SetRel.dom (text u₁ u₂ man woman adores abhors) = {_i : S | ∃ (x₁ : E) (x₂ : E), x₁ ∈ man ∧ x₂ ∈ woman ∧ (x₁, x₂) ∈ adores ∧ (x₂, x₁) ∈ abhors}
Built from
"Every¹ girl adores a² boy" ((33)) at its S-structure (34), the indefinite in situ.
{R : Type u_1} {S : Type u_2} {E : Type u_3} [DynamicSemantics.RegisterStructure R S E] (u₁ u₂ : R) (girl boy : Set E) (adores : SetRel E E) :
- everyNarrow u₁ u₂ girl boy adores = every u₁ (ofStatic girl) (ofStatic₂ adores (indef u₂ (ofStatic boy)))
Built from , , ,
Used by dom_everyNarrow
At the LF (35), decorated as (40), (33) quantifies a² boy in over the trace e₃.
{R : Type u_1} {S : Type u_2} {E : Type u_3} [DynamicSemantics.RegisterStructure R S E] (u₁ u₂ : R) (girl boy : Set E) (adores : SetRel E E) :
The definition is too large to print here; read it in the source.
Used by dom_everyWide
The ∀∃ reading of (33), from (34).
{R : Type u_1} {S : Type u_2} {E : Type u_3} [DynamicSemantics.RegisterStructure R S E] {u₁ u₂ : R} (h : u₁ ≠ u₂) (girl boy : Set E) (adores : SetRel E E) :
SetRel.dom (everyNarrow u₁ u₂ girl boy adores) = {_i : S | ∀ x₁ ∈ girl, ∃ x₂ ∈ boy, (x₁, x₂) ∈ adores}
Built from
The ∃∀ reading of (33) comes from (35), with the indefinite's referent available to a later
pronoun ((41)).
{R : Type u_1} {S : Type u_2} {E : Type u_3} [DynamicSemantics.RegisterStructure R S E] {u₁ u₂ : R} (h : u₁ ≠ u₂) (girl boy : Set E) (adores : SetRel E E) :
SetRel.dom (everyWide u₁ u₂ girl boy adores) = {_i : S | ∃ x₂ ∈ boy, ∀ x₁ ∈ girl, (x₁, x₂) ∈ adores}
Built from
"If a¹ man bores a² woman she₂ ignores him₁." ((4), translated as the box (6)).
{R : Type u_1} {S : Type u_2} {E : Type u_3} [DynamicSemantics.RegisterStructure R S E] (u₁ u₂ : R) (man woman : Set E) (bores ignores : SetRel E E) :
The definition is too large to print here; read it in the source.
Used by dom_conditional
The conditional has the truth conditions (8), in which the indefinites of the antecedent bind the pronouns of the consequent with universal force.
{R : Type u_1} {S : Type u_2} {E : Type u_3} [DynamicSemantics.RegisterStructure R S E] {u₁ u₂ : R} (h : u₁ ≠ u₂) (man woman : Set E) (bores ignores : SetRel E E) :
SetRel.dom (conditional u₁ u₂ man woman bores ignores) = {_i : S | ∀ (x₁ x₂ : E), x₁ ∈ man ∧ x₂ ∈ woman ∧ (x₁, x₂) ∈ bores → (x₂, x₁) ∈ ignores}
Built from
"A² cat catches a¹ fish and eats it₁." ((52), decorated as tree (56)). The conjoined VPs are
sequenced, so the referent of a¹ fish is accessible to it₁.
{R : Type u_1} {S : Type u_2} {E : Type u_3} [DynamicSemantics.RegisterStructure R S E] (u₁ u₂ : R) (cat fish : Set E) (catches eats : SetRel E E) :
The definition is too large to print here; read it in the source.
Used by dom_vpCoord
The truth conditions of (52).
{R : Type u_1} {S : Type u_2} {E : Type u_3} [DynamicSemantics.RegisterStructure R S E] {u₁ u₂ : R} (h : u₁ ≠ u₂) (cat fish : Set E) (catches eats : SetRel E E) :
SetRel.dom (vpCoord u₁ u₂ cat fish catches eats) = {_i : S | ∃ (x₂ : E) (x₁ : E), x₂ ∈ cat ∧ x₁ ∈ fish ∧ (x₂, x₁) ∈ catches ∧ (x₂, x₁) ∈ eats}
Built from
"John³ admires a¹ girl and a² boy who loves her₁." ((58), with the conjoined NP of (57)).
{R : Type u_1} {S : Type u_2} {E : Type u_3} [DynamicSemantics.RegisterStructure R S E] (u₁ u₂ : R) (john : E) (girl boy : Set E) (admires loves : SetRel E E) :
The definition is too large to print here; read it in the source.
Used by dom_npCoord
The truth conditions (60) of (58).
{R : Type u_1} {S : Type u_2} {E : Type u_3} [DynamicSemantics.RegisterStructure R S E] {u₁ u₂ : R} (h : u₁ ≠ u₂) (john : E) (girl boy : Set E) (admires loves : SetRel E E) :
SetRel.dom (npCoord u₁ u₂ john girl boy admires loves) = {_i : S | ∃ (x₁ : E) (x₂ : E), x₁ ∈ girl ∧ (john, x₁) ∈ admires ∧ x₂ ∈ boy ∧ (x₂, x₁) ∈ loves ∧ (john, x₂) ∈ admires}
Built from
"*John³ admires no¹ girl and a² boy who loves her₁." ((61)), in which no¹ cannot bind
her₁.
{R : Type u_1} {S : Type u_2} {E : Type u_3} [DynamicSemantics.RegisterStructure R S E] (u₁ u₂ : R) (john : E) (girl boy : Set E) (admires loves : SetRel E E) :
The definition is too large to print here; read it in the source.
Used by dom_npCoord_no
The truth conditions (65) of (61) are an open formula, which reads the pronoun's referent off the input state.
{R : Type u_1} {S : Type u_2} {E : Type u_3} [DynamicSemantics.RegisterStructure R S E] {u₁ u₂ : R} (h : u₁ ≠ u₂) (john : E) (girl boy : Set E) (admires loves : SetRel E E) :
SetRel.dom (npCoordNo u₁ u₂ john girl boy admires loves) = {i : S | ∃ (x₂ : E), (¬∃ x₁ ∈ girl, (john, x₁) ∈ admires) ∧ x₂ ∈ boy ∧ (x₂, DynamicSemantics.RegisterStructure.val u₁ i) ∈ loves ∧ (john, x₂) ∈ admires}
Built from
"Bill¹ and Sue² own a³ donkey." ((66)), with the conjoined names applied pointwise.
{R : Type u_1} {S : Type u_2} {E : Type u_3} [DynamicSemantics.RegisterStructure R S E] (u₃ : R) (bill sue : E) (donkey : Set E) (owns : SetRel E E) :
- reassignment u₃ bill sue donkey owns = (name bill * name sue) (ofStatic₂ owns (indef u₃ (ofStatic donkey)))
Built from , , ,
Used by reassignment_eq, dom_reassignment, reassignment_ne_merge
{R : Type u_1} {S : Type u_2} {E : Type u_3} [DynamicSemantics.RegisterStructure R S E] (u₃ : R) (bill sue : E) (donkey : Set E) (owns : SetRel E E) :
reassignment u₃ bill sue donkey owns = SetRel.comp (DynamicSemantics.Update.box {u₃} (DynamicSemantics.RegisterStructure.val u₃ ⁻¹' donkey ∩ {i : S | (bill, DynamicSemantics.RegisterStructure.val u₃ i) ∈ owns})) (DynamicSemantics.Update.box {u₃} (DynamicSemantics.RegisterStructure.val u₃ ⁻¹' donkey ∩ {i : S | (sue, DynamicSemantics.RegisterStructure.val u₃ i) ∈ owns}))
Built from
The truth conditions (68) of (66).
{R : Type u_1} {S : Type u_2} {E : Type u_3} [DynamicSemantics.RegisterStructure R S E] (u₃ : R) (bill sue : E) (donkey : Set E) (owns : SetRel E E) :
SetRel.dom (reassignment u₃ bill sue donkey owns) = {_i : S | (∃ x₃ ∈ donkey, (bill, x₃) ∈ owns) ∧ ∃ x₃ ∈ donkey, (sue, x₃) ∈ owns}
Built from
The boxes of (67) do not merge when Bill and Sue own only different donkeys.
{R : Type u_1} {S : Type u_2} {E : Type u_3} [DynamicSemantics.RegisterStructure R S E] [Nonempty S] {u₃ : R} {bill sue : E} {donkey : Set E} {owns : SetRel E E} (hb : ∃ x ∈ donkey, (bill, x) ∈ owns) (hs : ∃ x ∈ donkey, (sue, x) ∈ owns) (h : ¬∃ x ∈ donkey, (bill, x) ∈ owns ∧ (sue, x) ∈ owns) :
reassignment u₃ bill sue donkey owns ≠ DynamicSemantics.Update.box {u₃} (DynamicSemantics.RegisterStructure.val u₃ ⁻¹' donkey ∩ {i : S | (bill, DynamicSemantics.RegisterStructure.val u₃ i) ∈ owns} ∩ (DynamicSemantics.RegisterStructure.val u₃ ⁻¹' donkey ∩ {i : S | (sue, DynamicSemantics.RegisterStructure.val u₃ i) ∈ owns}))
Built from
Properness is representational (§III.5)
A proper box and a box that is not proper may have the same semantic value: (45), the translation of "No¹ girl walks", and (47), that of "*No¹ girl walks. If she₁ talks she₁ talks", denote the same relation in every model, but only (45) is proper. Acceptability of an indexing is therefore a property of its representation, which is why Muskens simplifies translations by lambda conversion and merging only.
The definition is too large to print here; read it in the source.
Built from
[ | talk u₁].
- talks = { referents := ∅, conditions := [DRT.Condition.atom { arity := 1, rel := GirlRel.talk, args := ![1] }] }
Built from
Used by improper
- proper = { referents := ∅, conditions := [DRT.Condition.neg girlWalks] }
Built from ,
Used by isProper_proper, toRel_improper_eq
- improper = { referents := ∅, conditions := [DRT.Condition.neg girlWalks, DRT.Condition.imp talks talks] }
Built from , ,
Used by not_isProper_improper, toRel_improper_eq
Built from
Built from
(45) and (47) denote the same relation in every model.
Built from , ,
fn. 4: the total-assignment semantics and re-declared referents
Muskens 1996's fn. 4 scopes the agreement of his semantics with standard DRT to total
assignments and notes a second difference: on [ | [x | man x] ⇒ [x | mortal x]], where x is
declared twice, standard DRT ignores the second declaration and says that every man is mortal,
while here the second x takes a new value and the box says that there is a mortal if there is
a man. The partial semantics DRS.Verifies (Verification/Partial.lean) renders standard DRT:
the re-declaration is inert, and in a model with a non-mortal man the two truth values differ
(fn4_diverges). The witness is proper (fn4_isProper), so what fails is reuse-freeness
(fn4_not_reuseFreeAt), the hypothesis of the reconciliation
DRS.trueRel_iff_exists_verifies.
The antecedent [x | man x].
- fn4Ante = { referents := {0}, conditions := [DRT.Condition.atom { arity := 1, rel := Fn4Rel.man, args := ![0] }] }
Built from
Used by fn4
The consequent [x | mortal x], re-declaring x.
- fn4Cons = { referents := {0}, conditions := [DRT.Condition.atom { arity := 1, rel := Fn4Rel.mortal, args := ![0] }] }
Built from
Used by fn4
Built from , ,
Used by fn4_isProper, fn4_not_reuseFreeAt, fn4_trueRel, fn4_not_isTrue, fn4_diverges
A man (0) who is not mortal, and a mortal (1).
The definition is too large to print here; read it in the source.
Built from
Built from
Built from
Built from
The reconciliation DRS.trueRel_iff_exists_verifies fails on the witness.
Built from