Abstract
Soft type assignment systems STA, STA + , and STA B characterise by means of reduction of terms the computation in complexity classes PTIME, NP, and PSPACE, respectively. All these systems are inspired by linear logic and include polymorphism similar to the one of System F. We show that the presence of polymorphism gives undecidability of typechecking and type inference. We also show that reductions in decidable monomorphic versions of these systems also capture the same complexity classes in a way sufficient for the traditional complexity theory. The reductions we propose show in addition that the monomorphic systems to serve as a programming language require some metalanguage support since the program which operates on data has form and type which depend on the size of the input.
This work was partly supported by the Polish government grant no N N206 355836.
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.
References
Atassi, V., Baillot, P., Terui, K.: Verification of PTIME reducibility for System F terms: type inference in dual light affine logic. Logical Methods in Computer Science 3(4:10), 1–32 (2007)
Gaboardi, M., Marion, J.-Y., Rocca, S.R.D.: A logical account of PSPACE. In: Proceedings of the 35th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2008, pp. 121–131. ACM, New York (2008)
Gaboardi, M., Marion, J.-Y., Rocca, S.R.D.: Soft linear logic and polynomial complexity classes. ENTCS 205, 67–87 (2008)
Gaboardi, M., Ronchi Della Rocca, S.: A Soft Type Assignment System for λ-Calculus. In: Duparc, J., Henzinger, T.A. (eds.) CSL 2007. LNCS, vol. 4646, pp. 253–267. Springer, Heidelberg (2007)
Gaboardi, M., Rocca, S.R.D.: Type inference for a polynomial lambda calculus. In: Berardi, S., Damiani, F., De’Liguoro, U. (eds.) Types for Proofs and Programs, pp. 136–152. Springer, Heidelberg (2009)
Girard, J.-Y.: Light linear logic. Information and Computation 143, 175–204 (1998)
Goerdt, A.: Characterizing complexity classes by general recursive definitions in higher types. In: Proceedings of the 2nd Workshop on Computer Science Logic, London, UK, pp. 99–117. Springer, Heidelberg (1989)
Greenlaw, R., Hoover, J.H., Ruzzo, W.L.: Limits to Parallel Computation: P-Completeness Theory. Oxford University Press, USA (1995)
Kfoury, A.J., Tiuryn, J., Urzyczyn, P.: The undecidability of the semi-unification problem. Information and Computation 102(1), 83–101 (1993)
Lafont, Y.: Soft linear logic and polynomial time. Theoretical Computer Science 318, 163–180 (2004)
Leivant, D., Marion, J.-Y.: Lambda calculus characterizations of poly-time. In: Bezem, M., Groote, J.F. (eds.) TLCA 1993. LNCS, vol. 664, pp. 274–288. Springer, Heidelberg (1993)
Leivant, D., Marion, J.-Y.: Ramified recurrence and computational complexity ii: Substitution and poly-space. In: Kleine Büning, H. (ed.) CSL 1995. LNCS, vol. 1092, pp. 486–500. Springer, Heidelberg (1996)
Mairson, H.: A simple proof of a theorem of Statman. Theoretical Computer Science (103), 213–226 (1992)
Mairson, H.G., Terui, K.: On the Computational Complexity of Cut-Elimination in Linear Logic. In: Blundo, C., Laneve, C. (eds.) ICTCS 2003. LNCS, vol. 2841, pp. 23–36. Springer, Heidelberg (2003)
Schubert, A.: The complexity of β-reduction in low orders. In: Abramsky, S. (ed.) TLCA 2001. LNCS, vol. 2044, pp. 400–414. Springer, Heidelberg (2001)
Statman, R.: The typed λ-calculus is not elementary recursive. Theoretical Computer Science (9), 73–81 (1979)
Wells, J.B.: Typability and type checking in the second-order λ-calculus are equivalent and undecidable. In: Proceedings of Ninth Annual IEEE Symposium on Logic in Computer Science, pp. 176–185 (July 1994)
Wierzbicki, T.: Complexity of the higher order matching. In: Ganzinger, H. (ed.) CADE 1999. LNCS (LNAI), vol. 1632, pp. 82–96. Springer, Heidelberg (1999)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag GmbH Berlin Heidelberg
About this paper
Cite this paper
Chrząszcz, J., Schubert, A. (2011). The Role of Polymorphism in the Characterisation of Complexity by Soft Types. In: Murlak, F., Sankowski, P. (eds) Mathematical Foundations of Computer Science 2011. MFCS 2011. Lecture Notes in Computer Science, vol 6907. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-22993-0_22
Download citation
DOI: https://doi.org/10.1007/978-3-642-22993-0_22
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-22992-3
Online ISBN: 978-3-642-22993-0
eBook Packages: Computer ScienceComputer Science (R0)