Springintveld, Jan Lower and upper bounds for reductions of types in \(\lambda{\underline \omega}\) and \(\lambda P\). (English) Zbl 0795.68028 Bezem, Marc (ed.) et al., Typed Lambda calculi and applications. International conference, TLCA ’93, March 16-18, 1993, Utrecht, the Netherlands. Proceedings. Berlin: Springer-Verlag. Lect. Notes Comput. Sci. 664, 391-405 (1993). Summary: For several important systems of the \(\lambda\)-cube we study the time- complexity of type conversion. Non-elementary lower bounds are given for the type-conversion problem for \(\lambda\underline{\omega}\) and \(\lambda P\) and hence for the systems that include one of these systems. For \(\lambda\underline{\omega}\) and \(\lambda P\) a super-exponential upper bound is given to the length of reduction sequences starting from types that are legal in these systems.For the entire collection see [Zbl 0866.00038]. Cited in 1 Document MSC: 68N15 Theory of programming languages 03B40 Combinatory logic and lambda calculus 68Q25 Analysis of algorithms and problem complexity 68Q45 Formal languages and automata Keywords:type reduction; calculus of constructions; \(\lambda\)-cube; type conversion PDFBibTeX XMLCite \textit{J. Springintveld}, Lect. Notes Comput. Sci. 664, 391--405 (1993; Zbl 0795.68028)