Core Dynamic Semantics Infrastructure

InfoStateOf P (sets of possibilities) and CCP P (context change potentials, the set-transformer view of dynamic meaning), shared by the PLA, DRT, DPL, and CDRT formalizations.

The relational Update S ([GS91], [Mus96]) of Connectives/Defs.lean is the primary dynamic type; CCP connects to it via lift R σ = { j | ∃ i ∈ σ, R i j } and lower φ i j = j ∈ φ {i}, which form a Galois connection. The IsDistributive CCPs — those that process elements independently — are exactly the image of lift; non-distributive operations (CCP.negTest, CCP.might, CCP.must) test the whole input state rather than filtering per-element.

@[reducible, inline]

abbrev Semantics.Dynamic.Core.InfoStateOf (P : Type u_1) : Type u_1

An InfoState is a set of possibilities.

Different theories instantiate P differently:

• PLA: Assignment × WitnessSeq
• DRT: Assignment
• Intensional: World × Assignment

Equations

• Semantics.Dynamic.Core.InfoStateOf P = Set P

@[reducible, inline]

abbrev Semantics.Dynamic.Core.CCP (P : Type u_1) : Type u_1

A Context Change Potential (CCP) is a function from states to states.

This is the semantic type for dynamic meanings.

Equations

• Semantics.Dynamic.Core.CCP P = (Semantics.Dynamic.Core.InfoStateOf P → Semantics.Dynamic.Core.InfoStateOf P)

def Semantics.Dynamic.Core.CCP.id {P : Type u_1} : CCP P

Identity CCP: leaves state unchanged

Equations

• Semantics.Dynamic.Core.CCP.id s = s

def Semantics.Dynamic.Core.CCP.absurd {P : Type u_1} : CCP P

Absurd CCP: yields empty state

Equations

• Semantics.Dynamic.Core.CCP.absurd x✝ = ∅

def Semantics.Dynamic.Core.CCP.seq {P : Type u_1} (u v : CCP P) : CCP P

Sequential composition of CCPs

Equations

• u.seq v s = v (u s)

def Semantics.Dynamic.Core.CCP.«term_;;_» : Lean.TrailingParserDescr

Equations

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

theorem Semantics.Dynamic.Core.CCP.seq_assoc {P : Type u_1} (u v w : CCP P) : (u.seq v).seq w = u.seq (v.seq w)

theorem Semantics.Dynamic.Core.CCP.id_seq {P : Type u_1} (u : CCP P) : id.seq u = u

theorem Semantics.Dynamic.Core.CCP.seq_id {P : Type u_1} (u : CCP P) : u.seq id = u

@[implicit_reducible]

def Semantics.Dynamic.Core.CCP.instMonoid {P : Type u_1} : Monoid (CCP P)

CCPs form a monoid under sequential composition. Scoped because CCP P is an abbreviation for Set P → Set P: a global instance would attach */1 to a bare function type for every importer. Activate with open scoped Semantics.Dynamic.Core.CCP.

Equations

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

theorem Semantics.Dynamic.Core.CCP.seq_absurd {P : Type u_1} (u : CCP P) : u.seq absurd = absurd

seq_absurd: anything followed by absurd is absurd

def Semantics.Dynamic.Core.CCP.neg {P : Type u_1} (φ : CCP P) : CCP P

Dynamic negation: complement within the input state.

This is the standard dynamic negation of [Hei82], [Vel96]: ¬φ(s) = s \ φ(s). Worlds survive iff they do not survive φ. Does not validate DNE on non-eliminative updates. For the whole-state consistency test (must-not), see negTest.

Equations

• φ.neg s = s \ φ s

noncomputable def Semantics.Dynamic.Core.CCP.negTest {P : Type u_1} (φ : CCP P) : CCP P

Test-based negation: passes (returns input) iff φ yields ∅.

A whole-state consistency test ("must-not"), NOT [Hei82]'s or [Vel96]'s negation (that is neg, set difference). The two coincide only when φ s = ∅ or φ s = s — see Studies/Beaver2001/ABLE.lean for the proven divergence.

Equations

• φ.negTest s = if Set.Nonempty (φ s) then ∅ else s

noncomputable def Semantics.Dynamic.Core.CCP.might {P : Type u_1} (φ : CCP P) : CCP P

