Contexts, renamings, and literals

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, and each one is a DRS-condition.

This is the substitution category on contexts, complementary to the extension category DRT.Ctx whose morphisms are DRSs composed by merge: Ctx grows a context by introducing referents, Context maps referents between contexts.

Main definitions

• DRT.Context, DRT.Context.Hom: contexts (L, X) and their morphisms, a Category.
• DRT.Literal: literals ±A(x̄) over a context, with Literal.map (renaming), Literal.neg, decidable equality and finiteness.
• DRT.Literal.toCondition: a literal as a DRS-condition — an atom, or a negated one-atom box.

Main statements

• DRT.Literal.toCondition_map: renaming a literal along a context morphism is Condition.map along any extension of the morphism to the referent type.

References

• [AS14]
• [KR93]

structure DRT.Context (L : FirstOrder.Language) (V : Type w) : Type (max v w)

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

• vocab : Finset ((n : ℕ) × L.Relations n)

  The vocabulary.

• vars : Finset V

  The referents.

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

A context morphism: an inclusion of vocabularies together with a map of referents.

• incl : c.vocab ⊆ c'.vocab

  The vocabulary inclusion.

• map : ↥c.vars → ↥c'.vars

  The referent map.

@[instance_reducible]

instance DRT.instCategoryContext {L : FirstOrder.Language} {V : Type w} : CategoryTheory.Category.{w, max w v} (Context L V)

Equations

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

structure DRT.Literal {L : FirstOrder.Language} {V : Type w} (c : Context L V) : Type (max v w)

A literal over a context: a signed atomic formula ±A(x̄).

• rel : ↥c.vocab

  The relation symbol.

• args : Fin (↑self.rel).fst → ↥c.vars

  The argument referents.

• pos : Bool

  The sign.

def DRT.Literal.equivSigma {L : FirstOrder.Language} {V : Type w} (c : Context L V) : Literal c ≃ (r : ↥c.vocab) × (Fin (↑r).fst → ↥c.vars) × Bool

Literals as dependent triples.

Equations

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

def DRT.Literal.map {L : FirstOrder.Language} {V : Type w} {c c' : Context L V} (f : c ⟶ c') (l : Literal c) : Literal c'

Renaming along a context morphism.

Equations

• DRT.Literal.map f l = { rel := ⟨↑l.rel, ⋯⟩, args := f.map ∘ l.args, pos := l.pos }

@[simp]

theorem DRT.Literal.map_id {L : FirstOrder.Language} {V : Type w} {c : Context L V} (l : Literal c) : map (CategoryTheory.CategoryStruct.id c) l = l

@[simp]

theorem DRT.Literal.map_comp {L : FirstOrder.Language} {V : Type w} {c c' c'' : Context L V} (f : c ⟶ c') (g : c' ⟶ c'') (l : Literal c) : map (CategoryTheory.CategoryStruct.comp f g) l = map g (map f l)

theorem DRT.Literal.map_injective {L : FirstOrder.Language} {V : Type w} {c c' : Context L V} {f : c ⟶ c'} (hf : Function.Injective f.map) : Function.Injective (map f)

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

The complementary literal.

Equations

• l.neg = { rel := l.rel, args := l.args, pos := !l.pos }

@[simp]

theorem DRT.Literal.neg_neg {L : FirstOrder.Language} {V : Type w} {c : Context L V} (l : Literal c) : l.neg.neg = l

@[simp]

theorem DRT.Literal.neg_map {L : FirstOrder.Language} {V : Type w} {c c' : Context L V} (f : c ⟶ c') (l : Literal c) : (map f l).neg = map f l.neg

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

The literal as a DRS-condition: an atom, or for a negative literal the negation of the one-atom box with no referents.

Equations

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

theorem DRT.Literal.toCondition_map {L : FirstOrder.Language} {V : Type w} {c c' : Context L V} [DecidableEq V] (f : c ⟶ c') (g : V → V) (hg : ∀ (t : ↥c.vars), g ↑t = ↑(f.map t)) (l : Literal c) : (map f l).toCondition = Condition.map g l.toCondition

Renaming a literal along f is Condition.map along any extension of f to the referent type.

@[instance_reducible]

instance DRT.instDecidableEqLiteral {L : FirstOrder.Language} {V : Type w} [DecidableEq V] [(n : ℕ) → DecidableEq (L.Relations n)] (c : Context L V) : DecidableEq (Literal c)

Equations

• DRT.instDecidableEqLiteral c l l' = decidable_of_iff (↑l.rel = ↑l'.rel ∧ List.ofFn l.args = List.ofFn l'.args ∧ l.pos = l'.pos) ⋯

@[instance_reducible]

instance DRT.instFintypeLiteral {L : FirstOrder.Language} {V : Type w} (c : Context L V) : Fintype (Literal c)

Equations

• DRT.instFintypeLiteral c = Fintype.ofEquiv ((r : ↥c.vocab) × (Fin (↑r).fst → ↥c.vars) × Bool) (DRT.Literal.equivSigma c).symm