Email Gateway (Sep 26 2021 at 13:49): Email Gateway (Sep 26 2021 at 13:49):From: Tobias Nipkow <nipkow@in.tum.de>
A Formalization of Weighted Path Orders and Recursive Path Orders
Christian Sternagel, René Thiemann and Akihisa Yamada
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.
https://www.isa-afp.org/entries/Weighted_Path_Order.html
Enjoy!
smime.p7s
Last updated: Jan 04 2025 at 20:18 UTC