A Constructive Proof of Higman's Lemma

unofficial copies [PDF], [PS]

by Chetan Murthy and James R. Russell

Proceedings of Fifth IEEE Symposium on Logic in Computer Science, pp. 257-269, (also Cornell TR 89-1049), 1990.


Higman's Lemma is a special case of the more general Kruskal's tree embedding theorem and the graph minor theorem. Prior to this work, only classical (and impredicative) proofs of the Lemma were known. Recently, there has been much interest in developing a constructive proof of the Lemma, primarily via Friedman's A-translation. In this paper we present a direct constructive proof. We achieve this by reducing the problem to a construction of certain sets of sequential regular expressions. We then exhibit a well-founded order on such sets, and the Lemma then follows by induction.