The DRT box

In discourse representation theory, a box contains two pieces of information: a universe of discourse referents, and a set of conditions recording what has been established about them. Boxes can be nested, and different theories instantiate conditions in different ways ([VBHB18]; [Liu21]). This file defines boxes and the extension relation of a box, between embeddings that agree off its universe.

Implementation notes

An embedding of discourse referents into a model is a total function V → M; the textbook's are partial, so a sub-box extends its input on its universe, rendered here as agreement off the universe (Box.Extends).

structure DRT.Box (V : Type w) (C : Type x) : Type (max w x)

A DRT box, generic over the condition type C; DRS instantiates C at Condition L V.

• referents : Finset V

  The universe U: the discourse referents the box introduces.

• conditions : List C

  The box's conditions.

theorem DRT.Box.ext {V : Type w} {C : Type x} {x y : Box V C} (referents : x.referents = y.referents) (conditions : x.conditions = y.conditions) : x = y

theorem DRT.Box.ext_iff {V : Type w} {C : Type x} {x y : Box V C} : x = y ↔ x.referents = y.referents ∧ x.conditions = y.conditions

The extension relation

def DRT.Box.Extends {V : Type w} {C : Type x} {M : Type u_1} (K : Box V C) (f g : V → M) : Prop

K.Extends f g (written f [K] g) if the output embedding g differs from the input f at most on K's universe — the total-assignment rendering of "f ⊆ g and Dom g = Dom f ∪ U_K".

Equations

• K.Extends f g = ∀ x ∉ K.referents, g x = f x

theorem DRT.Box.Extends.refl {V : Type w} {C : Type x} {M : Type u_1} (K : Box V C) (f : V → M) : K.Extends f f

theorem DRT.Box.extends_piecewise {V : Type w} {C : Type x} {M : Type u_1} [DecidableEq V] (K : Box V C) (f g : V → M) : K.Extends f (K.referents.piecewise g f)

f extends to the embedding taking g's values on the universe.

theorem DRT.Box.eqOn_piecewise_of_extends {V : Type w} {C : Type x} {M : Type u_1} {K : Box V C} {f₁ f₂ g : V → M} [DecidableEq V] (h₁ : K.Extends f₁ g) {S : Set V} (h : Set.EqOn f₁ f₂ (S \ ↑K.referents)) : Set.EqOn g (K.referents.piecewise g f₂) S

theorem DRT.Box.exists_extends_imp {V : Type w} {C : Type x} {M : Type u_1} {f₁ f₂ : V → M} [DecidableEq V] (K : Box V C) {S : Set V} {P : (V → M) → Prop} (hP : ∀ (g g' : V → M), Set.EqOn g g' S → P g → P g') (h : Set.EqOn f₁ f₂ (S \ ↑K.referents)) : (∃ (g : V → M), K.Extends f₁ g ∧ P g) → ∃ (g : V → M), K.Extends f₂ g ∧ P g

Some K-extension of the input satisfies P whenever one of another input does, if the inputs agree off the universe wherever P looks.

theorem DRT.Box.exists_extends_congr {V : Type w} {C : Type x} {M : Type u_1} {f₁ f₂ : V → M} [DecidableEq V] (K : Box V C) {S : Set V} {P : (V → M) → Prop} (hP : ∀ (g g' : V → M), Set.EqOn g g' S → P g → P g') (h : Set.EqOn f₁ f₂ (S \ ↑K.referents)) : (∃ (g : V → M), K.Extends f₁ g ∧ P g) ↔ ∃ (g : V → M), K.Extends f₂ g ∧ P g

theorem DRT.Box.forall_extends_imp {V : Type w} {C : Type x} {M : Type u_1} {f₁ f₂ : V → M} [DecidableEq V] (K : Box V C) {S : Set V} {P : (V → M) → Prop} (hP : ∀ (g g' : V → M), Set.EqOn g g' S → P g → P g') (h : Set.EqOn f₁ f₂ (S \ ↑K.referents)) : (∀ (g : V → M), K.Extends f₁ g → P g) → ∀ (g : V → M), K.Extends f₂ g → P g

Every K-extension of the input satisfies P whenever every one of another input does, if the inputs agree off the universe wherever P looks.

theorem DRT.Box.forall_extends_congr {V : Type w} {C : Type x} {M : Type u_1} {f₁ f₂ : V → M} [DecidableEq V] (K : Box V C) {S : Set V} {P : (V → M) → Prop} (hP : ∀ (g g' : V → M), Set.EqOn g g' S → P g → P g') (h : Set.EqOn f₁ f₂ (S \ ↑K.referents)) : (∀ (g : V → M), K.Extends f₁ g → P g) ↔ ∀ (g : V → M), K.Extends f₂ g → P g