The Essence of Eta-Expansion in Partial Evaluation

. Selective eta-expansion is a powerful "binding-time improvement", i.e., a sourceprogram modification that makes a partial evaluator yield better results. But like most bindingtime improvements, the exact problem it solves and the reason why have not been formalized and are only understood by few. In this paper, we describe the problem and the effect of eta-redexes in terms of monovariant binding-time propagation: eta-redexes preserve the static data flow of a source program by interfacing static higher-order values in dynamic contexts and dynamic higher-order values in static contexts. They contribute to two distinct binding-time improvements. We present two extensions of Gomard's monovariant binding-time analysis for the pure -calculus. Our extensions annotate and eta-expand -terms. The first one eta-expands static higher-order values in dynamic contexts. The second also eta-expands dynamic higher-order values in static contexts. As a significant application, we show that our firs..