Abstract :
We investigate a simply typed term system ℘Rω aimed at defining partial primitive recursive functionals over arbitrary Scott domains (Scott, 1982). A hierarchy of complexity classes Rnω for functionals definable in ℘Rω is given based on a hierarchy of term classes View the MathML source denoting the nth class of so-called prenormal terms. They come into play by the key observation that every term t can be transformed by what we call higher type modularization as a kind of inversion of normalization into an αβη equal term t′ having almost no structural complexity. However, it turns out that normalization of a prenormal term may increase its structural complexity with respect to the classes View the MathML source, and conversely, ground type modularization being still possible may reduce it. Thus the structural complexity of a prenormal term t defined as the least n with View the MathML source depends strongly on the representation of t.
We present a measure denoted View the MathML source for prenormal terms t to be read as tis of complexity n with valued free variablesView the MathML sourceand valued typeπ. It is shown that μ is stable on αβη equal terms and furthermore, View the MathML source. Moreover, if t is in a certain μ-normal form 2, the estimate above is even true with equality, that is μ(t) yields the structural complexity of the maximal modularization of t, clearly the best a purely structural measure can do.
μ-normal forms 2 do not always exist. The counterexample we give, however, clearly shows that μ does not only take into account the structural complexity of a prenormal term but also the nature and computationl complexity of the algorithm it represents.
