Abstract
In a previous work we introduced Dual Light Affine Logic (DLAL) ([BT04]) as a variant of Light Linear Logic suitable for guaranteeing complexity properties on lambda-calculus terms: all typable terms can be evaluated in polynomial time and all Ptime functions can be represented. In the present work we address the problem of typing lambda-terms in second-order DLAL. For that we give a procedure which, starting with a term typed in system F, finds all possible ways to decorate it into a DLAL typed term. We show that our procedure can be run in time polynomial in the size of the original Church typed system F term.
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
Atassi, V., Baillot, P., Terui, K.: Verification of Ptime reducibility for system F terms via Dual Light Affine Logic. Technical Report HAL ccsd-00021834 (July 2006)
Amadio, R.: Synthesis of max-plus quasi-interpretations. Fundamenta Informaticae 65, 29–60 (2005)
Asperti, A., Roversi, L.: Intuitionistic light affine logic. ACM Transactions on Computational Logic 3(1), 1–39 (2002)
Atassi, V.: Inférence de type en logique linéaire élémentaire. Master’s thesis, Université Paris 13 (2005)
Baillot, P.: Checking polynomial time complexity with types. In: Proceedings of IFIP TCS 2002, Montreal. Kluwer Academic Press, Dordrecht (2002)
Baillot, P.: Type inference for light affine logic via constraints on words. Theoretical Computer Science 328(3), 289–323 (2004)
Bellantoni, S., Cook, S.: New recursion-theoretic characterization of the polytime functions. Computational Complexity 2, 97–110 (1992)
Baillot, P., Terui, K.: Light types for polynomial time computation in lambda-calculus. In: Proceedings LICS 2004. IEEE Computer Society Press, Los Alamitos (2004)
Baillot, P., Terui, K.: A feasible algorithm for typing in elementary affine logic. In: Urzyczyn, P. (ed.) TLCA 2005. LNCS, vol. 3461, pp. 55–70. Springer, Heidelberg (2005)
Coppola, P., Dal Lago, U., Ronchi Della Rocca, S.: Elementary affine logic and the call-by-value lambda calculus. In: Urzyczyn, P. (ed.) TLCA 2005. LNCS, vol. 3461, pp. 131–145. Springer, Heidelberg (2005)
Coppola, P., Martini, S.: Typing lambda-terms in elementary logic with linear constraints. In: Abramsky, S. (ed.) TLCA 2001. LNCS, vol. 2044. Springer, Heidelberg (2001)
Coppola, P., Ronchi Della Rocca, S.: Principal typing in Elementary Affine Logic. In: Hofmann, M.O. (ed.) TLCA 2003. LNCS, vol. 2701, pp. 90–104. Springer, Heidelberg (2003)
Danos, V., Joinet, J.-B.: Linear logic and elementary time. Information and Computation 183(1), 123–137 (2003)
Girard, J.-Y.: Linear logic. Theoretical Computer Science 50, 1–102 (1987)
Girard, J.-Y.: Light linear logic. Information and Computation 143, 175–204 (1998)
Hofmann, M., Jost, S.: Static prediction of heap space usage for first-order functional programs. In: Proc. ACM POPL 2003 (2003)
Hofmann, M.: Linear types and non-size-increasing polynomial time computation. Information and Computation 183(1), 57–85 (2003)
Leivant, D., Marion, J.-Y.: Lambda-calculus characterisations of polytime. Fundamenta Informaticae 19, 167–184 (1993)
Marion, J.-Y., Moyen, J.-Y.: Efficient first order functional program interpreter with time bound certifications. In: Parigot, M., Voronkov, A. (eds.) LPAR 2000. LNCS, vol. 1955, pp. 25–42. Springer, Heidelberg (2000)
Terui, K.: Light Affine Lambda-calculus and polytime strong normalization. In: Proceedings LICS 2001. IEEE Computer Society, Los Alamitos (2001), Full version available at: http://research.nii.ac.jp/~terui
Terui, K.: Light affine set theory: a naive set theory of polynomial time. Studia Logica 77, 9–40 (2004)
Terui, K.: A translation of LAL into DLAL (preprint, 2004), http://research.nii.ac.jp/~terui
Wells, J.B.: Typability and type checking in system F are equivalent and undecidable. Ann. Pure Appl. Logic 98(1-3) (1999)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Atassi, V., Baillot, P., Terui, K. (2006). Verification of Ptime Reducibility for System F Terms Via Dual Light Affine Logic. In: Ésik, Z. (eds) Computer Science Logic. CSL 2006. Lecture Notes in Computer Science, vol 4207. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11874683_10
Download citation
DOI: https://doi.org/10.1007/11874683_10
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-45458-8
Online ISBN: 978-3-540-45459-5
eBook Packages: Computer ScienceComputer Science (R0)