Eleventh Annual IEEE Symposium on

Logic in Computer Science (LICS 1996)

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

Authors: Gerd Hillebrand Paris Kanellakis


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.


    author = 	 {Gerd Hillebrand and Paris Kanellakis},
    title = 	 {On the Expressive Power of Simply Typed and Let-Polymorphic Lambda Calculi},
    booktitle =  {Proceedings of the Eleventh Annual IEEE Symp. on Logic in Computer Science, {LICS} 1996},
    year =	 1996,
    editor =	 {Edmund M. Clarke},
    month =	 {July}, 
    pages =      {253-263},
    location =   {New Brunswick, NJ, USA}, 
    publisher =	 {IEEE Computer Society Press}