In this paper we adapt previous work on rewriting string diagrams using hypergraphs to the case where the underlying category has a traced comonoid structure, in which wires can be forked and the outputs of a morphism can be connected to its input. Such a structure is particularly interesting because any traced Cartesian (dataflow) category has an underlying traced comonoid structure. We show that certain subclasses of hypergraphs are fully complete for traced comonoid categories: that is to say, every term in such a category has a unique corresponding hypergraph up to isomorphism, and from every hypergraph with the desired properties, a unique term in the category can be retrieved up to the axioms of traced comonoid categories. We also show how the framework of double pushout rewriting (DPO) can be adapted for traced comonoid categories by characterising the valid pushout complements for rewriting in our setting. We conclude by presenting a case study in the form of recent work on an equational theory for sequential circuits: circuits built from primitive logic gates with delay and feedback. The graph rewriting framework allows for the definition of an operational semantics for sequential circuits.

翻译：本文对先前使用超图重写字符串图的工作进行了改编，将其扩展到底层范畴具有追踪余幺半群结构的情形。在此结构中，线束可分叉，且态射的输出可连接至其输入。此类结构尤为有趣，因为任何追踪笛卡尔（数据流）范畴都隐含了追踪余幺半群结构。我们证明了某些超图子类对追踪余幺半群范畴是完全完备的：即此类范畴中的每个项都存在唯一同构对应的超图，且每个满足所需性质的超图均可依据追踪余幺半群范畴的公理唯一还原出范畴中的项。我们还展示了如何通过刻画重写场景中有效的推出余补，将双推出重写（DPO）框架适配至追踪余幺半群范畴。最后，我们以近期关于时序电路等式理论的工作作为案例研究进行总结：这类电路由包含延迟与反馈的原始逻辑门构建而成。该图重写框架为时序电路操作语义的定义提供了实现途径。