Unifying the Knuth-Bendix, recursive path and polynomial orders
説明
We introduce a simplification order called the weighted path order (WPO). WPO compares weights of terms as in the Knuth-Bendix order (KBO), while WPO allows weights to be computed by an arbitrary interpretation which is weakly monotone and weakly simple. We investigate summations, polynomials and maximums for such interpretations. We show that KBO is a restricted case of WPO induced by summations, the polynomial order (POLO) is subsumed by WPO induced by polynomials, and the lexicographic path order (LPO) is a restricted case of WPO induced by maximums. By combining these interpretations, we obtain an instance of WPO that unifies KBO, LPO and POLO. We also present SMT encodings of our orders, as well as incorporating them in the dependency pair framework.
収録刊行物
-
- Proceedings of the 15th Symposium on Principles and Practice of Declarative Programming
-
Proceedings of the 15th Symposium on Principles and Practice of Declarative Programming 181-192, 2013-09-16
ACM