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 ]