Abstract
In this paper an implicit characterization of the complexity classes k-EXP and k-FEXP, for k ≥ 0, is given, by a type assignment system for a stratified λ-calculus, where types for programs are witnesses of the corresponding complexity class. Types are formulae of Elementary Linear Logic (ELL), and the hierarchy of complexity classes k-EXP is characterized by a hierarchy of types.
This work was supported by the LABEX MILYON (ANR-10-LABX-0070) of Université de Lyon, within the program ”Investissements d’Avenir” (ANR-11-IDEX-0007) operated by the French National Research Agency (ANR).
Chapter PDF
References
Baillot, P.: Stratified coherence spaces: a denotational semantics for light linear logic. Theor. Comput. Sci. 318(1-2), 29–55 (2004)
Baillot, P.: Elementary linear logic revisited for polynomial time and an exponential time hierarchy. In: Yang, H. (ed.) APLAS 2011. LNCS, vol. 7078, pp. 337–352. Springer, Heidelberg (2011)
Baillot, P., De Benedetti, E., Ronchi Della Rocca, S.: Characterizing polynomial and exponential complexity classes in elementary lambda-calculus. Tech. rep., 31 pages (2014), http://hal.archives-ouvertes.fr/hal-01015171
Bellantoni, S., Cook, S.A.: A new recursion-theoretic characterization of the polytime functions. Computational Complexity 2, 97–110 (1992)
Coppola, P., Dal Lago, U., Ronchi Della Rocca, S.: Light logics and the call-by-value lambda-calculus. Logical Methods in Computer Science 4(4) (2008)
Dal Lago, U.: Context semantics, linear logic, and computational complexity. ACM Trans. Comput. Log. 10(4) (2009)
Dal Lago, U., Masini, A., Zorzi, M.: Quantum implicit computational complexity. Theor. Comput. Sci. 411(2), 377–409 (2010)
Danos, V., Joinet, J.B.: Linear logic and elementary time. Inf. Comput. 183(1), 123–137 (2003)
Girard, J.Y.: Light linear logic. Inf. Comput. 143(2), 175–204 (1998)
Jones, N.D.: Computability and complexity - from a programming perspective. Foundations of computing series. MIT Press (1997)
Jones, N.D.: The expressive power of higher-order types or, life without cons. J. Funct. Program. 11(1), 5–94 (2001)
Lafont, Y.: Soft linear logic and polynomial time. Theor. Comput. Sci. 318(1-2), 163–180 (2004)
Leivant, D.: Predicative recurrence and computational complexity I: word recurrence and poly-time. In: Feasible Mathematics II, pp. 320–343. Birkhauser (1994)
Leivant, D.: Calibrating computational feasibility by abstraction rank. In: LICS, p. 345. IEEE Computer Society (2002)
Leivant, D., Marion, J.Y.: Lambda-calculus characterizations of poly-time. Fundam. Inform. 19(1/2), 167–184 (1993)
Madet, A.: Implicit Complexity in Concurrent Lambda-Calculi. Ph.D. thesis, Université Paris 7 (December 2012), http://tel.archives-ouvertes.fr/tel-00794977
Madet, A., Amadio, R.M.: An elementary affine lambda-calculus with multithreading and side effects. In: Ong, L. (ed.) Typed Lambda Calculi and Applications. LNCS, vol. 6690, pp. 138–152. Springer, Heidelberg (2011)
Marion, J.Y.: A type system for complexity flow analysis. In: LICS, pp. 123–132. IEEE Computer Society (2011)
Mazza, D.: Linear logic and polynomial time. Mathematical Structures in Computer Science 16(6), 947–988 (2006)
Ronchi Della Rocca, S., Paolini, L.: The Parametric Lambda-Calculus: a Metamodel for Computation. Texts in Theoretical Computer Science. Springer, Berlin (2004), http://www.springer.com/sgw/cda/frontpage/0,5-40356-72-14202886-0,00.html
Ronchi Della Rocca, S., Roversi, L.: Lambda-calculus and intuitionistic linear logic. Studia Logica 59(3), 417–448 (1997)
Terui, K.: Light affine lambda-calculus and polynomial time strong normalization. Arch. Math. Log. 46(3-4), 253–280 (2007)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 IFIP International Federation for Information Processing
About this paper
Cite this paper
Baillot, P., De Benedetti, E., Ronchi Della Rocca, S. (2014). Characterizing Polynomial and Exponential Complexity Classes in Elementary Lambda-Calculus. In: Diaz, J., Lanese, I., Sangiorgi, D. (eds) Theoretical Computer Science. TCS 2014. Lecture Notes in Computer Science, vol 8705. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-44602-7_13
Download citation
DOI: https://doi.org/10.1007/978-3-662-44602-7_13
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-662-44601-0
Online ISBN: 978-3-662-44602-7
eBook Packages: Computer ScienceComputer Science (R0)