The update algebra

import Linglib.Semantics.Dynamic.Update · namespace DynamicSemantics

Dynamic meanings come in two forms: a relational update Update S relates input states to output states, and a context change potential CCP S transforms sets of states as wholes. An update is a mathlib SetRel S S, so sequencing is SetRel.comp, truth at a state is SetRel.dom, and the strongest postcondition, the weakest precondition, and its dual are SetRel.image, SetRel.preimage, and SetRel.core; this file adds the tests and the static connectives built from them. The image sends an update to a transformer, lower recovers it, and the distributive transformers are exactly the relational images. Acceptance and the consequence relations of dynamic meanings are in Consequence.lean, and the monadic reading of the pair is in Collapse.lean.

Main definitions

Update S, Condition S: relations on states, sets of states.
Update.test, Update.neg, Update.impl, Update.disj: the test of a condition, and the conditions D.domᶜ, D₁.core D₂.dom, and D₁.dom ∪ D₂.dom.
Update.IsTest: updates that never change the state.
Update.maxBy: the outputs of an update at which a valuation is locally maximal.
Update.cumul, Update.strictLift: the cumulative and the strict lift of an update to plural states, Set.LiftRel of its relation and the images of its selections.
Update.dist: an update of plural states applied to each row's singleton state.
CCP.guard, CCP.might, CCP.must, CCP.negTest: whole-state tests.
CCP.IsEliminative, CCP.IsTest, CCP.IsDistributive, CCP.IsClassical: the classification of transformers.
CCP.up, CCP.down: the content–update coercions.
CCP.lower: the inverse of SetRel.image on distributive transformers.

Main results

Update S is a Monoid under sequencing (scoped); tests are its subidentities, by definition.
Update.dom_test, Update.preimage_test, Update.core_test, Update.test_comp_test: the calculus of tests.
Update.IsTest.eq_test_dom, CCP.IsTest.eq_guard: a test is the test of its truth condition, a guard of its acceptance condition.
Update.lower_image, CCP.image_lower: the image and lower are mutually inverse on distributive transformers.
Update.strictLift_subset_cumul, Update.singleton_mem_strictLift_iff: a strict lift is a cumulative one, and takes a one-row state to a one-row state.
CCP.isClassical_iff_up_down_eq, CCP.exists_eq_image_test_iff: the classical transformers are exactly the static ones — up of their own content, the images of tests; CCP.might_not_isDistributive separates.

Implementation notes

The algebraic instances are scoped: Update S abbreviates a set of pairs and CCP S a function type. Sequencing distributes over arbitrary unions by mathlib's SetRel.comp_sUnion and SetRel.sUnion_comp, and the image is left adjoint to the core by SetRel.image_core_gc. Update.neg does not validate double-negation elimination and CCP.negTest is not CCP.neg; the framework-specific repairs and comparisons live in the studies. Groenendijk & Stokhof 1991's entailment notions live in Studies/GroenendijkStokhof1991.lean.

References

The relational face

A dynamic meaning as a binary relation between input and output states. Sequencing is SetRel.comp, the trivial test SetRel.id, truth at a state SetRel.dom, the possible outputs SetRel.cod, and the strongest postcondition, weakest precondition, and its dual are SetRel.image, SetRel.preimage, and SetRel.core.

@[reducible, inline] abbrev Update L94–98

(S : Type u_1) :

Type u_1

Update S = SetRel S S

Instances Charlow2025.Staged.instLawfulLiftUpdateAssignmentForallNat, Charlow2025.instProgramDisjUpdateAssignment, Charlow2025.instSubstrateUpdateAssignment, Charlow2025.instTruthUpdateAssignmentForallNat

Used by Update.test, Update.neg, Update.impl, Update.disj, Update.mem_comp_test, Update.mem_test_comp, Update.mem_neg, Update.mem_impl, Update.mem_disj, Update.neg_eq_core_empty, Update.instMonoid, Update.mul_def, Update.IsTest, Update.IsTest.eq, Update.IsTest.comp, Update.IsTest.eq_test_dom, Update.IsTest.cod_eq_dom, Update.neg_eq_compl_dom, Update.impl_eq_core_dom, Update.disj_eq_dom_union_dom, Update.impl_comp, Update.dom_comp, Update.impl_eq_neg_comp_test_neg, Update.maxBy, Update.mem_maxBy, Update.mem_maxBy_iff_forall_gt, Update.maxBy_subset, Update.maxBy_eq_self, Update.cumul, Update.mem_cumul, Update.cumul_comp, Update.cumul_mono, Update.strictLift, Update.mem_strictLift, Update.strictLift_subset_cumul, Update.singleton_mem_strictLift_iff, Update.dist, Update.dom_dist, Update.dist_dist, CCP.lower, Update.image_isDistributive, Update.lower_image, Update.image_le_image_iff

