Calibrating computational feasibility by abstraction rank

Daniel Leivant

To appear at Symposium on Logic in Computer Science (LICS'2002), Copenhagen, Denmark, July 22nd - 25th, 2002


We characterize computationally the functions provable in second order logic with set existence restricted to natural classes of first order formulas. We showed elsewhere that set existence for first-order formulas yields precisely the Kalmar-elementary functions. Here we show that a classification of first-order set-existence by implicational rank yields a natural hierarchy of complexity classes: The functions (over words) constructively provable with set existence forformulas of implicational rank up to k are precisely the functions computable in deterministic time exp_k(n), whereexp_0 is P, and exp_{k+1} is 2 to the power exp_k. Moreover, set-existence for positive formulas yields exactly PTime, even if the underlying logic is classical. Our results can be formulated in a formgeneric to all free algebras. In particular, we conclude that a function over N computable by a program over N is provably terminating using set existence of rank up to k iff it iscomputable in deterministic space E_k(n), where E_0(n)=n, and E_{k+1} is 2 to the power E_k.

Server START Conference Manager
Update Time 15 Mar 2002 at 15:30:29
Start Conference Manager
Conference Systems