Skip to main content
SpringerLink
Log in

Semantic Labelling for Proving Termination of Combinatory Reduction Systems

  • Conference paper
Book cover Functional and Constraint Logic Programming (WFLP 2009)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 5979))

Included in the following conference series:

Abstract

We give a novel transformation method for proving termination of higher-order rewrite rules in Klop’s format called Combinatory Reduction System (CRS). The format CRS essentially covers the usual pure higher-order functional programs such as Haskell. Our method called higher-order semantic labelling is an extension of a method known in the theory of term rewriting. This attaches semantics of the arguments to each function symbol. We systematically define the labelling by using the complete algebraic semantics of CRS, Σ-monoids. We also examine the power of higher-order semantic labelling by several examples. This includes an interesting example from the viewpoint of functional programming.

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. Aczel, P.: A general Church-Rosser theorem. Technical report, University of Manchester (1978)

    Google Scholar 

  2. Blanqui, F., Jouannaud, J.-P., Okada, M.: Inductive data type systems. Theoretical Computer Science 272, 41–68 (2002)

    Article  MATH  MathSciNet  Google Scholar 

  3. Blanqui, F., Jouannaud, J.-P., Rubio, A.: The computability path ordering: The end of a quest. In: Kaminski, M., Martini, S. (eds.) CSL 2008. LNCS, vol. 5213, pp. 1–14. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  4. Blanqui, F.: Termination and confluence of higher-order rewrite systems. In: Bachmair, L. (ed.) RTA 2000. LNCS, vol. 1833, pp. 47–61. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  5. Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998)

    Google Scholar 

  6. Borralleras, C., Rubio, A.: A monotonic higher-order semantic path ordering. In: Nieuwenhuis, R., Voronkov, A. (eds.) LPAR 2001. LNCS (LNAI), vol. 2250, pp. 531–547. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  7. de Bruijn, N.: Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the church-rosser theorem. Indagationes Mathematicae 34, 381–391 (1972)

    Google Scholar 

  8. Danvy, O., Rose, K.H.: Higher-order rewriting and partial evaluation. In: Nipkow, T. (ed.) RTA 1998. LNCS, vol. 1379, pp. 286–301. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  9. Fiore, M., Plotkin, G., Turi, D.: Abstract syntax and variable binding. In: Proc. 14th Annual Symposium on Logic in Computer Science, pp. 193–202 (1999)

    Google Scholar 

  10. Hamana, M.: Free Σ-monoids: A higher-order syntax with metavariables. In: Chin, W.-N. (ed.) APLAS 2004. LNCS, vol. 3302, pp. 348–363. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  11. Hamana, M.: Universal algebra for termination of higher-order rewriting. In: Giesl, J. (ed.) RTA 2005. LNCS, vol. 3467, pp. 135–149. Springer, Heidelberg (2005)

    Google Scholar 

  12. Hamana, M.: Higher-order semantic labelling for inductive datatype systems. In: Ninth ACM-SIGPLAN International Conference on Principles and Practice of Declarative Programming (PPDP 2007), pp. 97–108 (2007)

    Google Scholar 

  13. Jouannaud, J.-P., Rubio, A.: Higher-order orderings for normal rewriting. In: Pfenning, F. (ed.) RTA 2006. LNCS, vol. 4098, pp. 387–399. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  14. Jouannaud, J.-P., Rubio, A.: Polymorphic higher-order recursive path orderings. Journal of ACM 54(1) (2007)

    Google Scholar 

  15. Jones, S.P., Tolmach, A., Hoare, T.: Playing by the rules: rewriting as a practical optimisation technique in GHC. In: Haskell Workshop 2001 (2001)

    Google Scholar 

  16. Klop, J.W.: Combinatory Reduction Systems. PhD thesis, CWI, Amsterdam. Mathematical Centre Tracts, vol. 127 (1980)

    Google Scholar 

  17. Klop, J.W., van Oostrom, V., van Raamsdonk, F.: Combinatory reduction systems: Introduction and survey. Theor. Comput. Sci. 121(1&2), 279–308 (1993)

    Article  MATH  Google Scholar 

  18. Mac Lane, S.: Categories for the Working Mathematician. Graduate Texts in Mathematics, vol. 5. Springer, New York (1971)

    MATH  Google Scholar 

  19. Nipkow, T.: Higher-order critical pairs. In: Proc. 6th IEEE Symp. Logic in Computer Science, pp. 342–349 (1991)

    Google Scholar 

  20. van de Pol, J.: Termination proofs for higher-order rewrite systems. In: Heering, J., Meinke, K., Möller, B., Nipkow, T. (eds.) HOA 1993. LNCS, vol. 816, pp. 305–325. Springer, Heidelberg (1994)

    Google Scholar 

  21. van Raamsdonk, F.: On termination of higher-order rewriting. In: Middeldorp, A. (ed.) RTA 2001. LNCS, vol. 2051, pp. 261–275. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  22. Terese: Term Rewriting Systems. Cambridge Tracts in Theoretical Computer Science, vol. 55. Cambridge University Press, Cambridge (2003)

    Google Scholar 

  23. Blanqui, F.: Termination and confluence of higher-order rewrite systems. In: Bachmair, L. (ed.) RTA 2000. LNCS, vol. 1833, pp. 47–61. Springer, Heidelberg (2000)

    MATH  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, Gunma University, Japan

    Makoto Hamana

Authors
  1. Makoto Hamana
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Departamento de Sistemas Informáticos y Computación, Universidad Politécnica de Valencia, Camino de vera, s/n, 46022, Valencia, Spain

    Santiago Escobar

Rights and permissions

Reprints and permissions

Copyright information

© 2010 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Hamana, M. (2010). Semantic Labelling for Proving Termination of Combinatory Reduction Systems. In: Escobar, S. (eds) Functional and Constraint Logic Programming. WFLP 2009. Lecture Notes in Computer Science, vol 5979. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-11999-6_5

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-11999-6_5

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-11998-9

  • Online ISBN: 978-3-642-11999-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation