Short Cut Fusion: Proved and Improved
- 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 particular program transformation technique which uses a single, local transformation — called the foldrbuild rule — to remove certain intermediate lists from modularly constructed functional programs. Arguments that short cut fusion is correct typically 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. The same techniques in fact yield a much more general result. For each algebraic data type we define a generalization augment of build which constructs substitution instances of its associated data structures. Together with the well-known generalization cata of folder to arbitrary algebraic data types, this allows us to formulate and prove correct for each a contextual equivalence-preserving cata-augment fusion rule. These rules optimize compositions of functions that uniformly consume algebraic data structures with functions that uniformly produce substitution instances of them.
Short Cut Fusion: Proved and Improved
PDF (Portable Document Format)
271 KB
Created on 9/30/2016
Views: 1235
Additional Information
- Publication
- Johann, Patricia (2001) "Short Cut Fusion: Proved and Improved". Proceedings, Workshop on the Semantics, Application, and Implementation of Program Generation (SAIG'01), Springer-Verlag LNCS 2196 (2001), pp. 47-71. Version Of Record Available From www.springer.com
- Language: English
- Date: 2001
- Keywords
- short cut fusion, cata-augment, polymorphic functions, free theorems