Applying G\"odel's Dialectica Interpretation to Obtain a Constructive Proof of Higman's Lemma
Logic in Computer Science
2012-10-12 v1 Discrete Mathematics
Abstract
We use G\"odel's Dialectica interpretation to analyse Nash-Williams' elegant but non-constructive "minimal bad sequence" proof of Higman's Lemma. The result is a concise constructive proof of the lemma (for arbitrary decidable well-quasi-orders) in which Nash-Williams' combinatorial idea is clearly present, along with an explicit program for finding an embedded pair in sequences of words.
Keywords
Cite
@article{arxiv.1210.3117,
title = {Applying G\"odel's Dialectica Interpretation to Obtain a Constructive Proof of Higman's Lemma},
author = {Thomas Powell},
journal= {arXiv preprint arXiv:1210.3117},
year = {2012}
}
Comments
In Proceedings CL&C 2012, arXiv:1210.2890