Used in Semantics/Dynamic/DPL/Context, Semantics/Dynamic/DPL/Semantics, Semantics/Dynamic/DRT/ContextChange, Semantics/Dynamic/DRT/Relational, Semantics/Dynamic/ICDRT and 16 more

A static property of a single state; test embeds conditions into updates.

@[reducible, inline] abbrev Condition L100–101

(S : Type u_1) :

Type u_1

Condition S = Set S

Used by Update.test, Update.neg, Update.impl, Update.disj, Update.mem_test, Update.mem_comp_test, Update.mem_test_comp, Update.mem_test_iff_left, Update.dom_test, Update.cod_test, Update.test_inj, Update.test_comp_test, Update.neg_test, Update.preimage_test, Update.core_test, Update.isTest_test, Update.cumul_test, CCP.up_eq_image_test, Update.image_test_isEliminative, CCP.exists_eq_image_test_iff

Used in Semantics/Dynamic/ICDRT, Semantics/Dynamic/PCDRT, Semantics/Dynamic/RegisterStructure, Charlow2021, Krifka2026 and 2 more

The connectives

test C checks C without changing the state.

def Update.test L109–110

{S : Type u_1} (C : Condition S) :

Update S

Update.test C = {(a, b) : S × S | a = b ∧ b ∈ C}

Built from ,

Used by Update.mem_test, Update.mem_comp_test, Update.mem_test_comp, Update.mem_test_iff_left, Update.dom_test, Update.cod_test, Update.test_injective, Update.test_inj, Update.test_univ, Update.test_comp_test, Update.neg_test, Update.image_test, Update.preimage_test, Update.core_test, Update.isTest_test, Update.IsTest.eq_test_dom, Update.impl_comp, Update.impl_eq_neg_comp_test_neg, Update.cumul_test, CCP.up_eq_image_test, Update.image_test_isEliminative, CCP.exists_eq_image_test_iff

Used in Semantics/Dynamic/DPL/Context, Semantics/Dynamic/DPL/Semantics, Semantics/Dynamic/PCDRT, Semantics/Dynamic/RegisterStructure, Brasoveanu2010 and 11 more

neg D holds at i iff D has no output from i.

def Update.neg L112–113

{S : Type u_1} (D : Update S) :

Condition S

D.neg = (SetRel.dom D)ᶜ

Built from ,

Used by Update.mem_neg, Update.neg_eq_core_empty, Update.neg_test, Update.neg_eq_compl_dom, Update.impl_eq_neg_comp_test_neg

Used in Semantics/Dynamic/DPL/Context, Semantics/Dynamic/DPL/Semantics, Semantics/Dynamic/DRT/Relational, Charlow2019, Charlow2025 and 4 more

impl D₁ D₂ holds at i iff every D₁-output from i has a D₂-output.

def Update.impl L115–116

{S : Type u_1} (D₁ D₂ : Update S) :

Condition S

D₁.impl D₂ = SetRel.core D₁ (SetRel.dom D₂)

Built from ,

Used by Update.mem_impl, Update.impl_eq_core_dom, Update.impl_comp, Update.impl_eq_neg_comp_test_neg

Used in Semantics/Dynamic/DPL/Context, Semantics/Dynamic/DPL/Semantics, Semantics/Dynamic/DRT/Relational, Semantics/Dynamic/RegisterStructure, GroenendijkStokhof1991 and 1 more

disj D₁ D₂ holds at i iff some disjunct has an output from i.

def Update.disj L118–119

{S : Type u_1} (D₁ D₂ : Update S) :

Condition S

D₁.disj D₂ = SetRel.dom D₁ ∪ SetRel.dom D₂

Built from ,

Used by Update.mem_disj, Update.disj_eq_dom_union_dom

Used in Semantics/Dynamic/DPL/Context, Semantics/Dynamic/DPL/Semantics, Semantics/Dynamic/DRT/Relational, GroenendijkStokhof1991

The update monoid

L143–150

L152

L154

Tests

A test's domain is its condition.

@[simp] theorem Update.dom_test L158–159

