Skip to main content
Springer Nature Link
Log in

The Hydra battle and Cichon’s principle

  • Published:
Applicable Algebra in Engineering, Communication and Computing Aims and scope

Abstract

In rewriting the Hydra battle refers to a term rewrite system \({\mathcal{H}}\) proposed by Dershowitz and Jouannaud. To date, \({\mathcal{H}}\) withstands any attempt to prove its termination automatically. This motivates our interest in term rewrite systems encoding the Hydra battle, as a careful study of such systems may prove useful in the design of automatic termination tools. Moreover it has been an open problem, whether any termination order compatible with \({\mathcal{H}}\) has to have the Howard–Bachmann ordinal as its order type, i.e., the proof theoretic ordinal of the theory of one inductive definition. We answer this question in the negative, by providing a reduction order compatible with \({\mathcal{H}}\) , whose order type is at most \({\epsilon_0}\) , the proof theoretic ordinal of Peano arithmetic.

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

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

Explore related subjects

Discover the latest articles, news and stories from top researchers in related subjects.

References

  1. Arts T., Giesl J.: Termination of term rewriting using dependency pairs. Theor. Comput. Sci. 236, 133–178 (2000)

    Article  MATH  MathSciNet  Google Scholar 

  2. Baader F., Nipkow T.: Term Rewriting and All That. Cambridge University Press, London (1998)

    Google Scholar 

  3. Beklemishev, L.: Representing worms as a term rewriting system. In: Mini-Workshop: Logic, Combinatorics and Independence Results, pp. 3093–3095. Mathematisches Forschungsinstitut Oberwolfach, Report No. 52/2006, 2006, 2006 (abstract)

  4. Buchholz W.: Proof-theoretical analysis of termination proofs. Ann. Pure Appl. Log. 75, 57–65 (1995)

    Article  MATH  MathSciNet  Google Scholar 

  5. Buchholz, W.: Another rewrite system for the standard Hydra battle. In: Mini-Workshop: Logic, Combinatorics and Independence Results, pp. 3011–3099. Mathematisches Forschungsinstitut Oberwolfach, Report No. 52/2006, 2006, 2006 (abstract)

  6. Buchholz W., Cichon E.-A., Weiermann A.: A uniform approach to fundamental sequences and hierarchies. Math. Log. Q. 40, 273–286 (1994)

    Article  MATH  MathSciNet  Google Scholar 

  7. Buss, S.-R. (eds): Handbook of Proof Theory, vol. 137. Elsevier Science, London (1998)

    Google Scholar 

  8. Cichon, E.-A.: Termination orderings and complexity characterisations. In: Aczel, P., Simmons, H., Wainer, S.S. (eds.) Proof Theory, pp. 171–193 (1992)

  9. Dershowitz, N.: 33 examples of termination. In: French Spring School of Theoretical Computer Science Advanced Course on Term Rewriting, Font Romeux, France, May 1993, LNCS, vol. 909, pp. 16–26 (1995)

  10. Dershowitz N., Jouannaud J.-P.: Rewrite systems. In: Leeuwen, J. (eds) Handbook of Theoretical Computer Science, pp. 245–319. Elsevier Science, London (1990)

    Google Scholar 

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

    Article  MATH  MathSciNet  Google Scholar 

  12. Dershowitz, N., Moser, G.: The Hydra battle revisited. In: Rewriting, Computation and Proof. LNCS, vol. 4600, pp. 1–27. Springer, Heidelberg (2007) (Essays Dedicated to Jean-Pierre Jouannaud on the Occasion of His 60th Birthday)

  13. Ferreira, M.C.F.: Termination of Term Rewriting. Well-Foundedness, Totality and Transformations. Ph.D. Thesis, University of Utrecht, November (1995)

  14. Hofbauer D.: Termination proofs by multiset path orderings imply primitive recursive derivation lengths. Theor. Comput. Sci. 105, 129–140 (1992)

    Article  MATH  MathSciNet  Google Scholar 

  15. Jech T.: Set Theory. Springer, Heidelberg (2002)

    Google Scholar 

  16. Kirby L., Paris J.: Accessible independence results for Peano arithmetic. Bull. Lond. Math. Soc. 4, 285–293 (1982)

    Article  MathSciNet  Google Scholar 

  17. Lepper I.: Derivation lengths and order types of Knuth-Bendix orders. Theor. Comput. Sci. 269, 433–450 (2001)

    Article  MATH  MathSciNet  Google Scholar 

  18. Lepper, I.: Simplification Orders in Term Rewriting. PhD thesis, WWU Münster, 2002. http://www.math.uni-muenster.de/logik/publ/diss/9.html

  19. Lepper I.: Simply terminating rewrite systems with long derivations. Arch. Math. Log. 43, 1–18 (2004)

    Article  MATH  MathSciNet  Google Scholar 

  20. Manna, Z., Ness, S.: On the termination of Markov algorithms. In: Proceedings of the Third Hawaii International Conference on System Science, pp. 789–792 (1970)

  21. Moser, G.: Derivational complexity of Knuth Bendix orders revisited. In: Proceedings of the 13th International Conference on Logic for Programming Artificial Intelligence and Reasoning. LNCS, vol. 4246, pp. 75–89. Springer, Heidelberg (2006)

  22. Moser, G., Weiermann, A.: Relating derivation lengths with the slow-growing hierarchy directly. In: Proceedings of the 14th International Conference on Rewriting Techniques and Applications, number 2706 in LNCS, pages 296–310. Springer Verlag, 2003

  23. Pohlers W.: Proof Theory: The First Step into Impredicativity. Universitext. Springer, Heidelberg (2008)

    Google Scholar 

  24. Takeuti G.: Proof Theory, 2nd edn. North-Holland, Amsterdam (1987)

    Google Scholar 

  25. TeReSe. Term Rewriting Systems. Cambridge Tracks in Theoretical Computer Science, vol. 55. Cambridge University Press, London (2003)

  26. Touzet, H.: Encoding the Hydra battle as a rewrite system. In: Proceedings of the 23rd International Symposium on Mathematical Foundations of Computer Science. LNCS 1450, pp. 267–276. Springer, Heidelberg (1998)

  27. Weiermann A.: Termination proofs for term rewriting systems with lexicographic path ordering imply multiply recursive derivation lengths. Theor. Comput. Sci. 139, 355–362 (1995)

    Article  MATH  MathSciNet  Google Scholar 

  28. Zantema H.: Termination of term rewriting: interpretation and type elimination. J. Symb. Comput. 17(1), 23–50 (1994)

    Article  MATH  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institute of Computer Science, University of Innsbruck, 6020, Innsbruck, Austria

    Georg Moser

Authors
  1. Georg Moser
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Georg Moser.

Rights and permissions

Reprints and permissions

About this article

Cite this article

Moser, G. The Hydra battle and Cichon’s principle. AAECC 20, 133–158 (2009). https://doi.org/10.1007/s00200-009-0094-4

Download citation

  • Received:

  • Revised:

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s00200-009-0094-4

Keywords

Search

Navigation