Docs / Semantics / Dynamic / DRT / Relational

The relational semantics of DRSs

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

This file interprets a DRS as a relation between embeddings. The relation of a DRS relates an input embedding to the outputs that differ from it at most on the universe and verify the DRS. It is the box Update.box of Semantics/Dynamic/RegisterStructure.lean over the universe, at the register structure of embeddings, so Muskens's relational semantics of DRT is the general one of boxes. A DRS is true under an input when some output is related to it.

Main definitions

DRT.DRS.toRel: the relation of a DRS.
DRT.DRS.trueRel: truth, the domain of that relation.

Main statements

DRT.verifies_neg_toRel: complex conditions are the connectives of Update on these relations.
DRT.DRS.toRel_merge: under freshness, merge denotes composition, by Update.box_comp_box.
DRT.DRS.trueRel_iff_exists_verifies: on a reuse-free DRS, truth agrees with partial embeddings.

Implementation notes

Muskens restricts the equivalence of his semantics with the standard one to constructs without constant discourse referents, which the DRSs here do not have.

References

Muskens 1996, Combining Montague semantics and discourse representation formalized
Groenendijk & Stokhof 1991, Dynamic Predicate Logic formalized

The relation of a DRS

The box relation of a DRS (SEM3) is the box over its universe testing its conditions.

def DRS.toRel L52–54

{L : FirstOrder.Language} {V : Type w} {M : Type x} [L.Structure M] [DecidableEq V] (K : DRS L V) :

DynamicSemantics.Update (V → M)

K.toRel = DynamicSemantics.Update.box K.referents {a : V → M | VerifiesTotal a K}

Used by DRS.toRel_iff, DRS.trueRel, DRS.trueRel_iff, verifies_neg_toRel, verifies_imp_toRel, verifies_dis_toRel, DRS.toRel_merge

Used in GroenendijkStokhof1991, Muskens1996

L56–58

A DRS is true under an input embedding a iff some output embedding is related to it, the domain of the box relation.

def DRS.trueRel L60–62

{L : FirstOrder.Language} {V : Type w} {M : Type x} [L.Structure M] [DecidableEq V] (K : DRS L V) (a : V → M) :

Prop

K.trueRel a = (a ∈ SetRel.dom K.toRel)

Built from

Used by DRS.trueRel_iff, DRS.trueRel_iff_exists_extends, DRS.trueRel_iff_realize_toFormula, DRS.dependsOn_trueRel, DRS.trueRel_map, DRS.trueRel_iff_exists_verifies, DRS.trueRel_iff_isTrue

Used in Muskens1996

L64–65

L67–69

The connectives (SEM2)

A negated sub-DRS is the spine's neg of its box relation.

theorem verifies_neg_toRel L73–76

{L : FirstOrder.Language} {V : Type w} {M : Type x} [L.Structure M] [DecidableEq V] (K : DRS L V) (f : V → M) :

VerifiesConditionTotal f (Condition.neg K) ↔ f ∈ K.toRel.neg

Built from

L78–80

L82–84

Truth

L88–91

L93–96

L98–103

The Merging Lemma

When the universe of K₂ is fresh for the conditions of K₁, K₁ ⊕ K₂ denotes the composition of their box relations (the Merging Lemma of §II.2).

theorem DRS.toRel_merge L107–122

{L : FirstOrder.Language} {V : Type w} {M : Type x} [L.Structure M] [DecidableEq V] (K₁ K₂ : DRS L V) (hfresh : Disjoint K₂.referents (Condition.varFinsetL K₁.conditions)) :

(K₁.merge K₂).toRel = SetRel.comp K₁.toRel K₂.toRel

Built from

Agreement with partial embeddings

On a reuse-free DRS, Muskens's relational truth from a total input agrees with the partial semantics from the partial reading of that input.

theorem DRS.trueRel_iff_exists_verifies L126–134

{L : FirstOrder.Language} {V : Type w} {M : Type x} [L.Structure M] [DecidableEq V] {X : Finset V} {K : DRS L V} (hrf : ReuseFreeAt X K) (hfv : K.freeVarFinset ⊆ X) {f : PartialAssign V M} {f' : V → M} (hdom : f.domain = ↑X) (hff' : ∀ x ∈ X, f x = ↑(f' x)) :

K.trueRel f' ↔ ∃ (g : PartialAssign V M), K.Verifies f g

Built from

L136–140