Compositional CDRT Fragment

@cite{muskens-1996}

§III.4 and §IV: Lexical translations (T₀) and generalized coordination for a fragment of English in Compositional DRT.

Semantic Types (Table 2, p. 164)

Muskens Type	Lean Type	Description
et	E → Prop	Static predicate
e(et)	E → E → Prop	Static relation
s(st)	DRS S	Dynamic proposition
[π]	Dref S E → DRS S	Dynamic predicate
[[π]]	DynPred S E → DRS S	Dynamic quantifier

Composition

Meanings compose via function application (T₂) and sequencing (T₃). These are native Lean operations, so the composition rules T₁–T₅ need no special formalization — they are just function application, dseq, and λ-abstraction.

Generalized Coordination (§IV)

and = sequencing applied pointwise; or = DRS disjunction applied pointwise. The same schema works at every syntactic category (S, VP, NP).

@[reducible, inline]

abbrev Semantics.Dynamic.CDRT.Fragment.DynPred (S : Type u_3) (E : Type u_4) : Type (max u_4 u_3)

Dynamic one-place predicate: type [π] in @cite{muskens-1996}.

Equations

• Semantics.Dynamic.CDRT.Fragment.DynPred S E = (Semantics.Dynamic.Core.DynamicTy2.Dref S E → Semantics.Dynamic.Core.DynProp.DRS S)

@[reducible, inline]

abbrev Semantics.Dynamic.CDRT.Fragment.DynQuant (S : Type u_3) (E : Type u_4) : Type (max u_4 u_3)

Dynamic generalized quantifier: type [[π]] in @cite{muskens-1996}.

Equations

• Semantics.Dynamic.CDRT.Fragment.DynQuant S E = (Semantics.Dynamic.CDRT.Fragment.DynPred S E → Semantics.Dynamic.Core.DynProp.DRS S)

def Semantics.Dynamic.CDRT.Fragment.cn {S : Type u_1} {E : Type u_2} (P : E → Prop) : DynPred S E

Common noun: farmer ↝ λv[|farmer v]. Type: [π] (dynamic one-place predicate).

Equations

• Semantics.Dynamic.CDRT.Fragment.cn P u = [Semantics.Dynamic.Core.DynamicTy2.atom1 P u]

def Semantics.Dynamic.CDRT.Fragment.iv {S : Type u_1} {E : Type u_2} (P : E → Prop) : DynPred S E

Intransitive verb: stink ↝ λv[|stinks v]. Type: [π] (same as common noun).

Equations

• Semantics.Dynamic.CDRT.Fragment.iv P u = [Semantics.Dynamic.Core.DynamicTy2.atom1 P u]

def Semantics.Dynamic.CDRT.Fragment.tv {S : Type u_1} {E : Type u_2} (R : E → E → Prop) : DynQuant S E → DynPred S E

Transitive verb: love ↝ λQλv(Q(λv'[|v loves v'])). Type: [[π]] → [π]. Takes an NP (object) and produces a VP.

Equations

• Semantics.Dynamic.CDRT.Fragment.tv R Q u = Q fun (v : Semantics.Dynamic.Core.DynamicTy2.Dref S E) => [Semantics.Dynamic.Core.DynamicTy2.atom2 R u v]

def Semantics.Dynamic.CDRT.Fragment.detA {S : Type u_1} {E : Type u_2} [Core.DynamicTy2.AssignmentStructure S E] (u : Core.DynamicTy2.Dref S E) : DynPred S E → DynQuant S E

Indefinite determiner: aⁿ ↝ λP'λP([uₙ]; P'(uₙ); P(uₙ)). Type: [π] → [[π]]. Takes a noun, produces a quantifier. Introduces discourse referent u.

Equations

• Semantics.Dynamic.CDRT.Fragment.detA u noun vp = [u]ᵈʳᵉᶠ ⨟ (noun u ⨟ vp u)

def Semantics.Dynamic.CDRT.Fragment.detEvery {S : Type u_1} {E : Type u_2} [Core.DynamicTy2.AssignmentStructure S E] (u : Core.DynamicTy2.Dref S E) : DynPred S E → DynQuant S E

Universal determiner: everyⁿ ↝ λP'λP(([uₙ]; P'(uₙ)) ⇒ P(uₙ)). Type: [π] → [[π]]. Dynamic implication gives universal force.

