Higher-Order Constrained Dependency Pairs for (Universal) Computability
Liye Guo, Kasper Hagens, Cynthia Kop, Deivid Vale
TL;DR
The paper addresses termination analysis for higher-order, logically constrained term rewriting systems ($LCSTRS$) in open-world settings and proposes extending the static dependency pair ($DP$) framework to this richer formalism. It introduces universal computability and public computability as notions enabling termination reasoning without closed-world assumptions, and provides a constrained DP framework with processor classes to support modular analysis. A key contribution is the first definition of dependency pairs for higher-order constrained rewriting, along with extensions of hierarchical combination ideas to $LCSTRS$ and new processors to handle public computability, thereby enabling open-world termination analysis. The approach is implemented in the open-source analyzer $Cora$ and validated through experimental evaluation on representative LCSTRS benchmarks, highlighting practical applicability to real-world programs with rich data types and constraints.
Abstract
Dependency pairs constitute a series of very effective techniques for the termination analysis of term rewriting systems. In this paper, we adapt the static dependency pair framework to logically constrained simply-typed term rewriting systems (LCSTRSs), a higher-order formalism with logical constraints built in. We also propose the concept of universal computability, which enables a form of open-world termination analysis through the use of static dependency pairs.