Complexity Analysis of Precedence Terminating Infinite Graph Rewrite Systems

TL;DR

This paper investigates a subclass of infinite graph rewrite systems with argument separation that are precedence terminating, demonstrating polynomial bounds on their runtime complexity and normal form sizes, and providing an alternative proof of prior results.

Contribution

It introduces precedence terminating graph rewrite systems with argument separation and proves polynomial bounds on their complexity and normal form sizes.

Findings

Polynomial bounds on runtime complexity

Polynomial bounds on normal form sizes

Alternative proof of Dal Lago et al.'s results

Abstract

The general form of safe recursion (or ramified recurrence) can be expressed by an infinite graph rewrite system including unfolding graph rewrite rules introduced by Dal Lago, Martini and Zorzi, in which the size of every normal form by innermost rewriting is polynomially bounded. Every unfolding graph rewrite rule is precedence terminating in the sense of Middeldorp, Ohsaki and Zantema. Although precedence terminating infinite rewrite systems cover all the primitive recursive functions, in this paper we consider graph rewrite systems precedence terminating with argument separation, which form a subclass of precedence terminating graph rewrite systems. We show that for any precedence terminating infinite graph rewrite system G with a specific argument separation, both the runtime complexity of G and the size of every normal form in G can be polynomially bounded. As a corollary, we obtain an alternative proof of the original result by Dal Lago et al.