×

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].

MSC:

68N15 Theory of programming languages
03B40 Combinatory logic and lambda calculus
68Q25 Analysis of algorithms and problem complexity
68Q45 Formal languages and automata
PDFBibTeX XMLCite