Abstract
For several important systems of the λ-cube we study the time-complexity of type conversion. Non-elementary lower bounds are given for the type-conversion problem for λ\(\underset{\raise0.3em\hbox{$\smash{\scriptscriptstyle-}$}}{\omega }\)and λP and hence for the systems that include one of these systems. For λ\(\underset{\raise0.3em\hbox{$\smash{\scriptscriptstyle-}$}}{\omega }\)and λP a super-exponential upper bound is given to the length of reduction sequences starting from types that are legal in these systems.
The investigations were supported by the Foundation for Computer Science in the Netherlands (SION) with financial support from the Netherlands Organization for Scientific Research (NWO).
Preview
Unable to display preview. Download preview PDF.
References
Barendregt, H.P., ‘Lambda calculi with types', in: Abramski, S., Gabbay, D.M. & Maibaum, T.S.E., eds., Handbook of Logic in Computer Science, Oxford University Press, 1992.
Coquand, Th. and Huet, G., ‘The calculus of constructions', Information and Computation, Vol. 76, pp. 95–120, 1988.
Geuvers, H. and Nederhof, M.-J., ‘Modular proof of strong normalization for the calculus of constructions', in: The Journal of Functional Programming, Vol.1, pp. 155–189, 1991.
Pollack, R., ‘Typechecking in pure type systems', in: Nördstrom, B., Petersson, K. and Plotkin, G., eds., Proceedings of the 1992 Workshop on Types for Proofs and Programs, Båstad, June 92, pp. 289–306.
Rose, H.E., Subrecursion. Functions and Hierarchies, Clarendon Press, Oxford, 1984.
Schwichtenberg, H., ‘An upperbound for reduction sequences in the typed λ-calculus', Archive for Mathematical Logic, Vol.30, pp. 405–408, 1991.
Statman, R., ‘The typed lambda calculus is not elementary recursive', Theoretical Computer Science, Vol. 9, pp. 73–81, 1979.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1993 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Springintveld, J. (1993). Lower and upper bounds for reductions of types in λ and λP (extended abstract). In: Bezem, M., Groote, J.F. (eds) Typed Lambda Calculi and Applications. TLCA 1993. Lecture Notes in Computer Science, vol 664. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0037120
Download citation
DOI: https://doi.org/10.1007/BFb0037120
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-56517-8
Online ISBN: 978-3-540-47586-6
eBook Packages: Springer Book Archive