Document Open Access Logo

A General Constructive Form of Higman’s Lemma

Authors Stefano Berardi , Gabriele Buriola, Peter Schuster

PDF
Thumbnail PDF

File

LIPIcs.CSL.2024.16.pdf
  • Filesize: 0.78 MB
  • 17 pages

Document Identifiers

Author Details

Stefano Berardi
  • Dipartimento di Informatica, Università di Torino, Italy
Gabriele Buriola
  • Dipartimento di Informatica, Università di Verona, Italy
Peter Schuster
  • Dipartimento di Informatica, Università di Verona, Italy

Acknowledgements

The present study was started while the third author worked within the project "Reducing complexity in algebra, logic, combinatorics - REDCOM" belonging to the programme "Ricerca Scientifica di Eccellenza 2018" of the Fondazione Cariverona. The second and the third author are members of the "Gruppo Nazionale per le Strutture Algebriche, Geometriche e le loro Applicazioni" (GNSAGA) of the Istituto Nazionale di Alta Matematica (INdAM). The authors wish to thank Daniel Fridlender for his interest and suggestions, and to express their gratitude to Thierry Coquand, whose original idea set the basis for this work. Last but not least, the anonymous reviewers' meticulous reading and constructive critique have been extremely helpful.

Cite AsGet BibTex

Stefano Berardi, Gabriele Buriola, and Peter Schuster. A General Constructive Form of Higman’s Lemma. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 16:1-16:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.CSL.2024.16

Abstract

In logic and computer science one often needs to constructivize a theorem ∀ f ∃ g.P(f,g), stating that for every infinite sequence f there is an infinite sequence g such that P(f,g). Here P is a computable predicate but g is not necessarily computable from f. In this paper we propose the following constructive version of ∀ f ∃ g.P(f,g): for every f there is a "long enough" finite prefix g₀ of g such that P(f,g₀), where "long enough" is expressed by membership to a bar which is a free parameter of the constructive version. Our approach with bars generalises the approaches to Higman’s lemma undertaken by Coquand-Fridlender, Murthy-Russell and Schwichtenberg-Seisenberger-Wiesnet. As a first test for our bar technique, we sketch a constructive theory of well-quasi orders. This includes yet another constructive version of Higman’s lemma: that every infinite sequence of words has an infinite ascending subsequence. As compared with the previous constructive versions of Higman’s lemma, our constructive proofs are closer to the original classical proofs.

Subject Classification

ACM Subject Classification
  • Theory of computation → Constructive mathematics
  • Theory of computation → Proof theory
  • Mathematics of computing → Discrete mathematics
