Docs / Semantics / Dynamic / DRT / Verification / Partial

Verification by partial embeddings

import Linglib.Semantics.Dynamic.DRT.Verification.Partial · namespace DRT

Source

This file defines verification in Kamp and Reyle's form. A pair of partial embeddings verifies a DRS when the output extends the input by exactly the universe of the DRS and verifies its conditions, an atomic condition requiring its referents to be valued. A DRS is true in a model when an embedding of its universe verifies it from the empty input. On DRSs that declare no referent twice this agrees with verification by total assignments.

Main definitions

Main statements

Implementation notes

  • On a DRS that re-declares a referent the two semantics diverge: [ | [x | man x] ⇒ [x | mortal x]] says that every man is mortal under Verifies, where the re-declaration is inert, and that there is a mortal if there is a man under VerifiesTotal (Studies/Muskens1996.lean).
  • Verifies reads an input at its occurring referents, not only the free ones: whether a re-declared referent is already valued matters. Congruence is therefore stated over varFinset; under VerifiesTotal the free referents suffice.

References

Verification by partial embeddings

DRS.Verifies K f g says the pair of partial embeddings ⟨f, g⟩ verifies K: the output g extends the input f by exactly the universe and verifies the conditions (Kamp, van Genabith and Reyle, Def. 19(i)). This packages how Def. 1.4.4(ii)(f) enters a sub-DRS; Def. 1.4.4(i), that f verifies K, is unary, and is Condition.HoldsAll K.conditions f here.

def DRS.VerifiesL60–65
{L : FirstOrder.Language} {V : Type w} {M : Type x} [L.Structure M] :
DRS L V → PartialAssign V M → PartialAssign V M → Prop

Built from

Used by Condition.Holds, DRS.verifies_iff, DRS.IsTrue, DRS.verifies_mk, Condition.holds_neg, Condition.holds_imp, Condition.holds_dis, DRS.Verifies.le, DRS.Verifies.domain_eq, DRS.Verifies.holdsAll, DRS.verifies_empty, DRS.verifies_singleton_nil_iff, DRS.exists_verifies_congr, DRS.exists_verifies_iff_isTrue, DRS.verifies_merge, DRS.exists_extends_verifiesTotal_iff_exists_verifies

Used in Semantics/Dynamic/DRT/ContextChange, Semantics/Dynamic/DRT/Relational

Condition.Holds c g says the partial embedding g verifies the DRS-condition c (Def. 1.4.4(ii)); an atomic condition requires its referents to be valued, and a sub-DRS is entered by extension.

def Condition.HoldsL66–74
{L : FirstOrder.Language} {V : Type w} {M : Type x} [L.Structure M] :
Condition L V → PartialAssign V M → Prop
Equations

Built from

Used by Condition.HoldsAll, Condition.holds_atom, Condition.holds_eq, Condition.holds_neg, Condition.holds_imp, Condition.holds_dis, Condition.holdsAll_cons, Condition.holdsAll_iff, Condition.holds_congr, Condition.verifiesConditionTotal_iff_holds

L75–78
L98–100
L102–103
L132–136
L154–195

Coincidence

Verification reads an embedding at its occurring referents: whether a re-declared referent is already valued matters (fn. 4), so the congruence is over varFinset, not freeVarFinset.

L267–304

The Merging Lemma

The Merging Lemma: a merge is verified by sequencing its parts, when the universe of K₂ captures no referent the conditions of K₁ use outside K₁'s own universe. Re-declaring a referent of K₁'s universe is inert, and no referential presupposition is needed.

theorem DRS.verifies_mergeL325–399
{L : FirstOrder.Language} {V : Type w} {M : Type x} [L.Structure M] {f g : PartialAssign V M} [DecidableEq V] (K₁ K₂ : DRS L V) (hfresh : Disjoint K₂.referents (Condition.varFinsetL K₁.conditions \ K₁.referents)) :
(K₁.merge K₂).Verifies f g ↔ ∃ (h : PartialAssign V M), K₁.Verifies f h ∧ K₂.Verifies h g

Built from

Reuse-freeness

No discourse referent is declared twice along a nesting path: each universe is fresh for the ambient declarations, threaded through sub-boxes the way verification threads the base (the antecedent of a ⇒ feeds its referents into the consequent). This is the hypothesis under which the total agree-off-universe semantics and the partial semantics coincide (DRS.exists_extends_verifiesTotal_iff_exists_verifies).

A DRS is reuse-free at ambient declarations X when its universe avoids X and its conditions are reuse-free at the grown set.

def DRS.ReuseFreeAtL415–418
{L : FirstOrder.Language} {V : Type w} [DecidableEq V] (X : Finset V) :
DRS L V → Prop

Built from

Used by Condition.ReuseFreeAt, Condition.reuseFreeAt_neg, Condition.reuseFreeAt_imp, Condition.reuseFreeAt_dis, DRS.reuseFreeAt_mk, DRS.decidableReuseFreeAt, DRS.exists_extends_verifiesTotal_iff_exists_verifies

Used in Semantics/Dynamic/DRT/Relational, Semantics/Dynamic/DRT/Translation, Muskens1996

L419–426
L427–430
L435–436
L438–439
L441–442
L450–451
L459–461
L468–479

Agreement with total assignments

On reuse-free DRSs the total and partial semantics agree: a total verifying extension restricts to a partial one, and a partial one totalizes by reading the input off its domain. On a DRS that re-declares a referent they diverge (fn. 4; witness in Studies/Muskens1996.lean).

On a reuse-free DRS the total and partial semantics agree: some total extension of f' verifies K iff some partial output verifies it from the partial reading of f'.

theorem DRS.exists_extends_verifiesTotal_iff_exists_verifiesL711–730
{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)) :
(∃ (g' : V → M), K.Extends f' g' ∧ VerifiesTotal g' K) ↔ ∃ (g : PartialAssign V M), K.Verifies f g

Built from ,