We demonstrate how category theory provides specifications that can efficiently be implemented via imperative algorithms and apply this to the field of graph rewriting. By examples, we show how this paradigm of software development makes it easy to quickly write correct and performant code. We provide a modern implementation of graph rewriting techniques at the level of abstraction of finitely-presented C-sets and clarify the connections between C-sets and the typed graphs supported in existing rewriting software. We emphasize that our open-source library is extensible: by taking new categorical constructions (such as slice categories, structured cospans, and distributed graphs) and relating their limits and colimits to those of their underlying categories, users inherit efficient algorithms for pushout complements and (final) pullback complements. This allows one to perform double-, single-, and sesqui-pushout rewriting over a broad class of data structures.
翻译:我们演示了范畴论如何提供可通过命令式算法高效实现的规范,并将其应用于图重写领域。通过实例,我们展示了这种软件开发范式如何使快速编写正确且高性能的代码变得容易。我们在有限展现C-集的抽象层次上提供了图重写技术的现代实现,并阐明了C-集与现有重写软件中支持的带类型图之间的联系。我们强调,我们的开源库是可扩展的:通过采用新的范畴构造(如切片范畴、结构化cospan和分布式图)并将其极限与余极限关联到其底层范畴的相应构造,用户可继承用于推出补和(最终)拉回补的高效算法。这使得能够在广泛的数据结构上执行双推、单推和倍半推出图重写。