A Characterisation of Multiply Recursive Functions with Higman’s Lemma
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.
KeywordsRecursive Function Order Type Notation System Total Termination Hardy Function
Unable to display preview. Download preview PDF.
- 2.E.A. Cichon and E. Tahhan Bittar, Ordinal recursive bounds for Higman’s theorem. To appear in Theoretical Computer Science.Google Scholar
- 3.D.H.J. De Jongh and R. Parikh, Well-partial orderings and hierarchies. Indagationes Mathematicae 14 (1977), p. 195–207.Google Scholar
- 5.N. Dershowitz et J.P. Jouannaud, Rewrite systems. Handbook of Theoretical Computer Science vol.B, North-Holland.Google Scholar
- 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
- 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
- 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.R. P_eter, Recursive Functions. Academic Press (1967)Google Scholar
- 12.J.W. Robbin, Subrecursive Hierarchies. Ph.D. PrincetonGoogle Scholar
- 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.H. Touzet, Encoding the Hydra Battle as a rewrite system. Proceedings of MFCS’98, Lecture Notes in Computer Science 1450 (1998).Google Scholar