Paper: A constructive proof of Higman's lemma (at LICS 1990)
Authors: Murthy, C.R. Russell, J.R.Abstract
G. Higman's lemma (1952) is a special case of the more general Kruskal's tree embedding theorem and the graph minor theorem. A direct constructive proof of the lemma with manifest computational content is presented. This is done by reducing the problem to a construction of certain sets of sequential regular expressions. A well-founded order on such sets is exhibited, and the lemma then follows by induction
BibTeX
@InProceedings{MurthyRussell-Aconstructiveproofo, author = {Murthy, C.R. and Russell, J.R.}, title = {A constructive proof of Higman's lemma}, booktitle = {Proceedings of the Fifth Annual IEEE Symp. on Logic in Computer Science, {LICS} 1990}, year = 1990, editor = {John Mitchell}, month = {June}, pages = {257--267}, location = {Philadelphia, PA, USA}, publisher = {IEEE Computer Society Press} }