Complexity Analysis of Precedence Terminating Infinite Graph Rewrite Systems

Naohi Eguchi
(Chiba University)

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.

In Aart Middeldorp and Femke van Raamsdonk: Proceedings 8th International Workshop on Computing with Terms and Graphs (TERMGRAPH 2014), Vienna, Austria, July 13, 2014, Electronic Proceedings in Theoretical Computer Science 183, pp. 33–47.
Published: 26th May 2015.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: