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 |
id |
crspringernat:10.1007/978-3-030-79876-5_16 |
---|---|
record_format |
openpolar |
spelling |
crspringernat:10.1007/978-3-030-79876-5_16 2024-03-10T08:32:49+00:00 Multi-Dimensional Interpretations for Termination of Term Rewriting Yamada, Akihisa 2021 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 unknown Springer International Publishing https://creativecommons.org/licenses/by/4.0 https://creativecommons.org/licenses/by/4.0 Automated Deduction – CADE 28 Lecture Notes in Computer Science page 273-290 ISSN 0302-9743 1611-3349 ISBN 9783030798758 9783030798765 book-chapter 2021 crspringernat https://doi.org/10.1007/978-3-030-79876-5_16 2024-02-13T16:25:50Z 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. Book Part Arctic Springer Nature Arctic 273 290 |
institution |
Open Polar |
collection |
Springer Nature |
op_collection_id |
crspringernat |
language |
unknown |
description |
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. |
format |
Book Part |
author |
Yamada, Akihisa |
spellingShingle |
Yamada, Akihisa Multi-Dimensional Interpretations for Termination of Term Rewriting |
author_facet |
Yamada, Akihisa |
author_sort |
Yamada, Akihisa |
title |
Multi-Dimensional Interpretations for Termination of Term Rewriting |
title_short |
Multi-Dimensional Interpretations for Termination of Term Rewriting |
title_full |
Multi-Dimensional Interpretations for Termination of Term Rewriting |
title_fullStr |
Multi-Dimensional Interpretations for Termination of Term Rewriting |
title_full_unstemmed |
Multi-Dimensional Interpretations for Termination of Term Rewriting |
title_sort |
multi-dimensional interpretations for termination of term rewriting |
publisher |
Springer International Publishing |
publishDate |
2021 |
url |
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 |
geographic |
Arctic |
geographic_facet |
Arctic |
genre |
Arctic |
genre_facet |
Arctic |
op_source |
Automated Deduction – CADE 28 Lecture Notes in Computer Science page 273-290 ISSN 0302-9743 1611-3349 ISBN 9783030798758 9783030798765 |
op_rights |
https://creativecommons.org/licenses/by/4.0 https://creativecommons.org/licenses/by/4.0 |
op_doi |
https://doi.org/10.1007/978-3-030-79876-5_16 |
container_start_page |
273 |
op_container_end_page |
290 |
_version_ |
1793128906246586368 |