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 PolyFun/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 PolyFun/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:2312.00990.

@[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".

def PFunctor.TraceList.positions {P : PFunctor.{uA, uB}} (events : P.TraceList) : List P.A

The ordered input positions of a typed event trace, retaining repeated occurrences.

@[simp]

theorem PFunctor.TraceList.positions_nil {P : PFunctor.{uA, uB}} : positions [] = []

@[simp]

theorem PFunctor.TraceList.positions_cons {P : PFunctor.{uA, uB}} (event : P.Idx) (events : P.TraceList) : positions (event :: events) = event.fst :: events.positions

@[simp]

theorem PFunctor.TraceList.length_positions {P : PFunctor.{uA, uB}} (events : P.TraceList) : events.positions.length = FreeMonoid.length events

def PFunctor.TraceList.DirectionsWithin {P : PFunctor.{uA, uB}} (allowed : (a : P.A) → Set (P.B a)) (events : P.TraceList) : Prop

Every event in a trace carries a direction allowed at its position.

The allowed directions remain fiber-indexed: checking an event ⟨a, b⟩ uses allowed a, so no equality casts or decidable equality on positions are needed.

@[simp]

theorem PFunctor.TraceList.directionsWithin_nil {P : PFunctor.{uA, uB}} (allowed : (a : P.A) → Set (P.B a)) : DirectionsWithin allowed []

@[simp]

theorem PFunctor.TraceList.directionsWithin_cons {P : PFunctor.{uA, uB}} (allowed : (a : P.A) → Set (P.B a)) (event : P.Idx) (events : P.TraceList) : DirectionsWithin allowed (event :: events) ↔ event.snd ∈ allowed event.fst ∧ DirectionsWithin allowed events

def PFunctor.TraceList.occurrences {P : PFunctor.{uA, uB}} [DecidableEq P.A] (target : P.A) (events : P.TraceList) : ℕ

Number of events at a given position in an erased execution trace.

def PFunctor.TraceList.getAt? {P : PFunctor.{uA, uB}} [DecidableEq P.A] (events : P.TraceList) (target : P.A) : ℕ → Option (P.B target)

The answer carried by the n-th event at target, if that occurrence exists.

theorem PFunctor.TraceList.getAt?_cons_zero {P : PFunctor.{uA, uB}} [DecidableEq P.A] (event : P.Idx) (tail : P.TraceList) (target : P.A) : getAt? (event :: tail) target 0 = if h : event.fst = target then some (h ▸ event.snd) else tail.getAt? target 0

theorem PFunctor.TraceList.getAt?_cons_succ {P : PFunctor.{uA, uB}} [DecidableEq P.A] (event : P.Idx) (tail : P.TraceList) (target : P.A) (n : ℕ) : getAt? (event :: tail) target (n + 1) = if event.fst = target then tail.getAt? target n else tail.getAt? target (n + 1)

@[simp]

theorem PFunctor.TraceList.getAt?_nil {P : PFunctor.{uA, uB}} [DecidableEq P.A] (target : P.A) (n : ℕ) : getAt? [] target n = none

@[simp]

theorem PFunctor.TraceList.getAt?_cons_self_zero {P : PFunctor.{uA, uB}} [DecidableEq P.A] (target : P.A) (answer : P.B target) (tail : P.TraceList) : getAt? (⟨target, answer⟩ :: tail) target 0 = some answer

@[simp]

theorem PFunctor.TraceList.getAt?_cons_self_succ {P : PFunctor.{uA, uB}} [DecidableEq P.A] (target : P.A) (answer : P.B target) (tail : P.TraceList) (n : ℕ) : getAt? (⟨target, answer⟩ :: tail) target (n + 1) = tail.getAt? target n

@[simp]

theorem PFunctor.TraceList.getAt?_cons_of_ne {P : PFunctor.{uA, uB}} [DecidableEq P.A] {a target : P.A} (hne : a ≠ target) (answer : P.B a) (tail : P.TraceList) (n : ℕ) : getAt? (⟨a, answer⟩ :: tail) target n = tail.getAt? target n

@[simp]

theorem PFunctor.TraceList.getAt?_isSome_iff_lt_occurrences {P : PFunctor.{uA, uB}} [DecidableEq P.A] (events : P.TraceList) (target : P.A) (n : ℕ) : (events.getAt? target n).isSome = true ↔ n < occurrences target events

A dependent trace lookup succeeds exactly for the counted occurrences.

theorem PFunctor.TraceList.getAt?_append_self_occurrences {P : PFunctor.{uA, uB}} [DecidableEq P.A] (before after : P.TraceList) (target : P.A) (answer : P.B target) : getAt? (List.append before (⟨target, answer⟩ :: after)) target (occurrences target before) = some answer

The event following a prefix is found at the prefix's occurrence count.

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

Relabel-and-filter the events of a trace list along a partial map of indices: List.filterMap with the monoid structure of TraceList made explicit. Trace.mapPartial is this operation pointwise.

@[simp]

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

theorem PFunctor.TraceList.mapPartial_mul {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} (f : P.Idx → Option Q.Idx) (a b : P.TraceList) : mapPartial f (a * b) = mapPartial f a * mapPartial f b

@[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.