Skip to main content
PRL Project

A Constructive Proof of Higman's Lemma

by Chetan Murthy, James R. Russell

Proceedings of Fifth IEEE Symposium on Logic in Computer Science

  • unofficial copies PDF, PS

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.

bibTex ref: MR90

cite link