A Unified Ordering for Termination Proving

TL;DR

This paper introduces the weighted path order (WPO), a unifying reduction order that encompasses many existing orders like KBO, LPO, and POLO, and demonstrates its effectiveness through theoretical and experimental validation.

Contribution

The paper presents WPO, a new unified reduction order that generalizes and subsumes several classical orders, with SMT encodings and experimental results.

Findings

WPO unifies KBO, LPO, and POLO within a single framework.

WPO subsumes matrix interpretations as a reduction pair.

Experimental results demonstrate the effectiveness of WPO in termination proving.

Abstract

We introduce a reduction order called the weighted path order (WPO) that subsumes many existing reduction orders. WPO compares weights of terms as in the Knuth-Bendix order (KBO), while WPO allows weights to be computed by a wide class of interpretations. 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. In order to fit WPO in the modern dependency pair framework, we further provide a reduction pair based on WPO and partial statuses. As a reduction pair, WPO also subsumes matrix interpretations. We finally present SMT encodings of our techniques, and demonstrate the significance of our work through experiments.