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.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

The Computability Path Order for Beta-Eta-Normal Higher-Order Rewriting

  • Johannes Niederhauser,
  • Aart Middeldorp

摘要

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.