Proving Termination of Unfolding Graph Rewriting for General Safe Recursion

TL;DR

This paper introduces a new termination proof and complexity analysis for unfolding graph rewriting, demonstrating polynomial runtime and size bounds for general safe recursion expressed through infinite graph rewriting.

Contribution

It presents a novel termination order and interpretation method for unfolding graph rewriting, enabling polynomial complexity analysis for general safe recursion.

Findings

Successful embedding of rewriting rules into the termination order

Polynomial runtime complexity for general safe recursion

New criteria for polynomial size of normal forms

Abstract

In this paper we present a new termination proof and complexity analysis of unfolding graph rewriting which is a specific kind of infinite graph rewriting expressing the general form of safe recursion. We introduce a termination order over sequences of terms together with an interpretation of term graphs into sequences of terms. Unfolding graph rewrite rules expressing general safe recursion can be successfully embedded into the termination order by the interpretation, yielding the polynomial runtime complexity. Moreover, generalising the definition of unfolding graph rewrite rules for general safe recursion, we propose a new criterion for the polynomial runtime complexity of infinite GRSs and for the polynomial size of normal forms in infinite GRSs.