Transitions between context fibers

[KvGR11] (Defs. 24, 27)

The hom type of indexed dynamic semantics: a Transition W M X Y is a world-indexed relation between an X-assignment and a Y-assignment, Y ⊇ X. Objects are bases; a DRS denotes an arrow X ⟶ X ∪ U; sequencing is world-pointwise relational composition. The predecessor of this file stated transitions on total assignments and carried supported_left/supported_right invariants; typing the relation at the assignments dissolves both, and the identity transition becomes plain equality rather than agreement-on-X.

Applying a transition acts fiberwise on sets of possibilities — the presheaf fibers of Category.lean — functorially (apply_comp). The chapter's own name for the induced map is the (regular) Context Change Potential (Def. 24); transition names the underlying relation, after the transition-system reading of dynamic semantics ([Fer92], cited there).

Main declarations

• Transition — the typed relation; id, comp and their laws.
• Transition.apply — Def. 24's context change, on fibers.
• Transition.copy — repackaging along base equalities (the Filter.copy pattern; the cast point, kept out of every statement).
• Transition.IsExtension — Def. 27(ii): established referents persist.
• Transition.randomAssign — the generating arrow X ⟶ insert x X.

structure DynamicSemantics.Transition (W : Type u_4) (M : Type u_5) {V : Type u_6} (X Y : Set V) : Type (max (max u_4 u_5) u_6)

A transition: a world-indexed relation from X-assignments to Y-assignments. The grow field makes arrows context-extending — bases never shrink.

• rel : W → (↑X → M) → (↑Y → M) → Prop

  The world-indexed relation between input and output assignments.

• grow : X ⊆ Y

  Bases only grow along an update.

theorem DynamicSemantics.Transition.ext_iff {W : Type u_4} {M : Type u_5} {V : Type u_6} {X Y : Set V} {x y : Transition W M X Y} : x = y ↔ x.rel = y.rel

theorem DynamicSemantics.Transition.ext {W : Type u_4} {M : Type u_5} {V : Type u_6} {X Y : Set V} {x y : Transition W M X Y} (rel : x.rel = y.rel) : x = y

def DynamicSemantics.Transition.id {W : Type u_1} {V : Type u_2} {M : Type u_3} (X : Set V) : Transition W M X X

The identity transition at X: equality of assignments.

Equations

• DynamicSemantics.Transition.id X = { rel := fun (x : W) (e e' : ↑X → M) => e = e', grow := ⋯ }

@[simp]

theorem DynamicSemantics.Transition.rel_id {W : Type u_1} {V : Type u_2} {M : Type u_3} {X : Set V} {w : W} {e e' : ↑X → M} : (id X).rel w e e' ↔ e = e'

def DynamicSemantics.Transition.comp {W : Type u_1} {V : Type u_2} {M : Type u_3} {X Y Z : Set V} (u : Transition W M X Y) (v : Transition W M Y Z) : Transition W M X Z

Sequencing: world-pointwise relational composition.

Equations

• u.comp v = { rel := fun (w : W) => Relation.Comp (u.rel w) (v.rel w), grow := ⋯ }

@[simp]

theorem DynamicSemantics.Transition.id_comp {W : Type u_1} {V : Type u_2} {M : Type u_3} {X Y : Set V} (u : Transition W M X Y) : (id X).comp u = u

@[simp]

theorem DynamicSemantics.Transition.comp_id {W : Type u_1} {V : Type u_2} {M : Type u_3} {X Y : Set V} (u : Transition W M X Y) : u.comp (id Y) = u

theorem DynamicSemantics.Transition.comp_assoc {W : Type u_1} {V : Type u_2} {M : Type u_3} {X Y Z : Set V} (u : Transition W M X Y) (v : Transition W M Y Z) {Z' : Set V} (t : Transition W M Z Z') : (u.comp v).comp t = u.comp (v.comp t)

Application to fibers

def DynamicSemantics.Transition.apply {W : Type u_1} {V : Type u_2} {M : Type u_3} {X Y : Set V} (u : Transition W M X Y) (T : Set (W × (↑X → M))) : Set (W × (↑Y → M))

Context change ([KvGR11], Def. 24), on the presheaf fibers: relate assignments through the transition, worlds preserved.

Equations

• u.apply T = {e' : W × (↑Y → M) | ∃ (e : ↑X → M), (e'.1, e) ∈ T ∧ u.rel e'.1 e e'.2}

theorem DynamicSemantics.Transition.mem_apply {W : Type u_1} {V : Type u_2} {M : Type u_3} {X Y : Set V} {u : Transition W M X Y} {T : Set (W × (↑X → M))} {w : W} {g : ↑Y → M} : (w, g) ∈ u.apply T ↔ ∃ (e : ↑X → M), (w, e) ∈ T ∧ u.rel w e g

@[simp]

theorem DynamicSemantics.Transition.apply_id {W : Type u_1} {V : Type u_2} {M : Type u_3} {X : Set V} (T : Set (W × (↑X → M))) : (id X).apply T = T

Applying the identity transition is the identity.

theorem DynamicSemantics.Transition.apply_comp {W : Type u_1} {V : Type u_2} {M : Type u_3} {X Y Z : Set V} (u : Transition W M X Y) (v : Transition W M Y Z) (T : Set (W × (↑X → M))) : (u.comp v).apply T = v.apply (u.apply T)

apply is functorial: sequencing then applying is applying twice.

Application to root states

def DynamicSemantics.Transition.applyState {W : Type u_1} {V : Type u_2} {M : Type u_3} {X Y : Set V} (u : Transition W M X Y) (I : State W V M) : State W V M

Context change on root states ([KvGR11], Def. 24 — the regular CCP): points of the X-stratum step to points of the Y-stratum through the transition, worlds preserved. Index-free: both sides are plain states.

Equations

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

theorem DynamicSemantics.Transition.uniformAt_applyState {W : Type u_1} {V : Type u_2} {M : Type u_3} {X Y : Set V} (u : Transition W M X Y) (I : State W V M) : State.UniformAt Y (u.applyState I)

Application lands in the target stratum.

theorem DynamicSemantics.Transition.applyState_comp {W : Type u_1} {V : Type u_2} {M : Type u_3} {X Y Z : Set V} (u : Transition W M X Y) (v : Transition W M Y Z) (I : State W V M) : (u.comp v).applyState I = v.applyState (u.applyState I)

Root application is functorial.

theorem DynamicSemantics.Transition.uniformEquiv_applyState {W : Type u_1} {V : Type u_2} {M : Type u_3} {X Y : Set V} (u : Transition W M X Y) {I : State W V M} (hI : State.UniformAt X I) : (State.uniformEquiv Y) ⟨u.applyState I, ⋯⟩ = u.apply ((State.uniformEquiv X) ⟨I, hI⟩)

Root and fiber semantics agree under the classification: on the X-stratum, the regular CCP applyState is apply, transported along State.uniformEquiv — the relational collapse computes the root-state update.

Random assignment

def DynamicSemantics.Transition.randomAssign {W : Type u_1} {V : Type u_2} {M : Type u_3} (X : Set V) (x : V) : Transition W M X (insert x X)

The random-assignment transition ([GS91a]'s random reset k[x]g, [Hei82]'s indefinite widening): preserve the input off x, leave the output free at x — the generating arrow X ⟶ insert x X of context extension.

Equations

• DynamicSemantics.Transition.randomAssign X x = { rel := fun (x_1 : W) (e : ↑X → M) (e' : ↑(insert x X) → M) => ∀ (v : V) (hv : v ∈ X), v ≠ x → e ⟨v, hv⟩ = e' ⟨v, ⋯⟩, grow := ⋯ }

Typing total-assignment relations

Frameworks state their clauses on total assignments (DPL's Definition 2, DRT's verification). ofTotal types such a relation at contexts by existential extension; the predecessor's supported_left/ supported_right fields return as hypotheses — ReadsAt/WritesAt — carried by the framework's own congruence lemmas, and under them the typing is faithful (ofTotal_rel_restrict) and functorial (ofTotal_comp).

def DynamicSemantics.Transition.ReadsAt {W : Type u_1} {V : Type u_2} {M : Type u_3} (X : Set V) (R : W → (V → M) → (V → M) → Prop) : Prop

The relation reads its input only at X.

Equations

• DynamicSemantics.Transition.ReadsAt X R = ∀ ⦃w : W⦄ ⦃f f' g : V → M⦄, Set.EqOn f f' X → (R w f g ↔ R w f' g)

def DynamicSemantics.Transition.WritesAt {W : Type u_1} {V : Type u_2} {M : Type u_3} (Y : Set V) (R : W → (V → M) → (V → M) → Prop) : Prop

The relation constrains its output only at Y.

Equations

• DynamicSemantics.Transition.WritesAt Y R = ∀ ⦃w : W⦄ ⦃f g g' : V → M⦄, Set.EqOn g g' Y → (R w f g ↔ R w f g')

def DynamicSemantics.Transition.ofTotal {W : Type u_1} {V : Type u_2} {M : Type u_3} {X Y : Set V} (h : X ⊆ Y) (R : W → (V → M) → (V → M) → Prop) : Transition W M X Y

Type a total-assignment relation at contexts, by existential extension of the assignments.

Equations

• DynamicSemantics.Transition.ofTotal h R = { rel := fun (w : W) (e : ↑X → M) (e' : ↑Y → M) => ∃ (f : V → M) (g : V → M), X.restrict f = e ∧ Y.restrict g = e' ∧ R w f g, grow := h }

theorem DynamicSemantics.Transition.ofTotal_rel_restrict {W : Type u_1} {V : Type u_2} {M : Type u_3} {X Y : Set V} {R : W → (V → M) → (V → M) → Prop} {h : X ⊆ Y} (hR : ReadsAt X R) (hW : WritesAt Y R) {w : W} {f g : V → M} : (ofTotal h R).rel w (X.restrict f) (Y.restrict g) ↔ R w f g

Under the support hypotheses, the typing is faithful: related assignments are exactly the restrictions of related assignments.

theorem DynamicSemantics.Transition.ofTotal_comp {W : Type u_1} {V : Type u_2} {M : Type u_3} {X Y Z : Set V} {R S : W → (V → M) → (V → M) → Prop} {h₁ : X ⊆ Y} {h₂ : Y ⊆ Z} (hS : ReadsAt Y S) : (ofTotal h₁ R).comp (ofTotal h₂ S) = ofTotal ⋯ fun (w : W) => Relation.Comp (R w) (S w)

Typing is functorial on composition, given read-support of the second relation: the mid-assignments stitch.

Repackaging along base equalities

The substrate-safe form of eqToHom conjugation (mathlib's Filter.copy pattern): composites whose indices differ by base identities — e.g. (X ∪ U₁) ∪ U₂ against X ∪ (U₁ ∪ U₂) — are equated through copy, keeping cast-free statements everywhere below the category layer.

def DynamicSemantics.Transition.copy {W : Type u_1} {V : Type u_2} {M : Type u_3} {X Y : Set V} (u : Transition W M X Y) {X' Y' : Set V} (hX : X = X') (hY : Y = Y') : Transition W M X' Y'

Repackage a transition along equalities of its bases.

Equations

• u.copy hX hY = hX ▸ hY ▸ u

@[simp]

theorem DynamicSemantics.Transition.copy_rfl {W : Type u_1} {V : Type u_2} {M : Type u_3} {X Y : Set V} (u : Transition W M X Y) : u.copy ⋯ ⋯ = u

@[simp]

theorem DynamicSemantics.Transition.copy_copy {W : Type u_1} {V : Type u_2} {M : Type u_3} {X Y : Set V} (u : Transition W M X Y) {X' Y' X'' Y'' : Set V} (hX : X = X') (hY : Y = Y') (hX' : X' = X'') (hY' : Y' = Y'') : (u.copy hX hY).copy hX' hY' = u.copy ⋯ ⋯

theorem DynamicSemantics.Transition.ofTotal_congr {W : Type u_1} {V : Type u_2} {M : Type u_3} {X Y : Set V} {R R' : W → (V → M) → (V → M) → Prop} (h h' : X ⊆ Y) (hR : R = R') : ofTotal h R = ofTotal h' R'

Typing respects relation equality; the growth proof is irrelevant.

theorem DynamicSemantics.Transition.ofTotal_copy {W : Type u_1} {V : Type u_2} {M : Type u_3} {X Y : Set V} {R : W → (V → M) → (V → M) → Prop} {h : X ⊆ Y} {Y' : Set V} (hY : Y = Y') : (ofTotal h R).copy ⋯ hY = ofTotal ⋯ R

Typed relations repackage by re-proving the growth.

theorem DynamicSemantics.Transition.copy_comp_copy {W : Type u_1} {V : Type u_2} {M : Type u_3} {X Y Z : Set V} (u : Transition W M X Y) (v : Transition W M Y Z) {X' Y' Z' : Set V} (hX : X = X') (hY : Y = Y') (hZ : Z = Z') : (u.copy hX hY).comp (v.copy hY hZ) = (u.comp v).copy hX hZ

Repackaged transitions compose to the repackaged composite.

@[simp]

theorem DynamicSemantics.Transition.apply_copy {W : Type u_1} {V : Type u_2} {M : Type u_3} {X Y : Set V} (u : Transition W M X Y) {X' Y' : Set V} (hX : X = X') (hY : Y = Y') (T : Set (W × (↑X' → M))) : (u.copy hX hY).apply T = Eq.ndrec (motive := fun {X' : Set V} => Set (W × (↑X' → M)) → Set (W × (↑Y' → M))) (fun (T : Set (W × (↑X → M))) => hY ▸ u.apply T) hX T

Application is invariant under repackaging.

@[simp]

theorem DynamicSemantics.Transition.applyState_copy {W : Type u_1} {V : Type u_2} {M : Type u_3} {X Y : Set V} (u : Transition W M X Y) {X' Y' : Set V} (hX : X = X') (hY : Y = Y') (I : State W V M) : (u.copy hX hY).applyState I = u.applyState I

Root application is invariant under repackaging.

Information growth (Def. 27)

def DynamicSemantics.Transition.IsExtension {W : Type u_1} {V : Type u_2} {M : Type u_3} {X Y : Set V} (u : Transition W M X Y) : Prop

A transition is an extension when outputs restrict to their inputs: established referents persist, only new ones are assigned.

Equations

• u.IsExtension = ∀ ⦃w : W⦄ ⦃e : ↑X → M⦄ ⦃e' : ↑Y → M⦄, u.rel w e e' → e = fun (v : ↑X) => e' ⟨↑v, ⋯⟩

theorem DynamicSemantics.Transition.isExtension_id {W : Type u_1} {V : Type u_2} {M : Type u_3} {X : Set V} : (id X).IsExtension

The identity is an extension.

theorem DynamicSemantics.Transition.IsExtension.comp {W : Type u_1} {V : Type u_2} {M : Type u_3} {X Y Z : Set V} {u : Transition W M X Y} {v : Transition W M Y Z} (hu : u.IsExtension) (hv : v.IsExtension) : (u.comp v).IsExtension

Extensions compose.