We propose a sequence of equational transformations and specializations which turns a divide-and-conquer skeleton in Haskell into parallel loop nest in C. Our initial skeleton is often viewed as general divide-and-conquer. The specializations impose a balanced call tree, a fixed degree of the problem division, and elementwise operations. Our goal is to select parallel implementations of divide-and-conquer via a space-time mapping, which can be determined at compile time. The correctness of our transformations is proved by equational reasoning in Haskell; recursion and iteration are handled by induction. Finally, we demonstrate the practicality of the skeleton by expressing Strassen's matrix multiplication in it.
Keywords: divide-and-conquer, equational reasoning, Haskell, parallelization, skeleton, space-time mapping.
Ulrike Peiker, Martin Griebl