Strictly orthogonal left linear rewrite systems and primitive recursion Original Research Article

Let F be a signature and R a strictly orthogonal rewrite system on ground terms of F. We give an effective proof of a bounding condition for R, based on a detailed analysis of how terms are transformed during the rewrite process, which allows us to give recursive bounds on the derivation lengths of terms. We give a syntactic characterisation of the Grzegorczyk hierarchy and a rewriting schema for calculating its functions. As a consequence of this, using results of Elias Tahhan–Bittar, it can be shown that, for n⩾3, the derivation length functions for functions in Grzegorczyk class View the MathML source belong to Grzegorczyk class View the MathML source. We also give recursive bounds for the derivation lengths of functions defined by parameter recursion.