A Generalization of Short-Cut Fusion and Its Correctness Proof

ASU Author/Contributor (non-ASU co-authors, if there are any, appear on document)
Patricia Johann Ph.D, Professor (Creator)
Institution
Appalachian State University (ASU )
Web Site: https://library.appstate.edu/

Abstract: Short-cut fusion is a program transformation technique that uses a single local transformation - called the foldr build rule - to remove certain intermediate lists from modularly constructed functional programs. Arguments that short-cut fusion is correct typical appeal either to intuition or to "free theorems" - even though the latter have not been known to hold for the languages supporting higher-order polymorphic functions and fixed point recursion in which short-cut fusion is usually applied. In this paper we use Pitts' recent demonstration that contextual equivalence in such languages is relationally parametric to prove that programs in them which have undergone short-cut fusion are contextually equivalent to their unfused counterparts. For each algebraic data type we then define a generalization of build which constructs substitution instances of its associated data structures, and use Pitts' techniques to prove the correctness of a contextual equivalence-preserving fusion rule which generalizes short-cut fusion. These rules optimize compositions of functions that uniformly consume algebraic data structures with functions that uniformly produces substitution instances of those data structures.

Additional Information

Publication
Johann, Patricia (2002) "A Generalization Of Short-Cut Fusion And Its Correctness Proof". Higher-Order and Symbolic Computation, vol. 15 pp. 273 - 300. ISSN: 1573-0557 Version Of Record Available At www.springer.com
Language: English
Date: 2002
Keywords
functional programming, program transformation, polymorphism, parametricity, operational semantics, correctness proofs, short-cut fusion, theorems for free

Email this document to