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.

翻译：山田提出的加权路径顺序是证明终止性的强大技术，并得到验证工具CeTA的支持，用于检查不可信的终止性证明。具体而言，CeTA包含一个经形式化验证的函数，通过给定WPO（即所有参数已固定）比较两个项的大小关系。该验证函数的缺陷在于最坏情况下具有指数级运行时间。为此，本文开发了一种基于记忆化的WPO多项式时间实现。该工作还改进了递归路径顺序的早期验证实现：RPO实现采用完整项作为内存键值，这种设计简化了正确性证明，但存在运行时开销。本工作采用数字作为键值，从而加速内存查找。尽管该修改在理论上微不足道，却为验证任务带来了若干挑战。