Multi-Dimensional Interpretations for Termination of Term Rewriting
Abstract Interpretation methods constitute a foundation of termination analysis for term rewriting. From time to time remarkable instances of interpretation methods appeared, such as polynomial interpretations, matrix interpretations, arctic interpretations, and their variants. In this paper we intr...
| Main Author: | |
|---|---|
| Format: | Book Part |
| Language: | unknown |
| Published: |
Springer International Publishing
2021
|
| Subjects: | |
| Online Access: | http://dx.doi.org/10.1007/978-3-030-79876-5_16 https://link.springer.com/content/pdf/10.1007/978-3-030-79876-5_16 |
| Summary: | Abstract Interpretation methods constitute a foundation of termination analysis for term rewriting. From time to time remarkable instances of interpretation methods appeared, such as polynomial interpretations, matrix interpretations, arctic interpretations, and their variants. In this paper we introduce a general framework, the multi-dimensional interpretation method, that subsumes these variants as well as many previously unknown interpretation methods as instances. Employing the notion of derivers, we prove the soundness of the proposed method in an elegant way. We implement the proposed method in the termination prover and verify its significance through experiments. |
|---|