Abstract
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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Asperti, A., Roversi, L.: Intuitionistic light affine logic. ACM Transactions on Computational Logic 3(1), 137–175 (2002)
Asperti, A.: Light affine logic. In: Proceedings of the 13th IEEE Syposium on Logic in Computer Science, pp. 300–308 (1998)
Baillot, P.: Stratified coherent spaces: a denotational semantics for light linear logic. Presented at the Second International Workshop on Implicit Computational Complexity (2000)
Danos, V., Joinet, J.-B.: Linear logic and elementary time. Information and Computation 183(1), 123–137 (2003)
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)
Girard, J.-Y.: Linear logic. Theoretical Computer Science 50, 1–102 (1987)
Girard, J.-Y.: Light linear logic. Information and Computation 143(2), 175–204 (1998)
Lafont, Y.: Soft linear logic and polynomial time. To appear in Theoretical Computer Science (2002)
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)
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)
Murawski, A., Ong, L.: Can safe recursion be interpreted in light logic? Presented at the Second International Workshop on Implicit Computational Complexity (2000)
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)
Roversi, L.: Light affine logic as a programming language: a first contribution. International Journal of Foundations of Computer Science 11(1), 113–152 (2000)
Terui, K.: Light logic and polynomial time computation. PhD thesis, Keio University (2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Dal Lago, U. (2003). On the Expressive Power of Light Affine Logic. In: Blundo, C., Laneve, C. (eds) Theoretical Computer Science. ICTCS 2003. Lecture Notes in Computer Science, vol 2841. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-45208-9_18
Download citation
DOI: https://doi.org/10.1007/978-3-540-45208-9_18
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-20216-5
Online ISBN: 978-3-540-45208-9
eBook Packages: Springer Book Archive