Paper: On the Expressive Power of Simply Typed and Let-Polymorphic Lambda Calculi (at LICS 1996)

Authors: Gerd G. Hillebrand Paris C. Kanellakis

Abstract

We present a functional framework for descriptive computational complexity, in which the Regular, First-order, Ptime, Pspace, k-Exptime, k-Expspace (k >= 1), and Elementary sets have syntactic characterizations. In this framework, typed lambda terms represent inputs and outputs as well as programs. The lambda calculi describing the above computational complexity classes are simply or Let-polymorphically typed with functionalities of fixed order. They consist of: order 0 atomic constants, order 1 equality among these constants, variables, application, and abstraction. Increasing functionality order by one for these languages corresponds to increasing the computational complexity by one alternation. This exact correspondence is established using a semantic evaluation of languages for each fixed order, which is the primary technical contribution of this paper.

BibTeX

  @InProceedings{HillebrandKanellaki-OntheExpressivePowe,
    author = 	 {Gerd G. Hillebrand and Paris C. Kanellakis},
    title = 	 {On the Expressive Power of Simply Typed and Let-Polymorphic Lambda Calculi},
    booktitle =  {Proceedings of the Eleventh Annual IEEE Symposium on Logic in Computer Science (LICS 1996)},
    year =	 {1996},
    month =	 {July}, 
    pages =      {253--263},
    location =   {New Brunswick, NJ, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }