Docs / Semantics / Dynamic / DRT / ContextChange

Context change potentials of DRSs

import Linglib.Semantics.Dynamic.DRT.ContextChange · namespace DRT.DRS

Over an intensional model — a family interp : W → L.Structure M of structures on a constant domain — a DRS updates possibilities: DRS.update relates two points of the same world whose assignments are related by the verification of Kamp, van Genabith and Reyle's Def. 19, and the context change potential DRS.ccp (Def. 24) is its image on information states. The state a DRS expresses relative to an assignment is DRS.relState (Def. 29), with the state it expresses outright (Def. 22) its value at the empty assignment.

Main statements

DRS.ccp_le: a context change potential only adds information (Def. 27(ii)).
DRS.ccp_eq_mul_ccp_stratum: on a state uniform at a base, context change is merge with the potential's value on the stratum — Heim's assertive update.
DRS.state_merge: updating the state of a context DRS gives the state of the merge.
DRS.image_world_state: the proposition a state determines (Def. 23(v)) is the set of worlds where the DRS is true (Def. 20).

References

Kamp et al. 2011, Discourse Representation Theory formalized
Heim 1982, The Semantics of Definite and Indefinite Noun Phrases formalized

Declarations

The dynamic value of a DRS on possibilities: worlds are preserved and assignments related by Def. 19.

def update L71–74

{L : FirstOrder.Language} {V : Type w} {M : Type x} {W : Type y} (interp : W → L.Structure M) (K : DRS L V) :

DynamicSemantics.Update (DynamicSemantics.Possibility W V (Flat M))

The definition is too large to print here; read it in the source.

Used by mem_update, ccp, update_merge

L76–78

The context change potential of a DRS (Def. 24): the image of its dynamic value on information states.

def ccp L80–82

{L : FirstOrder.Language} {V : Type w} {M : Type x} {W : Type y} (interp : W → L.Structure M) (K : DRS L V) (I : DynamicSemantics.State W V M) :

DynamicSemantics.State W V M

ccp interp K I = SetRel.image (update interp K) I

Built from

Used by mem_ccp, ccp_top, ccp_le, mem_ccp_stratum, ccp_eq_mul_ccp_stratum, ccp_merge, state_merge

Used in KampVanGenabithReyle2011

L84–87

The information state a DRS expresses relative to an assignment of its free referents (Def. 29(ii)).

def relState L89–92

{L : FirstOrder.Language} {V : Type w} {M : Type x} {W : Type y} (interp : W → L.Structure M) (K : DRS L V) (g : PartialAssign V M) :

DynamicSemantics.State W V M

relState interp K g = {q : DynamicSemantics.Possibility W V (Flat M) | VerifiesAt interp q.world K g q.assignment}

Built from

Used by mem_relState, state

Used in KampVanGenabithReyle2011

A context change potential only adds information (Def. 27(ii)).

theorem ccp_le L120–124

{L : FirstOrder.Language} {V : Type w} {M : Type x} {W : Type y} (interp : W → L.Structure M) {K : DRS L V} (I : DynamicSemantics.State W V M) :

ccp interp K I ≤ I

Built from

L126–149

On a state uniform at a base, context change is merge with the potential's value on the stratum: the context change potential of Def. 24 is Heim's assertive update.

theorem ccp_eq_mul_ccp_stratum L151–183

{L : FirstOrder.Language} {V : Type w} {M : Type x} {W : Type y} (interp : W → L.Structure M) {K : DRS L V} {I : DynamicSemantics.State W V M} {X : Set V} (hI : DynamicSemantics.State.UniformAt X I) :

ccp interp K I = I * ccp interp K (DynamicSemantics.State.stratum X)

Built from

L186–202

L204–214

Updating the state of a context DRS gives the state of the merge, as Kamp, van Genabith and Reyle observe of their (43) after Def. 24.

theorem state_merge L216–221

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

ccp interp K₂ (state interp K₁) = state interp (K₁.merge K₂)

Built from ,

The proposition the state of a DRS determines (Def. 23(v)) is the set of worlds where the DRS is true, for a proper DRS the proposition it expresses (Def. 20).

theorem image_world_state L223–232

{L : FirstOrder.Language} {V : Type w} {M : Type x} {W : Type y} (interp : W → L.Structure M) {K : DRS L V} :

DynamicSemantics.Possibility.world '' state interp K = {w : W | K.IsTrue M}

Built from