This paper concerns Higman's theorem for stringsgenerated over a finite alphabet. We give a constructiveproof of this theorem and we construct and characterisefunctions which bound the lengths of bad sequences. These bounding functions are described by ordinal-recursive definitions and their characterisation is achievedwith reference to Hardy hierarchies of number-theoretic functions.