Discourse Representation Structures (faithful, model-theoretic core)

[KR93]

A faithful Lean model of the canonical DRS data type, built on mathlib's FirstOrder.Language so its semantics can be given model-theoretically (via FirstOrder.Language.Structure / Realize), exactly as Kamp & Reyle define it (verifying embeddings into a model, Def. 1.4.4–1.4.5).

A DRS is a pair ⟨referents, conditions⟩ (Def. 1.4.1): referents is the universe U — a finite set of discourse referents — and conditions a collection of DRS-conditions. Conditions are atomic (rel, eq) or complex (neg, imp, dis); sub-DRSs occur only inside complex conditions. Relation symbols come arity-indexed from a FirstOrder.Language.

Main declarations

• DRS L V, Condition L V — the mutual data type over a language L (relation signature) and discourse-referent type V.
• DRS.merge — the ⊕ operation (set-union referents, concatenate conditions).
• DirectlySubordinate, Subordinate, WeakSubordinate — immediate subordination (Def. 1.4.10(i), extended to ⇒/∨ in Ch. 2) and its Relation.TransGen / ReflTransGen closures (Def. 1.4.10(ii)). Accessibility (Def. 1.4.11) is host-relative and lives in DRS/Basic.lean (accessibleFrom).

Implementation notes

• referents is the textbook "universe U"; named for its contents because universe is a Lean keyword and univ collides with Finset.univ.
• The recursive conditions field is a List: Lean forbids nesting an inductive through Finset/Multiset. Set semantics are imposed by the interpretation.
• The namespace is transitional DRT while the legacy _root_.DRS is migrated out; it promotes to the root namespace once the legacy type is retired.

inductive DRT.DRS (L : FirstOrder.Language) (V : Type w) : Type (max v w)

A discourse representation structure: the pair ⟨referents, conditions⟩ ([KR93], Def. 1.4.1). referents is the universe U (a finite set of discourse referents); conditions the DRS-conditions.

• mk {L : FirstOrder.Language} {V : Type w} (referents : Finset V) (conditions : List (Condition L V)) : DRS L V

inductive DRT.Condition (L : FirstOrder.Language) (V : Type w) : Type (max v w)

A DRS-condition ([KR93], Def. 1.4.1): atomic (rel, eq) or complex (neg, imp, dis). Sub-DRSs occur only inside complex conditions.

• rel {L : FirstOrder.Language} {V : Type w} {n : ℕ} (R : L.Relations n) (args : Fin n → V) : Condition L V

  Atomic condition: n-ary relation symbol R applied to referents args.

• eq {L : FirstOrder.Language} {V : Type w} (u v : V) : Condition L V

  Atomic equality condition u = v.

• neg {L : FirstOrder.Language} {V : Type w} (K : DRS L V) : Condition L V

  Complex condition ¬K.

• imp {L : FirstOrder.Language} {V : Type w} (ante cons : DRS L V) : Condition L V

  Complex condition K₁ ⇒ K₂ (antecedent ⇒ consequent).

• dis {L : FirstOrder.Language} {V : Type w} (left right : DRS L V) : Condition L V

  Complex condition K₁ ∨ K₂.

def DRT.DRS.referents {L : FirstOrder.Language} {V : Type w} : DRS L V → Finset V

The referents (universe U) of a DRS — the discourse referents it introduces.

Equations

• (DRT.DRS.mk u conditions).referents = u

def DRT.DRS.conditions {L : FirstOrder.Language} {V : Type w} : DRS L V → List (Condition L V)

The conditions of a DRS.

Equations

• (DRT.DRS.mk u conditions).conditions = conditions

@[simp]

theorem DRT.DRS.referents_mk {L : FirstOrder.Language} {V : Type w} (u : Finset V) (c : List (Condition L V)) : (mk u c).referents = u

@[simp]

theorem DRT.DRS.conditions_mk {L : FirstOrder.Language} {V : Type w} (u : Finset V) (c : List (Condition L V)) : (mk u c).conditions = c

def DRT.DRS.empty {L : FirstOrder.Language} {V : Type w} : DRS L V

The empty DRS ⟨∅, []⟩.

Equations

• DRT.DRS.empty = DRT.DRS.mk ∅ []

def DRT.DRS.merge {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (K₁ K₂ : DRS L V) : DRS L V

Merge ⊕: set-union the referents, concatenate the conditions. The binary DRS merge is [Mus96]'s compositional operation — Kamp & Reyle themselves combine DRSs incrementally via the construction algorithm, not a symmetric binary ⊕. An operation, not a syntactic constructor.

Equations

• K₁.merge K₂ = DRT.DRS.mk (K₁.referents ∪ K₂.referents) (K₁.conditions ++ K₂.conditions)

@[simp]

theorem DRT.DRS.merge_referents {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (K₁ K₂ : DRS L V) : (K₁.merge K₂).referents = K₁.referents ∪ K₂.referents

@[simp]

theorem DRT.DRS.merge_conditions {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (K₁ K₂ : DRS L V) : (K₁.merge K₂).conditions = K₁.conditions ++ K₂.conditions

Subordination and accessibility

inductive DRT.DirectlySubordinate {L : FirstOrder.Language} {V : Type w} : DRS L V → DRS L V → Prop

One-step subordination ("K' is directly subordinate to K"). The neg case is [KR93] Def. 1.4.10(i); the ⇒/∨ cases are its Chapter 2 extension:

• the body of a ¬ is subordinate to the containing DRS;
• the antecedent of a ⇒ is subordinate to the containing DRS;
• the consequent of a ⇒ is subordinate to its antecedent (the ⇒ asymmetry: antecedent referents are accessible in the consequent, not conversely);
• each disjunct of a ∨ is subordinate to the containing DRS.

• neg {L : FirstOrder.Language} {V : Type w} {D K : DRS L V} : Condition.neg K ∈ D.conditions → DirectlySubordinate K D
• impAnte {L : FirstOrder.Language} {V : Type w} {D a c : DRS L V} : Condition.imp a c ∈ D.conditions → DirectlySubordinate a D
• impCons {L : FirstOrder.Language} {V : Type w} {D a c : DRS L V} : Condition.imp a c ∈ D.conditions → DirectlySubordinate c a
• disL {L : FirstOrder.Language} {V : Type w} {D l r : DRS L V} : Condition.dis l r ∈ D.conditions → DirectlySubordinate l D
• disR {L : FirstOrder.Language} {V : Type w} {D l r : DRS L V} : Condition.dis l r ∈ D.conditions → DirectlySubordinate r D

@[reducible, inline]

abbrev DRT.Subordinate {L : FirstOrder.Language} {V : Type w} : DRS L V → DRS L V → Prop

K₁ < K₂: subordinate — transitive closure of DirectlySubordinate ([KR93], Def. 1.4.10(ii)).

Equations

• DRT.Subordinate = Relation.TransGen DRT.DirectlySubordinate

@[reducible, inline]

abbrev DRT.WeakSubordinate {L : FirstOrder.Language} {V : Type w} : DRS L V → DRS L V → Prop

K₁ ≤ K₂: weakly subordinate — reflexive-transitive closure ([KR93]; the ≤ of Def. 1.4.10).

Equations

• DRT.WeakSubordinate = Relation.ReflTransGen DRT.DirectlySubordinate