{S : Type u_1} (C : Condition S) :

SetRel.dom (test C) = C

Built from ,

Sequenced tests test the conjunction.

@[simp] theorem Update.test_comp_test L170–172

{S : Type u_1} (C₁ C₂ : Condition S) :

SetRel.comp (test C₁) (test C₂) = test (C₁ ∩ C₂)

Built from ,

L174

L176–177

The weakest precondition of a test conjoins its condition.

@[simp] theorem Update.preimage_test L179–181

{S : Type u_1} (C t : Condition S) :

SetRel.preimage (test C) t = C ∩ t

Built from ,

@[simp] theorem Update.core_test L183–184

{S : Type u_1} (C t : Condition S) :

SetRel.core (test C) t = Cᶜ ∪ t

Built from ,

An update is a test if it never changes the state (Groenendijk & Stokhof 1991, Definition 11): the tests are the subidentities.

def Update.IsTest L186–188

{S : Type u_1} (D : Update S) :

Prop

D.IsTest = (D ⊆ SetRel.id)

Built from

Used by Update.IsTest.eq, Update.isTest_test, Update.IsTest.comp, Update.IsTest.eq_test_dom, Update.IsTest.cod_eq_dom

Used in Semantics/Dynamic/DPL/Semantics, Elliott2020, GroenendijkStokhof1991, Mendes2025

L190

L192

theorem Update.IsTest.comp L194–196

{S : Type u_1} {D₁ D₂ : Update S} (h₁ : D₁.IsTest) (h₂ : D₂.IsTest) :

IsTest (SetRel.comp D₁ D₂)

Built from ,

A test is the test of its own domain, the remark after Groenendijk & Stokhof 1991's Definition 11 that a test is true at g iff it relates g to itself; the transformer-face mirror is CCP.IsTest.eq_guard.

theorem Update.IsTest.eq_test_dom L198–209

{S : Type u_1} {D : Update S} (h : D.IsTest) :

D = test (SetRel.dom D)

Built from , ,

Maximization

Maximization under a valuation f keeps the outputs of D at which f is maximal among the outputs. The maxima are local, since a nondeterministic D may have several.

def Update.maxBy L232–235

{S : Type u_1} {α : Type u_2} [LE α] (f : S → α) (D : Update S) :

Update S

Update.maxBy f D = {(i, j) : S × S | MaximalFor (fun (x : S) => (i, x) ∈ D) f j}

Built from

Used by Update.mem_maxBy, Update.mem_maxBy_iff_forall_gt, Update.maxBy_subset, Update.maxBy_eq_self

Used in Semantics/Dynamic/PCDRT, Semantics/Dynamic/RegisterStructure

The plural lift

The cumulative lift of an update to plural states (Brasoveanu 2010 (18)): the relation lifting Set.LiftRel of the update, which is cumulation ** in the sense of Beck & Sauerland 2000. Every input row has a D-successor among the output rows, and every output row a D-predecessor among the input rows.

def Update.cumul L259–263

{S : Type u_1} (D : Update S) :

Update (Set S)

D.cumul = {(I, J) : Set S × Set S | Set.LiftRel (fun (x1 x2 : S) => (x1, x2) ∈ D) I J}

Built from

Used by Update.mem_cumul, Update.cumul_id, Update.cumul_comp, Update.cumul_mono, Update.cumul_test, Update.strictLift_subset_cumul

Used in Semantics/Dynamic/PCDRT, Semantics/Dynamic/PPCDRT, Minor2022

The strict lift of an update to plural states (Minor 2022 (60)): each input row moves to one D-successor, and the output state is the image. Where the cumulative lift lets a row have several successors, a strict output is an image of its input, so never larger.

def Update.strictLift L292–296

{S : Type u_1} (D : Update S) :

Update (Set S)

D.strictLift = {(I, J) : Set S × Set S | ∃ (f : S → S), (∀ i ∈ I, (i, f i) ∈ D) ∧ f '' I = J}

Built from

Used by Update.mem_strictLift, Update.strictLift_subset_cumul, Update.singleton_mem_strictLift_iff

Used in Minor2022

L298–299

theorem Update.strictLift_subset_cumul L301–304

{S : Type u_1} (D : Update S) :

D.strictLift ⊆ D.cumul

Built from , ,

From a one-row state, the strict lift moves to a one-row state.

theorem Update.singleton_mem_strictLift_iff L306–311

{S : Type u_1} {D : Update S} {J : Set S} {i : S} :

