Paper: Stratified Bounded Affine Logic for Logarithmic Space (at LICS 2007)

Authors: Ulrich Schöpp

Abstract

A number of complexity classes, most notably PTIME, have been characterised by sub-systems of linear logic. In this paper we show that the functions computable in log-arithmic space can also be characterised by a restricted version of linear logic. We introduce Stratified Bounded Affine Logic (SBAL), a restricted version of Bounded Linear Logic, in which not only the modality ! but also the universal quantifier is bounded by a resource polynomial. We show that the proofs of certain sequents in SBAL represent exactly the functions computable logarithmic space. The proof that SBAL-proofs can be compiled to LOGSPACE functions rests on modelling computation by interaction dialogues in the style of game semantics. We formulate the compilation of SBAL-proofs to space-efficient programs as an interpretation in a realisability model, in which realisers are taken from a Geometry of Interaction situation.

BibTeX

  @InProceedings{Schopp-StratifiedBoundedAf,
    author = 	 {Ulrich Schöpp},
    title = 	 {Stratified Bounded Affine Logic for Logarithmic Space},
    booktitle =  {Proceedings of the Twenty-Second Annual IEEE Symposium on Logic in Computer Science (LICS 2007)},
    year =	 {2007},
    month =	 {July}, 
    pages =      {411--420},
    location =   {Wroclaw, Poland}, 
    publisher =	 {IEEE Computer Society Press}
  }