|
Short Cut Fusion is Correct. Patricia Johann. Journal of Functional Programming, vol. 13(4) (2003), pp. 797 - 814.
Short cut fusion has traditionally been treated purely syntactically, with little consideration given to the underlying semantics of the programs to which it is applied. In particular, the fact that the foldr-build rule holds only for languages admitting parametric models has been downplayed in the literature, and the application of short cut fusion to functional programs has been justified by appealing either to intuition about the operational behavior of build and foldr or to Wadler's "free theorems" (Wadler, 1989). But intuition is unsuitable as a basis for formal proofs, and the correctness of "free theorems" itself relies on the existence
of parametric models. Since no parametric models for modern functional languages are known to exist, these justifications of short cut fusion for them are far from satisfactory.
In this paper we provide the first-ever formal proof of the correctness of short cut fusion for a calculus supporting both higher-order polymorphic functions and fixpoint recursion.
Interesting and important.
Posted to functional by Ehud Lamm on 12/22/03; 11:07:58 PM
|
|
Short Cut Fusion is Correct
