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 develops basic results about boxes, including renaming, extension, and recursions.

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

@[reducible, inline]

abbrev DRT.Embedding (V : Type w) (M : Type u_5) : Type (max u_5 w)

An embedding function is a function that maps discourse referents to individuals in a model — here total (deviation note in DRS/Verification.lean). Only the model's domain M appears; its interpretation of the relation symbols enters with verification (f.Verifies K, DRS/Verification.lean).

Equations

• DRT.Embedding V M = (V → M)

theorem DRT.Box.sizeOf_lt_of_mem_conditions {V : Type w} {C : Type x} [SizeOf C] {K : Box V C} {c : C} (h : c ∈ K.conditions) : sizeOf c < sizeOf K

A condition of a box is smaller than the box — the recursion measure for definitions descending through the nested condition list.

Functorial action

def DRT.Box.map {V : Type w} {C : Type x} {W : Type u_1} {D : Type u_2} [DecidableEq W] (f : V → W) (g : C → D) (K : Box V C) : Box W D

K.map f g applies f to the universe and g to each condition.

Equations

• DRT.Box.map f g K = { referents := Finset.image f K.referents, conditions := List.map g K.conditions }

theorem DRT.Box.map_wfParam {V : Type w} {C : Type x} {W : Type u_1} {D : Type u_2} [DecidableEq W] {f : V → W} {g : C → D} {K : Box V C} : map f g (wfParam K) = { referents := Finset.image f K.referents, conditions := List.map g (wfParam K.conditions) }

Well-founded recursions may traverse sub-boxes with Box.map: preprocessing re-marks the condition list, exposing · ∈ K.conditions to termination proofs.

@[simp]

theorem DRT.Box.referents_map {V : Type w} {C : Type x} {W : Type u_1} {D : Type u_2} [DecidableEq W] {f : V → W} {g : C → D} {K : Box V C} : (map f g K).referents = Finset.image f K.referents

@[simp]

theorem DRT.Box.conditions_map {V : Type w} {C : Type x} {W : Type u_1} {D : Type u_2} [DecidableEq W] {f : V → W} {g : C → D} {K : Box V C} : (map f g K).conditions = List.map g K.conditions

@[simp]

theorem DRT.Box.map_id {V : Type w} {C : Type x} {K : Box V C} [DecidableEq V] : map id id K = K

@[simp]

theorem DRT.Box.map_id' {V : Type w} {C : Type x} {K : Box V C} [DecidableEq V] : map id (fun (c : C) => c) K = K

theorem DRT.Box.map_congr {V : Type w} {C : Type x} {W : Type u_1} {D : Type u_2} [DecidableEq W] {f : V → W} {g : C → D} {K : Box V C} {f' : V → W} {g' : C → D} {K' : Box V C} (hf : f = f') (hg : ∀ c ∈ K.conditions, g c = g' c) (hK : K = K') : map f g K = map f' g' K'

theorem DRT.Box.map_map {V : Type w} {C : Type x} {W : Type u_1} {D : Type u_2} {E : Type u_3} [DecidableEq W] {f : V → W} {g : C → D} {K : Box V C} {X : Type u_5} [DecidableEq X] {f' : W → X} {g' : D → E} : map f' g' (map f g K) = map (f' ∘ f) (g' ∘ g) K

theorem DRT.Box.map_eq_self {V : Type w} {C : Type x} [DecidableEq V] {g : C → C} {K : Box V C} (h : ∀ c ∈ K.conditions, g c = c) : map id g K = K

theorem DRT.Box.map_map_of_forall {V : Type w} {C : Type x} {W : Type u_1} {D : Type u_2} {E : Type u_3} [DecidableEq W] {g : C → D} {K : Box V C} {X : Type u_5} [DecidableEq X] (f : V → W) (f' : W → X) {g' : D → E} {g'' : C → E} (h : ∀ c ∈ K.conditions, g' (g c) = g'' c) : map f' g' (map f g K) = map (f' ∘ f) g'' K

The extension relation

def DRT.Box.Extends {V : Type w} {C : Type x} {M : Type u_4} (K : Box V C) (f g : Embedding 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