Traces into a monoid

Control.Trace ω X is the type X → ω for any monoid ω.

It is the universal carrier of "stateless effectful trace" data: each input contributes one element of a fixed monoid ω, and pointwise multiplication (via Pi.monoid) gives Trace ω X itself the structure of a monoid. Nothing in this file requires a monad.

Why a monoid, not a monad

Many bookkeeping / observation patterns share this exact shape:

• QueryLog spec — ω = List ((t : spec.Domain) × spec.Range t), i.e. the free monoid on indices,
• QueryCount ι — ω = ι → ℕ, a commutative monoid under pointwise addition,
• QueryCache spec — ω = (t : spec.Domain) → Option (spec.Range t) with at-most-once write semigroup,
• BoundaryAction.emit — ω = TraceList Δ.Out (the polynomial-trace specialisation in PFunctor/Trace.lean),
• abstract cost functions — ω any commutative monoid (e.g. ℝ≥0).

The monoid axioms are exactly what is needed to turn "one contribution per input" into a meaningful aggregate over a sequence of inputs.

The companion file ToMathlib/PFunctor/Trace.lean specialises this at ω = FreeMonoid (Idx P) for a polynomial functor P, recovering the universal "log of P-events" trace, together with a universal property Trace P X → Control.Trace ω X (toMonoid) coming from the free-monoid universal property.

Conventions

Trace is @[reducible] so that Pi.monoid and Pi.commMonoid apply directly, and so that downstream definitions like QueryLog and QueryCount can be exhibited as Trace-instances by rfl-clean abbreviations.

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 Control.Trace (ω : Type u) (X : Type v) : Type (max u v)

Trace ω X is the type X → ω of stateless valuations from inputs X into a monoid ω. It inherits a monoid structure from Pi.monoid, with 1 the constant trace and * the pointwise product.

See the module docstring for motivation and the catalogue of instances (QueryLog, QueryCount, ...) it is intended to subsume.

def Control.Trace.precomp {ω : Type u} {X Y : Type v} (f : Y → X) (t : Trace ω X) : Trace ω Y

Pre-compose a trace with f : Y → X, giving a trace on Y.

def Control.Trace.map {ω : Type u} {ω' : Type u'} {X : Type v} [MulOneClass ω] [MulOneClass ω'] (φ : ω →* ω') (t : Trace ω X) : Trace ω' X

Post-compose a trace with a monoid homomorphism.

Pointwise behaviour of precomp

@[simp]

theorem Control.Trace.precomp_apply {ω : Type u} {X Y : Type v} (f : Y → X) (t : Trace ω X) (y : Y) : precomp f t y = t (f y)

@[simp]

theorem Control.Trace.precomp_id {ω : Type u} {X : Type v} (t : Trace ω X) : precomp id t = t

@[simp]

theorem Control.Trace.precomp_comp {ω : Type u} {X Y Z : Type v} (g : Z → Y) (f : Y → X) (t : Trace ω X) : precomp g (precomp f t) = precomp (f ∘ g) t

@[simp]

theorem Control.Trace.precomp_one {ω : Type u} {X Y : Type v} [One ω] (f : Y → X) : precomp f 1 = 1

@[simp]

theorem Control.Trace.precomp_mul {ω : Type u} {X Y : Type v} [Mul ω] (f : Y → X) (t s : Trace ω X) : precomp f (t * s) = precomp f t * precomp f s

Pointwise behaviour of map

@[simp]

theorem Control.Trace.map_apply {ω : Type u} {ω' : Type u'} {X : Type v} [MulOneClass ω] [MulOneClass ω'] (φ : ω →* ω') (t : Trace ω X) (x : X) : map φ t x = φ (t x)

@[simp]

theorem Control.Trace.map_id {ω : Type u} {X : Type v} [MulOneClass ω] (t : Trace ω X) : map (MonoidHom.id ω) t = t

@[simp]

theorem Control.Trace.map_comp {ω : Type u} {ω' : Type u'} {ω'' : Type u''} {X : Type v} [MulOneClass ω] [MulOneClass ω'] [MulOneClass ω''] (g : ω' →* ω'') (f : ω →* ω') (t : Trace ω X) : map (g.comp f) t = map g (map f t)

@[simp]

theorem Control.Trace.map_precomp {ω : Type u} {ω' : Type u'} {X Y : Type v} [MulOneClass ω] [MulOneClass ω'] (φ : ω →* ω') (f : Y → X) (t : Trace ω X) : map φ (precomp f t) = precomp f (map φ t)

@[simp]

theorem Control.Trace.map_one {ω : Type u} {ω' : Type u'} {X : Type v} [MulOneClass ω] [MulOneClass ω'] (φ : ω →* ω') : map φ 1 = 1

@[simp]

theorem Control.Trace.map_mul {ω : Type u} {ω' : Type u'} {X : Type v} [MulOneClass ω] [MulOneClass ω'] (φ : ω →* ω') (t s : Trace ω X) : map φ (t * s) = map φ t * map φ s

def Control.Trace.mapHom {ω : Type u} {ω' : Type u'} {X : Type v} [Monoid ω] [Monoid ω'] (φ : ω →* ω') : Trace ω X →* Trace ω' X

Bundle map φ as a monoid homomorphism on the trace monoid.

This is the manifest algebraic content of map: post-composing a trace with a monoid hom is itself a monoid hom on the pointwise-monoid Trace ω X.

@[simp]

theorem Control.Trace.mapHom_apply {ω : Type u} {ω' : Type u'} {X : Type v} [Monoid ω] [Monoid ω'] (φ : ω →* ω') (t : Trace ω X) (a✝ : X) : (mapHom φ) t a✝ = map φ t a✝