Polyvariant Analysis of the Untyped Lambda Calculus

Resumé

We present a polyvariant closure, safety, and binding time analysis for the untyped lambda calculus. The innovation is to analyze each abstraction afresh at all syntactic application points. This is achieved by a semantics-preserving program transformation followed by a novel monovariant analysis, expressed using type constraints. The constraints are solved in cubic time by a single fixed-point computation.

Safety analysis is aimed at determining if a term will cause an error during evaluation. We have recently proved that the monovariant safety analysis accepts strictly more terms than simple type inference. This paper demonstrates that the polyvariant transformation makes even more terms acceptable, even some without higher-order polymorphic types. Furthermore, polyvariant binding time analysis can improve the partial evaluators that base a polyvariant specialization on only monovariant binding time analysis.