Skip to main content
SpringerLink
Log in

On the Power of Homeomorphic Embedding for Online Termination

  • Conference paper
  • First Online:
Static Analysis (SAS 1998)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 1503))

Included in the following conference series:

Abstract

Recently well-quasi orders in general, and homeomorphic embedding in particular, have gained popularity to ensure the termination of program analysis, specialisation and transformation techniques. In this paper we investigate and clarify for the first time, both intuitively and formally, the advantages of such an approach over one using well-founded orders. Notably we show that the homeomorphic embedding relation is strictly more powerful than a large class of involved well-founded approaches.

Part of the work was done while the author was Post-doctoral Fellow of the Fund for Scientific Research - Flanders Belgium (FWO) and visiting DIKU, University of Copenhagen.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. M. Alpuente, M. Falaschi, P. Julián, and G. Vidal. Spezialisation of lazy functional logic programs. In Proceedings PEPM’97, pages 151–162, Amsterdam, The Netherlands, 1997. ACM Press.

    Google Scholar 

  2. M. Alpuente, M. Falaschi, and G. Vidal. Narrowing-driven partial evaluation of functional logic programs. In H. Riis Nielson, editor, Proceedings ESOP’96, LNCS 1058, pages 45–61. Springer-Verlag, 1996.

    Google Scholar 

  3. K. R. Apt. Introduction to logic programming. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, chapter 10, pages 495–574. North-Holland Amsterdam, 1990.

    Google Scholar 

  4. R. Bol. Loop checking in partial deduction. The Journal of Logic Programming, 16(1&2):25–46, 1993.

    Article  MATH  MathSciNet  Google Scholar 

  5. M. Bruynooghe, D. De Schreye, and B. Martens. A general criterion for avoiding infnite unfolding during partial deduction. New Generation Computing, 11(1):47–79, 1992.

    MATH  Google Scholar 

  6. D. De Schreye and S. Decorte. Termination of logic programs: The never ending story. The Journal of Logic Programming, 19 & 20:199–260, May 1994.

    Google Scholar 

  7. N. Dershowitz. Termination of rewriting. Journal of Symbolic Computation, 3:69–116, 1987.

    Article  MATH  MathSciNet  Google Scholar 

  8. N. Dershowitz and J.-P. Jouannaud. Rewrite systems. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, Vol.B, pages 243–320. Elsevier, MIT Press, 1990.

    Google Scholar 

  9. N. Dershowitz and Z. Manna. Proving termination with multiset orderings. Communications of the ACM, 22(8):465–476, 1979.

    Article  MATH  MathSciNet  Google Scholar 

  10. J. Gallagher. Tutorial on specialisation of logic programs. In Proceedings PEPM’93, pages 88–98. ACM Press, 1993.

    Google Scholar 

  11. R. Glück, J. Jørgensen, B. Martens, and M. H. Sørensen. Controlling conjunctive partial deduction of definite logic programs. In H. Kuchen and S. Swierstra, editors, Proceedings PLILP’96, LNCS 1140, pages 152–166, Aachen, Germany, September 1996. Springer-Verlag.

    Google Scholar 

  12. R. Glück and M. H. Sørensen. A roadmap to supercompilation. In O. Danvy, R. Glück, and P. Thiemann, editors, Proceedings of the 1996 Dagstuhl Seminar on Partial Evaluation, LNCS 1110, pages 137–160, Schloß Dagstuhl, 1996. Springer-Verlag.

    Google Scholar 

  13. J. Gustedt. Algorithmic Aspects of Ordered Structures. PhD thesis, Technische Universität Berlin, 1992.

    Google Scholar 

  14. G. Higman. Ordering by divisibility in abstract algebras. Proceedings of the London Mathematical Society, 2:326–336, 1952.

    Article  MATH  MathSciNet  Google Scholar 

  15. G. Huet. Confluent reductions: Abstract properties and applications to term rewriting systems. Journal of the ACM, 27(4):797–821, 1980.

    Article  MATH  MathSciNet  Google Scholar 

  16. N. D. Jones. An introduction to partial evaluation. ACM Computing Surveys, 28(3):480–503, September 1996.

    Google Scholar 

  17. N. D. Jones, C. K. Gomard, and P. Sestoft. Partial Evaluation and Automatic Program Generation. Prentice Hall, 1993.

    Google Scholar 

  18. J. Jørgensen, M. Leuschel, and B. Martens. Conjunctive partial deduction in practice. In J. Gallagher, editor, Proceedings LOPSTR’96, LNCS 1207, pages 59–82, Stockholm, Sweden, August 1996. Springer-Verlag.

    Google Scholar 

  19. J. B. Kruskal. Well-quasi ordering, the tree theorem, and Vazsonyi’s conjecture. Transactions of the American Mathematical Society, 95:210–225, 1960.

    Article  MATH  MathSciNet  Google Scholar 

  20. L. Lafave and J. Gallagher. Constraint-based partial evaluation of rewriting-based functional logic programs. In N. Fuchs, editor, Proceedings LOPSTR’97, LNCS, Leuven, Belgium, July 1997. Springer-Verlag.

    Google Scholar 

  21. P. Lescanne. Well rewrite orderings and well quasi-orderings. Technical Report N∘ 1385, INRIA-Lorraine, France, January 1991.

    Google Scholar 

  22. M. Leuschel. The ECCE partial deduction system and the DPPD library of benchmarks. 1996–1998. Obtainable via http://www.cs.kuleuven.ac.be/~dtai.

  23. M. Leuschel. Advanced Techniques for Logic Program Specialisation. PhD thesis, K.U. Leuven, May 1997. Accessible via http://www.cs.kuleuven.ac.be/~michael.

  24. M. Leuschel. Homeomorphic Embedding for Online Termination. Technical Report, Department of Electronics and Computer Science, University of Southampton, 1998.

    Google Scholar 

  25. M. Leuschel and B. Martens. Global control for partial deduction through characteristic atoms and global trees. In O. Danvy, R. Glück, and P. Thiemann, editors, Proceedings of the 1996 Dagstuhl Seminar on Partial Evaluation, LNCS 1110, pages 263–283, Schloß Dagstuhl, 1996. Springer-Verlag.

    Google Scholar 

  26. M. Leuschel, B. Martens, and D. De Schreye. Controlling generalisation and polyvariance in partial deduction of normal logic programs. ACM Transactions on Programming Languages and Systems, 20(1):208–258, January 1998.

    Google Scholar 

  27. N. Lindenstrauss, Y. Sagiv, and A. Serebrenik. Unfolding the mystery of mergesort. In N. Fuchs, editor, Proceedings LOPSTR’97, LNCS, Leuven, Belgium, July 1997. Springer-Verlag.

    Google Scholar 

  28. J. W. Lloyd. Foundations of Logic Programming. Springer-Verlag, 1987.

    Google Scholar 

  29. J. W. Lloyd and J. C. Shepherdson. Partial evaluation in logic programming. The Journal of Logic Programming, 11(3&4):217–242, 1991.

    Article  MathSciNet  MATH  Google Scholar 

  30. R. Marlet. Vers une Formalisation de l’Évaluation Partielle. PhD thesis, Université de Nice-Sophia Antipolis, December 1994.

    Google Scholar 

  31. B. Martens. On the Semantics of Meta-Programming and the Control of Partial Deduction in Logic Programming. PhD thesis, K.U. Leuven, February 1994.

    Google Scholar 

  32. B. Martens and D. De Schreye. Automatic ifnite unfolding using well-founded measures. The Journal of Logic Programming, 28(2):89–146, August 1996.

    Google Scholar 

  33. B. Martens, D. De Schreye, and T. Horváth. Sound and complete partial deduction with unfolding based on well-founded measures. Theoretical Computer Science, 122(1–2):97–117, 1994.

    Article  MATH  MathSciNet  Google Scholar 

  34. B. Martens and J. Gallagher. Ensuring global termination of partial deduction while allowing flexible polyvariance. In L. Sterling, editor, Proceedings ICLP’95, pages 597–613, Kanagawa, Japan, June 1995. MIT Press.

    Google Scholar 

  35. J. Martin. Sonic partial deduction. Technical Report, Department of Electronics and Computer Science, University of Southampton, 1998.

    Google Scholar 

  36. P.-A. Melliès. On a duality between Kruskal and Dershowitz theorems. In K. G. Larsen, editor, Proceedings of ICALP’98, LNCS, Aalborg, Denmark, 1998. Springer-Verlag.

    Google Scholar 

  37. A. Middeldorp and H. Zantema. Simple termination of rewrite systems. Theoretical Computer Science, 175(1):127–158, 1997.

    Article  MATH  MathSciNet  Google Scholar 

  38. L. Plümer. Termination Proofs for Logic Programs. LNCS 446. Springer-Verlag, 1990.

    MATH  Google Scholar 

  39. L. Puel. Using unavoidable set of trees to generalize Kruskal’s theorem. Journal of Symbolic Computation, 8:335–382, 1989.

    Article  MATH  MathSciNet  Google Scholar 

  40. E. Ruf. Topics in Online Partial Evaluation. PhD thesis, Stanford University, March 1993.

    Google Scholar 

  41. D. Sahlin. Mixtus: An automatic partial evaluator for full Prolog. New Generation Computing, 12(1):7–51, 1993.

    Article  MATH  Google Scholar 

  42. M. H. Sørensen and R. Glück. An algorithm of generalization in positive supercompilation. In J. W. Lloyd, editor, Proceedings ILPS’95, pages 465–479, Portland, USA, December 1995. MIT Press.

    Google Scholar 

  43. M. H. Sørensen, R. Glück and N.D. Jones. A positive supercompiler. Journal of Functional Programming, 1996.

    Google Scholar 

  44. J. Stillman. Computational Problems in Equational Theorem Proving. PhD thesis, State University of New York at Albany, 1988.

    Google Scholar 

  45. V. F. Turchin. The concept of a supercompiler. ACM Transactions on Programming Languages and Systems, 8(3):292–325, 1986.

    Article  MATH  MathSciNet  Google Scholar 

  46. W. Vanhoof and B. Martens. To parse or not to parse. In N. Fuchs, editor, Proceedings LOPSTR’97, LNCS, Leuven, Belgium, July 1997. Springer-Verlag.

    Google Scholar 

  47. D. Weise, R. Conybeare, E. Ruf, and S. Seligman. Automatic online partial evaluation. In Proceedings of the Conference on Functional Programming Languages and Computer Architectures, LNCS 523, pages 165–191, Harvard University, 1991. Springer-Verlag.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, K.U. Leuven, Belgium

    Michael Leuschel

  2. Department of Electronics and Computer Science, University of Southampton, UK

    Michael Leuschel

  3. DIKU, University of Copenhagen, Denmark

    Michael Leuschel

Authors
  1. Michael Leuschel
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Dipartimento di Informatica, Università di Pisa, Corso Italia, 40, I-56125, Pisa, Italy

    Giorgio Levi

Rights and permissions

Reprints and permissions

Copyright information

© 1998 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Leuschel, M. (1998). On the Power of Homeomorphic Embedding for Online Termination. In: Levi, G. (eds) Static Analysis. SAS 1998. Lecture Notes in Computer Science, vol 1503. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-49727-7_14

Download citation

  • DOI: https://doi.org/10.1007/3-540-49727-7_14

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-65014-0

  • Online ISBN: 978-3-540-49727-1

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation