|
A
Formalization
of
Weighted
Path
Orders
and
Recursive
Path
Orders
Title: |
A Formalization of Weighted Path Orders and Recursive Path Orders |
Authors:
|
Christian Sternagel (c /dot/ sternagel /at/ gmail /dot/ com),
René Thiemann (rene /dot/ thiemann /at/ uibk /dot/ ac /dot/ at) and
Akihisa Yamada (akihisa /dot/ yamada /at/ aist /dot/ go /dot/ jp)
|
Submission date: |
2021-09-16 |
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},
}
|
License: |
BSD License |
Depends on: |
Knuth_Bendix_Order |
|