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

A Discourse Representation Structure (DRS).

Note: This is a simplified representation. Full DRT would have recursive structure with embedded DRSs.

• drefs : Set ℕ

  Universe: set of discourse referents introduced

• conditions : List ((ℕ → E) → Prop)

  Conditions: predicates over the referents

inductive Semantics.Dynamic.DRT.DRSCondition (E : Type u_1) : Type u_1

DRS condition: atomic predicate over discourse referents.

• atom {E : Type u_1} : ((ℕ → E) → Prop) → DRSCondition E
• neg {E : Type u_1} : DRS E → DRSCondition E
• impl {E : Type u_1} : DRS E → DRS E → DRSCondition E
• disj {E : Type u_1} : DRS E → DRS E → DRSCondition E

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

Full DRS with complex conditions.

• drefs : Set ℕ
• conditions : List (DRSCondition E)

def Semantics.Dynamic.DRT.DRS.merge {E : Type u_1} (k1 k2 : DRS E) : DRS E

DRS merge: combine two DRSs.

K₁; K₂ combines drefss and conditions.

Equations

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

def Semantics.Dynamic.DRT.DRS.accessible {E : Type u_1} (k : DRS E) (x : ℕ) : Prop

Accessibility in DRT: a referent is accessible from a condition if it's in the drefs of a dominating DRS.

This simplified version just checks if x is in the drefs.

Equations

• k.accessible x = (x ∈ k.drefs)

def Semantics.Dynamic.DRT.Embedding (E : Type u_1) : Type u_1

An embedding function maps discourse referents to entities.

Equations

• Semantics.Dynamic.DRT.Embedding E = (ℕ → E)

def Semantics.Dynamic.DRT.Embedding.extends {E : Type u_1} (f g : Embedding E) (dom : Set ℕ) : Prop

Embedding extends another if they agree on shared domain.

Equations

• f.extends g dom = ∀ x ∈ dom, f x = g x

def Semantics.Dynamic.DRT.DRS.satisfies {E : Type u_1} (k : DRS E) (f : Embedding E) : Prop

DRS satisfaction: embedding f satisfies DRS K in model M.

Simplified version checking conditions hold.

Equations

• k.satisfies f = ∀ cond ∈ k.conditions, cond f

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

A layered DRS condition: a standard DRS condition tagged with the content layer it contributes to.

@cite{van-der-sandt-maier-2003}: in LDRT, every condition carries a label indicating its discourse role. The layer determines how the condition behaves under denial:

• pr conditions survive propositional denial
• fr conditions survive presuppositional denial
• imp conditions survive implicature denial

• layer : Core.Semantics.ContentLayer.ContentLayer

  The content layer this condition contributes to

• condition : DRSCondition E

  The underlying DRS condition

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

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 fr (at-issue).

• drefs : Set ℕ

  Universe: discourse referents

• conditions : List (LayeredCondition E)

  Layered conditions

def Semantics.Dynamic.DRT.LDRS.atLayer {E : Type u_1} (k : LDRS E) (l : Core.Semantics.ContentLayer.ContentLayer) : List (DRSCondition E)

Extract all conditions at a given layer.

Equations

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

def Semantics.Dynamic.DRT.LDRS.toDRSFull {E : Type u_1} (k : LDRS E) : DRSFull E

Project an LDRS to a standard DRS by stripping layer tags.

Equations

• k.toDRSFull = { drefs := k.drefs, conditions := List.map (fun (x : Semantics.Dynamic.DRT.LayeredCondition E) => x.condition) k.conditions }

def Semantics.Dynamic.DRT.DRSFull.toLDRS {E : Type u_1} (k : DRSFull E) : LDRS E

Lift a standard DRS to an LDRS by tagging all conditions as at-issue.

A plain DRS is an LDRS where everything is fr.

Equations

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

theorem Semantics.Dynamic.DRT.LDRS.roundtrip_conditions {E : Type u_1} (k : DRSFull E) : k.toLDRS.toDRSFull.conditions = k.conditions

Round-trip: DRSFull → LDRS → DRSFull preserves conditions.

def Semantics.Dynamic.DRT.LDRS.merge {E : Type u_1} (k1 k2 : LDRS E) : LDRS E

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 {E : Type u_1} (k : LDRS E) (offLayers : List Core.Semantics.ContentLayer.ContentLayer) : List (LayeredCondition E)

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. The non-offensive conditions are resolved normally (forward anaphora into the post-correction context).

Equations

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

def Semantics.Dynamic.DRT.LDRS.survivingConditions {E : Type u_1} (k : LDRS E) (offLayers : List Core.Semantics.ContentLayer.ContentLayer) : List (LayeredCondition E)

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

Equations

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

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

Offensive + surviving = all conditions (partition).

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.merge_monotonic {E : Type u_1} (k1 k2 : LDRS E) : 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 {E : Type u_1} (k : LDRS E) (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.