Logic in Computer Science (LICS 2002)

Paper: Calibrating computational feasibility by abstraction rank (at LICS 2002)

Authors: Daniel Leivant

Abstract

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.

BibTeX

  @InProceedings{Leivant-Calibratingcomputat,
    author = 	 {Daniel Leivant},
    title = 	 {Calibrating computational feasibility by abstraction rank},
    booktitle =  {Proceedings of the Seventeenth Annual IEEE Symp. on Logic in Computer Science, {LICS} 2002},
    year =	 2002,
    editor =	 {Gordon Plotkin},
    month =	 {July}, 
    location =   {Copenhagen, Denmark}, 
    publisher =	 {IEEE Computer Society Press}
  }