Discourse Representation Theory

@cite{kamp-1981} @cite{kamp-reyle-1993}

Discourse Representation Theory (DRT), the pioneering framework for dynamic semantics using Discourse Representation Structures (DRSs).

Unified DRS Representation

This module builds on the canonical DRSExpr type from Core.DRSExpr, which captures the full recursive syntax of @cite{kamp-reyle-1993} Def 1.4.1:

• DRSExpr.box = K&R's ⟨U, Con⟩ (universe + conditions)
• DRSExpr.neg = negated condition (¬K)
• DRSExpr.impl = implicative condition (K₁ ⇒ K₂)
• DRSExpr.disj = disjunctive condition (K₁ ∨ K₂)
• DRSExpr.seq = discourse sequencing (K₁ ; K₂)

Syntactic operations (adr, occurs, acc, isFree, isProper) are defined in Core.DRSExpr. Semantic interpretation (interp, mergingLemma, reduce) is defined in Core.Accessibility.

K&R Model Theory (Def 1.2.1)

A KRModel formalizes @cite{kamp-reyle-1993}'s Definition 1.2.1: a triple ⟨U_M, Name_M, Pred_M⟩ providing the universe, name bearers, and predicate extensions for evaluating DRSs.

Subordination (Def 2.1.2)

The subordinate relation captures when one DRS is structurally embedded inside another — the key structural relation governing anaphoric accessibility in @cite{kamp-reyle-1993} Ch 2.

Layered DRT (LDRT)

@cite{van-der-sandt-maier-2003} extend DRT with content layers: each DRS condition carries a label (pr, fr, imp) indicating whether it contributes presuppositional, at-issue, or implicature content. This enables a unified treatment of denial.

structure Semantics.Dynamic.DRT.KRModel (E : Type u_1) : Type u_1

A model for a DRS vocabulary, following @cite{kamp-reyle-1993} Def 1.2.1.

A model M for vocabulary V is a triple ⟨U_M, Name_M, Pred_M⟩:

• U_M: a non-empty set of individuals (the universe)
• Name_M: maps individual constants to their bearers in U_M
• Pred_M: maps predicate constants to their extensions