Equations

• Semantics.Dynamic.CDRT.Fragment.detEvery u noun vp = [Semantics.Dynamic.Core.DynProp.dimpl ([u]ᵈʳᵉᶠ ⨟ noun u) (vp u)]

def Semantics.Dynamic.CDRT.Fragment.detNo {S : Type u_1} {E : Type u_2} [Core.DynamicTy2.AssignmentStructure S E] (u : Core.DynamicTy2.Dref S E) : DynPred S E → DynQuant S E

Negative determiner: noⁿ ↝ λP'λP[|not([uₙ]; P'(uₙ); P(uₙ))]. Type: [π] → [[π]].

Equations

• Semantics.Dynamic.CDRT.Fragment.detNo u noun vp = [∼[u]ᵈʳᵉᶠ ⨟ (noun u ⨟ vp u)]

def Semantics.Dynamic.CDRT.Fragment.properNP {S : Type u_1} {E : Type u_2} (name : Core.DynamicTy2.Dref S E) : DynQuant S E

Proper name NP: Maryⁿ ↝ λP.P(Mary). Type: [[π]]. Applies the VP directly to the name's dref.

Equations

• Semantics.Dynamic.CDRT.Fragment.properNP name P = P name

def Semantics.Dynamic.CDRT.Fragment.pro {S : Type u_1} {E : Type u_2} (u : Core.DynamicTy2.Dref S E) : DynQuant S E

Pronoun NP: heₙ ↝ λP.P(uₙ). Type: [[π]]. Picks up the dref from the antecedent.

Equations

• Semantics.Dynamic.CDRT.Fragment.pro u P = P u

def Semantics.Dynamic.CDRT.Fragment.cond {S : Type u_1} : Core.DynProp.DRS S → Core.DynProp.DRS S → Core.DynProp.DRS S

Conditional: if ↝ λpq[|p ⇒ q]. Type: DRS → DRS → DRS.

Equations

• Semantics.Dynamic.CDRT.Fragment.cond p q = [Semantics.Dynamic.Core.DynProp.dimpl p q]

def Semantics.Dynamic.CDRT.Fragment.auxNeg {S : Type u_1} {E : Type u_2} : DynPred S E → DynQuant S E → Core.DynProp.DRS S

Auxiliary negation: doesn't ↝ λPλQ[|not Q(P)] (T₀, p. 165). Type: [π] → [[π]] → DRS. Takes VP (P) then subject NP (Q), matching @cite{muskens-1996}'s argument order.

Equations

• Semantics.Dynamic.CDRT.Fragment.auxNeg P Q = [∼Q P]

and = generalized sequencing; or = generalized DRS disjunction. The same schema works at every syntactic category by applying the Boolean operation pointwise to the innermost DRS layer.

def Semantics.Dynamic.CDRT.Fragment.andS {S : Type u_1} : Core.DynProp.DRS S → Core.DynProp.DRS S → Core.DynProp.DRS S

Sentence-level and: K₁ and K₂ = K₁; K₂.

Equations

• Semantics.Dynamic.CDRT.Fragment.andS = Semantics.Dynamic.Core.DynProp.dseq

def Semantics.Dynamic.CDRT.Fragment.orS {S : Type u_1} : Core.DynProp.DRS S → Core.DynProp.DRS S → Core.DynProp.DRS S

Sentence-level or: K₁ or K₂ = [K₁ or K₂] (disjunction test).

Equations

• Semantics.Dynamic.CDRT.Fragment.orS D₁ D₂ = [Semantics.Dynamic.Core.DynProp.ddisj D₁ D₂]

def Semantics.Dynamic.CDRT.Fragment.andVP {S : Type u_1} {E : Type u_2} : DynPred S E → DynPred S E → DynPred S E

VP-level and: λv(P₁(v); P₂(v)).

Equations

• Semantics.Dynamic.CDRT.Fragment.andVP P₁ P₂ u = P₁ u ⨟ P₂ u

def Semantics.Dynamic.CDRT.Fragment.orVP {S : Type u_1} {E : Type u_2} : DynPred S E → DynPred S E → DynPred S E

VP-level or: λv[P₁(v) or P₂(v)].

Equations

