Skip to main content
SpringerLink
Log in
Book cover

International Workshop on Logic Programming Synthesis and Transformation

LOPSTR 1998: Logic-Based Program Synthesis and Transformation pp 199–218Cite as

Improving Homeomorphic Embedding for Online Termination

  • Conference paper
  • First Online:

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

Abstract

Well-quasi orders in general, and homeomorphic embedding in particular, have gained popularity to ensure online termination of program analysis, specialisation and transformation techniques. It has been recently shown that the homeomorphic embedding relation is strictly more powerful than a large class of involved well-founded approaches. In this paper we provide some additional investigations on the power of homeomorphic embedding. We, however, also illustrate that the homeomorphic embedding relation suffers from several inadequacies in contexts where logical variables arise. We therefore present new, extended homeomorphic embedding relations to remedy this problem.

Part of the work was done while the author was Post-doctoral Fellow of the Fund for Scientific Research - Flanders Belgium (FWO).

This is a preview of subscription content, 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

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. E. Albert, M. Alpuente, M. Falaschi, P. Julián, and G. Vidal. Improving control in functional logic program specialization. In G. Levi, editor, Static Analysis. Proceedings of SAS’98, LNCS 1503, pages 262–277, Pisa, Italy, September 1998. Springer-Verlag.

    Google Scholar 

  2. M. Alpuente, M. Falaschi, P. Julián, and G. Vidal. Spezialisation of lazy functional logic programs. In Proceedings of PEPM’97, the ACM Sigplan Symposium on Partial Evaluation and Semantics-Based Program Manipulation, pages 151–162, Amsterdam, The Netherlands, 1997. ACM Press.

    Google Scholar 

  3. M. Alpuente, M. Falaschi, and G. Vidal. Narrowing-driven partial evaluation of functional logic programs. In H. Riis Nielson, editor, Proceedings of the 6th European Symposium on Programming, ESOP’96, LNCS 1058, pages 45–61. Springer-Verlag, 1996.

    Google Scholar 

  4. 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 

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

    Article  MATH  MathSciNet  Google Scholar 

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

    MATH  Google Scholar 

  7. 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 

  8. D. De Schreye, R. Glück, J. Jørgensen, M. Leuschel, B. Martens, and M. H. Sørensen. Conjunctive partial deduction: Foundations, control, algorithms and experiments. To appear in The Journal of Logic Programming, 1999.

    Google Scholar 

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

    Article  MATH  MathSciNet  Google Scholar 

  10. 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 

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

    Article  MATH  MathSciNet  Google Scholar 

  12. J. Gallagher. Tutorial on specialisation of logic programs. In Proceedings of PEPM’93, the ACM Sigplan Symposium on Partial Evaluation and Semantics-Based Program Manipulation, pages 88–98. ACM Press, 1993.

    Google Scholar 

  13. R. Glück and J. Hatcliff, John Jørgensen. Generalization in hierarchies of online program specialization systems. In this volume.

    Google Scholar 

  14. 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 of the International Symposium on Programming Languages, Implementations, Logics and Programs (PLILP’96), LNCS 1140, pages 152–166, Aachen, Germany, September 1996. Springer-Verlag.

    Google Scholar 

  15. 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 

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

    Google Scholar 

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

    MATH  MathSciNet  Google Scholar 

  18. 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 

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

    Google Scholar 

  20. J. Jørgensen, M. Leuschel, and B. Martens. Conjunctive partial deduction in practice. In J. Gallagher, editor, Proceedings of the International Workshop on Logic Program Synthesis and Transformation (LOPSTR’96), LNCS 1207, pages 59–82, Stockholm, Sweden, August 1996. Springer-Verlag.

    Google Scholar 

  21. 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 

  22. L. Lafave and J. Gallagher. Constraint-based partial evaluation of rewriting-based functional logic programs. In N. Fuchs, editor, Proceedings of the International Workshop on Logic Program Synthesis and Transformation (LOPSTR’97), LNCS 1463, pages 168–188, Leuven, Belgium, July 1998.

    Chapter  Google Scholar 

  23. P. Lescanne. Rewrite orderings and termination of rewrite systems. In A. Tarlecki, editor, Mathematical Foundations of Computer Science 1991, LNCS 520, pages 17–27, Kazimierz Dolny, Poland, September 1991. Springer-Verlag.

    Google Scholar 

  24. P. Lescanne. Well rewrite orderings and well quasi-orderings. Technical Report No 1385, INRIA-Lorraine,France, January 1991.

    Google Scholar 

  25. M. Leuschel. The ecce partial deduction system and the dppd library of benchmarks. Obtainable via http://www.cs.kuleuven.ac.be/~dtai , 1996

  26. M. Leuschel. Advanced Techniques for Logic Program Specialisation. PhD thesis, K.U. Leuven, May 1997. Accessible via http://www.ecs.soton.ac.uk/~mal .

  27. M. Leuschel. Homeomorphic embedding for online termination. Technical Report DSSE-TR-98-11, Department of Electronics and Computer Science, University of Southampton, UK, October 1998.

    Google Scholar 

  28. M. Leuschel. On the power of homeomorphic embedding for online termination. In G. Levi, editor, Static Analysis. Proceedings of SAS’98, LNCS 1503, pages 230–245, Pisa, Italy, September 1998. Springer-Verlag.

    Google Scholar 

  29. M. Leuschel and D. De Schreye. Constrained partial deduction and the preservation of characteristic trees. New Generation Computing, 16(3):283–342, 1998.

    Article  Google Scholar 

  30. 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 

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

    Article  Google Scholar 

  32. N. Lindenstrauss, Y. Sagiv, and A. Serebrenik. Unfolding the mystery of mergesort. In N. Fuchs, editor, Proceedings of the International Workshop on Logic Program Synthesis and Transformation (LOPSTR’97), LNCS 1463, pages 206–225, Leuven, Belgium, July 1998.

    Chapter  Google Scholar 

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

    Google Scholar 

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

    Article  MATH  MathSciNet  Google Scholar 

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

    Google Scholar 

  36. 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 

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

    Article  MATH  Google Scholar 

  38. 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 

  39. 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 

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

    Article  MATH  MathSciNet  Google Scholar 

  41. L. Plümer. Termination Proofs for Logic Programs. LNCS446. Springer-Verlag, 1990.

    MATH  Google Scholar 

  42. 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 

  43. E. Ruf. Topics in Online Partial Evaluation. PhD thesis, Stanford University, March1993.

    Google Scholar 

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

    MATH  Google Scholar 

  45. M. H. Sørensen. Convergence of program transformers in the metric space of trees. In Mathematics of Program Construction, Proceedings of MPC’98, LNCS 1422, pages 315–337. Springer-Verlag, 1998.

    Chapter  Google Scholar 

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

    Google Scholar 

  47. M. H. Sørensen, R. Glück, and N. D. Jones. A positive supercompiler. Journal of Functional Programming, 6(6):811–838, 1996.

    MATH  Google Scholar 

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

    Google Scholar 

  49. 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 

  50. W. Vanhoof and B. Martens. To parse or not to parse. In N. Fuchs, editor, Proceedings of the International Workshop on Logic Program Synthesis and Transformation (LOPSTR’97), LNCS 1463, pages 322–342, Leuven, Belgium, July 1997.

    Chapter  Google Scholar 

  51. A. Weiermann. Complexity bounds for some finite forms of Kruskal’s theorem. Journal of Symbolic Computation, 18(5):463–488, November 1994.

    Article  MATH  MathSciNet  Google Scholar 

  52. 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 Electronics and Computer Science, University of Southampton, UK

    Michael Leuschel

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

    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. Department of Information Science, Uppsala University, Box 311, S-751 05, Uppsala, Sweden

    Pierre Flener

Rights and permissions

Reprints and permissions

Copyright information

© 1999 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Leuschel, M. (1999). Improving Homeomorphic Embedding for Online Termination. In: Flener, P. (eds) Logic-Based Program Synthesis and Transformation. LOPSTR 1998. Lecture Notes in Computer Science, vol 1559. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48958-4_11

Download citation

  • DOI: https://doi.org/10.1007/3-540-48958-4_11

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-65765-1

  • Online ISBN: 978-3-540-48958-0

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation