On the Expressive Power of Light Affine Logic

  • Ugo Dal Lago
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2841)


Light Affine Logic (LAL) is a formal system derived from Linear Logic that is claimed to correspond, through the Curry-Howard Isomorphism, to the class FPTIME of polytime functions. The completeness of the system with respect to FPTIME has been proved by embedding different presentations of this complexity class into LAL. The dual property of polytime soundness, on the other hand, has been stated and proved in a more debatable way, depending crucially on the underlying coding scheme. In this paper, we introduce two relevant classes of coding schemes, namely uniform and canonical coding schemes. We then investigate on the equality between FPTIME and the classes of functions that are representable in LAL using these coding schemes, obtaining a positive and a negative result.


Code Scheme Free Algebra Linear Logic Sequent Calculus Denotational Semantic 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Asperti, A., Roversi, L.: Intuitionistic light affine logic. ACM Transactions on Computational Logic 3(1), 137–175 (2002)CrossRefMathSciNetGoogle Scholar
  2. 2.
    Asperti, A.: Light affine logic. In: Proceedings of the 13th IEEE Syposium on Logic in Computer Science, pp. 300–308 (1998)Google Scholar
  3. 3.
    Baillot, P.: Stratified coherent spaces: a denotational semantics for light linear logic. Presented at the Second International Workshop on Implicit Computational Complexity (2000)Google Scholar
  4. 4.
    Danos, V., Joinet, J.-B.: Linear logic and elementary time. Information and Computation 183(1), 123–137 (2003)zbMATHCrossRefMathSciNetGoogle Scholar
  5. 5.
    Girard, J.-Y., Scedrov, A., Scott, P.J.: Bounded linear logic: A modular approach to polynomial time computability. Theoretical Computer Science 97(1), 1–66 (1992)zbMATHCrossRefMathSciNetGoogle Scholar
  6. 6.
    Girard, J.-Y.: Linear logic. Theoretical Computer Science 50, 1–102 (1987)zbMATHCrossRefMathSciNetGoogle Scholar
  7. 7.
    Girard, J.-Y.: Light linear logic. Information and Computation 143(2), 175–204 (1998)zbMATHCrossRefMathSciNetGoogle Scholar
  8. 8.
    Lafont, Y.: Soft linear logic and polynomial time. To appear in Theoretical Computer Science (2002)Google Scholar
  9. 9.
    Mairson, H., Neergard, P.M.: LAL is square: Representation and expressiveness in light affine logic. Presented at the Fourth International Workshop on Implicit Computational Complexity (2002)Google Scholar
  10. 10.
    Maurel, F.: Nondederministic light logics and NP-time. In: Proceedings of the 6th International Conference on Typed Lambda Calculi and Applications, pp. 241–255 (2003)Google Scholar
  11. 11.
    Murawski, A., Ong, L.: Can safe recursion be interpreted in light logic? Presented at the Second International Workshop on Implicit Computational Complexity (2000)Google Scholar
  12. 12.
    Murawski, A., Ong, L.: Evolving games and essential nets for affine polymorphism. In: Proceedings of 14th Annual Conference of the European Association of Computer Science Logic, pp. 360–375 (2000)Google Scholar
  13. 13.
    Roversi, L.: Light affine logic as a programming language: a first contribution. International Journal of Foundations of Computer Science 11(1), 113–152 (2000)CrossRefMathSciNetGoogle Scholar
  14. 14.
    Terui, K.: Light logic and polynomial time computation. PhD thesis, Keio University (2002)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2003

Authors and Affiliations

  • Ugo Dal Lago
    • 1
  1. 1.Dipartimento di Scienze dell’InformazioneUniversità di BolognaBolognaItaly

Personalised recommendations