Compatibility test ("might"): passes iff φ yields a nonempty result.

might(φ)(s) = s if φ(s) ≠ ∅, else ∅

Equations

• φ.might s = if Set.Nonempty (φ s) then s else ∅

noncomputable def Semantics.Dynamic.Core.CCP.must {P : Type u_1} (φ : CCP P) : CCP P

Full support test ("must"): passes iff φ returns input unchanged.

must(φ)(s) = s if φ(s) = s, else ∅

Equations

• φ.must s = if φ s = s then s else ∅

noncomputable def Semantics.Dynamic.Core.CCP.impl {P : Type u_1} (φ ψ : CCP P) : CCP P

Dynamic implication test: passes iff output of φ is preserved by ψ.

impl(φ,ψ)(s) = s if φ(s) ⊆ ψ(φ(s)), else ∅

Equations

• φ.impl ψ s = if φ s ⊆ ψ (φ s) then s else ∅

def Semantics.Dynamic.Core.CCP.disj {P : Type u_1} (φ ψ : CCP P) : CCP P

Dynamic disjunction via De Morgan: φ ∨ ψ = ¬(¬φ ; ¬ψ).

For eliminative updates this unfolds to φ(s) ∪ ψ(s \ φ(s)): the second disjunct is evaluated in the input updated with the negation of the first — the local-context clause of the satisfaction literature ([Bea01]; [Hei83] itself gives CCPs only for not/and/if).

Equations

• φ.disj ψ = (φ.neg.seq ψ.neg).neg

def Semantics.Dynamic.Core.CCP.entails {P : Type u_1} (φ ψ : CCP P) : Prop

Dynamic entailment: φ entails ψ iff ψ adds no information after φ.

Equations

• φ.entails ψ = ∀ (s : Semantics.Dynamic.Core.InfoStateOf P), Set.Nonempty (φ s) → ψ (φ s) = φ s

theorem Semantics.Dynamic.Core.CCP.entails_id {P : Type u_1} (φ : CCP P) : φ.entails id

Entailment is reflexive

def Semantics.Dynamic.Core.IsEliminative {P : Type u_1} (u : CCP P) : Prop

An update is eliminative if it never adds possibilities.

This is the fundamental property of dynamic semantics: information only grows (possibilities only decrease).

Equations

• Semantics.Dynamic.Core.IsEliminative u = ∀ (s : Semantics.Dynamic.Core.InfoStateOf P), u s ⊆ s

theorem Semantics.Dynamic.Core.eliminative_id {P : Type u_1} : IsEliminative CCP.id

Identity is eliminative

theorem Semantics.Dynamic.Core.eliminative_seq {P : Type u_1} (u v : CCP P) (hu : IsEliminative u) (hv : IsEliminative v) : IsEliminative (u.seq v)

Sequential composition preserves eliminativity

def Semantics.Dynamic.Core.IsExpansive {P : Type u_1} (u : CCP P) : Prop

An update is expansive if it never removes possibilities.

Expansive operations include discourse referent introduction (DRT/DPL), modal horizon expansion ([Kir24]), and accommodation. These are the dual of eliminative operations: where eliminative updates can only shrink the state, expansive updates can only grow it.

Equations

• Semantics.Dynamic.Core.IsExpansive u = ∀ (s : Semantics.Dynamic.Core.InfoStateOf P), s ⊆ u s

theorem Semantics.Dynamic.Core.expansive_id {P : Type u_1} : IsExpansive CCP.id

Identity is expansive

theorem Semantics.Dynamic.Core.expansive_seq {P : Type u_1} (u v : CCP P) (hu : IsExpansive u) (hv : IsExpansive v) : IsExpansive (u.seq v)

Sequential composition preserves expansiveness

theorem Semantics.Dynamic.Core.eliminative_expansive_id {P : Type u_1} (u : CCP P) (he : IsEliminative u) (hx : IsExpansive u) (s : InfoStateOf P) : u s = s

A CCP that is both eliminative and expansive is the identity on every input.

theorem Semantics.Dynamic.Core.isEliminative_iff_le_id {P : Type u_1} (u : CCP P) : IsEliminative u ↔ ∀ (s : InfoStateOf P), u s ≤ s

Eliminative ↔ antitone on the identity: u s ≤ s for all s.

