Docs / Semantics / Dynamic / DRT / Syntax

Discourse representation structures

import Linglib.Semantics.Dynamic.DRT.Syntax · namespace DRT

A discourse representation structure (DRS) pairs a finite set of discourse referents, its universe, with a list of conditions on them. A condition is atomic, an atom of a FirstOrder.Language or an equation between referents, or complex, a negation, conditional or disjunction of sub-DRSs, so DRSs and conditions are defined by simultaneous recursion. This file defines both, together with their syntactic theory: merge, renaming, occurring and free referents, and properness.

Main definitions

DRT.DRS, DRT.Condition: DRSs and conditions over a language L and referent type V.
DRT.DRS.merge, DRT.DRS.map: the merge of two DRSs, and renaming along f : V → W.
DRT.DRS.varFinset, DRT.DRS.freeVarFinset: occurring and free referents.
DRT.DRS.IsProper: no free referent.

Implementation notes

DRS is a structure in a mutual block with Condition, since Kamp and Reyle define the two by simultaneous recursion. Being recursive, it has no definitional eta, so a proof about a variable DRS that must unfold a recursive definition starts from cases K.
referents is the textbook universe U: universe is a Lean keyword and univ collides with Finset.univ. conditions is a List, since an inductive cannot nest through Finset or Multiset; set semantics is recovered by the interpretation (verifiesTotal_perm).
Renaming and occurring and free referents are each three mutually recursive functions, on DRSs, conditions and condition lists, by structural recursion through the nesting, so the kernel evaluates them and decide settles them on concrete DRSs.
DRT is the owning namespace, on the FirstOrder.Language pattern.

References

Kamp & Reyle 1993, From Discourse to Logic formalized
Muskens 1996, Combining Montague semantics and discourse representation formalized

Declarations

A discourse representation structure pairs a universe of discourse referents, the objects under discussion, with the conditions that record what has been said of them. These are the finite DRSs of Def. 1.5.1. Def. 1.4.1 lets both components be infinite, which Kamp and Reyle set aside for the rest of the volume (p. 128).

structure DRS L54–62

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

Type (max v w)

referents : Finset V
The universe U: the discourse referents the DRS introduces.
conditions : List (Condition L V)
The conditions of the DRS.

Built from

Used by Condition, DRS.empty, DRS.instInhabited, DRS.merge, DRS.referents_merge, DRS.conditions_merge, Condition.induction, DRS.map, DRS.referents_map, DRS.conditions_map, DRS.map_id, DRS.map_map, DRS.varFinset, DRS.freeVarFinset, Condition.varFinset_neg, Condition.varFinset_imp, Condition.varFinset_dis, Condition.freeVarFinset_neg, Condition.freeVarFinset_imp, Condition.freeVarFinset_dis, DRS.varFinset_eq, DRS.referents_subset_varFinset, DRS.varFinsetL_subset_varFinset, DRS.freeVarFinset_eq, DRS.coe_freeVarFinset, DRS.freeVarFinset_subset_iff, DRS.freeVarFinset_subset_varFinset, DRS.empty_merge, DRS.merge_empty, DRS.merge_assoc, DRS.freeVarFinset_merge_subset, DRS.IsProper, DRS.instDecidableIsProper, DRS.isProper_merge

Used in Semantics/Dynamic/DRT/Accessibility, Semantics/Dynamic/DRT/ContextChange, Semantics/Dynamic/DRT/Relational, Semantics/Dynamic/DRT/Sheaf/Presheaf, Semantics/Dynamic/DRT/Translation and 7 more

A DRS-condition is atomic, an atom or an equation, or complex, a negation (Def. 1.4.1) or a conditional or disjunction (Chapter 2). Sub-DRSs occur only inside complex conditions.

inductive Condition L64–76

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

Type (max v w)

atom {L : FirstOrder.Language} {V : Type w} (a : L.Atom V) : Condition L V
The atomic condition of an atom over the referents.
eq {L : FirstOrder.Language} {V : Type w} (u v : V) : Condition L V
Atomic equality condition u = v.
neg {L : FirstOrder.Language} {V : Type w} (K : DRS L V) : Condition L V
Complex condition ¬K.
imp {L : FirstOrder.Language} {V : Type w} (ante cons : DRS L V) : Condition L V
Complex condition K₁ ⇒ K₂ (antecedent ⇒ consequent).
dis {L : FirstOrder.Language} {V : Type w} (left right : DRS L V) : Condition L V
Complex condition K₁ ∨ K₂.

Built from

Used in Semantics/Dynamic/DRT/Accessibility, Semantics/Dynamic/DRT/Sheaf/Presheaf, Semantics/Dynamic/DRT/Translation, Semantics/Dynamic/DRT/Verification/Partial, Semantics/Dynamic/DRT/Verification/Total and 2 more

L82–83

L85

The merge K₁ ⊕ K₂ unions the referents and appends the conditions — Muskens 1996's compositional operation (Kamp & Reyle combine DRSs incrementally via the construction algorithm instead). An operation, not a syntactic constructor.

def DRS.merge L87–92

{L : FirstOrder.Language} {V : Type w} [DecidableEq V] (K₁ K₂ : DRS L V) :

DRS L V

K₁.merge K₂ = { referents := K₁.referents ∪ K₂.referents, conditions := K₁.conditions ++ K₂.conditions }

Built from

Used by DRS.referents_merge, DRS.conditions_merge, DRS.empty_merge, DRS.merge_empty, DRS.merge_assoc, DRS.freeVarFinset_merge_subset, DRS.isProper_merge

Used in Semantics/Dynamic/DRT/ContextChange, Semantics/Dynamic/DRT/Relational, Semantics/Dynamic/DRT/Verification/Partial, Semantics/Dynamic/DRT/Verification/Total, KampReyle1993 and 1 more

Renaming

K.map f renames the discourse referents of K along f.

def DRS.map L127–129

{L : FirstOrder.Language} {V : Type w} {W : Type x} [DecidableEq W] (f : V → W) :

DRS L V → DRS L W

DRS.map f { referents := U, conditions := cs } = { referents := Finset.image f U, conditions := Condition.mapList f cs }

Built from ,

Used by Condition.map, DRS.referents_map, DRS.conditions_map, DRS.map_id, DRS.map_map

Used in Semantics/Dynamic/DRT/Relational, Semantics/Dynamic/DRT/Sheaf/Gluing, Semantics/Dynamic/DRT/Verification/Total

Occurring and free referents

The occurring referents of a DRS are its universe and those of its conditions.

def DRS.varFinset L215–217

{L : FirstOrder.Language} {V : Type w} [DecidableEq V] :

DRS L V → Finset V

{ referents := U, conditions := cs }.varFinset = U ∪ Condition.varFinsetL cs

Built from ,

Used by Condition.varFinset, Condition.varFinset_neg, Condition.varFinset_imp, Condition.varFinset_dis, DRS.varFinset_mk, DRS.varFinset_eq, DRS.referents_subset_varFinset, DRS.varFinsetL_subset_varFinset, DRS.freeVarFinset_subset_varFinset

Used in Semantics/Dynamic/DRT/Verification/Partial, Maier2015

L218–225

L226–229

The free discourse referents of a DRS occur in its conditions and are bound neither by its universe nor by an ancestor reachable "left and up" (the antecedent of a ⇒ threads its referents into the consequent). K.freeVarFinset ⊆ b says every referent of K is bound in context b.

def DRS.freeVarFinset L233–238