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.
翻译:本文旨在将先前利用超图重写字符串图的研究工作,推广至底层范畴具有迹幺半群结构的情形。在此类结构中,导线可被分叉,且态射的输出可连接到其输入。这种结构尤其重要,因为任何迹笛卡尔(数据流)范畴都具有一个底层的迹幺半群结构。我们证明了超图的某些子类对于迹幺半群范畴是完全完备的:也就是说,此类范畴中的每个项都对应一个唯一的超图(在同构意义下),并且从每个具备所需性质的超图中,可以恢复出范畴中唯一的项(在迹幺半群范畴的公理意义下)。我们还展示了如何通过刻画我们设定中用于重写的有效推出补,将双推出重写框架适配于迹幺半群范畴。最后,我们以近期关于时序电路等式理论的研究作为案例进行展示:该电路由具有延迟和反馈功能的原始逻辑门构建而成。图重写框架为时序电路的操作语义定义提供了可能。