theorem Semantics.Dynamic.Core.isExpansive_iff_id_le {P : Type u_1} (u : CCP P) : IsExpansive u ↔ ∀ (s : InfoStateOf P), s ≤ u s

Expansive ↔ identity below: s ≤ u s for all s.

theorem Semantics.Dynamic.Core.IsEliminative.le_id {P : Type u_1} {u : CCP P} (h : IsEliminative u) (s : InfoStateOf P) : u s ≤ s

Eliminative updates are antitone at the identity: u ≤ id in the pointwise order.

theorem Semantics.Dynamic.Core.IsExpansive.id_le {P : Type u_1} {u : CCP P} (h : IsExpansive u) (s : InfoStateOf P) : s ≤ u s

Expansive updates satisfy id ≤ u in the pointwise order.

def Semantics.Dynamic.Core.IsTest {P : Type u_1} (u : CCP P) : Prop

A test is a CCP that either passes (returns input) or fails (returns ∅).

Tests don't change information - they check compatibility. Examples: might, must, presupposition triggers.

Equations

• Semantics.Dynamic.Core.IsTest u = ∀ (s : Semantics.Dynamic.Core.InfoStateOf P), u s = s ∨ u s = ∅

theorem Semantics.Dynamic.Core.test_eliminative {P : Type u_1} (u : CCP P) (h : IsTest u) : IsEliminative u

Tests are eliminative

theorem Semantics.Dynamic.Core.CCP.negTest_isTest {P : Type u_1} (φ : CCP P) : IsTest φ.negTest

theorem Semantics.Dynamic.Core.CCP.might_isTest {P : Type u_1} (φ : CCP P) : IsTest φ.might

theorem Semantics.Dynamic.Core.CCP.must_isTest {P : Type u_1} (φ : CCP P) : IsTest φ.must

theorem Semantics.Dynamic.Core.CCP.impl_isTest {P : Type u_1} (φ ψ : CCP P) : IsTest (φ.impl ψ)

theorem Semantics.Dynamic.Core.CCP.might_eq_negTest_negTest {P : Type u_1} (φ : CCP P) : φ.might = φ.negTest.negTest

Duality for the test pair: might φ = must-not (must-not φ). The analogous identity fails for set-difference neg (DNE holds instead on eliminative updates).

def Semantics.Dynamic.Core.supportOf {P : Type u_1} {φ : Type u_2} (sat : P → φ → Prop) (s : InfoStateOf P) (ψ : φ) : Prop

Support relation: s supports ψ if all possibilities in s satisfy ψ.

This is the fundamental entailment relation of dynamic semantics.

Equations

• Semantics.Dynamic.Core.supportOf sat s ψ = ∀ (p : P), p ∈ s → sat p ψ

def Semantics.Dynamic.Core.contentOf {P : Type u_1} {φ : Type u_2} (sat : P → φ → Prop) (ψ : φ) : InfoStateOf P

Content of a formula: all possibilities satisfying it.

Equations

• Semantics.Dynamic.Core.contentOf sat ψ = {p : P | sat p ψ}

theorem Semantics.Dynamic.Core.support_iff_subset_content {P : Type u_1} {φ : Type u_2} (sat : P → φ → Prop) (s : InfoStateOf P) (ψ : φ) : supportOf sat s ψ ↔ s ⊆ contentOf sat ψ

Galois connection: s ⊆ content ψ ↔ s supports ψ

This is the fundamental duality of dynamic semantics.

theorem Semantics.Dynamic.Core.support_mono {P : Type u_1} {φ : Type u_2} (sat : P → φ → Prop) (s t : InfoStateOf P) (ψ : φ) (h : t ⊆ s) (hs : supportOf sat s ψ) : supportOf sat t ψ

Support is downward closed: smaller states support more.

theorem Semantics.Dynamic.Core.empty_supports {P : Type u_1} {φ : Type u_2} (sat : P → φ → Prop) (ψ : φ) : supportOf sat ∅ ψ

Empty state supports everything (vacuously).

theorem Semantics.Dynamic.Core.content_mono {P : Type u_1} {φ : Type u_2} (sat : P → φ → Prop) (ψ₁ ψ₂ : φ) (h : ∀ (p : P), sat p ψ₁ → sat p ψ₂) : contentOf sat ψ₁ ⊆ contentOf sat ψ₂

