scholarly journals A proof-theoretic study of abstract termination principles

2019 ◽  
Vol 29 (8) ◽  
pp. 1345-1366 ◽  
Author(s):  
Thomas Powell
Keyword(s):  
Complexity Analysis ◽  
Theoretic Analysis ◽  
Rewrite Systems ◽  
Abstract Setting ◽  
Term Rewrite Systems ◽  
Recursive Path

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.

scholarly journals On Implementing Modular Complexity Analysis

10.29007/zm9s ◽  
2018 ◽  
Author(s):  
Harald Zankl ◽  
Martin Korp
Keyword(s):  
Complexity Analysis ◽  
Upper Bounds ◽  
Rewrite Systems ◽  
Recent Approach ◽  
Term Rewrite Systems

We recall the recent approach by (Zankl and Korp, 2010) to prove upper bounds on the (derivational) complexity of term rewrite systems modularly. In this note we show that this approach is suitable to tighten bounds after they have been established. The idea is to replace proof steps with a large bound by (new) proofs that yield smaller bounds. An evaluation of the approach shows the benefits.

scholarly journals Analyzing Runtime Complexity via Innermost Runtime Complexity

10.29007/1nbh ◽  
2018 ◽  
Author(s):  
Florian Frohn ◽  
Jürgen Giesl
Keyword(s):  
Complexity Analysis ◽  
State Of The Art ◽  
Upper Bounds ◽  
The State ◽  
Sufficient Criterion ◽  
Rewrite Systems ◽  
Evaluation Strategy ◽  
Term Rewrite Systems

There exist powerful techniques to infer upper bounds on the innermost runtime complexity of term rewrite systems (TRSs), i.e., on the lengths of rewrite sequences that follow an innermost evaluation strategy. However, the techniques to analyze the (full) runtime complexity of TRSs are substantially weaker. In this paper, we present a sufficient criterion to ensure that the runtime complexity of a TRS coincides with its innermost runtime complexity. This criterion can easily be checked automatically and it allows us to use all techniques and tools for innermost runtime complexity in order to analyze (full) runtime complexity. By extensive experiments with an implementation of our results in the tool AProVE, we show that this improves the state of the art of automated complexity analysis significantly.

Modular termination of prefix-constrained term rewrite systems

2022 ◽  
Vol 174 ◽  
pp. 106207
Author(s):  
Nirina Andrianarivelo ◽  
Pierre Réty
Keyword(s):  
Rewrite Systems ◽  
Term Rewrite Systems

Term rewrite systems and varieties of lattices

1995 ◽  
pp. 255-277
Author(s):  
Ralph Freese ◽  
Jaroslav Jezek ◽  
J. Nation
Keyword(s):  
Rewrite Systems ◽  
Varieties Of Lattices ◽  
Term Rewrite Systems

REDEX CAPTURING IN TERM GRAPH REWRITING

1990 ◽  
Vol 01 (04) ◽  
pp. 369-386 ◽  
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.

Sign in / Sign up

Export Citation Format

Share Document