A Formalization of Weighted Path Orders and Recursive Path Orders

Christian Sternagel 📧, René Thiemann 📧 and Akihisa Yamada 📧

September 16, 2021

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


We define the weighted path order (WPO) and formalize several properties such as strong normalization, the subterm property, and closure properties under substitutions and contexts. Our definition of WPO extends the original definition by also permitting multiset comparisons of arguments instead of just lexicographic extensions. Therefore, our WPO not only subsumes lexicographic path orders (LPO), but also recursive path orders (RPO). We formally prove these subsumptions and therefore all of the mentioned properties of WPO are automatically transferable to LPO and RPO as well. Such a transformation is not required for Knuth–Bendix orders (KBO), since they have already been formalized. Nevertheless, we still provide a proof that WPO subsumes KBO and thereby underline the generality of WPO.


BSD License


Session Weighted_Path_Order