Advertisement

Higman’s Lemma and Its Computational Content

  • Helmut SchwichtenbergEmail author
  • Monika Seisenberger
  • Franziskus Wiesnet
Chapter
Part of the Progress in Computer Science and Applied Logic book series (PCS, volume 28)

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.

Keywords

Higman’s Lemma Inductive definitions Minimal bad sequence Program extraction 

Notes

Acknowledgments

We would like to thank Daniel Fridlender and Iosif Petrakis for helpful contributions and comments.

References

  1. 1.
    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–106Google Scholar
  2. 2.
    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–399Google Scholar
  3. 3.
    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–82Google Scholar
  4. 4.
    E.A. Cichon, E.T. Bittar, Ordinal recursive bounds for Higman’s theorem. Theor. Comput. Sci. 201(1–2), 63–84 (1998)Google Scholar
  5. 5.
    Coq Development Team. The Coq Proof Assistant Reference Manual—Version 8.2. Inria (2009)Google Scholar
  6. 6.
    T. Coquand. A proof of Higman’s lemma by structural induction. Unpublished Manuscript, April 1993Google Scholar
  7. 7.
    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
  8. 8.
    D. de Jongh, R. Parikh, Well partial orderings and their order types. Indagationes Mathematicae 14, 195–207 (1977)Google Scholar
  9. 9.
    D. Fridlender, Ramsey’s Theorem in Type Theory. Licentiate Thesis, Chalmers University of Technology and University of Göteburg, 1993Google Scholar
  10. 10.
    D. Fridlender. Higman’s Lemma in Type Theory. Ph.D. thesis, Chalmers University of Technology, Göteborg, 1997Google Scholar
  11. 11.
    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–41Google Scholar
  12. 12.
    J.-Y. Girard, Proof Theory and Logical Complexity (Bibliopolis, Napoli, 1987)Google Scholar
  13. 13.
    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–172Google Scholar
  14. 14.
    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
  15. 15.
    G. Higman, Ordering by divisibility in abstract algebras. Proc. London Math. Soc. 2, 326–336 (1952)Google Scholar
  16. 16.
    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)Google Scholar
  17. 17.
    C. Murthy, Extracting constructive content from classical proofs. Technical Report 90–1151, Department of Computer Science, Ph.D. thesis. Cornell University, Ithaca, New York, 1990Google Scholar
  18. 18.
    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)Google Scholar
  19. 19.
    C. Nash-Williams, On well-quasi-ordering finite trees. Proc. Cambridge Phil. Soc. 59, 833–835 (1963)Google Scholar
  20. 20.
    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–297Google Scholar
  21. 21.
    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)Google Scholar
  22. 22.
    M. Rathjen, A. Weiermann, Proof-theoretic investigations on Kruskal’s theorem. Ann. Pure a. Appl. Logic 60, 49–88 (1993)Google Scholar
  23. 23.
    F. Richman, G. Stolzenberg, Well quasi-ordered sets. Adv. Math. 97, 145–153 (1993)Google Scholar
  24. 24.
    D. Schmidt, Well-Orderings and Their Maximal Order Types (Mathematisches Institut der Universität, Habilitationsschrift, Heidelberg, 1979)Google Scholar
  25. 25.
    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)Google Scholar
  26. 26.
    H. Schwichtenberg, S.S. Wainer, Proofs and Computations (Association for Symbolic Logic (Cambridge University Press, Cambridge, Perspectives in Logic, 2012)Google Scholar
  27. 27.
    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–255Google Scholar
  28. 28.
    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)Google Scholar
  29. 29.
    M. Seisenberger, On the Constructive Content of Proofs. Ph.D. thesis, Mathematisches Institut der Universität München, 2003Google Scholar
  30. 30.
    C. Sternagel, Certified Kruskal’s tree theorem. J. Formalized Reasoning 7(1), 45–62 (2014)Google Scholar
  31. 31.
    H. Touzet, Propriétés combinatoires pour la terminaison de systèmes de réécriture. Ph.D. thesis, Université Henri Poincaré, Nancy, 1997Google Scholar
  32. 32.
    H. Touzet, A characterisation of multiply recursive functions with Higman’s lemma. Inf. Comput. 178, 534–544 (2002)Google Scholar
  33. 33.
    V. Veldman, M. Bezem, Ramsey’s theorem and the pigeonhole principle in intuitionistic mathematics. J. London Math. Soc. 47, 193–211 (1993)Google Scholar
  34. 34.
    W. Veldman, An intuitionistic proof of Kruskal’s theorem. Arch. for Math. Logic 43(2), 215–264 (2004)Google Scholar
  35. 35.
    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–265Google Scholar

Copyright information

© Springer International Publishing Switzerland 2016

Authors and Affiliations

  • Helmut Schwichtenberg
    • 1
    Email author
  • Monika Seisenberger
    • 2
  • Franziskus Wiesnet
    • 1
  1. 1.Mathematisches InstitutLMUMunichGermany
  2. 2.Department of Computer ScienceSwansea UniversitySwansea SA28PPUK

Personalised recommendations