Ugo Dal Lago. On the expressive power of light affine logic. In Carlo Blundo and Cosimo Laneve, editors, Eight Italian Conference on Theoretical Computer Science, Proceedings, volume 2841 of Lecture Notes in Computer Science, pages 216-227. Springer, 2003.

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 LAL using these coding schemes, obtaining a positive and a negative result.

[ bib | http ]

Back