Termination of curryfied rewrite systems

  • Bjørn Kristoffersen
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1130)


This paper studies termination of curryfied term rewriting systems (CTRSs), where functional values are introduced by “partial application” The limitations of syntactic simplification orderings for such systems are discussed. A proof method is proposed, based on three techniques: 1) Requirements on stability and monotonicity are relaxed. 2) Variables and inner function symbols of (potentially) functional types are allowed to contribute in the underlying precedence. 3) A standard polymorphic type system is refined so as to express non-functional polymorphism. Founded on this method, the curryfied path ordering with status (CPOS) is introduced. CPOS coincides with the recursive path ordering with status on first-order terms, and is comparable in strength to other approaches for higher-order rewrite systems, but also allows for polymorphism. Under mild restrictions on the underlying precedence, the so called curry rules are oriented correctly under CPOS.


Function Symbol Principal Type Proof Method Lambda Calculus Type Substitution 
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.
    H. P. Barendregt. The lambda calculus: its syntax and semantics. North-Holland, Amsterdam, 1984.Google Scholar
  2. 2.
    V. Breazu-Tannen. Combining algebra and higher-order types. In Proceedings 3rd IEEE Symposium on Logic in Computer Science, Edinburgh, July 1988.Google Scholar
  3. 3.
    N. Dershowitz. Orderings for term-rewriting systems. Theoretical Computer Science, 17:279–301, 1982.Google Scholar
  4. 4.
    N. Dershowitz. Termination of rewriting. Journal Symbolic Computation, 3:69–116, 1987.Google Scholar
  5. 5.
    N. Dershowitz and C. Hoot. Topics in termination. LNCS, 690:198–212, 1993.Google Scholar
  6. 6.
    N. Dershowitz and J.-P. Jouannaud. Rewrite systems. In J. van Leuwen, editor, Handbook of theoretical computer science, pages 245–309. Elsevier Science Publishers B.V, 1990.Google Scholar
  7. 7.
    M.C.F. Ferreira and H. Zantema. Well-foundedness of term orderings. In Conditional Term Rewriting Systems, Proceedings 4th International Workshop '94, LNCS 968, pages 106–123. Springer-Verlag, 1995.Google Scholar
  8. 8.
    J. R. Hindley and J. P. Seldin, editors. Introduction to combinators and λ-calculus. London Mathematical Society Student Series. Cambridge University Press, 1986.Google Scholar
  9. 9.
    J.-P. Jouannaud and M. Okada. A computation model for executable higher-order algebraic specification languages. In Proceedings 6th IEEE Symposium on Logic in Computer Science, pages 350–361, 1991.Google Scholar
  10. 10.
    S. Kamin and J.J. Levý. Two generalizations of the recursive path ordering. Unpublished note, Department of Computer Science, University of Illinois, Urbana, IL, February 1980.Google Scholar
  11. 11.
    J.W. Klop. Combinatory reduction systems. Mathematical centre tracts, CWI, Amsterdam, 1980.Google Scholar
  12. 12.
    J.W. Klop. Term rewriting systems. In S. Abramsky, D.M. Gabbay, and T.S.E. Maibaum, editors, Handbook of logic in computer science, volume 2, chapter 1, pages 1–116. Clarendon Press, Oxford, 1992.Google Scholar
  13. 13.
    J.B. Kruskal. Well-quasi-ordering, the tree theorem, and Vazsonyi's conjecture. Trans. Amer. Math. Soc., 95:210–225, 1960.Google Scholar
  14. 14.
    P. Lescanne. On the recursive decomposition ordering with lexicographic status and other related orderings. Journal of Automated Reasoning, 6:39–49, 1990.Google Scholar
  15. 15.
    C. Loría-Sáenz. A theoretical framawork for reasoning about program construction based on extensions of rewrite systems. PhD thesis, Fachbereich Informatik der Universität Kaiserslautern, 1993.Google Scholar
  16. 16.
    O. Lysne and J. Piris. A termination ordering for higher order rewrite systems. In 6th International Conference on Rewriting Techniques and Applications '95, LNCS 914, pages 26–40. Springer-Verlag, 1995.Google Scholar
  17. 17.
    R. Milner. A theory of type polymorphism in programming. J. of Computer and System Sciences, 17:348–375, 1978.Google Scholar
  18. 18.
    R. Milner, M. Tofte, and R. Harper. The definition of Standard ML. The MIT Press, 1990.Google Scholar
  19. 19.
    J. C. Mitchell. Type systems for programming languages. In J. van Leuwen, editor, Handbook of theoretical computer science. Elsevier Science Publishers B.V, 1990.Google Scholar
  20. 20.
    T. Nipkow. Higher-order critical pairs. In Proceedings 6th IEEE Symposium on Logic in Computer Science, pages 342–349, 1991.Google Scholar
  21. 21.
    M. Tofte. Operational semantics and polymorphic type inference. PhD thesis, University of Edinburgh, 1987.Google Scholar
  22. 22.
    S. van Bakel and M. Fernández. Strong normalization of typeable rewrite systems. In First International Conference on Higher-Order Algebra, Logic, and Term Rewriting '93, LNCS 816, pages 21–39. Springer-Verlag, 1993.Google Scholar
  23. 23.
    S. van Bakel, S. van Brock, and J.E.W. Smetsers. Partial type assignment in left-linear term rewriting systems. LNCS, 581:300–321, 1992.Google Scholar
  24. 24.
    J. van de Pol. Termination proofs for higher-order rewriting systems. In First International Conference on Higher-Order Algebra, Logic, and Term Rewriting '93, LNCS 816, pages 305–325. Springer-Verlag, 1993.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1996

Authors and Affiliations

  • Bjørn Kristoffersen
    • 1
  1. 1.Department of InformaticsUniversity of OsloNorway

Personalised recommendations