Abstract

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.

BibTeX

@article{Weighted_Path_Order-AFP,
  author  = {Christian Sternagel and René Thiemann and Akihisa Yamada},
  title   = {A Formalization of Weighted Path Orders and Recursive Path Orders},
  journal = {Archive of Formal Proofs},
  month   = sep,
  year    = 2021,
  note    = {\url{https://isa-afp.org/entries/Weighted_Path_Order.html},
            Formal proof development},
  ISSN    = {2150-914x},
}