Abstract
We give new proofs of soundness (all representable functions on base types lies in certain complexity classes) for Elementary Affine Logic, LFPL (a language for polytime computation close to realistic functional programming introduced by one of us), Light Affine Logic and Soft Affine Logic. The proofs are based on a common semantical framework which is merely instantiated in four different ways. The framework consists of an innovative modification of realizability which allows us to use resource-bounded computations as realisers as opposed to including all Turing computable functions as is usually the case in realizability constructions. For example, all realisers in the model for LFPL are polynomially bounded computations whence soundness holds by construction of the model. The work then lies in being able to interpret all the required constructs in the model. While being the first entirely semantical proof of polytime soundness for light logics, our proof also provides a notable simplification of the original already semantical proof of polytime soundness for LFPL. A new result made possible by the semantic framework is the addition of polymorphism and a modality to LFPL thus allowing for an internal definition of inductive datatypes.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Asperti, A., Roversi, L.: Intuitionistic light affine logic. ACM Transactions on Computational Logic 3(1), 137–175 (2002)
Baillot, P., Mogbil, V.: Soft lambda-calculus: a language for polynomial time computation. In: Proceedings of the 7th International Conference on Foundations of Software Science and Computational Structures (2004)
Bellantoni, S., Niggl, K.H., Schwichtenberg, H.: Higher type recursion, ramification and polynomial time. Annals of Pure and Applied Logic 104, 17–30 (2000)
Cook, S., Urquhart, A.: Functional interpretations of feasible constructive arithmetic. Annals of Pure and Applied Logic 63(2), 103–200 (1993)
Coppola, P., Martini, S.: Typing lambda terms in elementary logic with linear constraints. In: Proceedings of the 6th International Conference on Typed Lambda-Calculus and Applications, pp. 76–90 (2001)
Crossley, J., Mathai, G., Seely, R.: A logical calculus for polynomialtime realizability. Journal of Methods of Logic in Computer Science 3, 279–298 (1994)
Lago, U.D., Hofmann, M.: Quantitative models and implicit complexity. Arxiv Preprint (2005), Available from http://arxiv.org/cs.LO/0506079
Girard, J.-Y.: Light linear logic. Information and Computation 143(2), 175–204 (1998)
Hofmann, M.: Linear types and non-size-increasing polynomial time computation. In: Proceedings of the 14th IEEE Syposium on Logic in Computer Science, pp. 464–473 (1999)
Hofmann Safe, M.: recursion with higher types and BCK-algebra. Annals of Pure and Applied Logic 104, 113–166 (2000)
Hofmann, M., Scott, P.: Realizability models for BLL-like languages. Theoretical Computer Science 318(1-2), 121–137 (2004)
Kreisel, G.: Interpretation of analysis by means of constructive functions of finite types. In: Heyting, A. (ed.) Constructivity in Mathematics, pp. 101–128. North-Holland, Amsterdam (1959)
Lafont Soft, Y.: linear logic and polynomial time. Theoretical Computer Science 318, 163–180 (2004)
van Emde Boas, P.: Machine models and simulation. In: Handbook of Theoretical Computer Science. Algorithms and Complexity, vol. A, pp. 1–66. Elsevier, Amsterdam (1990)
Xi, H., Pfenning, F.: Dependent types in practical programming. In: Proceedings of the 26th ACM SIGPLAN Symposium on Principles of Programming Languages, pp. 214–227 (1999)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Dal Lago, U., Hofmann, M. (2005). Quantitative Models and Implicit Complexity. In: Sarukkai, S., Sen, S. (eds) FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science. FSTTCS 2005. Lecture Notes in Computer Science, vol 3821. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11590156_15
Download citation
DOI: https://doi.org/10.1007/11590156_15
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-30495-1
Online ISBN: 978-3-540-32419-5
eBook Packages: Computer ScienceComputer Science (R0)