Reseña: Higman’s lemma and its computational content
Se ha publicado un artículo de razonamiento formalizado en Minlog sobre combinatoria titulado Higman’s lemma and its computational content.
Sus autores son
- Helmut Schwichtenberg (de la Univ. de Munich en Alemania),
- Monika Seisenberger (de la Univ. de Swansea en el Reino Unido) y
- Franziskus Wiesnet.
Su resumen es
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 proof was given by Coquand. Using more flexible structures, we present a proof that works for an arbitrary well-quasiordered alphabet. We report on a formalization of this proof in the proof assistant Minlog, and discuss machine extracted terms (in an extension of Gödel’s system T) expressing its computational content.