({i}, J) ∈ D.strictLift ↔ ∃ (j : S), (i, j) ∈ D ∧ J = {j}

Built from ,

The distributivity operator (39) of Brasoveanu 2008 (Minor 2022 (94)) updates the singleton state of every input row separately and glues the outputs together.

def Update.dist L313–317

{S : Type u_1} (D : Update (Set S)) :

Update (Set S)

D.dist = {(I, J) : Set S × Set S | ∃ (ρ : SetRel S (Set S)), Set.Nonempty ρ ∧ ρ.dom = I ∧ ⋃₀ ρ.cod = J ∧ ∀ p ∈ ρ, ({p.1}, p.2) ∈ D}

Built from

Used by Update.dom_dist, Update.dist_dist

Used in Minor2022

L319–329

L331–369

The transformer face

A context change potential is a transformer of whole information states.

@[reducible, inline] abbrev CCP L375–376

(S : Type u_1) :

Type u_1

CCP S = (Set S → Set S)

Used by CCP.seq, CCP.instMonoid, CCP.neg, CCP.guard, CCP.negTest, CCP.might, CCP.must, CCP.IsEliminative, CCP.IsEliminative.seq, CCP.IsTest, CCP.IsTest.isEliminative, CCP.IsTest.eq_guard, CCP.isTest_iff_exists_guard, CCP.IsDistributive, CCP.isDistributive_iff_map_sSup, CCP.up, CCP.down, CCP.IsEliminative.down_eq, CCP.IsClassical, CCP.might_not_isDistributive, CCP.lower, CCP.mem_lower, CCP.image_lower, CCP.exists_eq_image_test_iff, CCP.isClassical_iff_up_down_eq

Used in Semantics/Dynamic/Bilateral, Semantics/Dynamic/Consequence, Charlow2019, Charlow2021, Rudin2025a and 3 more

L382–383

L385–391

L393–395

Whole-state tests

guard C passes a state through iff it satisfies C, else crashes to ∅.

def CCP.guard L399–400

{S : Type u_1} (C : Set S → Prop) :

CCP S

CCP.guard C s = {p : S | p ∈ s ∧ C s}

Built from

Used by CCP.guard_pos, CCP.guard_neg, CCP.mem_guard, CCP.negTest, CCP.might, CCP.must, CCP.guard_isTest, CCP.IsTest.eq_guard, CCP.isTest_iff_exists_guard

Used in ElliottSudo2025

L402–403

L405–406

L408–409

negTest φ passes iff φ crashes — a whole-state consistency test, not the set-difference neg (see the implementation notes).

def CCP.negTest L411–413

{S : Type u_1} (φ : CCP S) :

CCP S

φ.negTest = CCP.guard fun (s : Set S) => ¬(φ s).Nonempty

Built from ,

might φ passes iff φ yields a nonempty result (Veltman 1996).

def CCP.might L415–416

{S : Type u_1} (φ : CCP S) :

CCP S

φ.might = CCP.guard fun (s : Set S) => (φ s).Nonempty

Built from ,

Used by CCP.might_not_isDistributive

Used in Charlow2019, EgreRossiSprenger2026b, ElliottSudo2025, Rudin2025a, Veltman1996 and 1 more

must φ passes iff φ returns its input unchanged (Veltman 1996).

def CCP.must L418–419

{S : Type u_1} (φ : CCP S) :

CCP S

φ.must = CCP.guard fun (s : Set S) => φ s = s

Built from ,

Used in Charlow2019, Yalcin2007

Classification

A transformer is eliminative if it never adds possibilities.

def CCP.IsEliminative L423–424

{S : Type u_1} (u : CCP S) :

Prop

u.IsEliminative = (u ≤ id)

Built from

Used by CCP.isEliminative_id, CCP.IsEliminative.seq, CCP.IsTest.isEliminative, CCP.IsEliminative.down_eq, CCP.IsClassical, Update.image_test_isEliminative

Used in Charlow2019, ElliottSudo2025

L426

L428–430

A transformer is a test if it passes its input through or crashes to ∅ — Veltman 1996's tests, Update.IsTest one carrier up.

def CCP.IsTest L432–434

{S : Type u_1} (u : CCP S) :

Prop

u.IsTest = ∀ (s : Set S), u s = s ∨ u s = ∅

Built from

Used by CCP.IsTest.isEliminative, CCP.guard_isTest, CCP.IsTest.eq_guard, CCP.isTest_iff_exists_guard

