基于迹余幺半群结构的重写 (Rewriting Modulo Traced Comonoid Structure)

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）框架适配于迹余幺半群范畴。最后，我们以近期关于时序电路等式理论的研究作为案例进行展示：该电路由具有延迟和反馈功能的原始逻辑门构成。图重写框架为时序电路的操作语义定义提供了基础。