Guarded Traced Categories

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 Simpson and Plotkin. Finally, we show that partial traces based on Hilbert-Schmidt operators in the category of Hilbert spaces are an instance of guarded traces.