A Term Rewriting Approach to the Automated Termination Analysis of Imperative Programs

Automated Termination Analysis for Haskell: From Term Rewriting to Programming Languages

Lecture Notes in Computer Science - Term Rewriting and Applications ◽

10.1007/11805618_23 ◽

2006 ◽

pp. 297-312 ◽

Cited By ~ 22

Author(s):

Jürgen Giesl ◽

Stephan Swiderski ◽

Peter Schneider-Kamp ◽

René Thiemann

Keyword(s):

Programming Languages ◽

Term Rewriting ◽

Termination Analysis

Download Full-text

Multi-Dimensional Interpretations for Termination of Term Rewriting

Automated Deduction – CADE 28 - Lecture Notes in Computer Science ◽

10.1007/978-3-030-79876-5_16 ◽

2021 ◽

pp. 273-290

Author(s):

Akihisa Yamada

Keyword(s):

General Framework ◽

Term Rewriting ◽

Termination Analysis ◽

Interpretation Method

AbstractInterpretation 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.

Download Full-text

Automated Termination Analysis for Logic Programs by Term Rewriting

Logic-Based Program Synthesis and Transformation - Lecture Notes in Computer Science ◽

10.1007/978-3-540-71410-1_13 ◽

2007 ◽

pp. 177-193 ◽

Cited By ~ 9

Author(s):

Peter Schneider-Kamp ◽

Jürgen Giesl ◽

Alexander Serebrenik ◽

René Thiemann

Keyword(s):

Term Rewriting ◽

Logic Programs ◽

Termination Analysis

Download Full-text

Transformation techniques for context-sensitive rewrite systems

Journal of Functional Programming ◽

10.1017/s0956796803004945 ◽

2004 ◽

Vol 14 (4) ◽

pp. 379-427 ◽

Cited By ~ 31

Author(s):

JÜRGEN GIESL ◽

AART MIDDELDORP

Keyword(s):

Functional Programming ◽

Term Rewriting ◽

Lazy Evaluation ◽

Transformation Techniques ◽

Termination Analysis ◽

Rewrite Systems ◽

Context Sensitive ◽

Term Rewrite Systems ◽

Huge Variety

Context-sensitive rewriting is a computational restriction of term rewriting used to model non-strict (lazy) evaluation in functional programming. The goal of this paper is the study and development of techniques to analyze the termination behavior of context-sensitive rewrite systems. For that purpose, several methods have been proposed in the literature which transform context-sensitive rewrite systems into ordinary rewrite systems such that termination of the transformed ordinary system implies termination of the original context-sensitive system. In this way, the huge variety of existing techniques for termination analysis of ordinary rewriting can be used for context-sensitive rewriting, too. We analyze the existing transformation techniques for proving termination of context-sensitive rewriting and we suggest two new transformations. Our first method is simple, sound, and more powerful than the previously proposed transformations. However, it is not complete, i.e., there are terminating context-sensitive rewrite systems that are transformed into non-terminating term rewrite systems. The second method that we present in this paper is both sound and complete. All these observations also hold for rewriting modulo associativity and commutativity.

Download Full-text