Discourse representation structures

A discourse representation structure (DRS) pairs a finite set of discourse referents, Kamp and Reyle's universe U, with a list of conditions on them (Def. 1.4.1). A condition is atomic, an atom of a FirstOrder.Language or an equation between referents, or complex, a negation or the conditional and binary disjunction of Chapter 2, and sub-DRSs occur only inside complex conditions. Muskens draws a DRS as a box [u₁ … uₙ | γ₁ … γₘ]. Verification and truth are in DRS/Verification.lean, the structural theory in DRS/Basic.lean.

Main declarations

• Condition, DRS: conditions and DRSs over a language L and referent type V; DRS L V is the generic container Box (DRS/Box.lean) instantiated at Condition L V.
• DRS.merge: the merge ⊕, which unions the referents and appends the conditions.
• DirectlySubordinate, Subordinate, WeakSubordinate: immediate subordination and its transitive and reflexive-transitive closures (Def. 1.4.10, Def. 2.1.2). Accessibility is read off occurrences and lives in DRS/Accessibility.lean.

Main statements

• WeakSubordinate.antisymm: weak subordination is a partial order.

Implementation notes

• referents is the textbook U; universe is a Lean keyword and univ collides with Finset.univ.
• Box is a container structure the condition syntax nests through, and DRS its instantiation at Condition L V — Def. 1.4.1's simultaneous recursion without a mutual block, keeping the structure API.
• conditions is a List, since an inductive cannot nest through Finset/Multiset; set semantics is recovered by the interpretation (verifies_perm, DRS/Verification.lean).
• DRT is the owning namespace, on the FirstOrder.Language pattern.

References

• [KR93]
• [Mus96]

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

A DRS-condition is atomic, an atom or an equation, or complex, a negation (Def. 1.4.1) or a conditional or disjunction (Chapter 2). Sub-DRSs occur only inside complex conditions.

• atom {L : FirstOrder.Language} {V : Type w} (a : L.Atom V) : Condition L V

  The atomic condition of an atom over the referents.

• 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 : Box V (Condition L V)) : Condition L V

  Complex condition ¬K.

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

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

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

  Complex condition K₁ ∨ K₂.

@[reducible, inline]

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

A discourse representation structure pairs a universe of discourse referents, the objects under discussion, with the conditions that record what has been said of them (Def. 1.4.1).

Equations

• DRT.DRS L V = DRT.Box V (DRT.Condition L V)

@[simp]

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

@[simp]

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

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

The empty DRS ⟨∅, []⟩.

Equations

• DRT.DRS.empty = { referents := ∅, conditions := [] }

@[instance_reducible]

instance DRT.DRS.instInhabited {L : FirstOrder.Language} {V : Type w} : Inhabited (DRS L V)

Equations

• DRT.DRS.instInhabited = { default := DRT.DRS.empty }

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

The merge K₁ ⊕ K₂ unions the referents and appends the conditions — [Mus96]'s compositional operation (Kamp & Reyle combine DRSs incrementally via the construction algorithm instead). An operation, not a syntactic constructor.

Equations

• K₁.merge K₂ = { referents := K₁.referents ∪ K₂.referents, conditions := K₁.conditions ++ K₂.conditions }

@[simp]

theorem DRT.DRS.referents_merge {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.conditions_merge {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (K₁ K₂ : DRS L V) : (K₁.merge K₂).conditions = K₁.conditions ++ K₂.conditions

theorem DRT.Condition.induction {L : FirstOrder.Language} {V : Type w} {motive : Condition L V → Prop} (atom : ∀ (a : L.Atom V), motive (atom a)) (eq : ∀ (u v : V), motive (eq u v)) (neg : ∀ (K : Box V (Condition L V)), (∀ c ∈ K.conditions, motive c) → motive (neg K)) (imp : ∀ (a c : Box V (Condition L V)), (∀ d ∈ a.conditions, motive d) → (∀ d ∈ c.conditions, motive d) → motive (imp a c)) (dis : ∀ (l r : Box V (Condition L V)), (∀ d ∈ l.conditions, motive d) → (∀ d ∈ r.conditions, motive d) → motive (dis l r)) (c : Condition L V) : motive c

Induction on conditions descends into sub-boxes, handling each constructor given the motive for every condition of its sub-boxes.

Subordination

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

DirectlySubordinate K' K says K' is a sub-box of one of K's conditions, by the neg case of Def. 1.4.10(i), the ⇒ cases of Def. 2.1.2 (which subordinates both components of a conditional to the containing DRS), and the ∨ cases of Def. 2.4.3(i)(c), where no disjunct is subordinate to another. It is a relation on DRS values, where the textbook's is on box occurrences. Every clause pins the containing box in its conclusion, since an unpinned clause (such as consequent-below-antecedent) would hold of every pair of DRSs via a manufactured container. The ⇒ visibility asymmetry is not subordination but accessibility (DRS/Accessibility.lean).

• neg {L : FirstOrder.Language} {V : Type w} {D K : DRS L V} : Condition.neg K ∈ D.conditions → DirectlySubordinate K D

  The body of a ¬ is directly subordinate to the containing DRS.

• impAnte {L : FirstOrder.Language} {V : Type w} {D a c : DRS L V} : Condition.imp a c ∈ D.conditions → DirectlySubordinate a D

  The antecedent of a ⇒ is directly subordinate to the containing DRS.

• impCons {L : FirstOrder.Language} {V : Type w} {D a c : DRS L V} : Condition.imp a c ∈ D.conditions → DirectlySubordinate c D

  The consequent of a ⇒ is directly subordinate to the containing DRS.

• disL {L : FirstOrder.Language} {V : Type w} {D l r : DRS L V} : Condition.dis l r ∈ D.conditions → DirectlySubordinate l D

  The left disjunct of a ∨ is directly subordinate to the containing DRS.

• disR {L : FirstOrder.Language} {V : Type w} {D l r : DRS L V} : Condition.dis l r ∈ D.conditions → DirectlySubordinate r D

  The right disjunct of a ∨ is directly subordinate to the containing DRS.

@[reducible, inline]

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

Subordinate is the < of Def. 1.4.10(ii), the transitive closure of DirectlySubordinate.

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

WeakSubordinate is the ≤ of Def. 1.4.10(ii), the reflexive-transitive closure of DirectlySubordinate.

Equations

• DRT.WeakSubordinate = Relation.ReflTransGen DRT.DirectlySubordinate

theorem DRT.DirectlySubordinate.sizeOf_lt {L : FirstOrder.Language} {V : Type w} {K' K : DRS L V} (h : DirectlySubordinate K' K) : sizeOf K' < sizeOf K

A directly subordinate DRS is a structurally smaller value.

theorem DRT.Subordinate.sizeOf_lt {L : FirstOrder.Language} {V : Type w} {K' K : DRS L V} (h : Subordinate K' K) : sizeOf K' < sizeOf K

Subordinate DRSs are structurally smaller; subordination chains terminate.

theorem DRT.Subordinate.irrefl {L : FirstOrder.Language} {V : Type w} (K : DRS L V) : ¬Subordinate K K

theorem DRT.WeakSubordinate.antisymm {L : FirstOrder.Language} {V : Type w} {K' K : DRS L V} (h : WeakSubordinate K' K) (h' : WeakSubordinate K K') : K' = K

Weak subordination is a partial order on DRS values.