Docs / Semantics / Dynamic / DRT / Sheaf / Presheaf

The presheaf of basic DRSs

import Linglib.Semantics.Dynamic.DRT.Sheaf.Presheaf · namespace DRT

This file defines the presheaf of basic discourse representation structures on the category of contexts: at a context (L, X) its sections are the consistent finite sets of literals over the context, and restriction along a context morphism f is substitution-preimage, F(f)(s) ⊢ ±A(x̄) ⟺ s ⊢ ±A(f(x̄)). A section s at (L, X) is the basic DRS (X, s), which Theory.toDRS realises as a DRS whose conditions are literals.

Main definitions

DRT.Theory: consistent finite sets of literals over a context, with Theory.restrict.
DRT.presheaf: the presheaf (Context L V)ᵒᵖ ⥤ Type.
DRT.Literal.toCondition, DRT.Theory.toDRS: literals as DRS-conditions, sections as basic DRSs.

Main statements

DRT.Literal.toCondition_map: renaming a literal is Condition.map along the extended referent map.
DRT.Theory.isBasic_toDRS: sections realise as basic DRSs.

Implementation notes

Abramsky and Sadrzadeh take the deductive closures of consistent finite sets of literals; in a relational language the closure adds no literal, so a section is the consistent set itself.

References

Abramsky & Sadrzadeh 2014, Semantic Unification: A Sheaf Theoretic Approach to Natural Language formalized
Kamp & Reyle 1993, From Discourse to Logic formalized

Declarations

A theory over a context is a consistent finite set of literals, the conditions of a basic DRS.

structure Theory L51–57

{L : FirstOrder.Language} {V : Type w} (c : Context L V) :

Type (max v w)

lits : Finset (Literal c)
The literals held true.
consistent : Literal.Consistent self.lits
No literal occurs with both signs.

Instances AbramskySadrzadeh2014.instDiscreteMeasurableSpaceTheory_studies, AbramskySadrzadeh2014.instMeasurableSpaceTheory_studies

Used by Theory.instBot, Theory.toDRS, Theory.referents_toDRS, Theory.coe_conditions_toDRS, Theory.isBasic_toDRS, Theory.instDecidableEq, Theory.restrict, Theory.mem_restrict, presheaf_obj, presheaf_map

Used in Semantics/Dynamic/DRT/Sheaf/Gluing, Semantics/Dynamic/DRT/Sheaf/Realizers, AbramskySadrzadeh2014, ChatzikyriakidisEtAl2025

L59–64

L66–67

L69–70

l.toCondition is the atom of l, or for a negative literal the negation of the one-atom box with no referents.

def Literal.toCondition L72–75

{L : FirstOrder.Language} {V : Type w} {c : Context L V} (l : Literal c) :

Condition L V

l.toCondition = if l.pos = true then Condition.atom l.atom else Condition.neg { referents := ∅, conditions := [Condition.atom l.atom] }

Built from

Used by Literal.toCondition_map, Theory.toDRS, Theory.coe_conditions_toDRS

Renaming a literal is Condition.map along the extended referent map.

theorem Literal.toCondition_map L77–81

{L : FirstOrder.Language} {V : Type w} [DecidableEq V] {c c' : Context L V} (f : c ⟶ c') (l : Literal c) :

(map f l).toCondition = Condition.map (Context.Hom.extend f) l.toCondition

Built from

L87

L89

s.toDRS is the basic DRS (X, s), with the context's referents and the literals as conditions.

Theory.toDRS L91–93

noncomputable def DRT.Theory.toDRS {L : FirstOrder.Language} {V : Type w} {c : Context L V} (s : Theory c) :

DRS L V

s.toDRS = { referents := c.vars, conditions := List.map Literal.toCondition s.lits.toList }

Built from ,

Used by Theory.referents_toDRS, Theory.coe_conditions_toDRS, Theory.isBasic_toDRS

Used in Semantics/Dynamic/DRT/Sheaf/Gluing, Semantics/Dynamic/DRT/Sheaf/Realizers

L95

L97–99

theorem Theory.isBasic_toDRS L101–107

{L : FirstOrder.Language} {V : Type w} {c : Context L V} (s : Theory c) :

s.toDRS.IsBasic

Built from , ,

L111

s.restrict f holds ±A(x̄) iff s holds ±A(f(x̄)).

def Theory.restrict L113–116

{L : FirstOrder.Language} {V : Type w} {c c' : Context L V} [DecidableEq V] [(n : ℕ) → DecidableEq (L.Relations n)] (f : c ⟶ c') (s : Theory c') :

Theory c

Theory.restrict f s = { lits := {l : Literal c | Literal.map f l ∈ s.lits}, consistent := ⋯ }

Built from

Used by Theory.mem_restrict, Theory.restrict_bot, presheaf_map

Used in Semantics/Dynamic/DRT/Sheaf/Gluing, Semantics/Dynamic/DRT/Sheaf/Realizers, AbramskySadrzadeh2014

L118–119

L121–122

Basic DRSs form a presheaf on contexts, restricting along context morphisms.

def presheaf L128–131

(L : FirstOrder.Language) (V : Type w) [DecidableEq V] [(n : ℕ) → DecidableEq (L.Relations n)] :

CategoryTheory.Functor (Context L V)ᵒᵖ (Type (max v w))

The definition is too large to print here; read it in the source.

Used by presheaf_obj, presheaf_map

Used in Semantics/Dynamic/DRT/Sheaf/Gluing, AbramskySadrzadeh2014, ChatzikyriakidisEtAl2025

L135

L137–138