Formalizing the Dependency Pair Criterion for Innermost Termination

TL;DR

This paper formalizes the dependency pair criterion within PVS to analyze innermost termination of rewriting systems, linking termination properties with practical applications in functional specifications.

Contribution

It provides a formal PVS framework for the dependency pair criterion specifically for innermost reduction, enhancing the analysis of termination in functional programming.

Findings

Formal PVS proof of the equivalence between innermost termination and dependency pair termination

Application of the criterion to verify termination of functional specifications

Enhanced tools for reasoning about termination in rewriting systems

Abstract

Rewriting is a framework for reasoning about functional programming. The dependency pair criterion is a well-known mechanism to analyze termination of term rewriting systems. Functional specifications with an operational semantics based on evaluation are related, in the rewriting framework, to the innermost reduction relation. This paper presents a PVS formalization of the dependency pair criterion for the innermost reduction relation: a term rewriting system is innermost terminating if and only if it is terminating by the dependency pair criterion. The paper also discusses the application of this criterion to check termination of functional specifications.