In our formalization, names and predicates are both identified by Nat indices (matching DRSExpr's atom constructor).

• names : ℕ → E

  Name interpretation: maps name indices to their bearers.

• preds : Core.Accessibility.RelInterp E

  Predicate interpretation: maps relation indices to truth on entity lists. This is exactly a RelInterp E from Core.Accessibility.

def Semantics.Dynamic.DRT.KRModel.toRelInterp {E : Type u_1} (M : KRModel E) : Core.Accessibility.RelInterp E

Extract a RelInterp from a K&R model for use with interp.

Equations

• M.toRelInterp = M.preds

def Semantics.Dynamic.DRT.trueIn {E : Type u_1} (M : KRModel E) (K : Core.DRSExpr.DRSExpr) : Prop

A DRS K is true in model M iff there is an embedding (assignment) that verifies all conditions (@cite{kamp-reyle-1993} Def 1.4.5).

Equations

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

inductive Semantics.Dynamic.DRT.ImmSubordinate : Core.DRSExpr.DRSExpr → Core.DRSExpr.DRSExpr → Prop

K₁ is immediately subordinate to K₂ if K₂'s conditions contain K₁ as a component of a complex condition (negation, implication, or disjunction). Matches @cite{kamp-reyle-1993} Def 2.1.2(i).

• neg (K : Core.DRSExpr.DRSExpr) (drefs : List ℕ) (pre post : List Core.DRSExpr.DRSExpr) : ImmSubordinate K (Core.DRSExpr.DRSExpr.box drefs (pre ++ [K.neg] ++ post))

  K is immediately subordinate to [... | ¬K, ...]

• implLeft (K₁ K₂ : Core.DRSExpr.DRSExpr) (drefs : List ℕ) (pre post : List Core.DRSExpr.DRSExpr) : ImmSubordinate K₁ (Core.DRSExpr.DRSExpr.box drefs (pre ++ [K₁.impl K₂] ++ post))

  K₁ is immediately subordinate to [... | K₁ ⇒ K₂, ...]

• implRight (K₁ K₂ : Core.DRSExpr.DRSExpr) (drefs : List ℕ) (pre post : List Core.DRSExpr.DRSExpr) : ImmSubordinate K₂ (Core.DRSExpr.DRSExpr.box drefs (pre ++ [K₁.impl K₂] ++ post))

  K₂ is immediately subordinate to [... | K₁ ⇒ K₂, ...]

• disjLeft (K₁ K₂ : Core.DRSExpr.DRSExpr) (drefs : List ℕ) (pre post : List Core.DRSExpr.DRSExpr) : ImmSubordinate K₁ (Core.DRSExpr.DRSExpr.box drefs (pre ++ [K₁.disj K₂] ++ post))

  K₁ is immediately subordinate to [... | K₁ ∨ K₂, ...]

• disjRight (K₁ K₂ : Core.DRSExpr.DRSExpr) (drefs : List ℕ) (pre post : List Core.DRSExpr.DRSExpr) : ImmSubordinate K₂ (Core.DRSExpr.DRSExpr.box drefs (pre ++ [K₁.disj K₂] ++ post))

  K₂ is immediately subordinate to [... | K₁ ∨ K₂, ...]

inductive Semantics.Dynamic.DRT.Subordinate : Core.DRSExpr.DRSExpr → Core.DRSExpr.DRSExpr → Prop

K₁ is subordinate to K₂ (written K₁ < K₂) if there is a chain of immediate subordination from K₁ to K₂. This is the transitive closure of ImmSubordinate. Matches @cite{kamp-reyle-1993} Def 2.1.2(ii).

• imm {K₁ K₂ : Core.DRSExpr.DRSExpr} : ImmSubordinate K₁ K₂ → Subordinate K₁ K₂

  One step of immediate subordination.

• trans {K₁ K₂ K₃ : Core.DRSExpr.DRSExpr} : Subordinate K₁ K₃ → Subordinate K₃ K₂ → Subordinate K₁ K₂

  Transitivity: if K₁ < K₃ and K₃ < K₂, then K₁ < K₂.

def Semantics.Dynamic.DRT.WeakSubordinate (K₁ K₂ : Core.DRSExpr.DRSExpr) : Prop

K₁ is weakly subordinate to K₂ (written K₁ ≤ K₂) iff K₁ = K₂ or K₁ < K₂. Matches @cite{kamp-reyle-1993} Def 2.1.2(iii).

Equations

• Semantics.Dynamic.DRT.WeakSubordinate K₁ K₂ = (K₁ = K₂ ∨ Semantics.Dynamic.DRT.Subordinate K₁ K₂)

structure Semantics.Dynamic.DRT.TaggedCondition : Type

A DRS condition tagged with its content layer.

@cite{van-der-sandt-maier-2003}: in LDRT, every condition carries a label indicating its discourse role. Uses DRSExpr as the condition type, unifying with the canonical DRS representation from Core.Accessibility.

• layer : Core.Semantics.ContentLayer.ContentLayer

  The content layer this condition contributes to.

• condition : Core.DRSExpr.DRSExpr

  The underlying DRS condition.

instance Semantics.Dynamic.DRT.instReprTaggedCondition : Repr TaggedCondition

Equations

• Semantics.Dynamic.DRT.instReprTaggedCondition = { reprPrec := Semantics.Dynamic.DRT.instReprTaggedCondition.repr }

def Semantics.Dynamic.DRT.instReprTaggedCondition.repr : TaggedCondition → ℕ → Std.Format

Equations

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

structure Semantics.Dynamic.DRT.LDRS : Type

A Layered DRS (LDRS): a DRS whose conditions carry content-layer tags.

This is the core data structure of @cite{van-der-sandt-maier-2003}'s LDRT. A standard DRS is the special case where all conditions are tagged atIssue.

• drefs : List ℕ

  Universe: discourse referent indices.

• conditions : List TaggedCondition

  Layered conditions.

def Semantics.Dynamic.DRT.instReprLDRS.repr : LDRS → ℕ → Std.Format

Equations

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

instance Semantics.Dynamic.DRT.instReprLDRS : Repr LDRS

Equations

• Semantics.Dynamic.DRT.instReprLDRS = { reprPrec := Semantics.Dynamic.DRT.instReprLDRS.repr }

def Semantics.Dynamic.DRT.LDRS.toDRSExpr (k : LDRS) : Core.DRSExpr.DRSExpr

Convert an LDRS to a plain DRSExpr by stripping layer tags.

Equations

• k.toDRSExpr = Semantics.Dynamic.Core.DRSExpr.DRSExpr.box k.drefs (List.map (fun (x : Semantics.Dynamic.DRT.TaggedCondition) => x.condition) k.conditions)

def Semantics.Dynamic.DRT.DRSExpr.toLDRS : Core.DRSExpr.DRSExpr → LDRS

Lift a DRSExpr.box to an LDRS by tagging all conditions as at-issue.

A plain DRS is an LDRS where everything is atIssue.

Equations

• One or more equations did not get rendered due to their size.
• Semantics.Dynamic.DRT.DRSExpr.toLDRS x✝ = { drefs := [], conditions := [{ layer := Core.Semantics.ContentLayer.ContentLayer.atIssue, condition := x✝ }] }

def Semantics.Dynamic.DRT.LDRS.atLayer (k : LDRS) (l : Core.Semantics.ContentLayer.ContentLayer) : List Core.DRSExpr.DRSExpr

Extract all conditions at a given layer.

Equations

• k.atLayer l = List.map (fun (x : Semantics.Dynamic.DRT.TaggedCondition) => x.condition) (List.filter (fun (x : Semantics.Dynamic.DRT.TaggedCondition) => x.layer == l) k.conditions)

def Semantics.Dynamic.DRT.LDRS.merge (k1 k2 : LDRS) : LDRS

LDRS merge: combine two layered DRSs, preserving layer tags.

Equations

• k1.merge k2 = { drefs := k1.drefs ++ k2.drefs, conditions := k1.conditions ++ k2.conditions }

def Semantics.Dynamic.DRT.LDRS.offensiveConditions (k : LDRS) (offLayers : List Core.Semantics.ContentLayer.ContentLayer) : List TaggedCondition

The offensive conditions of an LDRS with respect to a correction: those whose layer is in the offensive set.

In denial, these are the conditions that get retracted.

Equations

• k.offensiveConditions offLayers = List.filter (fun (x : Semantics.Dynamic.DRT.TaggedCondition) => offLayers.contains x.layer) k.conditions

def Semantics.Dynamic.DRT.LDRS.survivingConditions (k : LDRS) (offLayers : List Core.Semantics.ContentLayer.ContentLayer) : List TaggedCondition

The surviving conditions after denial: those NOT at offensive layers.

Equations

• k.survivingConditions offLayers = List.filter (fun (x : Semantics.Dynamic.DRT.TaggedCondition) => !offLayers.contains x.layer) k.conditions

The paper's deepest architectural claim: assertion is monotonic (merge only adds conditions), while denial is non-monotonic (surviving conditions are a subset of the original). Standard DRT update is monotonic; denial is the ONLY operation that removes information from the discourse context.

theorem Semantics.Dynamic.DRT.LDRS.offensive_surviving_partition (k : LDRS) (offLayers : List Core.Semantics.ContentLayer.ContentLayer) : (k.offensiveConditions offLayers).length + (k.survivingConditions offLayers).length = k.conditions.length

Offensive + surviving = all conditions (partition).

theorem Semantics.Dynamic.DRT.merge_monotonic (k1 k2 : LDRS) : k1.conditions.length ≤ (k1.merge k2).conditions.length

Assertion (merge) is monotonic: the result has at least as many conditions as the original LDRS.

theorem Semantics.Dynamic.DRT.denial_nonmonotonic (k : LDRS) (offLayers : List Core.Semantics.ContentLayer.ContentLayer) : (k.survivingConditions offLayers).length ≤ k.conditions.length

Denial (surviving conditions) is non-monotonic: the result has at most as many conditions as the original LDRS.

def Semantics.Dynamic.DRT.LDRS.interp {E : Type u_1} (rels : Core.Accessibility.RelInterp E) (k : LDRS) : Core.DynProp.DRS (Core.Assignment E)

Interpret an LDRS by stripping tags and using interp from Core.Accessibility. This gives the at-issue truth conditions; presuppositional and implicature content must be handled separately by the content-layer machinery.

Equations

• Semantics.Dynamic.DRT.LDRS.interp rels k = Semantics.Dynamic.Core.Accessibility.interp rels k.toDRSExpr

theorem Semantics.Dynamic.DRT.toLDRS_toDRSExpr_conditions (drefs : List ℕ) (conds : List Core.DRSExpr.DRSExpr) : (DRSExpr.toLDRS (Core.DRSExpr.DRSExpr.box drefs conds)).toDRSExpr = Core.DRSExpr.DRSExpr.box drefs conds

Round-trip: box → toLDRS → toDRSExpr preserves conditions.

@cite{van-der-sandt-maier-2003} §4.3: given a set of offensive layers (computed by Off from Core.Semantics.ContentLayer), RA* partitions the LDRS conditions: surviving conditions remain in the main DRS, offensive conditions are moved under negation.

def Semantics.Dynamic.DRT.LDRS.directedRA (k : LDRS) (offLayers : List Core.Semantics.ContentLayer.ContentLayer) : LDRS

Directed reverse anaphora (RA*): move offensive-layer conditions under negation, preserving non-offensive conditions.

@cite{van-der-sandt-maier-2003} §4.3, def (67).

Equations

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

def Semantics.Dynamic.DRT.LDRS.denialUpdate (state correction : LDRS) (offLayers : List Core.Semantics.ContentLayer.ContentLayer) : LDRS

Denial pipeline: merge correction, then apply RA*.

@cite{van-der-sandt-maier-2003} §4.3: in an assertion-denial-correction sequence ⟨σᵢ, σᵢ₊₁, σᵢ₊₂⟩, the correction is merged with the discourse state, then RA* retracts the offensive layers.

Equations

• state.denialUpdate correction offLayers = (state.merge correction).directedRA offLayers

theorem Semantics.Dynamic.DRT.LDRS.directedRA_preserves_drefs (k : LDRS) (offLayers : List Core.Semantics.ContentLayer.ContentLayer) : (k.directedRA offLayers).drefs = k.drefs

RA* always preserves discourse referents — denial retracts conditions, not referent introductions. This matches the paper's treatment: drefs introduced by σ₁ remain available for anaphoric reference even after denial (@cite{van-der-sandt-maier-2003} §3.6, ex. 51: "A man jumped off the bridge. He didn't jump, he was pushed.").