The Computability Path Order for Beta-Eta-Normal Higher-Order Rewriting (Full Version)

TL;DR

We lift the computability path order from plain higher-order rewriting to $\beta\eta$-normal higher-order rewriting using matching modulo $\beta\eta$, yielding the $NCPO$ order. $NCPO$ extends CPO with accessible subterms and small symbols and proves termination for HRSs when compatible, addressing cases NHORPO cannot handle. We implement a prototype that automates parameter search via SAT/SMT, compare $NCPO$ to NHORPO with neutralization and HORPO variants (WANDA, CSI^ho), and report that $NCPO$ has incomparable power to NHORPO with neutralization and can succeed where NHORPO fails. The results suggest $NCPO$ is a practical lightweight alternative for automated termination of $\beta\eta$-normal higher-order rewriting, with future work including transitivity questions and integrating $NCPO$ into dependency-pair frameworks.

Abstract

We lift the computability path order and its extensions from plain higher-order rewriting to higher-order rewriting on beta-eta-normal forms where matching modulo beta-eta is employed. The resulting order NCPO is shown to be useful on practical examples. In particular, it can handle systems where its cousin NHORPO fails even when it is used together with the powerful transformation technique of neutralization. We also argue that automating NCPO efficiently is straightforward using SAT/SMT solvers whereas this cannot be said about the transformation technique of neutralization. Our prototype implementation supports automatic termination proof search for NCPO and is also the first one to automate NHORPO with neutralization.