Question: If we have a rewrite system for primitive recursive functions, which simplifies each term according to how the function was defined, then what is the computational complexity of this calculation? That is, what is the coplexity of the normalization procedure? I have heard a claim that for a closed term calculating the value of the function requires transfinte induction up to $\epsilon\_0$. Is this true and where can I find a proof of this? 

For example in (Schwichtenberg & Wainer 2012) there is a lemma which says that a primitive recursive function is computable in $F\_{\alpha}$-bounded time, for some $\alpha<\omega$, where the set of all $F\_{\alpha}$ for $\alpha<\epsilon\_0$ is the Fast Growing Hierarchy. 

Is the measure of transfinite induction related to this way of bounding the complexity?

Answer: 
Actually there is no need for any transfinite induction.
A monotone interpretation yields that the derivation lengths
for any fixed term will be primitive recursive in the values of the numerals
plugged in. I have a paper in APAL with Cichon on the topic and, in addition, a paper
in JSL regarding Goedel's T showing that for T one needs epsilon\_0 recursion
for proving strong normalization by a monotone interpretation.

Best,

Andreas
Dear Andreas,

yes indeed. We have the follwing (not too difficult) fact: Let S^m(0) be the numeral for $m$.
For any PRA term $t(x\_1,\ldots,x\_n)$ The derivation length
of $t(S^{m\_1}(0),\ldots,S^{m\_n}(0))$ will be bounded by a primitive recursive
function (depending on $t$) with arguments $m\_1,\ldots,m\_n$. (Here I assume
standard rewrite systems for modelling primitive recursion.)

For terms from Gödel's T the derivation lengths become more complex depending
on the typelevel of the terms in question. 

My general conjecture is that 
for typical (not too small) subrecursive classes C the derivation lengths functions
for terms in C will not leave C.

The result for primitive recursion is not difficult whereas the result for Gödel's T is
somewhat involved.

For PRA there is also a tradeoff in terms of termination orderings.
Termination for rewrite systems for prim rec functions can be shown 
by the multiset path ordering. And termation proofs for the multiset
path ordering lead to prim rec derivation lengths (result by Dieter 
Hofbauer). The corresponding result for multiple recursion is one
of my earliest results in term rewriting theory. Wilfried Buchholz 
gave a nice prooftheoretic proof for these results in APAL.

There is also some nice application of term rewriting to more involved schemes of primitive
recursive functions. For example it can be used to show that prim rec functions
are closed under parameter recursion, or simple nested recursion, or even
unnested multiple recursion.

Best, 
Andreas