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

TL;DR

This paper extends the computability path order to higher-order rewriting on beta-eta-normal forms, enabling more effective automated termination proofs with practical implementation support.

Contribution

It introduces NCPO, an extension of the computability path order for higher-order rewriting on beta-eta-normal forms, and demonstrates its practical utility and automation capabilities.

Findings

NCPO can handle systems where NHORPO fails.

Automating NCPO with SAT/SMT solvers is straightforward.

Prototype implementation supports automatic termination proof search.

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.