Skip to main content
SpringerLink
Log in

Homeomorphic Embedding for Online Termination of Symbolic Methods

  • Chapter
  • First Online:
The Essence of Computation

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

Abstract

Well-quasi orders in general, and homeomorphic embedding in particular, have gained popularity to ensure the termination of techniques for program analysis, specialisation, transformation, and verification. In this paper we survey and discuss this use of homeomorphic embedding and clarify the advantages of such an approach over one using well-founded orders. We also discuss various extensions of the homeomorphic embedding relation. We conclude with a study of homeomorphic embedding in the context of metaprogramming, presenting some new (positive and negative) results and open problems.

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. P. A. Abdulla, K. Čerāns, B. Jonsson, and Y.-K. Tsay. General decidability theorems for infinite-state systems. In Proceedings, 11 th Annual IEEE Symposium on Logic in Computer Science, pages 313–321, New Brunswick, New Jersey, 27-30 July 1996. IEEE Computer Society Press.

    Google Scholar 

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

    Chapter  Google Scholar 

  3. E. Albert, M. Alpuente, M. Hanus, and G. Vidal. A partial evaluation framework for curry programs. In Proc. of the 6th International Conference on Logic for Programming and Automated Reasoning (LPAR’99), LNCS 1705, pages 376–395. Springer-Verlag, 1999.

    Chapter  Google Scholar 

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

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

  6. M. Alpuente, M. Falaschi, and G. Vidal. Partial Evaluation of Functional Logic Programs. ACM Transactions on Programming Languages and Systems, 20(4):768–844, 1998.

    Article  Google Scholar 

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

  8. K. R. Apt and F. Turini. Meta-logics and Logic Programming. MIT Press, 1995.

    Google Scholar 

  9. K. Benkerimi and J. W. Lloyd. A partial evaluation procedure for logic programs. In S. Debray and M. Hermenegildo, editors, Proceedings of the North American Conference on Logic Programming, pages 343–358. MIT Press, 1990.

    Google Scholar 

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

    Article  MATH  MathSciNet  Google Scholar 

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

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

  13. 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. The Journal of Logic Programming, 41(2 & 3):231–277, November 1999.

    Article  MATH  Google Scholar 

  14. N. Dershowitz. Orderings for term-rewriting systems. Theoretical Computer Science, 17(3):279–301, Mar. 1982.

    Article  MATH  MathSciNet  Google Scholar 

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

    Article  MATH  MathSciNet  Google Scholar 

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

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

    Article  MATH  MathSciNet  Google Scholar 

  18. A. Finkel. The minimal coverability graph for Petri nets. Lecture Notes in Computer Science, 674:210–243, 1993.

    Google Scholar 

  19. A. Finkel and P. Schnoebelen. Fundamental structures in well-structured infinite transition systems. In Proceedings of LATIN’98, LNCS 1380, pages 102–118. Springer-Verlag, 1998.

    Google Scholar 

  20. F. Fioravanti, A. Pettorossi, and M. Proietti. Rules and strategies for contextual specialization of constraint logic programs. Electronic Notes in Theoretical Computer Science, 30(2), December 1999.

    Google Scholar 

  21. F. Fioravanti, A. Pettorossi, and M. Proietti. Automated strategies for specializing constraint logic programs. In Logic Based Program Synthesis and Transformation. Proceedings of Lopstr’2000, LNCS 1207, pages 125–146, 2000.

    Google Scholar 

  22. H. Fujita and K. Furukawa. A self-applicable partial evaluator and its use in incremental compilation. New Generation Computing, 6(2 & 3):91–118, 1988.

    MATH  Google Scholar 

  23. D. A. Fuller and S. Abramsky. Mixed computation of Prolog programs. New Generation Computing, 6(2 & 3):119–141, June 1988.

    MATH  Google Scholar 

  24. Y. Futamura, K. Nogi, and A. Takano. Essence of generalized partial computation. Theoretical Computer Science, 90(1):61–79, 1991.

    Article  MATH  Google Scholar 

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

  26. J. Gallagher and M. Bruynooghe. The derivation of an algorithm for program specialisation. New Generation Computing, 9(3 & 4):305–333, 1991.

    Google Scholar 

  27. R. Glück. On the mechanics of metasystem hierarchies in program transformation. In M. Proietti, editor, Logic Program Synthesis and Transformation. Proceedings of LOPSTR’95, LNCS 1048, pages 234–251, Utrecht, The Netherlands, September 1995. Springer-Verlag.

    Google Scholar 

  28. R. Glück, J. Hatcli., and J. Jørgensen. Generalization in hierarchies of online program specialization systems. In P. Flener, editor, Logic-Based Program Synthesis and Transformation. Proceedings of LOPSTR’98, LNCS 1559, pages 179–198, Manchester, UK, June 1998. Springer-Verlag.

    Chapter  Google Scholar 

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

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

    Google Scholar 

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

    Google Scholar 

  32. M. Hanus. The integration of functions into logic programming. The Journal of Logic Programming, 19 & 20:583–628, May 1994.

    Google Scholar 

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

    MATH  MathSciNet  Google Scholar 

  34. P. Hill and J. Gallagher. Meta-programming in logic programming. In D. M. Gabbay, C. J. Hogger, and J. A. Robinson, editors, Handbook of Logic in Artificial Intelligence and Logic Programming, volume 5, pages 421–497. Oxford Science Publications, Oxford University Press, 1998.

    Google Scholar 

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

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

    Article  Google Scholar 

  37. N. D. Jones. Computability and Complexity: From a Programming Perspective. MIT Press, 1997.

    Google Scholar 

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

    Google Scholar 

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

    Google Scholar 

  40. R. M. Karp and R. E. Miller. Parallel program schemata. Journal of Computer and System Sciences, 3:147–195, 1969.

    MATH  MathSciNet  Google Scholar 

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

  42. L. Lafave and J. Gallagher. Constraint-based partial evaluation of rewritingbased functional logic programs. In N. Fuchs, editor, Logic Program Synthesis and Transformation. Proceedings of LOPSTR’97, LNCS 1463, pages 168–188, Leuven, Belgium, July 1997.

    Chapter  Google Scholar 

  43. H. Lehmann and M. Leuschel. Solving planning problems by partial deduction. In M. Parigot and A. Voronkov, editors, Proceedings of the International Conference on Logic for Programming and Automated Reasoning (LPAR’2000), LNAI 1955, pages 451–468, Reunion Island, France, 2000. Springer-Verlag.

    Google Scholar 

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

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

    Google Scholar 

  46. M. Leuschel. Improving homeomorphic embedding for online termination. In P. Flener, editor, Logic-Based Program Synthesis and Transformation. Proceedings of LOPSTR’98, LNCS 1559, pages 199–218, Manchester, UK, June 1998. Springer-Verlag.

    Chapter  Google Scholar 

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

    Chapter  Google Scholar 

  48. M. Leuschel. Logic program specialisation. In J. Hatcli., T. Æ. Mogensen, and P. Thiemann, editors, Partial Evaluation: Practice and Theory, LNCS 1706, pages 155–188, Copenhagen, Denmark, 1999. Springer-Verlag.

    Google Scholar 

  49. M. Leuschel and M. Bruynooghe. Logic program specialisation through partial deduction: Control issues. Theory and Practice of Logic Programming, 2(4 & 5):461–515, July & September 2002.

    Article  MATH  MathSciNet  Google Scholar 

  50. M. Leuschel and H. Lehmann. Coverability of reset Petri nets and other wellstructured transition systems by partial deduction. In J. Lloyd, editor, Proceedings of the International Conference on Computational Logic (CL’2000), LNAI 1861, pages 101–115, London, UK, 2000. Springer-Verlag.

    Google Scholar 

  51. M. Leuschel and H. Lehmann. Solving coverability problems of Petri nets by partial deduction. In M. Gabbrielli and F. Pfenning, editors, Proceedings of PPDP’2000, pages 268–279, Montreal, Canada, 2000. ACM Press.

    Google Scholar 

  52. 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, Partial Evaluation, International Seminar, LNCS 1110, pages 263–283, Schloβ Dagstuhl, 1996. Springer-Verlag.

    Google Scholar 

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

    Article  Google Scholar 

  54. M. Leuschel and T. Massart. Infinite state model checking by abstract interpretation and program specialisation. In A. Bossi, editor, Logic-Based Program Synthesis and Transformation. Proceedings of LOPSTR’99, LNCS 1817, pages 63–82, Venice, Italy, September 1999.

    Google Scholar 

  55. C. S. Lii, N. D. Jones, and A. M. Ben-Amram. The size-change principle for program termination. In Proceedings of POPL’01. ACM Press, January 2001.

    Google Scholar 

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

    Google Scholar 

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

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

    Google Scholar 

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

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

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

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

  63. J. Martin and M. Leuschel. Sonic partial deduction. In Proceedings of the Third International Ershov Conference on Perspectives of System Informatics, LNCS 1755, pages 101–112, Novosibirsk, Russia, 1999. Springer-Verlag.

    Google Scholar 

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

    Article  MATH  MathSciNet  Google Scholar 

  65. T. Mogensen and P. Sestoft. Partial evaluation. In A. Kent and J. G. Williams, editors, Encyclopedia of Computer Science and Technology, pages 247–279. Marcel Decker, 270 Madison Avenue, New York, New YOrk 10016, 1997.

    Google Scholar 

  66. A. Pettorossi and M. Proietti. Transformation of logic programs: Foundations and techniques. The Journal of Logic Programming, 19&20:261–320, May 1994.

    Google Scholar 

  67. A. Pettorossi and M. Proietti. A comparative revisitation of some program transformation techniques. In O. Danvy, R. Glück, and P. Thiemann, editors, Partial Evaluation, International Seminar, LNCS 1110, pages 355–385, Schloβ Dagstuhl, 1996. Springer-Verlag.

    Google Scholar 

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

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

    Google Scholar 

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

    MATH  Google Scholar 

  71. J. P. Secher and M. H. Sørensen. On perfect supercompilation. In Proceedings of the Third International Ershov Conference on Perspectives of System Informatics, LNCS 1755, pages 113–127, Novosibirsk, Russia, 1999. Springer-Verlag.

    Google Scholar 

  72. L. Song and Y. Futamura. A new termination approach for specialization. In W. Taha, editor, Proceedings of SAIG’00, LNCS 1924, pages 72–91. Springer-Verlag, 2000.

    Google Scholar 

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

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

  75. M. H. Sørensen and R. Glück. Introduction to supercompilation. In J. Hatcli., T. Æ. Mogensen, and P. Thiemann, editors, Partial Evaluation-Practice and Theory, LNCS 1706, pages 246–270, Copenhagen, Denmark, 1999. Springer-Verlag.

    Google Scholar 

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

    Article  MATH  Google Scholar 

  77. J. Stillman. Computational Problems in Equational Theorem Proving. PhDthesis, State University of New York at Albany, 1988.

    Google Scholar 

  78. A. Takeuchi and K. Furukawa. Partial evaluation of Prolog programs and its application to meta programming. In H.-J. Kugler, editor, Information Processing 86, pages 415–420, 1986.

    Google Scholar 

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

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

    Chapter  Google Scholar 

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

  82. 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, SO17 1BJ, Southampton, UK

    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. DIKU, University of Copenhagen, Universitetsparken 1, 2100, Copenhagen, Denmark

    Torben Æ. Mogensen

  2. Department of Computing and Information Sciences, Kansas State University, 234 Nichols Hall, 66506, Manhattan, KS, USA

    David A. Schmidt

  3. Department of Computer Science, University of Texas at Dallas, P.O. Box 830688, 75083, Richardson, TX, USA

    I. Hal Sudborough

Rights and permissions

Reprints and permissions

Copyright information

© 2002 Springer-Verlag Berlin Heidelberg

About this chapter

Cite this chapter

Leuschel, M. (2002). Homeomorphic Embedding for Online Termination of Symbolic Methods. In: Mogensen, T.Æ., Schmidt, D.A., Sudborough, I.H. (eds) The Essence of Computation. Lecture Notes in Computer Science, vol 2566. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-36377-7_17

Download citation

  • DOI: https://doi.org/10.1007/3-540-36377-7_17

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-00326-7

  • Online ISBN: 978-3-540-36377-4

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation