Confluence of Almost Parallel-Closed Generalized Term Rewriting Systems
摘要
Generalized Term Rewriting Systems (GTRSs) extend Conditional Term Rewriting Systems by (i) selecting the arguments of function symbols on which rewritings are allowed and (ii) allowing for more general conditions in rules, namely, atoms defined by a set of Horn clauses. They are useful to model and analyze properties of computations with sophisticated languages like Maude. Toyama proved that left-linear and almost parallel-closed Term Rewriting Systems (TRSs) are confluent. In this paper, we generalize and extend his result to GTRSs without requiring left-linearity. This improves Toyama’s result, as we show with some examples. Also, Toyama’s result entails confluence of weakly orthogonal TRSs, thus providing a syntactic criterion for proving confluence without requiring termination. We similarly introduce weakly V-orthogonal GTRSs, which are confluent. Weak V-orthogonality checking is implemented in the confluence tool CONFident, to improve its ability to deal with context-sensitive and conditional term rewriting systems.