The Weighted Path Order for Termination of Term Rewriting
Akihisa Yamada, 晃久 山田 · Institutional Repositories DataBase (IRDB) · 2014
Termination of term rewrite systems (TRSs) has been widely studied and various automated termination provers have been developed. Nevertheless, there is still an increasing demand on the power and scalability of termination provers. This thesis aims at proposing a powerful method for automatically proving termination of TRSs, and moreover providing its efficient implementation. We propose a novel method called the weighted path order , which subsumes many existing techniques. In particular, we unify the three most celebrated and longstanding methods: the Knuth-Bendix order, the polynomial interpretation order, and the lexicographic path order. Further to incorporate the new order into the dependency pair framework, the modern standard of termination proving, we propose a new technique called partial status. In this setting, our method moreover subsumes the matrix interpretation method, as well as many other well-known techniques. Then we present how to encode our method as a satisfiability modulo theory (SMT) problem, for which various efficient solvers exist. Our method is implemented as a new termination prover NaTT. With only a few other techniques implemented, NaTT is the second strongest tool in the International Termination Competition (full-run 2013), demonstrating the power of our method. We also present new techniques for cooperating with SMT solvers which advance the efficiency of the tool; NaTT ran almost five times faster than any other tool participated in the competition. In addition, we consider extensions of the Knuth-Bendix order that cope with associativity and commutativity (AC) axioms. The orders of Steinbach and of Korovin and Voronkov are revisited; we enhance the former to a more powerful AC-compatible order and modify the latter to amend its lack of monotonicity on non-ground terms. We compare these variants by investigating computational complexity, as well as experiments on problems in termination and completion.