The presheaf of basic DRSs

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.Condition.IsLiteral, DRT.DRS.IsBasic: literal conditions and basic DRSs.
• DRT.Theory.toDRS: the basic DRS of a section.

Main statements

• DRT.Theory.isBasic_toDRS: sections realise as basic DRSs.

References

• [AS14]
• [KR93]

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

A consistent finite set of literals over a context — a basic DRS's conditions, whose deductive closure adds no literals.

• lits : Finset (Literal c)

  The literals held true.

• consistent (l : Literal c) : l ∈ self.lits → l.neg ∉ self.lits

  No literal occurs with both signs.

theorem DRT.Theory.ext_iff {L : FirstOrder.Language} {V : Type w} {c : Context L V} {x y : Theory c} : x = y ↔ x.lits = y.lits

theorem DRT.Theory.ext {L : FirstOrder.Language} {V : Type w} {c : Context L V} {x y : Theory c} (lits : x.lits = y.lits) : x = y

def DRT.Condition.IsLiteral {L : FirstOrder.Language} {V : Type w} : Condition L V → Prop

A literal condition: an atom, or the negation of a one-atom box with no referents.

Equations

• (DRT.Condition.rel R args).IsLiteral = True
• (DRT.Condition.neg K).IsLiteral = (K.referents = ∅ ∧ ∃ (n : ℕ) (R : L.Relations n) (args : Fin n → V), K.conditions = [DRT.Condition.rel R args])
• x✝.IsLiteral = False

def DRT.DRS.IsBasic {L : FirstOrder.Language} {V : Type w} (K : DRS L V) : Prop

A basic DRS: every condition is a literal.

Equations

• K.IsBasic = ∀ d ∈ K.conditions, d.IsLiteral

@[instance_reducible]

instance DRT.Theory.instBot {L : FirstOrder.Language} {V : Type w} {c : Context L V} : Bot (Theory c)

Equations

• DRT.Theory.instBot = { bot := { lits := ∅, consistent := ⋯ } }

@[simp]

theorem DRT.Theory.lits_bot {L : FirstOrder.Language} {V : Type w} {c : Context L V} : ⊥.lits = ∅

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

The basic DRS (X, s) of a section: the context's referents with the literals as conditions.

Equations

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

@[simp]

theorem DRT.Theory.referents_toDRS {L : FirstOrder.Language} {V : Type w} {c : Context L V} (s : Theory c) : s.toDRS.referents = c.vars

theorem DRT.Theory.coe_conditions_toDRS {L : FirstOrder.Language} {V : Type w} {c : Context L V} (s : Theory c) : ↑s.toDRS.conditions = Multiset.map Literal.toCondition s.lits.val

theorem DRT.Theory.isBasic_toDRS {L : FirstOrder.Language} {V : Type w} {c : Context L V} (s : Theory c) : s.toDRS.IsBasic

@[instance_reducible]

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

Equations

• x✝¹.instDecidableEq x✝ = decidable_of_iff (x✝¹.lits = x✝.lits) ⋯

def DRT.Theory.restrict {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

Restriction along a context morphism: F(f)(s) ⊢ ±A(x̄) ⟺ s ⊢ ±A(f(x̄)).

Equations

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

@[simp]

theorem DRT.Theory.mem_restrict {L : FirstOrder.Language} {V : Type w} {c c' : Context L V} [DecidableEq V] [(n : ℕ) → DecidableEq (L.Relations n)] {f : c ⟶ c'} {s : Theory c'} {l : Literal c} : l ∈ (restrict f s).lits ↔ Literal.map f l ∈ s.lits

def DRT.presheaf (L : FirstOrder.Language) (V : Type w) [DecidableEq V] [(n : ℕ) → DecidableEq (L.Relations n)] : CategoryTheory.Functor (Context L V)ᵒᵖ (Type (max v w))

The presheaf of basic DRSs: theories at each context, restriction along context morphisms.

Equations

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

@[simp]

theorem DRT.presheaf_obj {L : FirstOrder.Language} {V : Type w} [DecidableEq V] [(n : ℕ) → DecidableEq (L.Relations n)] (c : (Context L V)ᵒᵖ) : (presheaf L V).obj c = Theory (Opposite.unop c)

@[simp]

theorem DRT.presheaf_map {L : FirstOrder.Language} {V : Type w} [DecidableEq V] [(n : ℕ) → DecidableEq (L.Relations n)] {c c' : (Context L V)ᵒᵖ} (f : c ⟶ c') (s : Theory (Opposite.unop c)) : (CategoryTheory.ConcreteCategory.hom ((presheaf L V).map f)) s = Theory.restrict f.unop s