scholarly journals Automation of Recursive Path Ordering for Infinite Labelled Rewrite Systems

2006 ◽  
pp. 332-346 ◽  
Author(s):  
Adam Koprowski ◽  
Hans Zantema
Keyword(s):  
Rewrite Systems ◽  
Path Ordering ◽  
Recursive Path

TERMINATION OF ABSTRACT REDUCTION SYSTEMS

2009 ◽  
Vol 20 (01) ◽  
pp. 57-82
Author(s):  
JEREMY E. DAWSON ◽  
RAJEEV GORÉ
Keyword(s):  
General Theorem ◽  
Combinatory Logic ◽  
Rewrite Systems ◽  
Path Ordering

We present a general theorem capturing conditions required for the termination of abstract reduction systems. We show that our theorem generalises another similar general theorem about termination of such systems. We apply our theorem to give interesting proofs of termination for typed combinatory logic. Thus, our method can handle most path-orderings in the literature as well as the reducibility method typically used for typed combinators. Finally we show how our theorem can be used to prove termination for incrementally defined rewrite systems, including an incremental general path ordering. All proofs have been formally machine-checked in Isabelle/HOL.

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 recursive path ordering

1985 ◽  
Vol 40 ◽  
pp. 323-328 ◽  
Author(s):  
M.S. Krishnamoorthy ◽  
P. Narendran
Keyword(s):  
Path Ordering ◽  
Recursive Path

Termination of rewriting in the Calculus of Constructions

2003 ◽  
Vol 13 (2) ◽  
pp. 339-414 ◽  
Author(s):  
DARIA WALUKIEWICZ-CHRZĄSZCZ
Keyword(s):  
Lambda Calculus ◽  
Term Rewriting ◽  
Higher Order ◽  
Strong Normalization ◽  
Term Rewriting System ◽  
Calculus Of Constructions ◽  
Path Ordering ◽  
Higher Order Functions ◽  
Rewriting Rules ◽  
Recursive Path

We show how to incorporate rewriting into the Calculus of Constructions and we prove that the resulting system is strongly normalizing with respect to beta and rewrite reductions. An important novelty of this paper is the possibility to define rewriting rules over dependently typed function symbols. We prove strong normalization for any term rewriting system, such that all function symbols satisfy the, so called, star dependency condition, and every rule is accepted by the Higher Order Recursive Path Ordering (which is an extension of the method created by Jouannaud and Rubio for the setting of the simply typed lambda calculus). The proof of strong normalization is done by using a typed version of reducibility candidates due to Coquand and Gallier. Our criterion is general enough to accept definitions by rewriting of many well-known higher order functions, for example dependent recursors for inductive types or proof carrying functions. This makes it a very good candidate for inclusion in a proof assistant based on the Curry-Howard isomorphism.

scholarly journals Graph Path Orderings

10.29007/6hkk ◽  
2018 ◽  
Author(s):  
Nachum Dershowitz ◽  
Jean-Pierre Jouannaud
Keyword(s):  
Building Block ◽  
Finite Set ◽  
Rewrite Rules ◽  
Path Ordering ◽  
The Many ◽  
Recursive Path

We define well-founded rewrite orderings on graphs and show that they can be used to show termination of a set of graph rewrite rules by verifying all their cyclic extensions. We then introduce the graph path ordering inspired by the recursive path ordering on terms and show that it is a well-founded rewrite ordering on graphs for which checking termination of a finite set of graph rewrite rules is decidable. Our ordering applies to arbitrary finite, directed, labeled, ordered multigraphs, hence provides a building block for rewriting with graphs, which should impact the many areas in which computations take place on graphs.

A path ordering for proving termination of AC rewrite systems

1995 ◽  
Vol 14 (2) ◽  
pp. 293-316 ◽  
Author(s):  
Deepak Kapur ◽  
G. Sivakumar ◽  
Hantao Zhang
Keyword(s):  
Rewrite Systems ◽  
Path Ordering
Sign in / Sign up

Export Citation Format

Share Document