The one-object collapse and the Kleisli reading #

The descent from indexed dynamic semantics to level 0 — the relational algebra of procedures over a single state space ([MvBV11]'s "Dynamic Constants as Operators in Relational Algebra") — and the canonicity of level 0 itself. An update S → S → Prop is a Kleisli arrow S → Set S of the powerset monad — definitionally — so sequencing is Kleisli composition, the trivial test is pure, and lift is bind ([Cha14b]'s monadic view of dynamic semantics, as theorems); lift is then an equivalence onto the completely-join-preserving transformers (sSupHom), so the transformer algebra is the suplattice completion of the relational one and the non-distributive tests (might, must) are exactly the residue. Categorically, RelCat ≌ KleisliCat Set, and the indexed tower reads Ctx ⥤ RelCat ≌ KleisliCat Set ↪ suplattice endomaps, every arrow canonical. The collapsed state space at X is the X-stratum of root states, classified by Possibility.domainEquiv/State.uniformEquiv, and the relational action computes the root-state CCP through that classification (Transition.uniformEquiv_applyState) — the extraction of a relational meaning from a DRT-style one, as a morphism ([VV96]).

The powerset monad is one column of the effect view of dynamic semantics ([Mog91], [Sha01b], [BC24b]): a framework's update algebra is the Kleisli algebra of its chosen effect. Partiality is the Part column (Partial.lean's seq_eq_kleisliComp); probabilistic and continuation-based systems choose further effects.

Main definitions #

Ctx.collapse: the functor Ctx W M V ⥤ RelCat sending a context to its possibility space and a transition to its world-threaded relation.
liftEquiv: Update S ≃ sSupHom (Set S) (Set S).
relCatEquivKleisli: RelCat ≌ KleisliCat Set. [UPSTREAM] candidate — pure category theory, absent from mathlib.

Main results #

Ctx.collapse_faithful: a transition is recoverable from its collapsed relation; what the collapse forgets is the base-indexing of objects.
seq_eq_kleisliComp, test_top_eq_pure, lift_eq_bind: the monadic reading of the update algebra.
isDistributive_iff_map_sSup, liftEquiv_seq: distributive CCPs are exactly the completely-join-preserving maps, and lift/lower is an equivalence onto them, sending sequencing to composition.

Implementation notes #

The predecessor collapsed through base-agreement classes of total assignments — the quotient was forced because the untyped toUpdate sent identities to agreement-on-X rather than equality. Typed transitions are unital, so the collapse lands in RelCat directly, with no setoid.

References #

The collapse to `RelCat` #

source

def DynamicSemantics.Ctx.collapse (W : Type u_4) (M : Type u_5) (V : Type u_6) :

CategoryTheory.Functor (Ctx W M V) CategoryTheory.RelCat

The one-object collapse: forget the base-indexing, sending a context to its possibility space and a transition to its world-threaded relation. Unital by typing — no quotient needed.

Equations

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

Instances For

source

instance DynamicSemantics.Ctx.collapse_faithful {W : Type u_1} {M : Type u_2} {V : Type u_3} :

(collapse W M V).Faithful

The collapse is faithful: a transition is recoverable from its world-threaded relation. What the collapse forgets is only the base-indexing of the objects.

The Set-monad reading #

source

theorem DynamicSemantics.seq_eq_kleisliComp {S : Type u_1} (D₁ D₂ : S → Set S) :

Update.seq D₁ D₂ = D₁ >=> D₂

Sequencing is Kleisli composition for the powerset monad: an update is a Kleisli arrow S → Set S, definitionally.

source

theorem DynamicSemantics.test_top_eq_pure {S : Type u_1} :

(Update.test fun (x : S) => True) = fun (i : S) => pure i

The trivial test is pure.

source

theorem DynamicSemantics.lift_eq_bind {S : Type u_1} (R : Update S) (σ : Set S) :

lift R σ = σ >>= R

lift is bind: the relational image is the monad's extension operator.

Distributivity is complete join preservation #

source

theorem DynamicSemantics.isDistributive_iff_map_sSup {S : Type u_1} (φ : CCP S) :

φ.IsDistributive ↔ ∀ (T : Set (Set S)), φ (sSup T) = sSup (φ '' T)

A CCP is distributive iff it preserves arbitrary joins of states.

source

def DynamicSemantics.liftEquiv {S : Type u_1} :

Update S ≃ sSupHom (Set S) (Set S)

The relational algebra is exactly the completely-join-preserving fragment of the transformer algebra: lift/lower as an equivalence onto sSupHom.

Equations