A characterisation of multiply recursive functions with higman's lemma

摘要

We prove that string rewriting systems which reduce by Higman'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 derviation length via the Hardy hierarchy.