Asymptotic Speedups, Bisimulation and Distillation (Work in Progress)

  • Neil D. JonesEmail author
  • G. W. Hamilton
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8974)


Distillation is a fully automatic program transformation that can yield superlinear program speedups. Bisimulation is a key to the proof that distillation is correct, i.e., preserves semantics. However the proof, based on observational equivalence, is insensitive to program running times. This paper shows how distillation can give superlinear speedups on some “old chestnut” programs well-known from the early program transformation literature: naive reverse, factorial sum, and Fibonacci.


Free Variable Label Transition System Case Expression Partial Evaluator Root State 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.



This paper has been much improved as a result of discussions with Luke Ong and Jonathan Kochems at Oxford University. Referee comments were also very useful. This work was supported, in part, by DIKU at the University of Copenhagen, and by Science Foundation Ireland grant 10/CE/I1855 to Lero - the Irish Software Engineering Research Centre (


  1. 1.
    Burstall, R., Darlington, J.: A transformation system for developing recursive programs. J. ACM 24(1), 44–67 (1977)CrossRefzbMATHMathSciNetGoogle Scholar
  2. 2.
    Debois, S.: Imperative program optimization by partial evaluation. In: PEPM (ACM SIGPLAN 2004 Workshop on Partial Evaluation and Program Manipulation), pp. 113–122 (2004)Google Scholar
  3. 3.
    Ershov, A.P.: On the essence of compilation. In: Neuhold, E. (ed.) Formal Description of Programming Concepts, pp. 391–420. North-Holland, Amsterdam (1978)Google Scholar
  4. 4.
    Futamura, Y.: Partial evaluation of computation process - an approach to a compiler-compiler. High. Order Symb. Comput. 12(4), 381–391 (1999)CrossRefzbMATHGoogle Scholar
  5. 5.
    Gordon, A.D.: Bisimilarity as a theory of functional programming. Theor. Comput. Sci. 228(1–2), 5–47 (1999)CrossRefzbMATHGoogle Scholar
  6. 6.
    Hamilton, G.W.: Distillation: extracting the essence of programs. In: Proceedings of the ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation, pp. 61–70 (2007)Google Scholar
  7. 7.
    Hamilton, G.W., Jones, N.D.: Distillation with labelled transition systems. In: PEPM (ACM SIGPLAN 2012 Workshop on Partial Evaluation and Program Manipulation), pp. 15–24. ACM (2012)Google Scholar
  8. 8.
    Hamilton, G.W., Jones, N.D.: Proving the correctness of unfold/fold program transformations using bisimulation. In: Clarke, E., Virbitskaite, I., Voronkov, A. (eds.) PSI 2011. LNCS, vol. 7162, pp. 153–169. Springer, Heidelberg (2012) CrossRefGoogle Scholar
  9. 9.
    Jones, N., Gomard, C., Sestoft, P.: Partial Evaluation and Automatic Program Generation. Prentice Hall, New York (1993) zbMATHGoogle Scholar
  10. 10.
    Jones, N.D.: Computability and Complexity - From a Programming Perspective. Foundations of Computing Series. MIT Press, Cambridge (1997) zbMATHGoogle Scholar
  11. 11.
    Jones, N.D.: Transformation by interpreter specialisation. Sci. Comput. Program. 52, 307–339 (2004)CrossRefzbMATHGoogle Scholar
  12. 12.
    Lacey, D., Jones, N.D., Wyk, E.V., Frederiksen, C.C.: Compiler optimization correctness by temporal logic. High. Order Symb. Comput. 17(3), 173–206 (2004)CrossRefzbMATHGoogle Scholar
  13. 13.
    Milner, R.: Communication and Concurrency. PHI Series in Computer Science. Prentice Hall, Upper Saddle River (1989) zbMATHGoogle Scholar
  14. 14.
    Sørensen, M.H., Glück, R., Jones, N.: A positive supercompiler. J. Funct. Program. 6(6), 811–838 (1996)CrossRefGoogle Scholar
  15. 15.
    Turchin, V.F.: Supercompilation: techniques and results. In: Bjorner, D., Broy, M., Pottosin, I.V. (eds.) PSI 1996. LNCS, vol. 1181, pp. 227–248. Springer, Heidelberg (1996) CrossRefGoogle Scholar
  16. 16.
    Turchin, V.: The concept of a supercompiler. ACM Trans. Program. Lang. Syst. 8(3), 90–121 (1986)MathSciNetGoogle Scholar
  17. 17.
    Wadler, P.: Deforestation: transforming programs to eliminate trees. In: Ganzinger, H. (ed.) ESOP 1988. LNCS, vol. 300, pp. 344–358. Springer, Heidelberg (1988) Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2015

Authors and Affiliations

  1. 1.Computer Science DepartmentUniversity of CopenhagenCopenhagenDenmark
  2. 2.School of ComputingDublin City UniversityDublin 9Ireland

Personalised recommendations