Lambda the Ultimate

inactiveTopic Short Cut Fusion is Correct
started 12/22/2003; 11:07:42 PM - last post 12/24/2003; 4:03:28 AM
Ehud Lamm - Short Cut Fusion is Correct  blueArrow
12/22/2003; 11:07:42 PM (reads: 5695, responses: 1)
Short Cut Fusion is Correct
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

Ehud Lamm - Re: Short Cut Fusion is Correct  blueArrow
12/24/2003; 4:03:28 AM (reads: 155, responses: 0)
Our discussion of Wadler's paper is here.