An Extensional Characterization of Lambda-Lifting and Lambda-Dropping

Lambda-lifting and lambda-dropping respectively transform a block-structured functional program into recursive equations and vice versa. Lambda-lifting is known since the early 80's, whereas lambda-dropping is more recent. Both are split into an analysis and a transformation. Published work, however, has only concentrated on the analysis part. We focus here on the transformation part and more precisely on its formal correctness, which is an open problem. One of our two main theorems suggests us to define extensional versions of lambda-lifting and lambda-dropping, which we visualize both using ML and using type-directed partial evaluation.See revised version BRICS-RS-99-21