Docs / Semantics / Dynamic / DRT / Sheaf / Context

Contexts, renamings, and literals

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

This file defines the category of contexts of discourse representation theory in its sheaf-theoretic reading: a context is a finite vocabulary of relation symbols together with a finite set of discourse referents, and a morphism is an inclusion of vocabularies with a map of referents — a relabelling, an inclusion, or an identification of referents. Literals over a context are signed atoms; they rename covariantly along context morphisms.

Main definitions

DRT.Context, DRT.Context.Hom: contexts (L, X) and their morphisms, a Category, with the referents functor Context.varsFunctor.
DRT.Literal: literals ±A(x̄) over a context, with Literal.map (renaming), the complementary literal -l, decidable equality and finiteness.
DRT.Literal.functor: literals as a functor to types.
DRT.Literal.Consistent: sets of literals containing no complementary pair.

References

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

Declarations

A context (L, X) pairs a finite vocabulary of relation symbols with a finite set of referents.

structure Context L44–50

(L : FirstOrder.Language) (V : Type w) :

Type (max v w)

vocab : Finset ((n : ℕ) × L.Relations n)
The vocabulary.
vars : Finset V
The referents.

Used by Context.Hom, instCategoryContext, Context.hom_ext, Context.hom_ext_iff, Context.id_map, Context.comp_map, Context.Hom.extend, Context.Hom.extend_coe, Context.varsFunctor, Context.varsFunctor_map, Literal, Literal.equivSigma, Literal.map, Literal.map_id, Literal.map_comp, Literal.map_injective, Literal.instInvolutiveNeg, Literal.pos_neg, Literal.neg_ne_self, Literal.neg_map, Literal.functor, Literal.functor_map, Literal.Consistent, Literal.Consistent.mono, instDecidableEqLiteral, instFintypeLiteral, instDecidableConsistent

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

A context morphism includes the vocabulary and maps the referents.

structure Context.Hom L54–59

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

Type w

incl : c.vocab ⊆ c'.vocab
The vocabulary inclusion.
map : ↥c.vars → ↥c'.vars
The referent map.

Built from

The referent maps make the referents of contexts a functor to types.

def Context.varsFunctor L86–89

(L : FirstOrder.Language) (V : Type w) :

CategoryTheory.Functor (Context L V) (Type w)

Context.varsFunctor L V = { obj := fun (c : Context L V) => ↥c.vars, map := fun {X Y : Context L V} (f : X ⟶ Y) => TypeCat.ofHom f.map, map_id := ⋯, map_comp := ⋯ }