Content is antitone in entailment.

theorem Semantics.Dynamic.Core.sep_monotone {P : Type u_1} (pred : P → Prop) : Monotone fun (s : Set P) => {p : P | p ∈ s ∧ pred p}

Filtering a set by a predicate is monotone. This is the shared foundation for monotonicity of updateFromSat, atom, pred1, pred2, etc.

theorem Semantics.Dynamic.Core.sep_eliminative {P : Type u_1} (pred : P → Prop) : IsEliminative fun (s : Set P) => {p : P | p ∈ s ∧ pred p}

Filtering a set by a predicate is eliminative.

def Semantics.Dynamic.Core.updateFromSat {P : Type u_1} {φ : Type u_2} (sat : P → φ → Prop) (ψ : φ) : CCP P

The standard update construction: filter by satisfaction.

This is how PLA, DRT, DPL all define updates.

Equations

• Semantics.Dynamic.Core.updateFromSat sat ψ s = {p : P | p ∈ s ∧ sat p ψ}

theorem Semantics.Dynamic.Core.updateFromSat_eliminative {P : Type u_1} {φ : Type u_2} (sat : P → φ → Prop) (ψ : φ) : IsEliminative (updateFromSat sat ψ)

Standard updates are eliminative

theorem Semantics.Dynamic.Core.mem_updateFromSat {P : Type u_1} {φ : Type u_2} (sat : P → φ → Prop) (ψ : φ) (s : InfoStateOf P) (p : P) : p ∈ updateFromSat sat ψ s ↔ p ∈ s ∧ sat p ψ

Standard update membership

theorem Semantics.Dynamic.Core.updateFromSat_eq_inter_content {P : Type u_1} {φ : Type u_2} (sat : P → φ → Prop) (ψ : φ) (s : InfoStateOf P) : updateFromSat sat ψ s = s ∩ contentOf sat ψ

Update equals intersection with content

theorem Semantics.Dynamic.Core.support_iff_update_eq {P : Type u_1} {φ : Type u_2} (sat : P → φ → Prop) (ψ : φ) (s : InfoStateOf P) : supportOf sat s ψ ↔ updateFromSat sat ψ s = s

Support-Update equivalence

def Semantics.Dynamic.Core.dynamicEntailsOf {P : Type u_1} {φ : Type u_2} (sat : P → φ → Prop) (ψ₁ ψ₂ : φ) : Prop

Dynamic entailment: φ dynamically entails ψ if updating with φ always yields a state that supports ψ.

Equations

• Semantics.Dynamic.Core.dynamicEntailsOf sat ψ₁ ψ₂ = ∀ (s : Semantics.Dynamic.Core.InfoStateOf P), Semantics.Dynamic.Core.supportOf sat (Semantics.Dynamic.Core.updateFromSat sat ψ₁ s) ψ₂

theorem Semantics.Dynamic.Core.dynamicEntails_refl {P : Type u_1} {φ : Type u_2} (sat : P → φ → Prop) (ψ : φ) : dynamicEntailsOf sat ψ ψ

Dynamic entailment is reflexive

theorem Semantics.Dynamic.Core.dynamicEntails_trans {P : Type u_1} {φ : Type u_2} (sat : P → φ → Prop) (ψ₁ ψ₂ ψ₃ : φ) (h1 : dynamicEntailsOf sat ψ₁ ψ₂) (h2 : dynamicEntailsOf sat ψ₂ ψ₃) : dynamicEntailsOf sat ψ₁ ψ₃

Dynamic entailment is transitive

theorem Semantics.Dynamic.Core.updateFromSat_monotone {P : Type u_1} {φ : Type u_2} (sat : P → φ → Prop) (ψ : φ) : Monotone (updateFromSat sat ψ)

updateFromSat is monotone in the state argument: larger input states yield larger output states. Uses mathlib's Monotone (i.e., s ≤ t → f s ≤ f t where ≤ on Set is ⊆).

structure Semantics.Dynamic.Core.Possibility (W : Type u_1) (E : Type u_2) : Type (max u_1 u_2)

A possibility: world paired with variable assignment.

This is the concrete state type for world-sensitive dynamic semantics (DPL, DRT, CDRT, PLA). The assignment field uses Assignment E from the CCP infrastructure.

• world : W
• assignment : Assignment E

def Semantics.Dynamic.Core.Possibility.agreeOn {W : Type u_1} {E : Type u_2} (p q : Possibility W E) (vars : Set ℕ) : Prop

Two possibilities agree on all variables in a set.

Equations

• p.agreeOn q vars = ∀ (x : ℕ), x ∈ vars → p.assignment x = q.assignment x

def Semantics.Dynamic.Core.Possibility.sameWorld {W : Type u_1} {E : Type u_2} (p q : Possibility W E) : Prop

Same world, possibly different assignment.

Equations

• p.sameWorld q = (p.world = q.world)

def Semantics.Dynamic.Core.Possibility.extend {W : Type u_1} {E : Type u_2} (p : Possibility W E) (x : ℕ) (e : E) : Possibility W E

Extend an assignment at a single variable, using Function.update.

Equations

• p.extend x e = { world := p.world, assignment := Function.update p.assignment x e }

@[simp]

theorem Semantics.Dynamic.Core.Possibility.extend_at {W : Type u_1} {E : Type u_2} (p : Possibility W E) (x : ℕ) (e : E) : (p.extend x e).assignment x = e

@[simp]

theorem Semantics.Dynamic.Core.Possibility.extend_other {W : Type u_1} {E : Type u_2} (p : Possibility W E) (x y : ℕ) (e : E) (h : y ≠ x) : (p.extend x e).assignment y = p.assignment y

@[simp]

theorem Semantics.Dynamic.Core.Possibility.extend_world {W : Type u_1} {E : Type u_2} (p : Possibility W E) (x : ℕ) (e : E) : (p.extend x e).world = p.world

@[reducible, inline]

abbrev Semantics.Dynamic.Core.InfoState (W : Type u_1) (E : Type u_2) : Type (max u_2 u_1)

Information state: set of possibilities.

This is InfoStateOf (Possibility W E) — a specialization of the generic InfoStateOf to world-assignment possibilities.

Equations

• Semantics.Dynamic.Core.InfoState W E = Set (Semantics.Dynamic.Core.Possibility W E)

def Semantics.Dynamic.Core.InfoState.univ {W : Type u_1} {E : Type u_2} : InfoState W E

The trivial state: all possibilities.

Equations

• Semantics.Dynamic.Core.InfoState.univ = Set.univ

def Semantics.Dynamic.Core.InfoState.empty {W : Type u_1} {E : Type u_2} : InfoState W E

The absurd state: no possibilities.

Equations

• Semantics.Dynamic.Core.InfoState.empty = ∅

def Semantics.Dynamic.Core.InfoState.consistent {W : Type u_1} {E : Type u_2} (s : InfoState W E) : Prop

State is consistent (non-empty).

Equations

• s.consistent = Set.Nonempty s

def Semantics.Dynamic.Core.InfoState.trivial {W : Type u_1} {E : Type u_2} (s : InfoState W E) : Prop

State is trivial (all possibilities).

Equations

• s.trivial = (s = Set.univ)

def Semantics.Dynamic.Core.InfoState.definedAt {W : Type u_1} {E : Type u_2} (s : InfoState W E) (x : ℕ) : Prop

Variable x is defined in state s iff all possibilities agree on x's value.

Equations

• s.definedAt x = ∀ (p q : Semantics.Dynamic.Core.Possibility W E), p ∈ s → q ∈ s → p.assignment x = q.assignment x

def Semantics.Dynamic.Core.InfoState.definedVars {W : Type u_1} {E : Type u_2} (s : InfoState W E) : Set ℕ

The set of defined variables in a state.

Equations

• s.definedVars = {x : ℕ | s.definedAt x}

def Semantics.Dynamic.Core.InfoState.novelAt {W : Type u_1} {E : Type u_2} (s : InfoState W E) (x : ℕ) : Prop

Variable x is novel in state s iff x is not defined.

Equations

• s.novelAt x = ¬s.definedAt x

theorem Semantics.Dynamic.Core.InfoState.novelAt_iff_disagree {W : Type u_1} {E : Type u_2} (s : InfoState W E) (x : ℕ) (hs : s.consistent) : s.novelAt x ↔ ∃ (p : Possibility W E), ∃ (q : Possibility W E), p ∈ s ∧ q ∈ s ∧ p.assignment x ≠ q.assignment x

