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范畴提供一个推测性迹算子。本研究的主要动机是为执行由图重写驱动的复杂计算提供形式化且图形化的语法，而图重写本身是一种用于数据变换的图形语言。