A Verified Efficient Implementation of the Weighted Path Order

TL;DR

This paper presents a polynomial-time, memoized implementation of the Weighted Path Order (WPO) for termination proofs, improving efficiency and verification speed over previous methods.

Contribution

It introduces a new memoization-based implementation of WPO with numeric keys, enhancing runtime performance and verification efficiency.

Findings

Achieves polynomial runtime for WPO verification

Reduces verification overhead by using numeric keys

Improves upon earlier verified recursive path order implementation

Abstract

The Weighted Path Order of Yamada is a powerful technique for proving termination. It is also supported by CeTA, a certifier for checking untrusted termination proofs. To be more precise, CeTA contains a verified function that computes for two terms whether one of them is larger than the other for a given WPO, i.e., where all parameters of the WPO have been fixed. The problem of this verified function is its exponential runtime in the worst case. Therefore, in this work we develop a polynomial time implementation of WPO that is based on memoization. It also improves upon an earlier verified implementation of the Recursive Path Order: the RPO-implementation uses full terms as keys for the memory, a design which simplified the soundness proofs, but has some runtime overhead. In this work, keys are just numbers, so that the lookup in the memory is faster. Although trivial on paper, this change introduces some challenges for the verification task.