Higher-Order Constrained Dependency Pairs for (Universal) Computability

TL;DR

This paper extends dependency pair techniques to higher-order constrained rewriting systems, introducing universal computability for open-world termination analysis in logical, simply-typed frameworks.

Contribution

It adapts static dependency pair methods to LCSTRSs and introduces the concept of universal computability for broader termination analysis.

Findings

Extended dependency pair framework to LCSTRSs

Introduced universal computability for open-world termination

Enhanced static dependency pair techniques for higher-order systems

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.