Information states

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 least upper bound, dually union as greatest lower bound; subsistence as the dual lowerClosure kernel; the uniform strata, 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).

State is a type synonym in the OrderDual mold: ≤ is informativeness while ⊆ keeps its literal meaning, and since neither kernel is antisymmetric, State is a Preorder only.

References

• [KvGR11], Defs. 0.23 (information states), 0.25 (informativeness), 0.26 (consistent merge)
• [ES25a], Def. 3.3 (subsistence); [GSV96]
• [VV96] (monoidal processing); [Hei82]

Information states

def DynamicSemantics.State (W : Type u_4) (V : Type u_5) (M : Type u_6) : Type (max (max u_6 u_5) u_4)

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

Equations

• DynamicSemantics.State W V M = Set (DynamicSemantics.Possibility W V (Part M))

@[reducible]

instance DynamicSemantics.State.instMembershipPossibilityPart {W : Type u_1} {V : Type u_2} {M : Type u_3} : Membership (Possibility W V (Part M)) (State W V M)

Equations

• DynamicSemantics.State.instMembershipPossibilityPart = { mem := DynamicSemantics.State.instMembershipPossibilityPart._aux_1 }

@[implicit_reducible]

instance DynamicSemantics.State.instHasSubset {W : Type u_1} {V : Type u_2} {M : Type u_3} : HasSubset (State W V M)

Equations

• DynamicSemantics.State.instHasSubset = { Subset := fun (s s' : DynamicSemantics.State W V M) => ∀ ⦃p : DynamicSemantics.Possibility W V (Part M)⦄, p ∈ s → p ∈ s' }

@[reducible]

instance DynamicSemantics.State.instEmptyCollection {W : Type u_1} {V : Type u_2} {M : Type u_3} : EmptyCollection (State W V M)

Equations

• DynamicSemantics.State.instEmptyCollection = { emptyCollection := DynamicSemantics.State.instEmptyCollection._aux_1 }

@[reducible]

instance DynamicSemantics.State.instUnion {W : Type u_1} {V : Type u_2} {M : Type u_3} : Union (State W V M)

Equations

• DynamicSemantics.State.instUnion = { union := DynamicSemantics.State.instUnion._aux_1 }

@[reducible]

instance DynamicSemantics.State.instInter {W : Type u_1} {V : Type u_2} {M : Type u_3} : Inter (State W V M)

Equations

• DynamicSemantics.State.instInter = { inter := DynamicSemantics.State.instInter._aux_1 }

@[reducible]

instance DynamicSemantics.State.instSDiff {W : Type u_1} {V : Type u_2} {M : Type u_3} : SDiff (State W V M)

Equations

• DynamicSemantics.State.instSDiff = { sdiff := DynamicSemantics.State.instSDiff._aux_1 }

theorem DynamicSemantics.State.ext {W : Type u_1} {V : Type u_2} {M : Type u_3} {s s' : State W V M} (h : ∀ (p : Possibility W V (Part M)), p ∈ s ↔ p ∈ s') : s = s'

theorem DynamicSemantics.State.ext_iff {W : Type u_1} {V : Type u_2} {M : Type u_3} {s s' : State W V M} : s = s' ↔ ∀ (p : Possibility W V (Part M)), p ∈ s ↔ p ∈ s'

@[implicit_reducible]

instance DynamicSemantics.State.instPreorder {W : Type u_1} {V : Type u_2} {M : Type u_3} : Preorder (State W V M)

s ≤ s' iff s' carries at least as much information as s.

Equations

• DynamicSemantics.State.instPreorder = Preorder.lift upperClosure

theorem DynamicSemantics.State.le_def {W : Type u_1} {V : Type u_2} {M : Type u_3} {s s' : State W V M} : s ≤ s' ↔ ∀ q ∈ s', ∃ p ∈ s, p ≤ q

Every point of the stronger state lies above a point of the weaker.

@[implicit_reducible]

instance DynamicSemantics.State.instOrderBot {W : Type u_1} {V : Type u_2} {M : Type u_3} : OrderBot (State W V M)

The initial information state ⊥ = W × {g_⊤}.

Equations

• DynamicSemantics.State.instOrderBot = { bot := Set.range DynamicSemantics.Possibility.bot, bot_le := ⋯ }

theorem DynamicSemantics.State.mem_bot {W : Type u_1} {V : Type u_2} {M : Type u_3} {r : Possibility W V (Part M)} : r ∈ ⊥ ↔ ∀ (v : V), r.assignment v = ⊥

Membership in the initial state: no referent defined.

@[implicit_reducible]

instance DynamicSemantics.State.instOrderTop {W : Type u_1} {V : Type u_2} {M : Type u_3} : OrderTop (State W V M)

The absurd state ⊤ = ∅ is maximally informative.

Equations

• DynamicSemantics.State.instOrderTop = { top := ∅, le_top := ⋯ }

@[simp]

theorem DynamicSemantics.State.top_eq_empty {W : Type u_1} {V : Type u_2} {M : Type u_3} : ⊤ = ∅

Subsistence

Subsistence ([ES25a], Def. 3.3, after [GSV96] 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.

Consistent merge as multiplication

@[implicit_reducible]

instance DynamicSemantics.State.instCommMonoid {W : Type u_1} {V : Type u_2} {M : Type u_3} : CommMonoid (State W V M)

s * s' is consistent merge — the joins of pairs of points, one from each state — and 1 = ⊥.

Equations

• DynamicSemantics.State.instCommMonoid = { mul := Set.lubs, mul_assoc := ⋯, one := ⊥, one_mul := ⋯, mul_one := ⋯, npow_zero := ⋯, npow_succ := ⋯, mul_comm := ⋯ }

theorem DynamicSemantics.State.one_eq_bot {W : Type u_1} {V : Type u_2} {M : Type u_3} : 1 = ⊥

theorem DynamicSemantics.State.mem_mul {W : Type u_1} {V : Type u_2} {M : Type u_3} {s s' : State W V M} {r : Possibility W V (Part M)} : r ∈ s * s' ↔ ∃ p ∈ s, ∃ q ∈ s', Compat p q ∧ r = p.union q

Membership in the merge, in union form.

theorem DynamicSemantics.State.upperClosure_mul {W : Type u_1} {V : Type u_2} {M : Type u_3} {s s' : State W V M} : upperClosure (s * s') = upperClosure s ⊔ upperClosure s'

The Smyth face of the merge: upper closures compose by join.

theorem DynamicSemantics.State.left_le_mul {W : Type u_1} {V : Type u_2} {M : Type u_3} {s s' : State W V M} : s ≤ s * s'

The merge is above the left factor.

theorem DynamicSemantics.State.right_le_mul {W : Type u_1} {V : Type u_2} {M : Type u_3} {s s' : State W V M} : s' ≤ s * s'

The merge is above the right factor.

theorem DynamicSemantics.State.mul_le {W : Type u_1} {V : Type u_2} {M : Type u_3} {s s' t : State W V M} (h : s ≤ t) (h' : s' ≤ t) : s * s' ≤ t

Anything above both factors is above their merge.

theorem DynamicSemantics.State.isLUB_mul {W : Type u_1} {V : Type u_2} {M : Type u_3} {s s' : State W V M} : IsLUB {s, s'} (s * s')

The merge is the least upper bound of its factors.

instance DynamicSemantics.State.instCovariantClassHMulLe {W : Type u_1} {V : Type u_2} {M : Type u_3} : CovariantClass (State W V M) (State W V M) (fun (x1 x2 : State W V M) => x1 * x2) fun (x1 x2 : State W V M) => x1 ≤ x2

Merge is monotone in the informativeness order.

Union is the meet

Merge is the join of the informativeness order; plain union is its meet — 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.

theorem DynamicSemantics.State.upperClosure_union {W : Type u_1} {V : Type u_2} {M : Type u_3} {s s' : State W V M} : upperClosure (s ∪ s') = upperClosure s ⊓ upperClosure s'

The Smyth face of the union: upper closures compose by meet.

theorem DynamicSemantics.State.union_le_left {W : Type u_1} {V : Type u_2} {M : Type u_3} {s s' : State W V M} : s ∪ s' ≤ s

The union is below the left component.

theorem DynamicSemantics.State.union_le_right {W : Type u_1} {V : Type u_2} {M : Type u_3} {s s' : State W V M} : s ∪ s' ≤ s'

The union is below the right component.

theorem DynamicSemantics.State.le_union {W : Type u_1} {V : Type u_2} {M : Type u_3} {s s' t : State W V M} (h : t ≤ s) (h' : t ≤ s') : t ≤ s ∪ s'

Anything below both components is below their union.

theorem DynamicSemantics.State.isGLB_union {W : Type u_1} {V : Type u_2} {M : Type u_3} {s s' : State W V M} : IsGLB {s, s'} (s ∪ s')

The union is the greatest lower bound of its components.

States up to informational equivalence

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

def DynamicSemantics.State.antisymmetrizationOrderIso {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 (Part M))

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

Equations

• One or more equations did not get rendered due to their size.

Familiarity

The worldly content of a state — Def. 0.23(v)'s proposition, [ES25a] Def. 3.1's 𝒲 — is the image Possibility.world '' s.

def DynamicSemantics.State.Familiar {W : Type u_1} {V : Type u_2} {M : Type u_3} (s : State W V M) (x : V) : Prop

A referent is familiar at a state: defined at every point.

Equations

• s.Familiar x = ∀ p ∈ s, (p.assignment x).Dom

The uniform stratum

def DynamicSemantics.State.UniformAt {W : Type u_1} {V : Type u_2} {M : Type u_3} (X : Set V) (s : State W V M) : Prop

The state is uniform at X: every point defines exactly the referents in X.

Equations

• DynamicSemantics.State.UniformAt X s = ∀ p ∈ s, p.domain = X

theorem DynamicSemantics.State.uniformAt_bot {W : Type u_1} {V : Type u_2} {M : Type u_3} : UniformAt ∅ ⊥

The initial state is uniform at the empty base.

theorem DynamicSemantics.State.UniformAt.isAntichain {W : Type u_1} {V : Type u_2} {M : Type u_3} {s : State W V M} {X : Set V} (hs : UniformAt X s) : IsAntichain (fun (x1 x2 : Possibility W V (Part M)) => x1 ≤ x2) s

A uniform stratum is an antichain: comparable points with one domain are equal.

theorem DynamicSemantics.State.UniformAt.mul_eq_inter {W : Type u_1} {V : Type u_2} {M : Type u_3} {s s' : State W V M} {X : Set V} (hs : UniformAt X s) (hs' : UniformAt X s') : s * s' = s ∩ s'

Within one stratum, merge is intersection.

def DynamicSemantics.State.restrict {W : Type u_1} {V : Type u_2} {M : Type u_3} (X : Set V) (s : State W V M) : State W V M

Restriction of a state: pointwise, by direct image.

Equations

• DynamicSemantics.State.restrict X s = DynamicSemantics.Possibility.restrict X '' s

theorem DynamicSemantics.State.mem_restrict {W : Type u_1} {V : Type u_2} {M : Type u_3} {s : State W V M} {p : Possibility W V (Part M)} {X : Set V} : p ∈ restrict X s ↔ ∃ q ∈ s, Possibility.restrict X q = p

Membership in a restriction.

theorem DynamicSemantics.State.UniformAt.restrict_eq {W : Type u_1} {V : Type u_2} {M : Type u_3} {s : State W V M} {X : Set V} (hs : UniformAt X s) : State.restrict X s = s

Restriction fixes its stratum.

theorem DynamicSemantics.State.mem_lowerClosure_iff_mem_restrict {W : Type u_1} {V : Type u_2} {M : Type u_3} {s : State W V M} {p : Possibility W V (Part M)} {X : Set V} (hp : p.domain = X) : p ∈ lowerClosure s ↔ p ∈ restrict X s

A point at the stratum's domain lies below s iff it lies in the restriction of s.

theorem DynamicSemantics.State.UniformAt.mem_upperClosure_iff_restrict_mem {W : Type u_1} {V : Type u_2} {M : Type u_3} {s : State W V M} {q : Possibility W V (Part M)} {X : Set V} (hs : UniformAt X s) : q ∈ upperClosure s ↔ Possibility.restrict X q ∈ s

A point lies above a uniform s iff its restriction is a point of s.

theorem DynamicSemantics.State.UniformAt.mem_lowerClosure {W : Type u_1} {V : Type u_2} {M : Type u_3} {s : State W V M} {p : Possibility W V (Part M)} {X : Set V} (hs : UniformAt X s) (hp : p.domain = X) : p ∈ lowerClosure s ↔ p ∈ s

Into a uniform stratum, subsistence is membership.

theorem DynamicSemantics.State.UniformAt.lowerClosure_le_iff {W : Type u_1} {V : Type u_2} {M : Type u_3} {s s' : State W V M} {X : Set V} (hs : UniformAt X s) (hs' : UniformAt X s') : lowerClosure s ≤ lowerClosure s' ↔ s ⊆ s'

On a uniform stratum, subsistence is inclusion.

theorem DynamicSemantics.State.UniformAt.mem_upperClosure {W : Type u_1} {V : Type u_2} {M : Type u_3} {s : State W V M} {q : Possibility W V (Part M)} {X : Set V} (hs : UniformAt X s) (hq : q.domain = X) : q ∈ upperClosure s ↔ q ∈ s

Into a uniform stratum, domination is membership.

theorem DynamicSemantics.State.UniformAt.le_iff_superset {W : Type u_1} {V : Type u_2} {M : Type u_3} {s s' : State W V M} {X : Set V} (hs : UniformAt X s) (hs' : UniformAt X s') : s ≤ s' ↔ s' ⊆ s

On a uniform stratum, informativeness is reverse inclusion.

theorem DynamicSemantics.State.UniformAt.mul {W : Type u_1} {V : Type u_2} {M : Type u_3} {s s' : State W V M} {X Y : Set V} (hs : UniformAt X s) (hs' : UniformAt Y s') : UniformAt (X ∪ Y) (s * s')

Merge unites strata.

theorem DynamicSemantics.State.UniformAt.lowerClosure_le_iff_restrict {W : Type u_1} {V : Type u_2} {M : Type u_3} {s s' : State W V M} {X : Set V} (hs : UniformAt X s) : lowerClosure s ≤ lowerClosure s' ↔ s ⊆ State.restrict X s'

Subsistence out of a stratum is inclusion into the restricted image.

theorem DynamicSemantics.State.UniformAt.le_iff_restrict_subset {W : Type u_1} {V : Type u_2} {M : Type u_3} {s s' : State W V M} {X : Set V} (hs : UniformAt X s) : s ≤ s' ↔ State.restrict X s' ⊆ s

Informativeness out of a stratum is reverse inclusion of the restricted image.

theorem DynamicSemantics.State.lowerClosure_restrict_le {W : Type u_1} {V : Type u_2} {M : Type u_3} {s : State W V M} {X : Set V} : lowerClosure (restrict X s) ≤ lowerClosure s

Restriction only forgets: the restricted state subsists in the original.

theorem DynamicSemantics.State.UniformAt.restrict {W : Type u_1} {V : Type u_2} {M : Type u_3} {s : State W V M} {X Y : Set V} (hs : UniformAt Y s) : UniformAt (X ∩ Y) (State.restrict X s)

Restriction meets the stratification.

theorem DynamicSemantics.State.restrict_restrict {W : Type u_1} {V : Type u_2} {M : Type u_3} {s : State W V M} {X Y : Set V} : restrict X (restrict Y s) = restrict (X ∩ Y) s

Restriction composes along intersections.

The uniform classification

def DynamicSemantics.State.uniformEquiv {W : Type u_1} {V : Type u_2} {M : Type u_3} (X : Set V) : { I : State W V M // UniformAt X I } ≃ Set (W × (↑X → M))

Uniform states at X are sets of world–X-assignment pairs.

Equations

• DynamicSemantics.State.uniformEquiv X = (Equiv.Set.powerset {p : DynamicSemantics.Possibility W V (Part M) | p.domain = X}).trans (Equiv.Set.congr (DynamicSemantics.Possibility.domainEquiv X))

@[simp]

theorem DynamicSemantics.State.mem_uniformEquiv {W : Type u_1} {V : Type u_2} {M : Type u_3} {X : Set V} {I : { I : State W V M // UniformAt X I }} {e : W × (↑X → M)} : e ∈ (uniformEquiv X) I ↔ ↑((Possibility.domainEquiv X).symm e) ∈ ↑I

def DynamicSemantics.State.randomAssign {W : Type u_1} {V : Type u_2} {M : Type u_3} [DecidableEq V] (s : State W V M) (x : V) : State W V M

Random assignment: indeterministically extend each point to a defined value at x.

Equations

• s.randomAssign x = {p : DynamicSemantics.Possibility W V (Part M) | ∃ q ∈ s, ∃ (m : M), p = q.update x (Part.some m)}

theorem DynamicSemantics.State.familiar_randomAssign {W : Type u_1} {V : Type u_2} {M : Type u_3} [DecidableEq V] (s : State W V M) (x : V) : (s.randomAssign x).Familiar x

Random assignment makes its referent familiar.