The Substitution Vanishes

  • Armin Kühnemann
  • Andreas Maletti
Part of the Lecture Notes in Computer Science book series (LNCS, volume 4019)


Accumulation techniques were invented to transform functional programs, which intensively use append functions (like inefficient list reversal), into more efficient programs, which use accumulating parameters instead (like efficient list reversal). In this paper we present a generalized and automatic accumulation technique that also handles programs operating with unary functions on arbitrary tree structures and employing substitution functions on trees which may replace different designated symbols by different trees. We show that this transformation does not deteriorate the efficiency with respect to call-by-need reduction.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Abadi, M., Cardelli, L., Curien, P.-L., Levy, J.-J.: Explicit substitutions. Journal of Functional Programming 1(4), 375–416 (1991)zbMATHCrossRefMathSciNetGoogle Scholar
  2. 2.
    Ariola, Z.M., Felleisen, M., Maraist, J., Odersky, M., Wadler, P.: A call-by-need lambda calculus. In: POPL 1995, Proceedings, pp. 233–246. ACM Press, New York (1995)CrossRefGoogle Scholar
  3. 3.
    Bauer, F.L., Wössner, H.: Algorithmic Language and Program Development. Springer, Heidelberg (1982)zbMATHGoogle Scholar
  4. 4.
    Bird, R.S.: The promotion and accumulation strategies in transformational programming. ACM TOPLAS 6(4), 487–504 (1984)zbMATHCrossRefMathSciNetGoogle Scholar
  5. 5.
    Boiten, E.A.: The many disguises of accumulation. Tech.Report 91-26, Dept. of Informatics, University of Nijmegen (1991)Google Scholar
  6. 6.
    Burstall, R.M., Darlington, J.: A transformation system for developing recursive programs. J. Assoc. Comput. Mach. 24, 44–67 (1977)zbMATHMathSciNetGoogle Scholar
  7. 7.
    Chitil, O.: Type inference builds a short cut to deforestation. In: ICFP 1999, Paris, France, vol. 34, pp. 249–260. ACM Sigplan Notices (1999)Google Scholar
  8. 8.
    Engelfriet, J.: Some open questions and recent results on tree transducers and tree languages. In: Book, R.V. (ed.) Formal language theory; perspectives and open problems, pp. 241–286. Academic Press, New York (1980)Google Scholar
  9. 9.
    Engelfriet, J., Vogler, H.: Macro tree transducers. J. Comput. Syst. Sci. 31, 71–145 (1985)zbMATHCrossRefMathSciNetGoogle Scholar
  10. 10.
    Engelfriet, J., Vogler, H.: Modular tree transducers. Theoret. Comput. Sci. 78, 267–304 (1991)zbMATHCrossRefMathSciNetGoogle Scholar
  11. 11.
    Engelfriet, J., Vogler, H.: The translation power of top-down tree-to-graph transducers. J. Comput. Syst. Sci. 49, 258–305 (1994)zbMATHCrossRefMathSciNetGoogle Scholar
  12. 12.
    Giesl, J., Kühnemann, A., Voigtländer, J.: Deaccumulation — Improving provability. In: Saraswat, V.A. (ed.) ASIAN 2003. LNCS, vol. 2896, pp. 146–160. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  13. 13.
    Gill, A., Launchbury, J., Peyton Jones, S.L.: A short cut to deforestation. In: FPCA 1993, Copenhagen, Denmark, pp. 223–231. ACM Press, New York (1993)CrossRefGoogle Scholar
  14. 14.
    Hughes, J.: A novel representation of lists and its application to the function “reverse”. Information Processing Letters 22, 141–144 (1986)CrossRefGoogle Scholar
  15. 15.
    Kühnemann, A.: Comparison of deforestation techniques for functional programs and for tree transducers. In: Middeldorp, A. (ed.) FLOPS 1999. LNCS, vol. 1722, pp. 114–130. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  16. 16.
    Kühnemann, A., Glück, R., Kakehi, K.: Relating accumulative and non-accumulative functional programs. In: Middeldorp, A. (ed.) RTA 2001. LNCS, vol. 2051, pp. 154–168. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  17. 17.
    Maletti, A.: Direct construction and efficiency analysis for the accumulation technique for 2-modular tree transducers. Master’s thesis, TU Dresden (2002)Google Scholar
  18. 18.
    Partsch, H.: Specification and Transformation of Programs – A Formal Approach to Software Development. Springer, Heidelberg (1990)zbMATHGoogle Scholar
  19. 19.
    Rounds, W.C.: Mappings and grammars on trees. Math. Syst. Th. 4, 257–287 (1970)zbMATHCrossRefMathSciNetGoogle Scholar
  20. 20.
    Sands, D.: A naïve time analysis and its theory of cost equivalence. Journal of Logic and Computation 5(4), 495–541 (1995)zbMATHCrossRefMathSciNetGoogle Scholar
  21. 21.
    Thatcher, J.W.: Generalized2 sequential machine maps. J. Comput. Syst. Sci. 4, 339–367 (1970)zbMATHMathSciNetCrossRefGoogle Scholar
  22. 22.
    Voigtländer, J.: Concatenate, reverse and map vanish for free. In: ICFP 2002, Pittsburgh, USA, pp. 14–25. ACM Press, New York (2002)CrossRefGoogle Scholar
  23. 23.
    Voigtländer, J.: Formal efficiency analysis for tree transducer composition. Tech.Report TUD-FI04-08, TU Dresden, Theory Comput. Syst. (to appear, 2004)Google Scholar
  24. 24.
    Voigtländer, J.: Tree Transducer Composition as Program Transformation. PhD thesis, TU Dresden (2004)Google Scholar
  25. 25.
    Wadler, P.: The concatenate vanishes. Note, University of Glasgow, 1987 (Revised, 1989)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2006

Authors and Affiliations

  • Armin Kühnemann
    • 1
  • Andreas Maletti
    • 1
  1. 1.Institute for Theoretical Computer Science, Department of Computer ScienceDresden University of TechnologyDresdenGermany

Personalised recommendations