Modular termination of prefix-constrained term rewrite systems

Abstract We carry out a proof-theoretic analysis of the wellfoundedness of recursive path orders in an abstract setting. We outline a general termination principle and extract from its wellfoundedness proof subrecursive bounds on the size of derivation trees that can be defined in Gödel’s system T plus bar recursion. We then carry out a complexity analysis of these terms and demonstrate how this can be applied to bound the derivational height of term rewrite systems.

Download Full-text

REDEX CAPTURING IN TERM GRAPH REWRITING

International Journal of Foundations of Computer Science ◽

10.1142/s0129054190000266 ◽

1990 ◽

Vol 01 (04) ◽

pp. 369-386 ◽

Cited By ~ 5

Author(s):

WILLIAM M. FARMER ◽

RONALD J. WATRO

Keyword(s):

Fixed Point ◽

Efficient Method ◽

Natural Generalization ◽

Linear Term ◽

Time And Space ◽

Graph Rewriting ◽

Rewrite Systems ◽

Arbitrary Structure ◽

Term Rewrite Systems

Term graphs are a natural generalization of terms in which structure sharing is allowed. Structure sharing makes term graph rewriting a time- and space-efficient method for implementing term rewrite systems. Certain structure sharing schemes can lead to a situation in which a term graph component is rewritten to another component that contains the original. This phenomenon, called redex capturing, introduces cycles into the term graph which is being rewritten—even when the graph and the rule themselves do not contain cycles. In some applications, redex capturing is undesirable, such as in contexts where garbage collectors require that graphs be acyclic. In other applications, for example in the use of the fixed-point combinator Y, redex capturing acts as a rewriting optimization. We show, using results about infinite rewritings of trees, that term graph rewriting with arbitrary structure sharing (including redex capturing) is sound for left-linear term rewrite systems.

Download Full-text

New Undecidability Results for Properties of Term Rewrite Systems

Electronic Notes in Theoretical Computer Science ◽

10.1016/j.entcs.2012.11.012 ◽

2012 ◽

Vol 290 ◽

pp. 69-85 ◽

Cited By ~ 1

Author(s):

Rakesh Verma

Keyword(s):

Rewrite Systems ◽

Term Rewrite Systems

Download Full-text

Polytool: Polynomial interpretations as a basis for termination analysis of logic programs

Theory and Practice of Logic Programming ◽

10.1017/s1471068410000025 ◽

2010 ◽

Vol 11 (1) ◽

pp. 33-63 ◽

Cited By ~ 7

Author(s):

MANH THANG NGUYEN ◽

DANNY DE SCHREYE ◽

JÜRGEN GIESL ◽

PETER SCHNEIDER-KAMP

Keyword(s):

Logic Programs ◽

Termination Analysis ◽

Rewrite Systems ◽

Analysis Techniques ◽

Programming Paradigm ◽

Generating Polynomial ◽

Direct Generalization ◽

Term Rewrite Systems

AbstractOur goal is to study the feasibility of porting termination analysis techniques developed for one programming paradigm to another paradigm. In this paper, we show how to adapt termination analysis techniques based on polynomial interpretations—very well known in the context of term rewrite systems—to obtain new (nontransformational) termination analysis techniques for definite logic programs (LPs). This leads to an approach that can be seen as a direct generalization of the traditional techniques in termination analysis of LPs, where linear norms and level mappings are used. Our extension generalizes these to arbitrary polynomials. We extend a number of standard concepts and results on termination analysis to the context of polynomial interpretations. We also propose a constraint-based approach for automatically generating polynomial interpretations that satisfy the termination conditions. Based on this approach, we implemented a new tool, called Polytool, for automatic termination analysis of LPs.

Download Full-text