On the Expressive Power of Light Affine Logic
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.
KeywordsCode Scheme Free Algebra Linear Logic Sequent Calculus Denotational Semantic
Unable to display preview. Download preview PDF.
- 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.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
- 8.Lafont, Y.: Soft linear logic and polynomial time. To appear in Theoretical Computer Science (2002)Google Scholar
- 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.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.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.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
- 14.Terui, K.: Light logic and polynomial time computation. PhD thesis, Keio University (2002)Google Scholar