Work it, wrap it, fix it, fold it

Article English OPEN
Sculthorpe, N ; Hutton, G (2014)
  • Publisher: Cambridge University Press
  • Related identifiers: doi: 10.1017/S0956796814000045
  • Subject:
    acm: TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS

The worker/wrapper transformation is a general-purpose technique for refactoring recursive programs to improve their performance. The two previous approaches to formalising the technique were based upon different recursion operators and different correctness conditions. In this article we show how these two approaches can be generalised in a uniform manner by combining their correctness conditions, extend the theory with new conditions that are both necessary and sufficient to ensure the correctness of the worker/wrapper technique, and explore the benefits that result. All the proofs have been mechanically verified using the Agda system.
  • References (17)
    17 references, page 1 of 2

    Backhouse, Roland. (2002). Galois Connections and Fixed Point Calculus. Pages 89-150 of: Algebraic and Coalgebraic Methods in the Mathematics of Program Construction. Springer.

    Bird, Richard, & de Moor, Oege. (1997). Algebra of Programming. Prentice Hall.

    Burstall, Rod. M., & Darlington, John. (1977). A Transformation System for Developing Recursive Programs. Journal of the ACM, 24(1), 44-67.

    Farmer, Andrew, Gill, Andy, Komp, Ed, & Sculthorpe, Neil. (2012). The HERMIT in the Machine: A Plugin for the Interactive Transformation of GHC Core Language Programs. Pages 1-12 of: Haskell Symposium. ACM.

    Gammie, Peter. (2011). Strict Unwraps Make Worker/Wrapper Fusion Totally Correct. Journal of Functional Programming, 21(2), 209-213.

    Gill, Andy, & Hutton, Graham. (2009). The Worker/Wrapper Transformation. Journal of Functional Programming, 19(2), 227-251.

    Hoare, Tony. (1972). Proof of Correctness of Data Representations. Acta Informatica, 1(4), 271-281.

    Hutton, Graham, Jaskelioff, Mauro, & Gill, Andy. (2010). Factorising Folds for Faster Functions. Journal of Functional Programming, 20(3&4), 353-373.

    Meijer, Erik, Fokkinga, Maarten M., & Paterson, Ross. (1991). Functional Programming with Bananas, Lenses, Envelopes and Barbed Wire. Pages 124-144 of: Functional Programming Languages and Computer Architecture. Springer.

    Morgan, Carroll, & Gardiner, P. H. B. (1990). Data Refinement by Calculation. Acta Informatica, 27(6), 481-503.

  • Metrics
    No metrics available
Share - Bookmark