Paper: Stratified Bounded Affine Logic for Logarithmic Space (at LICS 2007)
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{Schpp-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} }