Infinitary Combinatory Reduction Systems

(Extended Abstract)
  • Jeroen Ketema
  • Jakob Grue Simonsen
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3467)


We define infinitary combinatory reduction systems (iCRSs). This provides the first extension of infinitary rewriting to higher-order rewriting. We lift two well-known results from infinitary term rewriting systems and infinitary λ-calculus to iCRSs:

  1. 1

    every reduction sequence in a fully-extended left-linear iCRS is compressible to a reduction sequence of length at most ω, and

  2. 2

    every complete development of the same set of redexes in an orthogonal iCRS ends in the same term.



Function Symbol Depth Measure Outgoing Edge Label Edge Complete Development 
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. 1.
    Dershowitz, N., Kaplan, S., Plaisted, D.A.: Rewrite, rewrite, rewrite, rewrite, rewrite... TCS 83, 71–96 (1991)zbMATHCrossRefMathSciNetGoogle Scholar
  2. 2.
    Kennaway, R., Klop, J.W., Sleep, R., de Vries, F.J.: Transfinite reductions in orthogonal term rewriting systems. I&C 119, 18–38 (1995)zbMATHGoogle Scholar
  3. 3.
    Terese: Term Rewriting Systems. Cambridge University Press, Cambridge (2003)Google Scholar
  4. 4.
    Kennaway, J.R., Klop, J.W., Sleep, M., de Vries, F.J.: Infinitary lambda calculus. TCS 175, 93–125 (1997)zbMATHCrossRefGoogle Scholar
  5. 5.
    Klop, J.W.: Combinatory Reduction Systems. PhD thesis, Rijksuniversiteit Utrecht (1980)Google Scholar
  6. 6.
    Klop, J.W., van Oostrom, V., van Raamsdonk, F.: Combinatory reduction systems: introduction and survey. TCS 121, 279–308 (1993)zbMATHCrossRefGoogle Scholar
  7. 7.
    Arnold, A., Nivat, M.: The metric space of infinite trees. Algebraic and topological properties. Fundamenta Informaticae 3, 445–476 (1980)zbMATHMathSciNetGoogle Scholar
  8. 8.
    Barendregt, H.P.: The Lambda Calculus: Its Syntax and Semantics, 2nd edn. Elsevier Science, Amsterdam (1985)zbMATHGoogle Scholar
  9. 9.
    Hanus, M., Prehofer, C.: Higher-order narrowing with definitional trees. In: Ganzinger, H. (ed.) RTA 1996. LNCS, vol. 1103, pp. 138–152. Springer, Heidelberg (1996)Google Scholar
  10. 10.
    van Oostrom, V.: Higher-order families. In: Ganzinger, H. (ed.) RTA 1996. LNCS, vol. 1103, pp. 392–407. Springer, Heidelberg (1996)Google Scholar
  11. 11.
    Kennaway, R., van Oostrom, V., de Vries, F.J.: Meaningless terms in rewriting. The Journal of Functional and Logic Programming 1 (1999)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Jeroen Ketema
    • 1
  • Jakob Grue Simonsen
    • 2
  1. 1.Department of Computer ScienceVrije Universiteit AmsterdamAmsterdamThe Netherlands
  2. 2.Department of Computer ScienceUniversity of Copenhagen (DIKU)Copenhagen ØDenmark

Personalised recommendations