Skip to main content
SpringerLink
Log in

A Constructive Proof of the Topological Kruskal Theorem

  • Conference paper
Book cover Mathematical Foundations of Computer Science 2013 (MFCS 2013)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 8087))

Abstract

We give a constructive proof of Kruskal’s Tree Theorem—precisely, of a topological extension of it. The proof is in the style of a constructive proof of Higman’s Lemma due to Murthy and Russell (1990), and illuminates the role of regular expressions there. In the process, we discover an extension of Dershowitz’ recursive path ordering to a form of cyclic terms which we call μ-terms. This all came from recent research on Noetherian spaces, and serves as a teaser for their theory.

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

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Abdulla, P.A., Čerāns, K., Jonsson, B., Tsay, Y.-K.: Algorithmic analysis of programs with well quasi-ordered domains. Inf. Comput. 160(1-2), 109–127 (2000)

    Article  MATH  Google Scholar 

  2. Abdulla, P.A., Collomb-Annichini, A., Bouajjani, A., Jonsson, B.: Using forward reachability analysis for verification of lossy channel systems. Formal Methods in System Design 25(1), 39–65 (2004)

    Article  MATH  Google Scholar 

  3. Abdulla, P.A., Jonsson, B.: Verifying programs with unreliable channels. In: LICS 1993, pp. 160–170. IEEE Computer Society Press (1993)

    Google Scholar 

  4. Acciai, L., Boreale, M.: Deciding safety properties in infinite-state pi-calculus via behavioural types. In: Albers, S., Marchetti-Spaccamela, A., Matias, Y., Nikoletseas, S., Thomas, W. (eds.) ICALP 2009, Part II. LNCS, vol. 5556, pp. 31–42. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  5. Berghofer, S.: A constructive proof of Higman’s lemma in Isabelle. In: Berardi, S., Coppo, M., Damiani, F. (eds.) TYPES 2003. LNCS, vol. 3085, pp. 66–82. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  6. Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development—Coq’Art: The Calculus of Inductive Constructions. Texts in Theor. Comp. Sci., an EATCS Series, vol. XXV. Springer (2004)

    Google Scholar 

  7. Coquand, T., Fridlender, D.: A proof of Higman’s lemma by structural induction (November 2003) (unpublished note), http://www.cse.chalmers.se/~coquand/open1.ps

  8. Coupet-Grimal, S., Delobel, W.: An effective proof of the well-foundedness of the multiset path ordering. Appl. Algebra Eng., Commun. Comput. 17(6), 453–469 (2006)

    Article  MathSciNet  MATH  Google Scholar 

  9. Dawson, J.E., Goré, R.: A general theorem on termination of rewriting. In: Marcinkowski, J., Tarlecki, A. (eds.) CSL 2004. LNCS, vol. 3210, pp. 100–114. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  10. de Groote, P., Guillaume, B., Salvati, S.: Vector addition tree automata. In: LICS 2004, pp. 64–73. IEEE Computer Society Press (2004)

    Google Scholar 

  11. Dershowitz, N.: A note on simplification orderings. Inf. Proc. Letters 9(5), 212–215 (1979)

    Article  MathSciNet  MATH  Google Scholar 

  12. Dershowitz, N.: Orderings for term-rewriting systems. Theor. Comp. Sci. 17(3), 279–301 (1982)

    Article  MathSciNet  MATH  Google Scholar 

  13. Dershowitz, N.: Termination of rewriting. J. Symb. Comp. 3, 69–116 (1987)

    Article  MathSciNet  MATH  Google Scholar 

  14. Dershowitz, N.: Jumping and escaping: Modular termination and the abstract path ordering. Theor. Comp. Sci. 464, 35–47 (2012)

    Article  MathSciNet  MATH  Google Scholar 

  15. Dershowitz, N., Hoot, C.: Natural termination. Theor. Comp. Sci. 142(2), 179–207 (1995)

    Article  MathSciNet  MATH  Google Scholar 

  16. Dershowitz, N., Jouannaud, J.-P.: Rewrite systems. In: van Leeuwen, J. (ed.) Handbook of Theor. Comp. Sci., ch. 6, pp. 243–320. Elsevier (1990)

    Google Scholar 

  17. Dershowitz, N., Manna, Z.: Proving termination with multiset orderings. Comm. ACM 22(8), 465–476 (1979)

    Article  MathSciNet  MATH  Google Scholar 

  18. Dickson, L.E.: Finiteness of the odd perfect and primitive abundant numbers with n distinct prime factors. Amer. J. Math. 35(4), 413–422 (1913)

    Article  MathSciNet  MATH  Google Scholar 

  19. Ferreira, M.C.F., Zantema, H.: Well-foundedness of term orderings. In: Lindenstrauss, N., Dershowitz, N. (eds.) CTRS 1994. LNCS, vol. 968, pp. 106–123. Springer, Heidelberg (1995)

    Chapter  Google Scholar 

  20. Finkel, A., Goubault-Larrecq, J.: Forward analysis for WSTS, part I: Completions. In: STACS 2009, Freiburg, Germany, pp. 433–444. Leibniz-Zentrum für Informatik, Intl. Proc. in Informatics 3 (2009)

    Google Scholar 

  21. Finkel, A., Goubault-Larrecq, J.: Forward analysis for WSTS, part II: Complete WSTS. In: Albers, S., Marchetti-Spaccamela, A., Matias, Y., Nikoletseas, S., Thomas, W. (eds.) ICALP 2009, Part II. LNCS, vol. 5556, pp. 188–199. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  22. Finkel, A., Goubault-Larrecq, J.: Forward analysis for WSTS, part I: Completions. Logical Methods in Computer Science (2012) (submitted)

    Google Scholar 

  23. Finkel, A., Goubault-Larrecq, J.: Forward analysis for WSTS, part II: Complete WSTS. Logical Methods in Computer Science 8(3:28) (2012)

    Google Scholar 

  24. Finkel, A., McKenzie, P., Picaronny, C.: A well-structured framework for analysing Petri net extensions. Inf. Comput. 195(1-2), 1–29 (2004)

    Article  MathSciNet  MATH  Google Scholar 

  25. Finkel, A., Schnoebelen, P.: Well-structured transition systems everywhere! Theor. Comp. Sci. 256(1-2), 63–92 (2001)

    Article  MathSciNet  MATH  Google Scholar 

  26. Goubault-Larrecq, J.: Well-founded recursive relations. In: Fribourg, L. (ed.) CSL 2001. LNCS, vol. 2142, pp. 484–497. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  27. Goubault-Larrecq, J.: On Noetherian spaces. In: LICS 2007, pp. 453–462. IEEE Computer Society Press (2007)

    Google Scholar 

  28. Goubault-Larrecq, J.: Noetherian spaces in verification. In: Abramsky, S., Gavoille, C., Kirchner, C., Meyer auf der Heide, F., Spirakis, P.G. (eds.) ICALP 2010. LNCS, vol. 6199, pp. 2–21. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  29. Goubault-Larrecq, J.: Non-Hausdorff Topology and Domain Theory—Selected Topics in Point-Set Topology. New Mathematical Monographs, vol. 22. Cambridge University Press (2013)

    Google Scholar 

  30. Higman, G.: Ordering by divisibility in abstract algebras. Proc. London Math. Soc. 2(7), 326–336 (1952)

    Article  MathSciNet  MATH  Google Scholar 

  31. Kamin, S., Lévy, J.-J.: Attempts for generalizing the recursive path orderings. Unpublished letter to N. Dershowitz (1980), http://nachum.org/term/kamin-levy80spo.pdf

  32. Karp, R.M., Miller, R.E.: Parallel program schemata. J. Comp. Sys. Sci. 3(2), 147–195 (1969)

    Article  MathSciNet  MATH  Google Scholar 

  33. Kruskal, J.B.: Well-quasi-ordering, the tree theorem, and Vazsonyi’s conjecture. Trans. AMS 95(2), 210–225 (1960)

    MathSciNet  MATH  Google Scholar 

  34. Lazič, R., Newcomb, T., Ouaknine, J., Roscoe, A.W., Worrell, J.: Nets with tokens which carry data. Fund. Informaticae 88(3), 251–274 (2008)

    MATH  Google Scholar 

  35. Lescanne, P.: Some properties of decomposition ordering, a simplification ordering to prove termination of rewriting systems. RAIRO Theor. Inform. 16(4), 331–347 (1982)

    MathSciNet  MATH  Google Scholar 

  36. Meyer, R.: On boundedness in depth in the π-calculus. In: Ausiello, G., Karhumäki, J., Mauri, G., Ong, L. (eds.) TCS 2008. IFIP, vol. 273, pp. 477–489. Springer, Boston (2008)

    Google Scholar 

  37. Murthy, C.R., Russell, J.R.: A constructive proof of Higman’s lemma. In: LICS 1990, pp. 257–267. IEEE Computer Society Press (1990)

    Google Scholar 

  38. Nash-Williams, C.S.-J.A.: On well-quasi-ordering infinite trees. Proc. Cambridge Phil. Soc. 61, 697–720 (1965)

    Article  MathSciNet  MATH  Google Scholar 

  39. Nipkow, T.: An inductive proof of the wellfoundedness of the multiset order. Technical report, Technische Universität München (October 1998)

    Google Scholar 

  40. Ogawa, M.: A linear time algorithm for monadic querying of indefinite data over linearly ordered domains. Inf. Comput. 186(2), 236–259 (2003)

    Article  MATH  Google Scholar 

  41. Richman, F., Stolzenberg, G.: Well quasi-ordered sets. Technical report, Northeastern University, Boston, MA and Harvard University, Cambridge, MA (1990)

    Google Scholar 

  42. Rosa-Velardo, F., Martos-Salgado, M.: Multiset rewriting for the verification of depth-bounded processes with name binding. Inf. Comput. 215, 68–87 (2012)

    Article  MathSciNet  MATH  Google Scholar 

  43. Seisenberger, M.: Kruskal’s tree theorem in a constructive theory of inductive definitions. In: Proc. Symp. Reuniting the Antipodes—Constructive and Nonstandard Views of the Continuum. Synthese Library, vol. 306. Kluwer Academic Publishers, Dordrecht (1999, 2001)

    Google Scholar 

  44. van der Meyden, R.: The complexity of querying indefinite data about linearly ordered domains. J. Comp. Sys. Sci. 54(1), 113–135 (1997)

    Article  MATH  Google Scholar 

  45. Veldman, W.: An intuitionistic proof of Kruskal’s theorem. Report 0017, Dept. of Mathematics, U. Nijmegen (2000)

    Google Scholar 

  46. Verma, K.N., Goubault-Larrecq, J.: Karp-Miller trees for a branching extension of VASS. Discr. Math. & Theor. Comp. Sci. 7(1), 217–230 (2005)

    MathSciNet  MATH  Google Scholar 

  47. Wies, T., Zufferey, D., Henzinger, T.A.: Forward analysis of depth-bounded processes. In: Ong, L. (ed.) FOSSACS 2010. LNCS, vol. 6014, pp. 94–108. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. LSV, ENS Cachan, CNRS, INRIA, France

    Jean Goubault-Larrecq

Authors
  1. Jean Goubault-Larrecq
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Institute for Science and Technology, 3400, Klosterneuburg, Austria

    Krishnendu Chatterjee

  2. Charles University, 11800, Prague, Czech Republic

    Jirí Sgall

Rights and permissions

Reprints and permissions

Copyright information

© 2013 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Goubault-Larrecq, J. (2013). A Constructive Proof of the Topological Kruskal Theorem. In: Chatterjee, K., Sgall, J. (eds) Mathematical Foundations of Computer Science 2013. MFCS 2013. Lecture Notes in Computer Science, vol 8087. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-40313-2_3

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-40313-2_3

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-40312-5

  • Online ISBN: 978-3-642-40313-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation