Traces of polynomial-functor events

For a polynomial functor P, the universal "log of P-events" is the free monoid on indices Idx P = Σ a : P.A, P.B a. This file packages that monoid together with the abstract Control.Trace machinery from ToMathlib/Control/Trace.lean.

Main definitions

• PFunctor.TraceList P — the carrier FreeMonoid (Idx P), definitionally List (Σ a, P.B a).
• PFunctor.Trace P X — the type of X-indexed P-event traces, i.e. X → TraceList P, with monoid structure inherited pointwise.
• PFunctor.Trace.mapPartial, mapChart, restrictLeft, restrictRight — the standard push / filter operations along chart morphisms and direct-sum projections.
• PFunctor.Trace.toMonoid — the universal property: every valuation Idx P → ω extends uniquely to a monoid hom TraceList P →* ω, and so to a trace map Trace P X → Control.Trace ω X.

Boundary-emitter intuition

Reading Trace P X as "for each input x : X, the finite, ordered list of P-events that get emitted on the boundary": this is precisely the boundary shape of a stateless effectful Mealy machine in the List-Writer Kleisli category. Stateful executors (e.g. running over an OracleComp) are handled separately in VCVio/OracleComp/QueryTracking/.

The canonical user inside this repository is BoundaryAction.emit in VCVio/Interaction/UC/OpenProcess.lean, where Trace Δ.Out X records the list of output-port packets a node emits when the local state transitions to x : X. Operations such as mapBoundary, wireLeft, wireRight, and the tensor embeddings of open processes are implemented directly by PFunctor.Trace.mapChart and PFunctor.Trace.mapPartial against appropriate boundary morphisms.

References

• Bonchi, Di Lavore, Romàn — Effectful Mealy machines and Kleisli categories.
• Hancock, Setzer — Interactive programs and weakly final coalgebras in dependent type theory.
• Spivak, Niu — Polynomial Functors: A Mathematical Theory of Interaction, arXiv:2202.00534.

@[reducible]

def PFunctor.TraceList (P : PFunctor.{uA, uB}) : Type (max uA uB)

The free monoid on P-events. Definitionally FreeMonoid (Idx P), which in turn is reducibly List (Idx P). This is the universal carrier for "finite ordered logs of P-events".

@[reducible]

def PFunctor.Trace (P : PFunctor.{uA, uB}) (X : Type v) : Type (max uA uB v)

An X-indexed trace of P-events: for each input x : X, a finite ordered list of P-events. Specialisation of Control.Trace at ω = TraceList P, inheriting a pointwise monoid structure.

def PFunctor.Trace.mapPartial {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} {X : Type v} (f : P.Idx → Option Q.Idx) (t : P.Trace X) : Q.Trace X

Relabel-and-filter a trace along a partial map of indices. This is the single primitive for moving traces between polynomial functors: total chart pushforward and summand restriction are both specialisations of it.

def PFunctor.Trace.mapChart {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} {X : Type v} (φ : P.Chart Q) : P.Trace X → Q.Trace X

Push a P-trace forward along a chart P → Q.

def PFunctor.Trace.precomp {P : PFunctor.{uA₁, uB₁}} {X Y : Type v} (f : Y → X) (t : P.Trace X) : P.Trace Y

Pre-compose a P-trace with f : Y → X (input variance).

def PFunctor.Trace.toMonoid {P : PFunctor.{uA₁, uB₁}} {X : Type v} {ω : Type w} [Monoid ω] (φ : P.Idx → ω) : P.Trace X → Control.Trace ω X

The universal map into any monoid-valued trace via the free-monoid universal property. Every valuation φ : Idx P → ω extends uniquely to a monoid homomorphism FreeMonoid (Idx P) →* ω; toMonoid φ post-composes a P-trace with that hom.

Pointwise behaviour

@[simp]

theorem PFunctor.Trace.mapPartial_apply {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} {X : Type v} (f : P.Idx → Option Q.Idx) (t : P.Trace X) (x : X) : mapPartial f t x = List.filterMap f (t x)

@[simp]

theorem PFunctor.Trace.mapChart_apply {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} {X : Type v} (φ : P.Chart Q) (t : P.Trace X) (x : X) : mapChart φ t x = List.filterMap (fun (i : P.Idx) => some (φ.mapIdx i)) (t x)

@[simp]

theorem PFunctor.Trace.toMonoid_apply {P : PFunctor.{uA₁, uB₁}} {X : Type v} {ω : Type w} [Monoid ω] (φ : P.Idx → ω) (t : P.Trace X) (x : X) : toMonoid φ t x = (FreeMonoid.lift φ) (t x)

Functoriality of mapPartial and mapChart

@[simp]

theorem PFunctor.Trace.mapPartial_some {P : PFunctor.{uA₁, uB₁}} {X : Type v} (t : P.Trace X) : mapPartial (fun (i : P.Idx) => some i) t = t

theorem PFunctor.Trace.mapPartial_comp {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} {R : PFunctor.{uA₃, uB₃}} {X : Type v} (g : Q.Idx → Option R.Idx) (f : P.Idx → Option Q.Idx) (t : P.Trace X) : mapPartial g (mapPartial f t) = mapPartial (fun (i : P.Idx) => (f i).bind g) t

@[simp]

theorem PFunctor.Trace.mapChart_id {P : PFunctor.{uA₁, uB₁}} {X : Type v} (t : P.Trace X) : mapChart (Chart.id P) t = t

@[simp]

theorem PFunctor.Trace.mapChart_comp {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} {R : PFunctor.{uA₃, uB₃}} {X : Type v} (g : Q.Chart R) (f : P.Chart Q) (t : P.Trace X) : mapChart (g ∘c f) t = mapChart g (mapChart f t)

Trivial-trace lemmas

The unit trace 1 : Trace P X = fun _ => [] is annihilated by all relabel / filter operations. These are needed downstream to reason about boundary actions whose default emission is the empty trace.

@[simp]

theorem PFunctor.Trace.mapPartial_one {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} {X : Type v} (f : P.Idx → Option Q.Idx) : mapPartial f 1 = 1

@[simp]

theorem PFunctor.Trace.mapChart_one {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} {X : Type v} (φ : P.Chart Q) : mapChart φ 1 = 1

Naturality of toMonoid

Pushing a P-trace along a chart φ : P → Q and then evaluating against a Q-valuation ψ is the same as evaluating against the precomposed P-valuation ψ ∘ Chart.mapIdx φ. This is exactly the free-monoid naturality square.

@[simp]

theorem PFunctor.Trace.toMonoid_mapChart {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} {X : Type v} {ω : Type w} [Monoid ω] (ψ : Q.Idx → ω) (φ : P.Chart Q) (t : P.Trace X) : toMonoid ψ (mapChart φ t) = toMonoid (ψ ∘ φ.mapIdx) t

Restriction along direct-sum projections

The summand restriction operations need P and Q to share the B universe so that P + Q typechecks.

def PFunctor.Trace.restrictLeft {P Q : PFunctor.{uA, uB}} {X : Type v} : (P + Q).Trace X → P.Trace X

Restrict a trace on P + Q to its P-summand.

def PFunctor.Trace.restrictRight {P Q : PFunctor.{uA, uB}} {X : Type v} : (P + Q).Trace X → Q.Trace X

Restrict a trace on P + Q to its Q-summand.