Characterizing complexity classes by general recursive definitions in higher types

Abstract

General recursive definitions in higher (finite) types, a different notation of finitely typed λ-terms with if-then-else and fixpoints, can be classified into an infinite syntactic hierarchy: A definition is in the n'th stage of this hierarchy, a so called rank-n-definition, iff n is an upper bound on the levels of the types occurring in it.

We restrict attention to definitions defining first-order functions, i.e. functions of type ind x...x ind→ind, ind for individuals, higher types only occur as detour in between.

Interpreting these definitions over finite structures we show: Rank-(n+1)-definitions characterize the complexity class

$$\begin{gathered}\cup DTIME(exp_n (p(x)),(exp_o (x) = x,exp_{n + 1} (x) = 2^{exp_n (x)} ). \hfill \\p(x) a poly \hfill \\\end{gathered}$$

This generalizes the result of Gurevich, Sazonov [Gu 83, Sa 80], that “normal” recursive definitions over finite structures characterize PTIME.