• Semantics.Dynamic.CDRT.Fragment.orVP P₁ P₂ u = [Semantics.Dynamic.Core.DynProp.ddisj (P₁ u) (P₂ u)]

def Semantics.Dynamic.CDRT.Fragment.andNP {S : Type u_1} {E : Type u_2} : DynQuant S E → DynQuant S E → DynQuant S E

NP-level and: λP(Q₁(P); Q₂(P)).

Equations

• Semantics.Dynamic.CDRT.Fragment.andNP Q₁ Q₂ P = Q₁ P ⨟ Q₂ P

def Semantics.Dynamic.CDRT.Fragment.orNP {S : Type u_1} {E : Type u_2} : DynQuant S E → DynQuant S E → DynQuant S E

NP-level or: λP[Q₁(P) or Q₂(P)].

Equations

• Semantics.Dynamic.CDRT.Fragment.orNP Q₁ Q₂ P = [Semantics.Dynamic.Core.DynProp.ddisj (Q₁ P) (Q₂ P)]

def Semantics.Dynamic.CDRT.Fragment.exampleText {S : Type u_1} {E : Type u_2} [Core.DynamicTy2.AssignmentStructure S E] (u₁ u₂ : Core.DynamicTy2.Dref S E) (man woman : E → Prop) (adores abhors : E → E → Prop) : Core.DynProp.DRS S

Example derivation: "A¹ man adores a² woman. She₂ abhors him₁."

Translation (p. 167, derivation tree (39)): [u₁]; [man u₁]; [u₂]; [woman u₂]; [u₁ adores u₂]; [u₂ abhors u₁]

Truth conditions (formula (24)): ∃x₁ x₂ (man(x₁) ∧ woman(x₂) ∧ adores(x₁,x₂) ∧ abhors(x₂,x₁))

Equations

• One or more equations did not get rendered due to their size.

def Semantics.Dynamic.CDRT.Fragment.donkeySentence {S : Type u_1} {E : Type u_2} [Core.DynamicTy2.AssignmentStructure S E] (u₁ u₂ : Core.DynamicTy2.Dref S E) (farmer donkey_ : E → Prop) (owns beats : E → E → Prop) : Core.DynProp.DRS S

Example: "Every¹ farmer who owns a² donkey beats it₂."

The donkey sentence, with universal force from detEvery and anaphoric it₂ picking up the dref from the indefinite. Translation: ([u₁]; [farmer u₁]; [u₂]; [donkey u₂]; [u₁ owns u₂]) ⇒ [u₁ beats u₂]

Equations

• One or more equations did not get rendered due to their size.

def Semantics.Dynamic.CDRT.Fragment.vpCoordExample {S : Type u_1} {E : Type u_2} [Core.DynamicTy2.AssignmentStructure S E] (u₁ u₂ : Core.DynamicTy2.Dref S E) (cat fish : E → Prop) (catches eats : E → E → Prop) : Core.DynProp.DRS S

Example: "A² cat catches a¹ fish and eats it₁." (§IV, p. 179, tree (56))

VP coordination with cross-conjunct anaphora: it₁ in "eats it₁" picks up the dref introduced by "a¹ fish" in "catches a¹ fish".

This works because andVP sequences the VP meanings, so the dref introduced by the first conjunct is accessible in the second.

Equations

• One or more equations did not get rendered due to their size.

theorem Semantics.Dynamic.CDRT.Fragment.andVP_eq_dseq {S : Type u_1} {E : Type u_2} (P₁ P₂ : DynPred S E) (u : Core.DynamicTy2.Dref S E) : andVP P₁ P₂ u = P₁ u ⨟ P₂ u

VP and is definitionally sequencing at the dref argument.

theorem Semantics.Dynamic.CDRT.Fragment.orVP_eq_test_ddisj {S : Type u_1} {E : Type u_2} (P₁ P₂ : DynPred S E) (u : Core.DynamicTy2.Dref S E) : orVP P₁ P₂ u = [Core.DynProp.ddisj (P₁ u) (P₂ u)]

VP or is definitionally disjunction at the dref argument.

theorem Semantics.Dynamic.CDRT.Fragment.andS_eq_dseq {S : Type u_1} : andS = Core.DynProp.dseq

Sentence and is sequencing.