### 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

- Logic/Rewriting
- Computer science/Algorithms

### 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

- Indexed_Term
- List_Memo_Functions
- WPO_Approx
- WPO_Mem_Impl
- RPO_Unbounded
- RPO_Mem_Impl

### Depends on

- A Formalization of Weighted Path Orders and Recursive Path Orders

### Auto-related entries

- The Generalized Multiset Ordering is NP-Complete
- Compositional BD Security
- The Hales–Jewett Theorem
- Irrational numbers from THE BOOK
- The Safely Composable DOM

## Cite

×

Efficient_Weighted_Path_Order-AFP

    @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:

- Sep 13, 2023 : Isabelle2023
- Jun 2, 2023 : Isabelle2022