A static higher-order dependency pair framework
From MaRDI portal
Abstract: We revisit the static dependency pair method for proving termination of higher-order term rewriting and extend it in a number of ways: (1) We introduce a new rewrite formalism designed for general applicability in termination proving of higher-order rewriting, Algebraic Functional Systems with Meta-variables. (2) We provide a syntactically checkable soundness criterion to make the method applicable to a large class of rewrite systems. (3) We propose a modular dependency pair framework for this higher-order setting. (4) We introduce a fine-grained notion of formative and computable chains to render the framework more powerful. (5) We formulate several existing and new termination proving techniques in the form of processors within our framework. The framework has been implemented in the (fully automatic) higher-order termination tool WANDA.
Recommendations
- Refinement types as higher-order dependency pairs
- Rewriting Techniques and Applications
- Dependency Pairs for Rewriting with Non-free Constructors
- Term Rewriting and Applications
- Logic for Programming, Artificial Intelligence, and Reasoning
- A dependency pair framework for innermost complexity analysis of term rewrite systems
- scientific article; zbMATH DE number 1722701
- Context-sensitive dependency pairs
- Context-Sensitive Dependency Pairs
Cited in
(5)
This page was built for publication: A static higher-order dependency pair framework
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6070806)
