Higman's Lemma and Its Computational Content

Schwichtenberg, Helmut; Seisenberger, Monika and Wiesnet, Franziskus (2016): Higman's Lemma and Its Computational Content. In: Advances in Proof Theory. Progress in Computer Science and Applied Logic, Vol. 28. Cham: Birkhäuser. pp. 353-375

Abstract

Higman's Lemma is a fascinating result in infinite combinatorics, with manyfold applications in logic and computer science. It has been proven several times using different formulations and methods. The aim of this paper is to look at Higman's Lemma from a computational and comparative point of view. We give a proof of Higman's Lemma that uses the same combinatorial idea as Nash-Williams' indirect proof using the so-called minimal bad sequence argument, but which is constructive. For the case of a two letter alphabet such a proofwas given by Coquand. Using more flexible structures, we present a proof that works for an arbitrary wellquasiordered alphabet. We report on a formalization of this proof in the proof assistant Minlog, and discuss machine extracted terms (in an extension of Godel's system T) expressing its computational content.

• Item Type: Book Section
• Faculties: Mathematics, Computer Science and Statistics > Mathematics
• Subjects: 500 Science > 510 Mathematics
• ISBN: 978-3-319-29196-3; 978-3-319-29198-7
• Place of Publication: Cham
• Language: English