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 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.
Dedicated to Gerhard Jäger on the occasion of his 60th birthday
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
- 2.
A similar phenomenon is addressed in Coq [5] by the so-called Set/Prop distinction. However, enriching the logic by n.c. universal quantification (and similarly n.c. implication) seems to be more flexible.
- 3.
- 4.
References
U. Berger, Program extraction from normalization proofs, in Typed Lambda Calculi and Applications, ed. by M. Bezem, J. Groote, LNCS, vol. 664, (Springer, Berlin, 1993), pp. 91–106
U. Berger, K. Miyamoto, H. Schwichtenberg, M. Seisenberger, Minlog–A Tool for Program Extraction Supporting Algebras and Coalgebras, in Algebra and Coalgebra in Computer Science, ed. by A. Corradini, B. Klin, C. Cîrstea, CALCO’11, LNCS, vol. 6859, (Springer, Berlin, 2011), pp. 393–399
S. Berghofer, A constructive proof of Higman’s lemma in Isabelle, Types for Proofs and Programs. Lecture Notes in Computer Science, vol. 3085 (Springer, Berlin, 2004), pp. 66–82
E.A. Cichon, E.T. Bittar, Ordinal recursive bounds for Higman’s theorem. Theor. Comput. Sci. 201(1–2), 63–84 (1998)
Coq Development Team. The Coq Proof Assistant Reference Manual—Version 8.2. Inria (2009)
T. Coquand. A proof of Higman’s lemma by structural induction. Unpublished Manuscript, April 1993
T. Coquand, D. Fridlender, A proof of Higman’s lemma by structural induction. Unpublished Manuscript (1993), http://www.cse.chalmers.se/~coquand/open1.ps, Nov 1993
D. de Jongh, R. Parikh, Well partial orderings and their order types. Indagationes Mathematicae 14, 195–207 (1977)
D. Fridlender, Ramsey’s Theorem in Type Theory. Licentiate Thesis, Chalmers University of Technology and University of Göteburg, 1993
D. Fridlender. Higman’s Lemma in Type Theory. Ph.D. thesis, Chalmers University of Technology, Göteborg, 1997
J. Goubault-Larrecq, A constructive proof of the topological Kruskal theorem, in Mathematical foundations of computer science 2013, ed. by K. Chatterjee, J. Sgall, 38th international symposium, MFCS 2013, LNCS, vol. 8087, (Springer, Berlin, 2013), pp. 22–41
J.-Y. Girard, Proof Theory and Logical Complexity (Bibliopolis, Napoli, 1987)
R. Hasegawa, Well-ordering of algebra and Kruskal’s theorem, in Logic, Language and Computation, ed. by N.D. Jones, M. Hagiya, M. Sato, Festschrift in Honor of Satoru Takasu. Lecture Notes in Computer Science, vol. 792, (Springer, Berlin, 1994), pp. 133–172
H. Herbelin, A program from an A-translated impredicative proof of Higman’s lemma (1994), http://www.lix.polytechnique.fr/coq/pylons/contribs/files/HigmanNW/trunk/HigmanNW.Higman.html
G. Higman, Ordering by divisibility in abstract algebras. Proc. London Math. Soc. 2, 326–336 (1952)
F.-J. Martín-Mateos, J.-L. Ruiz-Reina, J.-A. Alonso, M.-J. Hidalgo, Proof pearl: a formal proof of Higman’s lemma in ACL2. J. Autom. Reasoning 47(3), 229–250 (2011)
C. Murthy, Extracting constructive content from classical proofs. Technical Report 90–1151, Department of Computer Science, Ph.D. thesis. Cornell University, Ithaca, New York, 1990
C.R. Murthy, J.R. Russell, A constructive proof of Higman’s lemma, in Proceedings of the Sixth Symposium on Logic in Computer Science, pp. 257–267 (1990)
C. Nash-Williams, On well-quasi-ordering finite trees. Proc. Cambridge Phil. Soc. 59, 833–835 (1963)
M. Ogawa, Generation of a linear time query processing algorithm based on well-quasi-orders, in TACS ’01 Proceedings of the 4th International Symposium on Theoretical Aspects of Computer Software, LNCS, vol. 2215 (Springer, Berlin, 2001), pp. 283–297
T. Powell, Applying Gödel’s Dialectica interpretation to obtain a constructive proof of Higman’s lemma, in Proceedings of Classical Logic and Computation (CLAC’12), EPTCS, vol. 97 pp. 49–62 (2012)
M. Rathjen, A. Weiermann, Proof-theoretic investigations on Kruskal’s theorem. Ann. Pure a. Appl. Logic 60, 49–88 (1993)
F. Richman, G. Stolzenberg, Well quasi-ordered sets. Adv. Math. 97, 145–153 (1993)
D. Schmidt, Well-Orderings and Their Maximal Order Types (Mathematisches Institut der Universität, Habilitationsschrift, Heidelberg, 1979)
K. Schütte, S.G. Simpson, Ein in der reinen Zahlentheorie unbeweisbarer Satz über endliche Folgen von natürlichen Zahlen. Archiv für Mathematische Logik und Grundlagenforschung 25, 75–89 (1985)
H. Schwichtenberg, S.S. Wainer, Proofs and Computations (Association for Symbolic Logic (Cambridge University Press, Cambridge, Perspectives in Logic, 2012)
M. Seisenberger, Kruskal’s tree theorem in a constructive theory of inductive definitions, in Reuniting the Antipodes—Constructive and Nonstandard Views of the Continuum, ed. by P. Schuster, U. Berger, H. Osswald, Synthese Library, vol. 306 (Kluwer Academic Publisher, Dordrecht, 2001), pp. 241–255
M. Seisenberger, An inductive version of Nash-Williams Minimal-Bad-Sequence argument for Higman’s lemma, in Types for Proofs and Programs, LNCS, vol. 2277 (Springer, Berlin, 2001)
M. Seisenberger, On the Constructive Content of Proofs. Ph.D. thesis, Mathematisches Institut der Universität München, 2003
C. Sternagel, Certified Kruskal’s tree theorem. J. Formalized Reasoning 7(1), 45–62 (2014)
H. Touzet, Propriétés combinatoires pour la terminaison de systèmes de réécriture. Ph.D. thesis, Université Henri Poincaré, Nancy, 1997
H. Touzet, A characterisation of multiply recursive functions with Higman’s lemma. Inf. Comput. 178, 534–544 (2002)
V. Veldman, M. Bezem, Ramsey’s theorem and the pigeonhole principle in intuitionistic mathematics. J. London Math. Soc. 47, 193–211 (1993)
W. Veldman, An intuitionistic proof of Kruskal’s theorem. Arch. for Math. Logic 43(2), 215–264 (2004)
D. Vytiniotis, T. Coquand, D. Wahlstedt, Stop when you are almost-full–Adventures, in constructive termination, in Proceedings, ITP 2012, ed. by L. Beringer, A. Felty, LNCS, vol. 7406, (Springer Verlag, Berlin, Heidelberg, New York, 2012), pp. 250–265
Acknowledgments
We would like to thank Daniel Fridlender and Iosif Petrakis for helpful contributions and comments.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer International Publishing Switzerland
About this chapter
Cite this chapter
Schwichtenberg, H., Seisenberger, M., Wiesnet, F. (2016). Higman’s Lemma and Its Computational Content. In: Kahle, R., Strahm, T., Studer, T. (eds) Advances in Proof Theory. Progress in Computer Science and Applied Logic, vol 28. Birkhäuser, Cham. https://doi.org/10.1007/978-3-319-29198-7_11
Download citation
DOI: https://doi.org/10.1007/978-3-319-29198-7_11
Published:
Publisher Name: Birkhäuser, Cham
Print ISBN: 978-3-319-29196-3
Online ISBN: 978-3-319-29198-7
eBook Packages: Mathematics and StatisticsMathematics and Statistics (R0)