Abstract
In recent years increasing consensus has emerged that program transformers, e.g., partial evaluation and unfold/fold transformations, should terminate; a compiler should stop even if it performs fancy optimizations! A number of techniques to ensure termination of program transformers have been invented, but their correctness proofs are sometimes long and involved.
We present a framework for proving termination of program transformers, cast in the metric space of trees. We first introduce the notion of an abstract program transformer; a number of well-known program transformers can be viewed as instances of this notion. We then formalize what it menus that an abstract program transformer terminates and give a general sufficient condition for an abstract program transformer to terminate. We also consider some specific techniques for satisfying the condition. As applications we show that termination of some well-known program transformers either follows directly from the specific techniques or is easy to establish using the general condition.
Our framework facilitates simple termination proofs for program transformers. Also, since our framework is independent of the language being transformed, a single correctness proof can be given in our framework for program transformers using essentially the same technique in the context of different languages. Moreover, it is easy to extend termination proofs for program transformers to accommodate changes to these transformers. Finally, the framework may prove useful for designing new termination techniques for program transformers.
This is a preview of subscription content, log in via an institution.
Preview
Unable to display preview. Download preview PDF.
References
M. Alpuente, M. Falaschi, and G. Vidal. Narrowing-driven partial evaluation of functional logic programs. In H.R. Nielson, editor, European Symposium on Programming, volume 1058 of Lecture Notes in Computer Science, pages 46–61. Springer-Verlag, 1996.
A. Arnold and M. Nivat. Metric interpretations of infinite trees and semantics of non deterministic recursive programs. Theoretical Computer Science, 11:181–205, 1980.
A. Arnold and M. Nivat. The metric space of infinite trees. Algebraic and topological properties. Fundamenta Informaticae, III(4):445–476, 1980.
R. Bird. Tabulation techniques for recursive programs. ACM Computing Surveys, 12(4):403–417, 1980.
D. Bjørner, A.P. Ershov, and N.D. Jones, editors. Partial Evaluation and Mixed Computation. North-Holland, Amsterdam, 1988.
S.L. Bloom. All solutions of a system of recursion equations in infinite trees and other contraction theories. Journal of Computer and System Sciences, 27:225 255, 1983.
S.L. Bloom, C.C. Elgot, and J.B Wright. Vector iteration in pointed iterative theories. SIAM Journal of Computing, 9(3):525–540, 1980.
S.L. Bloom and D. Patterson. Easy solutions are hard to find. In Colloquium on Trees in Algebra and Programming, volume 112 of Lecture Notes in Computer Science, pages 135–146. Springer-Verlag, 1981.
S.L. Bloom and R. Tindell. Compatible orderings on the metric theory of trees. SIAM Journal of Computing, 9(4):683–691, 1980.
M. Bruynooghe, D. Do Schreye, and B. Krekels. Compiling control. Journal of Logic programming, 6:135–102, 1989.
R.M. Burstall and J. Darlington. A transformation system for developing recursive programs. Journal of the Association for Computing Machines, 24(1):44–67, 1977.
B. Courcelle. Fundamental properties of infinite trees. Th eorctical Computer Science, 25:95–109, 1983.
O. Danvy, R. Glück, and P. Thiemann, editors. Partial Evaluation, volume 1110 of Lecture Notes in Computer Science. Springer-Verlag, 1990.
N. Dershowitz. Termination of rewriting. Journal of Symbolic Computation, 3, 1987.
Y. Futamura and K. Nogi. Generalized partial computation. In Bjørner et al. [5], pages 133–151.
R. Glück, J. Jørgensen, B. Martens, and M.H. Sørensen. Controlling conjunctive partial deduction. In II. Kuchen and D.S. Swierstra, editors, Programming Languages: Implementations, Logics and Programs, volume 1140 of Lecture Notes in Computer Science, pages 137–151. Springer-Verlag, 1996.
R. Glück and M.H. Sørensen. Partial deduction and driving are equivalent. In M. Hermenegildo and J. Penjam, editors, Programming Languages: Implementations, Logics and Programs, volume 844 of Lecture Notes in Computer Science, pages 165–181. Springer-Verlag, 1994.
R. Glück and M.H. Sørensen. A roadmap to metacomputation by supercompilation. In Danvy et al. [13], pages 137–160.
G. Higman. Ordering by divisibility in abstract algebras. Proceedings of the London Mathematical Society, (3) 2:326–336, 1952.
N.D. Jones. The essence of program transformation by partial evaluation and driving. In N.D. Jones, M. Hagiya, and M. Sato, editors, Logic, Language, and Computation, volume 792 of Lecture Notes in Computer Science, pages 206–224. Springer-Verlag, 1994. Festschrift in honor of S.Takasu.
N.D. Jones, C.K. Gomard, and P. Sestoft. Partial Evaluation and Automatic Program Generation. Prentice-Hall, 1993.
J.B. Kruskal. Well-quasi-ordering, the tree theorem, and Vazsonyi's conjecture. Transactions of the American Mathematical Society, 95:210–225, 1960.
M. Leuschel and B. Martens. Global control for partial deduction through characteristic atoms and global trees. In Danvy et al. [13], pages 263–283.
J.W. Lloyd. Foundations of Logic Programming. Springer-Verlag, 1984.
M. Main, A. Melton, M. Mislove, and D. Schmidt, editors. Mathematical Foundations of Programming Language Semantics, volume 298 of Lecture Notes in Computer Science. Springer-Verlag, 1987.
B. Martens and J. Gallagher. Ensuring global termination of partial deduction while allowing flexible polyvariancc. In L. Sterling, editor, International Conference on Logic Programming, pages 597–613. MIT Press, 1995.
J. Mycielski and W. Taylor. A compactification of the algebra of terms. Algebra Universalis, 6:159–163, 1976.
C.St.J.A. Nash-Williams. On well-quasi-ordering finite trees. Proceedings of the Cambridge Mathematical Society, 59:833–835, 1963.
A. Pettorossi. A powerful strategy for deriving efficient programs by transformation. In ACM Conference on Lisp and Functional Programming, pages 273–281. ACM Press, 1984.
A. Pettorossi and M. Proietti. A comparative revisitation of some program transformation techniques. In Danvy et al. [13], pages 355–385.
M. Proietti and A. Pettorossi. The loop absorption and the generalization strategies for the development of logic programs and partial deduction. Journal of Logic programming, 16:123–161, 1993.
W. Rudin. Principles of Mathematical Analysis. Mathematics Series. McGraw-Hill, third edition, 1976.
E. Ruf and D. Weise. On the specialization of online program specializers. Journal of Functional Programming, 3(3):251–281, 1993.
M.D. Smyth. Topology. In S. Abramsky, D.M. Gabbay, and T.S.E. Maibaum, editors, Handbook of Logic in Computer Science, volume II, pages 641–761. Oxford University Press, 1992.
M.H. Sørenscn and R. Glück. An algorithm of generalization in positive supercompilat.ion. In J.W. Lloyd, editor, Logic Programming: Proceedings of the 1995 International Symposium, pages 465–479. MIT Press, 1995.
M.H. Sørensen, R. Glück, and N.D. Jones. Towards unifying deforestation, supercompilation, partial evaluation, and generalized partial computation. In D. Sannella, editor, European Symposium on Programming, volume 788 of Lecture Notes in Computer Science, pages 485–500. Springer-Verlag, 1994.
M.H. Sørensen, R. Glück, and N.D. Jones. A positive supercompiler. Journal of Functional Programming, 6(6):811–838, 1996.
H. Tamaki and T. Sato. Unfold/fold transformation of logic programs. In S.-å. Tärnlund, editor, International Conference on Logic Programming, pages 127–138. Uppsala University, 1984.
V.F. Turchin. The concept of a supercompiler. ACM Transactions on Programming Languages and Systems, 8(3):292–325, 1986.
V.F. Turchin. The algorithm of generalization in the supercompiler. In Bjørner et al. [5], pages 531–549.
V.F. Turchin. On generalization of lists and strings in supercompilation. Technical Report CSc. TR 96-002, City College of the City University of New York, 1996.
P.L. Wadler. Deforestation: Transforming programs to eliminate intermediate trees. Theoretical Computer Science, 73:231–248, 1990.
D. Weise, R. Conybeare, B. Ruf, and S. Seligman. Automatic online partial evaluation. In J. Hughes, editor, Conference on Functional Programming and Computer Architecture, volume 523 of Lecture Notes in Computer Science, pages 165–191. Springer-Verlag, 1991.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1998 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Sørensen, M.H.B. (1998). Convergence of program transformers in the metric space of trees. In: Jeuring, J. (eds) Mathematics of Program Construction. MPC 1998. Lecture Notes in Computer Science, vol 1422. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0054297
Download citation
DOI: https://doi.org/10.1007/BFb0054297
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-64591-7
Online ISBN: 978-3-540-69345-1
eBook Packages: Springer Book Archive