In a consistent state, novel means assignments actually disagree.

def Semantics.Dynamic.Core.InfoState.worlds {W : Type u_1} {E : Type u_2} (s : InfoState W E) : Set W

Project to the set of worlds in the state.

Equations

• s.worlds = {w : W | ∃ (p : Semantics.Dynamic.Core.Possibility W E), p ∈ s ∧ p.world = w}

structure Semantics.Dynamic.Core.Context (W : Type u_1) (E : Type u_2) : Type (max u_1 u_2)

Context extends InfoState with metadata.

• state : InfoState W E
• definedVars : Set ℕ
• domain : Set E

def Semantics.Dynamic.Core.Context.initial {W : Type u_1} {E : Type u_2} : Context W E

Empty context with all possibilities.

Equations

• Semantics.Dynamic.Core.Context.initial = { state := Semantics.Dynamic.Core.InfoState.univ }

def Semantics.Dynamic.Core.Context.consistent {W : Type u_1} {E : Type u_2} (c : Context W E) : Prop

Context is consistent iff its state is.

Equations

• c.consistent = c.state.consistent

def Semantics.Dynamic.Core.Context.introduce {W : Type u_1} {E : Type u_2} (c : Context W E) (x : ℕ) : Context W E

Mark a variable as defined.

Equations

• c.introduce x = { state := c.state, definedVars := c.definedVars ∪ {x}, domain := c.domain }

def Semantics.Dynamic.Core.Context.narrow {W : Type u_1} {E : Type u_2} (c : Context W E) (s : InfoState W E) : Context W E

Narrow the state.

Equations

• c.narrow s = { state := c.state ∩ s, definedVars := c.definedVars, domain := c.domain }

