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.

BibTeX

@inproceedings{JNAM-CADE25,
  author    = "Johannes Niederhauser and Aart Middeldorp",
  title     = "The Computability Path Order for Beta-Eta-Normal Higher-Order Rewriting",
  booktitle = "Proceedings of the 30th International Conference on Automated Deduction",
  editor    = "Clark Barrett and Uwe Waldmann",
  series    = "Lecture Notes in Artificial Intelligence",
  volume    = 15943,
  pages     = "207--225",
  year      = 2025,
  doi       = "10.1007/978-3-031-99984-0_12"
}