A Verified Efficient Implementation of the Weighted Path Order

René Thiemann 🌐 and Elias Wenninger

June 1, 2023

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

Abstract

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.

License

BSD License

Topics

Related publications

  • Thiemann, R., Schöpf, J., Sternagel, C., & Yamada, A. (2020). Certifying the Weighted Path Order (Invited Talk). Schloss Dagstuhl – Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPICS.FSCD.2020.4
  • Yamada, A., Kusakari, K., & Sakabe, T. (2015). A unified ordering for termination proving. Science of Computer Programming, 111, 110–134. https://doi.org/10.1016/j.scico.2014.07.009

Session Efficient_Weighted_Path_Order

Depends on

Cite

× 
@article{Efficient_Weighted_Path_Order-AFP,
  author  = {René Thiemann and Elias Wenninger},
  title   = {A Verified Efficient Implementation of the Weighted Path Order},
  journal = {Archive of Formal Proofs},
  month   = {June},
  year    = {2023},
  note    = {\url{https://isa-afp.org/entries/Efficient_Weighted_Path_Order.html},
             Formal proof development},
  ISSN    = {2150-914x},
}
Download

Download

× Download latest

Older releases: