Implementing graph algorithms efficiently in a rule-based language is challenging because graph pattern matching is expensive. In this paper, we present a number of linear-time implementations of graph algorithms in GP 2, an experimental programming language based on graph transformation rules which aims to facilitate program analysis and verification. We focus on two classes of rule-based graph programs: graph reduction programs which check some graph property, and programs using a depth-first search to test some property or perform an operation such as producing a 2-colouring or a topological sorting. Programs of the first type run in linear time without any constraints on input graphs while programs of the second type require input graphs of bounded degree to run in linear time. Essential for achieving the linear time complexity are so-called rooted rules in GP 2, which, in many situations, can be matched in constant time. For each of our programs, we prove both correctness and complexity, and also give empirical evidence for their run time.
翻译:在基于规则的语言中高效实施图形算法是困难的,因为图形模式匹配费用昂贵。 在本文中,我们展示了以图形转换规则为基础的GP 2中一些线性时间执行图形算法的实验性编程语言,该语言以图形转换规则为基础,目的是便利程序分析和核实。我们侧重于两类基于规则的图表程序:用于检查某些图形属性的图形减少程序,以及使用深度第一搜索程序测试某些属性或进行生成 2 色或地形排序等操作的程序。第一种类型的程序在线性时间运行,输入图没有任何限制,而第二种类型的程序则需要具有约束度的输入图,以线性时间运行。实现线性时间复杂性的关键是在GP 2中所谓的扎根规则,在许多情况下,这些规则可以随时匹配。对于我们的每一个程序,我们都证明了其正确性和复杂性,并提供了运行时间的经验证据。