L436–437

L439–440

A test is the guard of its own acceptance condition — the mirror of Update.IsTest.eq_test_dom.

theorem CCP.IsTest.eq_guard L442–448

{S : Type u_1} {u : CCP S} (h : u.IsTest) :

u = guard fun (s : Set S) => u s = s

Built from , ,

L450–451

A transformer is distributive if it acts per-element: φ s = ⋃ i ∈ s, φ {i} — equivalently, it preserves arbitrary joins (isDistributive_iff_map_sSup).

def CCP.IsDistributive L453–457

{S : Type u_1} (φ : CCP S) :

Prop

φ.IsDistributive = ∀ (s : Set S), φ s = {p : S | ∃ i ∈ s, p ∈ φ {i}}

Built from

Used by CCP.isDistributive_iff_map_sSup, CCP.IsClassical, CCP.might_not_isDistributive, Update.image_isDistributive, CCP.image_lower

Used in Charlow2019, Charlow2021, KampVanGenabithReyle2011

L459–490

The classical fragment

The static update a content determines is intersection with it.

def CCP.up L494–495

{S : Type u_1} (c : Set S) :

CCP S

CCP.up c s = s ∩ c

Built from

Used by CCP.down_up, CCP.monotone_up, CCP.isClassical_up, CCP.up_eq_image_test, CCP.isClassical_iff_up_down_eq

Used in Semantics/Dynamic/Bilateral, Semantics/Dynamic/Consequence, Dekker2012, EgreRossiSprenger2026b, Rudin2025a and 3 more

The content an update determines is the set of indices whose singleton it updates successfully.

def CCP.down L497–499

{S : Type u_1} (u : CCP S) :

Set S

u.down = {i : S | (u {i}).Nonempty}

Built from

Used by CCP.down_up, CCP.IsEliminative.down_eq, CCP.isClassical_iff_up_down_eq

Used in Charlow2021

L501–502

L504–506

An update is classical if it is eliminative and distributive.

def CCP.IsClassical L508–509

{S : Type u_1} (u : CCP S) :

Prop

u.IsClassical = (u.IsEliminative ∧ u.IsDistributive)

Built from , ,

Used by CCP.isClassical_up, CCP.exists_eq_image_test_iff, CCP.isClassical_iff_up_down_eq

Used in Semantics/Dynamic/Consequence, Spector2026, Stalnaker1978

L511–512

L514–517

might is not distributive, since a whole-state test can pass where every per-singleton test fails.

theorem CCP.might_not_isDistributive L519–532

∃ (S : Type) (φ : CCP S), ¬φ.might.IsDistributive

Built from , ,

The bridge

lower φ relates i to the outputs of φ on the singleton {i}. The other direction is the relational image SetRel.image, the strongest postcondition of Muskens et al. 2011.

def CCP.lower L544–547

{S : Type u_1} (φ : CCP S) :

Update S

φ.lower = {p : S × S | p.2 ∈ φ {p.1}}

Built from ,

Used by CCP.mem_lower, Update.lower_image, CCP.image_lower

Used in Charlow2019, Charlow2021

L549

L551–552

lower is a left inverse of the image, so the relational face loses nothing.

theorem Update.lower_image L554–556

{S : Type u_1} (R : Update S) :

CCP.lower (SetRel.image R) = R

Built from ,

The image is a right inverse of lower on distributive transformers.

theorem CCP.image_lower L558–560

{S : Type u_1} (φ : CCP S) (hd : φ.IsDistributive) :

SetRel.image φ.lower = φ

Built from , ,

L562–566

The static fragment

Van Benthem's additivity (van Benthem 1986; Rothschild & Yalcin 2016; Gillies 2022): the classical transformers are exactly the images of tests. Update semantics keeps eliminativity but its whole-state tests break distributivity; DPL's random reassignment does the reverse (Groenendijk & Stokhof 1990, §4).

L575–576

L578–580

A transformer is the image of a test iff it is classical.

theorem CCP.exists_eq_image_test_iff L582–590

{S : Type u_1} {φ : CCP S} :

(∃ (C : Condition S), φ = SetRel.image (Update.test C)) ↔ φ.IsClassical

Built from , , ,

The classical updates are exactly the static ones, with up ∘ down as their normal form.

theorem CCP.isClassical_iff_up_down_eq L592–599

{S : Type u_1} {φ : CCP S} :

φ.IsClassical ↔ up φ.down = φ

Built from , , ,