DRT's category of contexts

Well-formed DRSs are the morphisms of a category whose objects are contexts (bases of discourse referents): a morphism X ⟶ Y is a DRS whose free referents are supplied by X (the referential presupposition), whose occurring referents are visible — declared in the context or introduced by the DRS itself — and whose introductions are fresh for the context, growing X to Y. Composition is merge; identity is the empty DRS.

The visibility invariant derives the Merging Lemma's capture-freshness side condition, so composition needs no hypotheses. Interpretation (Ctx.sem) is an identity-on-objects functor into the semantic category of contexts DynamicSemantics.Ctx, functorial on composition by the Merging Lemma (DRS.transition_merge).

Main definitions

• DRT.Ctx L V: contexts, with well-formed DRSs as morphisms and merge as composition.
• DRT.Ctx.sem: interpretation as a functor into DynamicSemantics.Ctx W M V, given a model of the language.

Implementation notes

This is a syntactic category in the sense of categorical logic (objects are declarations of variables, type theory's bases, cf. [Vis98]), and the context-under-merge category of [VV96]'s bracketing approach ([MvBV11]'s m-categories). DRT.Ctx and DynamicSemantics.Ctx name the two levels of DRT's architecture, not rival theories: contexts compose by merging boxes at the representation level and by relational composition of transitions at the semantic level.

References

• [VV96], [Vis98], [muskens-1996] (the merge algebra and context typing)
• [KvGR11], [KR93]

structure DRT.Ctx (L : FirstOrder.Language) (V : Type w) : Type w

An object of DRT's category of contexts: a base of discourse referents available in the context.

• base : Finset V

  The available discourse referents.

theorem DRT.Ctx.ext_iff {L : FirstOrder.Language} {V : Type w} {x y : Ctx L V} : x = y ↔ x.base = y.base

theorem DRT.Ctx.ext {L : FirstOrder.Language} {V : Type w} {x y : Ctx L V} (base : x.base = y.base) : x = y

structure DRT.Ctx.Hom {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (X Y : Ctx L V) : Type (max v w)

A morphism X ⟶ Y: a DRS whose free referents are supplied by X, whose occurring referents are visible, and whose fresh introductions grow X to Y.

• drs : DRS L V

  The underlying DRS.

• presup : self.drs.freeVarFinset ⊆ X.base

  The referential presupposition: free referents are supplied by the context.

• varFinsetL_le : Condition.varFinsetL self.drs.conditions ⊆ X.base ∪ self.drs.referents

  Visibility: every occurring referent is contextual or introduced.

• fresh : Disjoint X.base self.drs.referents

  Introductions are fresh for the context.

• target : X.base ∪ self.drs.referents = Y.base

  The context grows by the introduced referents.

theorem DRT.Ctx.Hom.ext {L : FirstOrder.Language} {V : Type w} {inst✝ : DecidableEq V} {X Y : Ctx L V} {x y : X.Hom Y} (drs : x.drs = y.drs) : x = y

theorem DRT.Ctx.Hom.ext_iff {L : FirstOrder.Language} {V : Type w} {inst✝ : DecidableEq V} {X Y : Ctx L V} {x y : X.Hom Y} : x = y ↔ x.drs = y.drs

@[instance_reducible]

instance DRT.Ctx.instCategory {L : FirstOrder.Language} {V : Type w} [DecidableEq V] : CategoryTheory.Category.{max v w, w} (Ctx L V)

Equations

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

@[simp]

theorem DRT.Ctx.drs_id {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (X : Ctx L V) : (CategoryTheory.CategoryStruct.id X).drs = DRS.empty

@[simp]

theorem DRT.Ctx.drs_comp {L : FirstOrder.Language} {V : Type w} [DecidableEq V] {X Y Z : Ctx L V} (u : X ⟶ Y) (v : Y ⟶ Z) : (CategoryTheory.CategoryStruct.comp u v).drs = u.drs.merge v.drs

def DRT.Ctx.sem {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (W : Type u_1) (M : Type u_2) [L.Structure M] [Nonempty M] : CategoryTheory.Functor (Ctx L V) (DynamicSemantics.Ctx W M V)

Interpretation is a functor: a model of L sends DRT's category of contexts to the semantic one, identically on objects and a DRS to its transition — and functoriality on composition is the Merging Lemma, its capture-freshness side condition derived from the visibility invariant.

Equations

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