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?
Best Answer
I find some aspects of this question difficult to understand. For example, the part about "calculating the value of the function requires transfinite induction up to $\varepsilon_0$" seems to conflate methods of proof (like transfinite induction) with methods of computation. Also, much (if not all) of the question appears to be about primitive recursive functionals of higher type (as in Gödel's Dialectica interpretation) rather than mere primitive recursive functions. So, the following may not be what the OP was looking for, but here goes anyway:
Not much can be said about the time complexity of computing primitive recursive functions (from natural numbers to natural numbers) except that it's primitive recursive and thus bounded by a finite level $F_n$ of the Grzegorczyk hierarchy (essentially equivalent to the fast-growing hierarchy, I believe).
On the other hand, for primitive recursive functionals of finite type, you can consider the problem of evaluating terms of type 0 (i.e., terms that denote natural numbers). Here, the only bound I can see for the time-complexity is level $\varepsilon_0$ of the Grzegorczyk hierarchy. For any fixed primitive recursive functional, evaluation of its numerical values would take time bounded by $F_\alpha$ for some $\alpha<\varepsilon_0$, but different functionals would need different $\alpha$'s, with no uniform bound below $\varepsilon_0$.
The relevance of the proof principle of transfinite induction up to $\varepsilon_0$ (for open formulas) is that this is what is needed, on top of primitive recursive arithmetic, to prove that every closed term of type 0, built from primitive recursive functionals of higher type, can be reduced to a numerical value.