General Ramified Recurrence is Sound for Polynomial Time

TL;DR

This paper extends Leivant's ramified recurrence characterization of polynomial-time functions from word algebras to general free algebras by using graph representations to efficiently share subterms.

Contribution

It generalizes the soundness of ramified recurrence for polynomial time to all free algebras through graph-based term representations.

Findings

Extended ramified recurrence to general free algebras

Graph representations enable sharing of subterms

Maintains polynomial time bounds

Abstract

Leivant's ramified recurrence is one of the earliest examples of an implicit characterization of the polytime functions as a subalgebra of the primitive recursive functions. Leivant's result, however, is originally stated and proved only for word algebras, i.e. free algebras whose constructors take at most one argument. This paper presents an extension of these results to ramified functions on any free algebras, provided the underlying terms are represented as graphs rather than trees, so that sharing of identical subterms can be exploited.