def Semantics.Dynamic.Core.InfoState.subsistsIn {W : Type u_1} {E : Type u_2} (s s' : InfoState W E) : Prop

State subsistence: s subsists in s' iff every possibility in s has a descendant in s'.

Equations

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

def Semantics.Dynamic.Core.«term_⪯_» : Lean.TrailingParserDescr

Equations

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

theorem Semantics.Dynamic.Core.InfoState.subsistsIn_refl {W : Type u_1} {E : Type u_2} (s : InfoState W E) : s.subsistsIn s

Subsistence is reflexive.

theorem Semantics.Dynamic.Core.InfoState.subset_subsistsIn {W : Type u_1} {E : Type u_2} {s s' : InfoState W E} (h : s ⊆ s') : s.subsistsIn s'

Subset implies subsistence.

def Semantics.Dynamic.Core.InfoState.supports {W : Type u_1} {E : Type u_2} (s : InfoState W E) (φ : W → Bool) : Prop

State s supports proposition φ iff φ holds at all worlds in s.

Equations

• s.supports φ = ∀ (p : Semantics.Dynamic.Core.Possibility W E), p ∈ s → φ p.world = true

def Semantics.Dynamic.Core.InfoState.«term_⊫_» : Lean.TrailingParserDescr

Equations

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

theorem Semantics.Dynamic.Core.InfoState.supports_mono {W : Type u_1} {E : Type u_2} {s s' : InfoState W E} (h : s ⊆ s') (φ : W → Bool) (hsupp : s'.supports φ) : s.supports φ

Support is preserved by subset.

@[reducible, inline]

abbrev Semantics.Dynamic.Core.State (W : Type u_1) (E : Type u_2) : Type (max u_2 u_1)

State: set of world-assignment pairs.

Isomorphic to InfoState W E but uses a flat product instead of the Possibility structure. Prefer InfoState for new code.

Equations

• Semantics.Dynamic.Core.State W E = Set (W × Core.Assignment E)

@[reducible, inline]

abbrev Semantics.Dynamic.Core.StateCCP (W : Type u_1) (E : Type u_2) : Type (max u_2 u_1)

State-level CCP: context change potential over world-assignment states. Definitionally equal to CCP (W × Assignment E), so all CCP infrastructure (monoid, negation, might, tests, entailment, Galois connection) applies.

Equations

• Semantics.Dynamic.Core.StateCCP W E = Semantics.Dynamic.Core.CCP (W × Core.Assignment E)

def Semantics.Dynamic.Core.IsDistributive {P : Type u_1} (φ : CCP P) : Prop

A CCP is distributive when it processes each element of the input independently: φ(s) = ⋃_{i∈s} φ({i}).

Equations

• Semantics.Dynamic.Core.IsDistributive φ = ∀ (s : Semantics.Dynamic.Core.InfoStateOf P), φ s = {p : P | ∃ (i : P), i ∈ s ∧ p ∈ φ {i}}

theorem Semantics.Dynamic.Core.updateFromSat_isDistributive {P : Type u_1} {φ : Type u_2} (sat : P → φ → Prop) (ψ : φ) : IsDistributive (updateFromSat sat ψ)

updateFromSat is always distributive: it filters per-element.

theorem Semantics.Dynamic.Core.might_not_isDistributive : ∃ (P : Type), ∃ (φ : CCP P), ¬IsDistributive φ.might

CCP.might is not distributive: the whole-context test can pass while individual-element tests fail.

Witness: P = Bool, φ keeps only true. might φ {true, false} = {true, false} (whole-context test passes), but per-singleton: might φ {false} = ∅ (test fails on false-only context). So false is in the whole-context result but not the distributive union.

The relational type Update S = S → S → Prop from DynProp is the primary dynamic semantic type. Every Update gives rise to a distributive CCP via the relational image (lift), and every distributive CCP arises this way (lower). The round-trip is the identity in both directions (for distributive CCPs).

Non-distributive CCP operations (negTest, might, must) test the whole input state and have no direct Update counterpart — they are genuine additions of the set-transformer perspective.

def Semantics.Dynamic.Core.lift {S : Type u_1} (R : DynProp.Update S) : CCP S

Lift a relational Update meaning to a CCP (set transformer).

This is the relational image: given input state σ, collect all outputs reachable from any element of σ. The resulting CCP is always distributive (lift_isDistributive).

Equations

• Semantics.Dynamic.Core.lift R σ = {j : S | ∃ (i : S), i ∈ σ ∧ R i j}

def Semantics.Dynamic.Core.lower {S : Type u_1} (φ : CCP S) : DynProp.Update S

Lower a CCP to a relational Update meaning.

lower φ i j holds iff j is in the output of the singleton {i}. This is the inverse of lift for distributive CCPs.

Equations

• Semantics.Dynamic.Core.lower φ i j = (j ∈ φ {i})

theorem Semantics.Dynamic.Core.lift_dseq {S : Type u_1} (R₁ R₂ : DynProp.Update S) : lift (R₁ ⨟ R₂) = (lift R₁).seq (lift R₂)

Lifting preserves sequential composition: lift (R₁ ⨟ R₂) = lift R₁ ;; lift R₂.

theorem Semantics.Dynamic.Core.lift_test {S : Type u_1} (C : DynProp.Condition S) : lift (DynProp.test C) = fun (σ : InfoStateOf S) => {i : S | i ∈ σ ∧ C i}

Lifting a test produces a per-element filter: lift (test C) σ = { i ∈ σ | C i }.

theorem Semantics.Dynamic.Core.lift_isDistributive {S : Type u_1} (R : DynProp.Update S) : IsDistributive (lift R)

Lifted CCPs are always distributive.

theorem Semantics.Dynamic.Core.lower_lift {S : Type u_1} (R : DynProp.Update S) : lower (lift R) = R

Round-trip: lower (lift R) = R. The relational type loses no information when lifted and lowered.

theorem Semantics.Dynamic.Core.lift_lower {S : Type u_1} (φ : CCP S) (hd : IsDistributive φ) : lift (lower φ) = φ

Round-trip: lift (lower φ) = φ for distributive CCPs. Distributive CCPs are exactly the relational images.

theorem Semantics.Dynamic.Core.lift_test_isEliminative {S : Type u_1} (C : DynProp.Condition S) : IsEliminative (lift (DynProp.test C))

lift (test C) is eliminative: it only removes elements.

theorem Semantics.Dynamic.Core.updateFromSat_eq_lift_test {P : Type u_2} {φ : Type u_3} (sat : P → φ → Prop) (ψ : φ) : updateFromSat sat ψ = lift (DynProp.test fun (p : P) => sat p ψ)

updateFromSat is the lifting of test applied to a satisfaction relation. This connects the CCP-native updateFromSat to the primary relational algebra.