What does it mean for an algebraic rewrite rule to subsume another rule (that may then be called a subrule)? We view subsumptions as rule morphisms such that the simultaneous application of a rule and a subrule (i.e. the application of a subsumption morphism) yields the same result as a single application of the subsuming rule. Simultaneous applications of categories of rules are obtained by Global Coherent Transformations and illustrated on graphs in the DPO approach. Other approaches are possible since these transformations are formulated in an abstract Rewriting Environment, and such environments exist for various approaches to Algebraic Rewriting, including DPO, SqPO and PBPO.
翻译:代数重写规则在什么意义上能够包容另一条规则(被包容的规则可称为子规则)?我们将包容关系视为规则态射,使得一条规则与其子规则的同时应用(即包容态射的应用)与单次应用包容性规则产生相同的结果。通过全局相干变换可实现规则范畴的同时应用,并以DPO方法中的图为例进行说明。由于这些变换是在抽象重写环境中形式化定义的,而此类环境存在于多种代数重写方法中,包括DPO、SqPO和PBPO,因此其他方法亦具可行性。