Abstract
This paper shows that a bisimulation approach can be used to prove the correctness of unfold/fold program transformation algorithms. As an illustration, we show how our approach can be use to prove the correctness of positive supercompilation (due to Sørensen et al). Traditional program equivalence proofs show the original and transformed programs are contextually equivalent, i.e., have the same termination behaviour in all closed contexts. Contextual equivalence can, however, be difficult to establish directly.
Gordon and Howe use an alternative approach: to represent a program’s behaviour by a labelled transition system whose bisimilarity relation is a congruence that coincides with contextual equivalence. Labelled transition systems are well-suited to represent global program behaviour.
On the other hand, unfold/fold program transformations use generalization and folding, and neither is easy to describe contextually, due to use of non-local information. We show that weak bisimulation on labelled transition systems gives an elegant framework to prove contextual equivalence of original and transformed programs. One reason is that folds can be seen in the context of corresponding unfolds.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Abramsky, S.: The lazy lambda calculus. In: Research Topics in Functional Programming, pp. 65–116. Addison-Wesley (1990)
Bol, R.: Loop Checking in Partial Deduction. Journal of Logic Programming 16(1-2), 25–46 (1993)
Burstall, R., Darlington, J.: A transformation system for developing recursive programs. Journal of the ACM 24(1), 44–67 (1977)
Dershowitz, N., Jouannaud, J.P.: Rewrite Systems. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, pp. 243–320. Elsevier, MIT Press (1990)
Gordon, A.D.: Bisimilarity as a theory of functional programming. Theoretical Computer Science 228(1-2), 5–47 (1999)
Hamilton, G.: 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)
Higman, G.: Ordering by Divisibility in Abstract Algebras. Proceedings of the London Mathematical Society 2, 326–336 (1952)
Howe, D.J.: Proving congruence of bisimulation in functional programming languages. Information and Computation 124(2), 103–112 (1996)
Jones, N., Gomard, C., Sestoft, P.: Partial Evaluation and Automatic Program Generation. Prentice Hall (1993)
Kruskal, J.: Well-Quasi Ordering, the Tree Theorem, and Vazsonyi’s Conjecture. Transactions of the American Mathematical Society 95, 210–225 (1960)
Lacey, D., Jones, N.D., Wyk, E.V., Frederiksen, C.C.: Compiler optimization correctness by temporal logic. Higher-Order and Symbolic Computation 17(3), 173–206 (2004)
Leuschel, M.: On the Power of Homeomorphic Embedding for Online Termination. In: Proceedings of the International Static Analysis Symposium, Pisa, Italy, pp. 230–245 (1998)
Marlet, R.: Vers une Formalisation de l’Évaluation Partielle. Ph.D. thesis, Université de Nice - Sophia Antipolis (1994)
Sands, D.: Proving the Correctness of Recursion-Based Automatic Program Transformations. Theoretical Computer Science 167(1-2), 193–233 (1996)
Sørensen, M.H., Glück, R.: An Algorithm of Generalization in Positive Supercompilation. In: Tison, S. (ed.) CAAP 1994. LNCS, vol. 787, pp. 335–351. Springer, Heidelberg (1994)
Sørensen, M.H., Glück, R., Jones, N.: A Positive Supercompiler. Journal of Functional Programming 6(6), 811–838 (1996)
Turchin, V.: Program Transformation by Supercompilation. In: Ganzinger, H., Jones, N.D. (eds.) Programs as Data Objects. LNCS, vol. 217, pp. 257–281. Springer, Heidelberg (1986)
Wadler, P.: Deforestation: Transforming Programs to Eliminate Trees. In: Ganzinger, H. (ed.) ESOP 1988. LNCS, vol. 300, pp. 344–358. Springer, Heidelberg (1988)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Hamilton, G.W., Jones, N.D. (2012). Proving the Correctness of Unfold/Fold Program Transformations Using Bisimulation. In: Clarke, E., Virbitskaite, I., Voronkov, A. (eds) Perspectives of Systems Informatics. PSI 2011. Lecture Notes in Computer Science, vol 7162. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-29709-0_15
Download citation
DOI: https://doi.org/10.1007/978-3-642-29709-0_15
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-29708-3
Online ISBN: 978-3-642-29709-0
eBook Packages: Computer ScienceComputer Science (R0)