Information states

import Linglib.Semantics.Dynamic.State · namespace DynamicSemantics

This file defines an information state — a set of possibilities with partial assignments — and its order and algebra: informativeness as the preorder lifted along upperClosure, with initial state ⊤ and absurd state ⊥ = ∅; consistent merge as the monoid * and greatest lower bound, dually union as least upper bound; subsistence as the dual lowerClosure kernel; the strata State.stratum X, the least informative states at each domain, which carry the union of domains to the merge and through which merging with a uniform state factors as extension then filtering (State.mul_eq_sep_of_uniformAt); the uniform states, where both kernels collapse to inclusion; and the classifications of a stratum as world–assignment pairs (State.uniformEquiv) and of states up to informational equivalence as the complete lattice of upper sets (State.antisymmetrizationOrderIso). With no discourse referents a state is a set of worlds ordered by inclusion (State.worldOrderIso), the state of propositional update semantics.

State is a type synonym whose ≤ is informativeness, oriented like the inclusion order of Set and of DynamicSemantics.CCP: a more informed state lies lower, and discarding points descends (le_of_subset). The order is the one mathlib's Galois connection gc_upperClosure_coe induces on sets, and since neither kernel is antisymmetric, State is a Preorder only. Kamp et al. 2011 orient informativeness the other way, with the initial state at the bottom, and the content is the same.

Implementation notes

A state has no domain apart from its points: State.Familiar and State.Novel quantify over the points, so at the absurd state ⊥ = ∅ every referent is both familiar and novel. Heim's files keep their domain of cards apart from their satisfaction set, so that a false file still has cards; a consumer that needs a familiarity failure at a state must assume it nonempty.

References

Kamp et al. 2011, Discourse Representation Theory formalized
Groenendijk et al. 1996, Coreference and Modality
Visser & Vermeulen 1996, Dynamic Bracketing and Discourse Representation

Information states

An information state is a set of world–assignment pairs.

def State L62–63

(W : Type u_4) (V : Type u_5) (M : Type u_6) :

Type (max (max u_6 u_5) u_4)

State W V M = Set (Possibility W V (Flat M))

Used by State.instMembershipPossibilityFlat, State.instHasSubset, State.instEmptyCollection, State.instUnion, State.instInter, State.instSDiff, State.ext, State.ext_iff, State.instPreorder, State.le_def, State.instOrderTop, State.instOrderBot, State.le_of_subset, State.eq_empty_of_le_bot, State.instMul, State.instOne, State.mem_mul_iff_unify, State.mem_mul, State.instCommMonoid, State.empty_mul, State.mul_empty, State.upperClosure_mul, State.mul_le_left, State.mul_le_right, State.le_mul, State.isGLB_mul, State.instCovariantClassHMulLe, State.upperClosure_union, State.left_le_union, State.right_le_union, State.union_le, State.isLUB_union, State.antisymmetrizationOrderIso, State.Familiar, State.Novel, State.Familiar.mono, State.Novel.mono, State.Familiar.of_le, State.Familiar.mul_left, State.Familiar.mul_right, State.Novel.mul, State.stratum, State.UniformAt, State.uniformAt_iff_subset_stratum, State.mul_stratum_empty, State.mem_mul_stratum, State.mul_stratum_eq_self, State.familiar_mul_stratum, State.Familiar.mul_stratum_singleton, State.mul_eq_sep_of_uniformAt, State.atomAt, State.mul_atomAt, State.UniformAt.isAntichain, State.UniformAt.mul_eq_inter, State.restrict, State.mem_restrict, State.UniformAt.restrict_eq, State.mem_lowerClosure_iff_mem_restrict, State.UniformAt.mem_upperClosure_iff_restrict_mem, State.UniformAt.mem_lowerClosure, State.UniformAt.lowerClosure_le_iff, State.UniformAt.mem_upperClosure, State.UniformAt.le_iff_subset, State.UniformAt.mul, State.UniformAt.lowerClosure_le_iff_restrict, State.UniformAt.le_iff_restrict_subset, State.lowerClosure_restrict_le, State.UniformAt.restrict, State.restrict_restrict, State.uniformEquiv, State.mem_uniformEquiv, State.worldOrderIso, State.randomAssign, State.familiar_randomAssign, State.Familiar.randomAssign, State.Novel.randomAssign, State.randomAssign_le, State.Novel.mul_stratum_singleton

Used in Semantics/Dynamic/DRT/ContextChange, Semantics/Dynamic/FileChange, Elliott2020, Heim1982, Heim1983 and 1 more

theorem State.le_of_subset L111–112

{W : Type u_1} {V : Type u_2} {M : Type u_3} {s s' : State W V M} (h : s ⊆ s') :

s ≤ s'

Built from

L114–115

Subsistence

Subsistence (Elliott & Sudo 2025, Def. 3.3, after Groenendijk et al. 1996 Defs. 2.8–2.9) is not a new relation: a point subsists in a state iff it lies in the lower closure of its point set (mem_lowerClosure: some point of the state extends it), and a state subsists in another iff lowerClosure s ≤ lowerClosure s' — the closure kernel dual to ≤, with ⊥ = ∅ at the bottom of both.

Consistent merge as multiplication

Union is the join

Merge is the meet of the informativeness order; plain union is its join — pooling two states keeps exactly their common information. ∪ is not merge: within a stratum merge is intersection (mul_eq_inter_of_uniform), the eliminative regime.

States up to informational equivalence

The Smyth kernel is full: UpperSet's complete lattice is the algebra of states up to equivalence, and Def. 26's unrestricted (arbitrary-family) merge is sSup there.

Up to informational equivalence, states are exactly the upper sets of possibilities, ordered by inclusion.

def State.antisymmetrizationOrderIso L234–254

{W : Type u_1} {V : Type u_2} {M : Type u_3} :

(Antisymmetrization (State W V M) fun (x1 x2 : State W V M) => x1 ≤ x2) ≃o (UpperSet (Possibility W V (Flat M)))ᵒᵈ

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

Built from

Familiarity

The worldly content of a state — Def. 23(v)'s proposition, Elliott & Sudo 2025 Def. 3.1's 𝒲 — is the image Possibility.world '' s.

Strata

The stratum at X is the least informative state defining exactly the referents in X; the states uniform at X are its subsets, and strata multiply as their bases unite, so stratum carries the union of bases to the merge. Merging with a state uniform at X factors through the stratum: extension along X, then filtering by restriction to X (mul_eq_sep_of_uniformAt) — Heim 1982's atomic rule, whose satisfaction clause filters and whose domain clause extends.

The stratum at X: every point defining exactly the referents in X.

def State.stratum L300–301