Universal Algebra for Termination of Higher-Order Rewriting

  • Makoto Hamana
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3467)


We show that the structures of binding algebras and Σ-monoids by Fiore, Plotkin and Turi are sound and complete models of Klop’s Combinatory Reduction Systems (CRSs). These algebraic structures play the same role of universal algebra for term rewriting systems. Restricting the algebraic structures to the ones equipped with well-founded relations, we obtain a complete characterisation of terminating CRSs. We can also naturally extend the characterisation to rewriting on meta-terms by using the notion of Σ-monoids.


Structural Term Function Symbol Universal Algebra Monoidal Category Binding Signature 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [Acz78]
    Aczel, P.: A general Church-Rosser theorem. Technical report, University of Manchester (1978)Google Scholar
  2. [dB72]
    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
  3. [DR98]
    Danvy, O., Rose, K.H.: Higher-order rewriting and partial evaluation. In: Nipkow, T. (ed.) RTA 1998. LNCS, vol. 1379, p. 286. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  4. [FPT99]
    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
  5. [Ham03]
    Hamana, M.: Term rewriting with variable binding: An initial algebra approach. In: Fifth ACM-SIGPLAN International Conference on Principles and Practice of Declarative Programming (PPDP 2003), pp. 148–159 (2003)Google Scholar
  6. [Ham04]
    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)CrossRefGoogle Scholar
  7. [JR01]
    Jouannaud, J.-P., Rubio, A.: Higher-order recursive path orderings à la carte. In: International Workshop on Rewriting in Proof and Computation (RPC 2001), pp. 161–175 (2001)Google Scholar
  8. [Klo80]
    Klop, J.W.: Combinatory Reduction Systems. PhD thesis, CWI, Amsterdam, vol.127 of Mathematical Centre Tracts (1980)Google Scholar
  9. [KOR93]
    Klop, J.W., van Oostrom, V., van Raamsdonk, F.: Combinatory reduction systems: Introduction and survey. Theor. Comput. Sci. 121(1&2), 279–308 (1993)zbMATHCrossRefGoogle Scholar
  10. [LRD95]
    Lescanne, P., Rouyer-Degli, J.: Explicit substitutions with de Bruijn’s levels. In: Hsiang, J. (ed.) RTA 1995. LNCS, vol. 914, pp. 294–308. Springer, Heidelberg (1995)Google Scholar
  11. [Mac71]
    Mac Lane, S.: Categories for the Working Mathematician. Graduate Texts in Mathematics, vol. 5. Springer, New York (1971)zbMATHGoogle Scholar
  12. [Oos94]
    van Oostrom, V.: Confluence for Abstract and Higher-Order Rewriting. PhD thesis, Vrije Universiteit, Amsterdam (1994)Google Scholar
  13. [OR94]
    van Oostrom, V., van Raamsdonk, F.: Comparing combinatory reduction systems and higher-order rewrite systems. In: Heering, J., Meinke, K., Möller, B., Nipkow, T. (eds.) HOA 1993. LNCS, vol. 816, Springer, Heidelberg (1994)Google Scholar
  14. [Plo98]
    Plotkin, G.: Binding algebras: A step between universal algebra and type theory (invited talk). In: Rewriting Techniques and Applications, 9th International Conference, RTA 1998, Tsukuba, Japan (1998)Google Scholar
  15. [Pol94]
    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
  16. [Pol96]
    van de Pol, J.: Termination of Higher-order Rewrite Systems. PhD thesis, Universiteit Utrecht (1996)Google Scholar
  17. [Raa]
    van Raamsdonk, F.: Examples of higher-order rewriting systems, at
  18. [Zan94]
    Zantema, H.: Termination of term rewriting: interpretation and type elimination. Journal of Symbolic Computation 17, 23–50 (1994)zbMATHCrossRefMathSciNetGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Makoto Hamana
    • 1
  1. 1.Department of Computer ScienceGunma UniversityJapan

Personalised recommendations