On Proving the Correctness of Program Transformations Based on Free Theorems for Higher-order Polymorphic Calculi

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

Abstract: A number of program transformations currently of interest can be derived from Wadler's "free theorems" for calculi approximately modern functional languages. Although delicate but fundamental issues arise in proving the correctness of free theorems-based program transformations, these issues are usually left unaddressed in correctness proofs appearing in the literature. As a result, most such proofs are incomplete, and most free theorems-based transformations are applied to programs in calculi for which they are not actually known to be correct.The purpose of this paper is three-fold. First, we raise and clarify some of the issues that must be addressed when constructing correctness proofs for free theorems-based program transformations. Second, we offer a principled approach to developing such proofs. Third, we use Pitts' recent work on parametricity and observational equivalence to show how our approach can be used to give the first proof that transformations based on the Acid Rain theorems preserve observational equivalence of programs in a polymorphic lambda calculus supporting FPC-style fixpoints and algebraic data types. Correctness of the foldr-build rule, the destroy-unfoldr rule, and the hylofusion program transformation for this calculus follows immediately. The same approach is expected to yield complete correctness proofs for free theorems-based transformations in calculi which even more closely resemble languages with which programmers are concerned in practice.

Additional Information

Johann, Patricia. (2005) "On Proving the Correctness of Program Transformations Based on Free Theorems for Higher-order Polymorphic Calculi". Mathematical Structures in Computer Science, vol. 15, no. 2 (2005), pp. 201 - 229. ISSN: 0960-1295 Version Of Record Available From www.cambridge.org
Language: English
Date: 2005
polymorphic calculi, free theorems, unfoldr, PolyFix

Email this document to