Abstract

We investigate a simply typed term system ℘R ω aimed at defining partial primitive recursive functionals over arbitrary Scott domains . A hierarchy of complexity classes R n ω for functionals definable in ℘R ω is given based on a hierarchy of term classes ℘R n ωpn denoting the n th 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 ℘R n ωpn , 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 t ϵ ℘R n ωpn depends strongly on the representation of t . We present a measure denoted μ = n rel v , ϱ for prenormal terms t to be read as t is of complexity n with valued free variables v and valued type π . It is shown that μ is stable on αβη equal terms and furthermore, μ ⩽ min {n |∃t′ ϵ ℘R n ω pn .t′ = αβη t} . Moreover, if t is in a certain μ- normal form 2, the estimate above is even true with equality, that is μ 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