Email Gateway (Jun 01 2023 at 23:04): Email Gateway (Jun 01 2023 at 23:04):From: Tobias Nipkow <nipkow@in.tum.de>
A Verified Efficient Implementation of the Weighted Path Order
René Thiemann and Elias Wenninger
The Weighted Path Order (WPO) of Yamada is a powerful technique for proving
termination. In a previous AFP entry, the WPO was defined and properties of WPO
have been formally verified. However, the implementation of WPO was naive,
leading to an exponential runtime in the worst case.
Therefore, in this AFP entry we provide a poly-time implementation of WPO. The
implementation is based on memoization. Since WPO generalizes the recursive path
order (RPO), we also easily derive an efficient implementation of RPO.
https://www.isa-afp.org/entries/Efficient_Weighted_Path_Order.html
Enjoy this latest contribution to the ever growing formalization of term
rewriting theory!
Last updated: Apr 20 2024 at 01:05 UTC