Keywords
  • intuitionistic logic
  • constructive mathematics
  • formal proof
  • inductive predicate
  • bar induction
  • well quasi-order
  • Higman’s lemma

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. P. Aczel. An introduction to inductive definitions, volume 90 of Stud. Logic Found. Math., pages 739-782. North-Holland, 1977. Google Scholar
  2. S. Berardi and S. Steila. Ramsey’s Theorem for Pairs and k Colors as a sub-Classical Principle of Arithmetic. J. Symbolic Logic, 82(2):737-753, 2017. Google Scholar
  3. J. Berger. Dickson’s Lemma and Higman’s Lemma are Equivalent. South American Journal of Logic, 2(1):35-39, 2016. Google Scholar
  4. S. Berghofer. A Constructive Proof of Higman’s Lemma in Isabelle. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), volume 3085 of Lecture Notes in Computer Science, pages 66-82, Berlin, Heidelberg, 2004. Springer Berlin Heidelberg. Google Scholar
  5. Yves Bertot and Ekaterina Komendantskaya. Inductive and coinductive components of corecursive functions in coq. Electronic Notes in Theoretical Computer Science, 203(5):25-47, 2008. Proceedings of the Ninth Workshop on Coalgebraic Methods in Computer Science (CMCS 2008). URL: https://doi.org/10.1016/j.entcs.2008.05.018.
  6. G. Buriola, P. Schuster, and I. Blechschmidt. A Constructive Picture of Noetherian Conditions and Well Quasi-orders. In Gianluca Della Vedova, Besik Dundua, Steffen Lempp, and Florin Manea, editors, Unity of Logic and Computation, pages 50-62, Cham, 2023. Springer Nature Switzerland. Google Scholar
  7. T. Coquand and D. Fridlender. A proof of Higman’s lemma by structural induction. Unpublished Manuscript. http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.47.486, November 1993.
  8. Thierry Coquand and Henrik Persson. Gröbner bases in type theory. In T. Altenkirch, W. Naraschewski, and B. Reus, editors, Types for Proofs and Programs (Irsee, 1998), volume 1657 of Lecture Notes in Comput. Sci., pages 33-46. Springer, Berlin, 1999. Google Scholar
  9. D. Fridlender. Higman’s Lemma in Type Theory. PhD thesis, Chalmers University of Technology, Göteborg, 1997. Google Scholar
  10. J. Goubault-Larrecq. A Constructive Proof of the Topological Kruskal Theorem. In Krishnendu Chatterjee and Jirí Sgall, editors, Mathematical Foundations of Computer Science 2013, pages 22-41, Berlin, Heidelberg, 2013. Springer Berlin Heidelberg. Google Scholar
  11. G. Higman. Ordering by Divisibility in Abstract Algebras. Proceedings of the London Mathematical Society, s3-2(1):326-336, 1952. Google Scholar
  12. J.B. Kruskal. Well-quasi-ordering, the tree theorem, and Vazsonyi’s conjecture. Trans. Amer. Math. Soc., 95:210-225, 1960. Google Scholar
  13. J.B. Kruskal. The theory of well-quasi-ordering: A frequently discovered concept. J. Comb. Theory A, 13:297-305, 1972. Google Scholar
  14. Ray Mines, Fred Richman, and Wim Ruitenburg. A Course in Constructive Algebra. Springer, New York, 1988. Universitext. Google Scholar
  15. C.R. Murthy and J.R. Russell. A constructive proof of Higman’s lemma. 5th Annual Symposium on Logic in Computer Science, Philadelphia PA, pages 257-267, 1992. Google Scholar
  16. C.St.J.A. Nash-William. On well-quasi-ordering finite trees. Proc. Cambridge Phil. Soc., 59:833-835, 1963. Google Scholar
  17. Hervé Perdry. Strongly Noetherian rings and constructive ideal theory. J. Symb. Comput., 37(4):511-535, 2004. Google Scholar
  18. Hervé Perdry and Peter Schuster. Noetherian orders. Math. Structures Comput. Sci., 21:111-124, 2011. Google Scholar
  19. T. Powell. Applying Gödel’s Dialectica interpretation to obtain a constructive proof of Higman’s lemma. Proceedings of Classical Logic and Computation (CLAC'12), volume 97 of EPTCS:49-62, 2012. Google Scholar
  20. T. Powell. Well Quasi-orders and the Functional Interpretation. In Peter M. Schuster, Monika Seisenberger, and Andreas Weiermann, editors, Well-Quasi Orders in Computation, Logic, Language and Reasoning: A Unifying Concept of Proof Theory, Automata Theory, Formal Languages and Descriptive Set Theory, pages 221-269, Cham, 2020. Springer International Publishing. URL: https://doi.org/10.1007/978-3-030-30229-0_9.
  21. Michael Rathjen. Generalized inductive definitions in constructive set theory. In Laura Crosilla and Peter Schuster, editors, From Sets and Types to Topology and Analysis: Towards Practicable Foundations for Constructive Mathematics, volume 48 of Oxford Logic Guides, chapter 16. Clarendon Press, Oxford, 2005. Google Scholar
  22. F. Richman and G. Stolzenberg. Well quasi-ordered sets. Advances in Mathematics, 97:145-153, 1993. Google Scholar
  23. H. Schwichtenberg, M. Seisenberger, and F. Wiesnet. Higman’s Lemma and Its Computational Content. In R. Kahle, T. Strahm, and T. Studer, editors, Advances in Proof Theory, pages 353-375, Cham, 2016. Springer International Publishing. URL: https://doi.org/10.1007/978-3-319-29198-7_11.
  24. M. Seisenberger. An Inductive Version of Nash-Williams' Minimal-Bad-Sequence Argument for Higman’s Lemma. Types for Proofs and Programs, LNCS Vol. 2277, 2001. Google Scholar
  25. Monika Seisenberger. Kruskal’s tree theorem in a constructive theory of inductive definitions. In P. Schuster, U. Berger, and H. Osswald, editors, Reuniting the antipodes - constructive and nonstandard views of the continuum (Venice, 1999), volume 306 of Synthese Library, pages 241-255. Kluwer, Dordrecht, 2001. Google Scholar
  26. C. Sternagel. A Mechanized Proof of Higman’s Lemma by Open Induction. In Peter M. Schuster, Monika Seisenberger, and Andreas Weiermann, editors, Well-Quasi Orders in Computation, Logic, Language and Reasoning: A Unifying Concept of Proof Theory, Automata Theory, Formal Languages and Descriptive Set Theory, pages 339-350, Cham, 2020. Springer International Publishing. URL: https://doi.org/10.1007/978-3-030-30229-0_12.
  27. A.S. Troelstra. Metamathematica Investigation of Intuitionistic Arithmetic and Analysis. ILLC pre-publication series, pages X-93-05, 1993. Google Scholar
  28. W. Veldman. An Intuitionistic Proof of Kruskal’s Theorem. Archive for Mathematical Logic, 43(2):215-264, 2004. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact