Paper: Light Logics and Optimal Reduction: Completeness and Complexity (at LICS 2007)

Authors: Patrick Baillot Paolo Coppola Ugo Dal Lago

Abstract

Typing of lambda-terms in Elementary and Light Affine Logic (EAL , LAL resp.) has been studied for two different reasons: on the one hand the evaluation of typed terms using LAL (EAL resp.) proof-nets admits a guaranteed polynomial (elementary, resp.) bound; on the other hand these terms can also be evaluated by optimal reduction using the abstract version of Lamping’s algorithm. The first reduction is global while the second one is local and asynchronous. We prove that for LAL (EAL resp.) typed terms, Lamping’s abstract algorithm also admits a polynomial (elementary, resp.) bound. We also show its soundness and completeness (for EAL and LAL with type fixpoints), by using a simple geometry of interaction model (context semantics).

BibTeX

  @InProceedings{BaillotCoppolaDalLa-LightLogicsandOptim,
    author = 	 {Patrick Baillot and Paolo Coppola and Ugo Dal Lago},
    title = 	 {Light Logics and Optimal Reduction: Completeness and Complexity},
    booktitle =  {Proceedings of the Twenty-Second Annual IEEE Symposium on Logic in Computer Science (LICS 2007)},
    year =	 {2007},
    month =	 {July}, 
    pages =      {421--430},
    location =   {Wroclaw, Poland}, 
    publisher =	 {IEEE Computer Society Press}
  }