Guarded Traced Categories
Sergey Goncharov, Lutz Schr\"oder

TL;DR
This paper introduces an abstract framework for guarded traced categories, unifying recursion and iteration through guardedness, and relates it to existing concepts like Conway operators and fixpoint operators, with applications to Hilbert spaces.
Contribution
It develops a general notion of guardedness in symmetric monoidal categories and connects guarded traces to known fixpoint theories, unifying recursion and iteration.
Findings
Guarded traced categories generalize recursion and iteration.
Guarded traces are equivalent to guarded Conway operators in certain cases.
Hilbert space operators provide concrete examples of guarded traces.
Abstract
Notions of guardedness serve to delineate the admissibility of cycles, e.g. in recursion, corecursion, iteration, or tracing. We introduce an abstract notion of guardedness structure on a symmetric monoidal category, along with a corresponding notion of guarded traces, which are defined only if the cycles they induce are guarded. We relate structural guardedness, determined by propagating guardedness along the operations of the category, to geometric guardedness phrased in terms of a diagrammatic language. In our setup, the Cartesian case (recursion) and the co-Cartesian case (iteration) become completely dual, and we show that in these cases, guarded tracedness is equivalent to presence of a guarded Conway operator, in analogy to an observation on total traces by Hasegawa and Hyland. Moreover, we relate guarded traces to unguarded categorical uniform fixpoint operators in the style of…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
