Skip to main content
SpringerLink
Log in

Higman's lemma in type theory

  • Conference paper
  • First Online:
Types for Proofs and Programs (TYPES 1996)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 1512))

Included in the following conference series:

Abstract

This paper starts with a brief exploration of the history of Higman's lemma with emphasis on Veldman's recent intuitionistic proof, which established the lemma in its most general form. The rest of the paper is devoted to the description of a type-theoretic proof of such a general form of Higman's lemma. This involves considering type-theoretic formulations of bar induction, fan theorem, Ramsey theorem, and Higman's lemma. The proof was formalized in Martin-Löf's type theory without universes, and edited and checked in the proof editor ALF.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. P. Abdulla, K. Cerans, B. Jonsson, and Y.-K. Tsay. General decidability theorems for infinite-state systems. In 11th Annual IEEE Symposium on Logic in Computer Science. Proceedings, 1996.

    Google Scholar 

  2. P. Abdulla and B. Jonsson. Verifying programs with unreliable channels. In 8th Annual IEEE Symposium on Logic in Computer Science. Proceedings, pages 160–170, 1993.

    Google Scholar 

  3. L. Brouwer. Points and spaces. Canadian Journal of Mathematics, 6:1–17, 1954.

    MATH  MathSciNet  Google Scholar 

  4. H. Curry and R. Feys. Combinatory Logic, volume I. North-Holland, 1958.

    Google Scholar 

  5. T. Coquand, D. Fridlender, and H. Herbelin. A proof of higman's lemma by structural induction. Unpublished manuscript, 1993.

    Google Scholar 

  6. R. Constable et al. Implementing Mathematics with the NuPRL Proof Development System. Prentice-Hall, Englewood Cliffs, NJ, 1986.

    Google Scholar 

  7. T. Coquand. Pattern matching with dependent types. In Proceeding from the logical framework workshop at Båstad, June 1992.

    Google Scholar 

  8. L. Dickson. Finiteness of the odd perfect and primitive abundant numbers with n distinct prime factors. American Journal of Mathematics, 35:413–426, 1913.

    Article  MATH  MathSciNet  Google Scholar 

  9. N. Dershowitz and J.-P. Jouannaud. Rewrite systems. In J. Van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B, chapter 6, page 273. Elsevier, 1990.

    Google Scholar 

  10. M. Dummett. Elements of intuitionism. Clarendon Press, Oxford, 1977.

    MATH  Google Scholar 

  11. P. Dybjer. Inductive families. Formal Aspects of Computing, 6:440–465, 1994.

    Article  MATH  Google Scholar 

  12. P. Erdös and R. Rado. Sets having a divisor property. American Mathematical Monthly, 59:255–257, 1952.

    Article  MathSciNet  Google Scholar 

  13. P. Erdös. Problem 4358. American Mathematical Monthly, 56:480, 1949.

    Article  MathSciNet  Google Scholar 

  14. H. Friedman. Classically and intuitionistically provably recursive functions. In D. Scott and G. Muller, editors, Higher Set Theory, volume 669 of Lecture Notes in Mathematics, pages 21–28. Springer-Verlag, 1978.

    Google Scholar 

  15. D. Fridlender. Ramsey's theorem in type theory. Licentiate Thesis, Chalmers University of Technology and University of Göteborg, Sweden, October 1993.

    Google Scholar 

  16. K. Gödel. Zur intuitionistischen arithmetik und zahlentheorie. Ergebnisse eines mathematischen Kolloquiums, 4:34–38, 1933. English: [Göd65].

    MATH  Google Scholar 

  17. K. Gödel. On intuitionistic arithmetic and number theory. In M. Davis, editor, The Undecidable, pages 75–81, Raven Press, 1965.

    Google Scholar 

  18. L. Haines. On free monoids partially ordered by embedding. Journal of Combinatorial Theory, 6:94–98, 1969.

    MATH  MathSciNet  Google Scholar 

  19. G. Higman. Ordering by divisibility in abstract algebras. Proceedings of the London Mathematical Society, (3) 2:326–336, 1952.

    MATH  MathSciNet  Google Scholar 

  20. W. Howard. The formulae-as-types notion of construction. In J. Seldin and J. Hindley, editors, To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pages 479–490. Academic Press, London, 1980.

    Google Scholar 

  21. D. de Jongh and R. Parikh. Well-partial orderings and hierarchies. Indagationes Mathematicae, 39:195–207, 1977.

    Google Scholar 

  22. P. Jullien. Sur un théorème d'extension dans la théorie des mots. Comptes Rendus de la Academie de Sciences de Paris, (A) 266:851–854, 1968.

    MATH  MathSciNet  Google Scholar 

  23. J. Kruskal. Well-Quasi-Ordering, the tree theorem, and Vazsonyi's conjecture. Transactions of the American Mathematical Society, 95:210–225, 1960.

    Article  MATH  MathSciNet  Google Scholar 

  24. J. Kruskal. The Theory of Well-Quasi-Ordering: A Frequently Discovered Concept. Journal of Combinatorial Theory (A), 13:297–305, 1972.

    Article  MATH  MathSciNet  Google Scholar 

  25. L. Magnusson. The Implementation of ALF—a Proof Editor based on Martin-Löf's Monomorphic Type Theory with Explicit Substitution. PhD thesis, Department of Computing Science, Chalmers University of Technology and University of Göteborg, 1994.

    Google Scholar 

  26. P. Martin-Löf. Notes on Constructive Mathematics. Almqvist & Wiksell, 1968.

    Google Scholar 

  27. P. Martin-Löf. An Intuitionistic Theory of Types: Predicative Part. In H. E. Rose and J. C. Shepherdson, editors, Logic Colloquium 1973, pages 73–118, Amsterdam, 1975. North-Holland Publishing Company.

    Google Scholar 

  28. P. Martin-Löf. Intuitionistic Type Theory. Bibliopolis, Napoli, 1984.

    Google Scholar 

  29. E. Martino and P. Giaretta. Brouwer, dummett and the bar theorem. In Atti del Convengo Nazionale di Logica. Bibliopolis, 1979.

    Google Scholar 

  30. C. Murthy and J. Russell. A constructive proof of higman's lemma. In Fifth annual IEEE Symposium on Logic in Computer Science, pages 257–267, 1990.

    Google Scholar 

  31. C. Murthy. Extracting Constructive Content from Classical Proofs. PhD thesis, Cornell University, 1990.

    Google Scholar 

  32. C. Nash-Williams. On well-quasi-ordering finite trees. Proceedings of the Cambridge Philosophical Society, 59:833–835, 1963.

    Article  MATH  MathSciNet  Google Scholar 

  33. B. Neumann. On ordered division rings. Transaction of the American Mathematical Society, 66:202–252, 1949.

    Article  MATH  Google Scholar 

  34. B. Nordström, K. Petersson, and J. Smith. Programming in Martin-Löf's Type Theory. An Introduction. Oxford University Press, 1990.

    Google Scholar 

  35. F. Richman and G. Stolzenberg. Well Quasi-Ordered Sets. Advances in Mathematics, 97:145–153, 1993.

    Article  MATH  MathSciNet  Google Scholar 

  36. D. Schmidt. Well-Partial-Orderings and Their Maximal Order Types. Habilitationsschrift, 1979.

    Google Scholar 

  37. S. Simpson. Ordinal numbers and the hilbert basis theorem. The Journal of Symbolic Logic, 53:961–974, 1988.

    Article  MATH  MathSciNet  Google Scholar 

  38. J. Smith. The Independence of Peano's Fourth Axiom from Martin-Löf's Type Theory without Universes. Journal of Symbolic Logic, 53:840–845, 1988.

    Article  MATH  MathSciNet  Google Scholar 

  39. K. Schütte and S. Simpson. Ein in der reinen zahlentheorie unberweisbarer satz über endliche folgen von natürlichen zahlen. Archiv für Mathematische Logik und Grundlagenfroschung, 25:75–89, 1985.

    Article  MATH  Google Scholar 

  40. A. Tasistro. Substitution, record types and subtyping in type theory, with applications to the theory of programming. PhD thesis, Department of Computing Science at Chalmers University of Technology and University of Göteborg, 1997.

    Google Scholar 

  41. W. Veldman and M. Bezem. Ramsey's theorem and the pigeonhole principle in intuitionistic mathematics. Journal of the London Mathematical Society, (2) 47:193–211, 1993.

    MATH  MathSciNet  Google Scholar 

  42. W. Veldman. Intuitionistic proof of the general non-decidable case of higman's lemma. Personal communication, 1994.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computing Science, University of Göteborg and Chalmers University of Technology, S 412 96, Göteborg, Sweden

    Daniel Fridlender

Authors
  1. Daniel Fridlender
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Eduardo Giménez Christine Paulin-Mohring

Rights and permissions

Reprints and permissions

Copyright information

© 1998 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Fridlender, D. (1998). Higman's lemma in type theory. In: Giménez, E., Paulin-Mohring, C. (eds) Types for Proofs and Programs. TYPES 1996. Lecture Notes in Computer Science, vol 1512. Springer, Berlin, Heidelberg . https://doi.org/10.1007/BFb0097789

Download citation

  • DOI: https://doi.org/10.1007/BFb0097789

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-65137-6

  • Online ISBN: 978-3-540-49562-8

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation