Higher-Order and Symbolic Computation, 14(2/3)221-260

Type-Based Useless-Variable Elimination

Naoki Kobayashi, Department of Computer Science, Graduate School of Information Science and Engineering, Tokyo Institute of Technology, 2-12-1 Ookayama, Meguro-ku, Tokyo 152-8552, Japan

Abstract: Useless-variable elimination is a transformation that eliminates variables whose values does not affect the result of a computation. We present a type-based method for useless-variable elimination and prove its correctness. The algorithm is a surprisingly simple extension of the usual type-reconstruction algorithm. Our method has several attractive features. First, it is simple, so that the proof of the correctness is clear and the method can be easily extended to deal with a polymorphic language. Second, it is efficient: for a simply-typed ?-calculus, it runs in time almost linear in the size of an input expression. Moreover, our transformation is optimal in a certain sense among those that preserve well-typedness, both for the simply-typed language and for an ML-style polymorphically-typed language.

Keywords: control-flow analysis, type-based analysis, type inference, useless-variable elimination

This article can be downloaded [here]. 		[picture of journal cover]

July 2003 - hosc@brics.dk