We define a class of hyperbalancedλ-terms by imposing syntactic constraints on the construction of λ-terms, and show that such terms are strongly normalizable. Furthermore, we show that for any hyperbalanced term, the total number of superdevelopments needed to compute its normal form can be statically determined at the beginning of reduction. To obtain the latter result, we develop an algorithm that, in a hyperbalanced term M, statically detects all inessential (or unneeded) subterms which can be replaced by fresh variables without effecting the normal form of M; that is, full garbage collection can be performed before starting the reduction. Finally, we show that, modulo a restricted η-expansion, all simply typable λ-terms are hyperbalanced, implying importance of the class of hyperbalanced terms.
CITATION STYLE
Khasidashvili, Z., & Piperno, A. (1999). Normalization of typable terms by superdevelopments. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1584, pp. 260–283). Springer Verlag. https://doi.org/10.1007/10703163_18
Mendeley helps you to discover research relevant for your work.