A Characterisation of Multiply Recursive Functions with Higman’s Lemma

  • Héléne Touzet
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1631)


We prove that string rewriting systems which reduce by Hig-man’s lemma exhaust the multiply recursive functions. This result provides a full characterisation of the expressiveness of Higman’s lemma when applied to rewriting theory. The underlying argument of our construction is to connect the order type and the derivation length via the Hardy hierarchy.


Recursive Function Order Type Notation System Total Termination Hardy Function 
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.
    E.A. Cichon, A short proof of two recently discovered independence results using recursion theoretic methods. Proceedings of the American Mathematical Society, vol 97 (1983), p.704–706.CrossRefMathSciNetGoogle Scholar
  2. 2.
    E.A. Cichon and E. Tahhan Bittar, Ordinal recursive bounds for Higman’s theorem. To appear in Theoretical Computer Science.Google Scholar
  3. 3.
    D.H.J. De Jongh and R. Parikh, Well-partial orderings and hierarchies. Indagationes Mathematicae 14 (1977), p. 195–207.Google Scholar
  4. 4.
    N. Dershowitz, Orderings for term rewriting systems. Theoretical Computer Science 17-3 (1982), p. 279–301.CrossRefMathSciNetGoogle Scholar
  5. 5.
    N. Dershowitz et J.P. Jouannaud, Rewrite systems. Handbook of Theoretical Computer Science vol.B, North-Holland.Google Scholar
  6. 6.
    M.C.F. Ferreira and H. Zantema, Total termination of term rewriting. Proceedings of RTA-93, Lecture notes in Computer Science 690, p. 213–227.Google Scholar
  7. 7.
    G. Higman, Ordering by divisibility in abstract algebras. Bull. London Mathematical Society 3-2 (1952), p. 326–336.CrossRefMathSciNetGoogle Scholar
  8. 8.
    D. Hofbauer and C. Lautemann, Termination proofs and the length of derivations. Proceedings of RTA-88, Lecture Notes in Computer Science 355.Google Scholar
  9. 9.
    D. Hofbauer, Termination proofs with multiset path orderings imply primitive recursive derivation lengths. Theoretical Computer Science 105-1 (1992), p.129–140.CrossRefMathSciNetGoogle Scholar
  10. 10.
    U. Martin et E.A. Scott, The order types of termination orderings on monadic terms, strings and multisets. 8th Annual Symposium on Logic in Computer Science, IEEE (1993), p. 356–363.Google Scholar
  11. 11.
    R. P_eter, Recursive Functions. Academic Press (1967)Google Scholar
  12. 12.
    J.W. Robbin, Subrecursive Hierarchies. Ph.D. PrincetonGoogle Scholar
  13. 13.
    H. Touzet, A complex example of a simplifying rewrite system. Proceedings of ICALP’98, Lecture Notes in Computer Science 1442 (1998).Google Scholar
  14. 14.
    H. Touzet, Encoding the Hydra Battle as a rewrite system. Proceedings of MFCS’98, Lecture Notes in Computer Science 1450 (1998).Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1999

Authors and Affiliations

  • Héléne Touzet
    • 1
  1. 1.LIFL - Université Lille 1Villeneuve d’AscqFrance

Personalised recommendations