We extend the higher-order termination method of dynamic dependency pairs to Algebraic Functional Systems (AFSs). In this setting, simply typed lambda-terms with algebraic reduction and separate -steps are considered. For left-linear AFSs, the method is shown to be complete. For so-called local AFSs we dene a variation of usable rules and an extension of argument lterings. All these techniques have been implemented in the higher-order termination tool WANDA.
The definitions for HRSs @cite_37 @cite_5 do not immediately carry over to AFSs, since AFSs may have rules of functional type, and @math -reduction is a separate rewrite step. A short paper by Blanqui @cite_12 introduces static dependency pairs on a form of rewriting which includes AFSs, but it poses some restrictions, such as base-type rules. The present work considers dynamic dependency pairs for AFSs and is most related to @cite_37 , but is adapted for the different formalism. Our method conservatively extends the one for first-order rewriting and provides a characterisation of termination for left-linear AFSs. We have chosen for a dynamic rather than a static approach because, although the static approach is stronger when applicable, the dynamic definitions can be given without restrictions. The restrictions we do provide, to weaken the subterm property and enable for instance argument filterings, are optional. We will say some words about integrating the static and dynamic approaches in .
@cite_5 @cite_37 @cite_12
2119852735 1505645573 2964098951
Higher-order rewrite systems (HRSs) and simply-typed term rewriting systems (STRSs) are computational models of functional programs. We recently proposed an extremely powerful method, the static dependency pair method, which is based on the notion of strong computability, in order to prove termination in STRSs. In this paper, we extend the method to HRSs. Since HRSs include λ-abstraction but STRSs do not, we restructure the static dependency pair method to allow λ-abstraction, and show that the static dependency pair method also works well on HRSs without new restrictions. This paper explores how to extend the dependency pair technique for proving termination of higher-order rewrite systems. We show that the termination property of higher-order rewrite systems can be checked by the non-existence of an infinite R-chain, which is an extension of Arts’ and Giesl’s result for the first-order case. It is clarified that the subterm property of the quasi-ordering, used for proving termination automatically, is indispensable. Arts and Giesl proved that the termination of a first-order rewrite system can be reduced to the study of its dependency pairs''. We extend these results to rewrite systems on simply typed lambda-terms by using Tait's computability technique.