The category Set* of sets and partial functions is well-known to be traced monoidal, meaning that a partial function S+U -/-> T+U can be coherently transformed into a partial function S -/-> T. This transformation is generally described in terms of an implicit procedure that must be run. We make this procedure explicit by enriching the traced category in Cat#, the symmetric monoidal category of categories and cofunctors: each hom-category has such procedures as objects, and advancement through the procedures as arrows. We also generalize to traced Kleisli categories beyond Set*, providing a conjectural trace operator for the Kleisli category of any polynomial monad of the form t+1. The main motivation for this work is to give a formal and graphical syntax for performing sophisticated computations powered by graph rewriting, which is itself a graphical language for data transformation.

翻译：集合与部分函数的范畴Set*是已知的可迹幺半范畴，这意味着部分函数S+U -/-> T+U可被一致地转化为部分函数S -/-> T。这一转化通常需通过隐式过程描述。我们通过将可迹范畴在Cat#（范畴与余函子构成的对称幺半范畴）中丰富化，使该过程显式化：每个同态范畴以这类过程为对象，以过程中的推进为态射。我们还将这一方法推广至Set*之外的可迹Kleisli范畴，为形如t+1的多项式单子的Kleisli范畴提出了一种猜想性的迹算子。本研究的主要动机是为基于图重写（其本身是一种用于数据变换的图形语言）的复杂计算提供形式化图形语法。