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.
Similar content being viewed by others
Explore related subjects
Discover the latest articles, news and stories from top researchers in related subjects.References
Arts T., Giesl J.: Termination of term rewriting using dependency pairs. Theor. Comput. Sci. 236, 133–178 (2000)
Baader F., Nipkow T.: Term Rewriting and All That. Cambridge University Press, London (1998)
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)
Buchholz W.: Proof-theoretical analysis of termination proofs. Ann. Pure Appl. Log. 75, 57–65 (1995)
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)
Buchholz W., Cichon E.-A., Weiermann A.: A uniform approach to fundamental sequences and hierarchies. Math. Log. Q. 40, 273–286 (1994)
Buss, S.-R. (eds): Handbook of Proof Theory, vol. 137. Elsevier Science, London (1998)
Cichon, E.-A.: Termination orderings and complexity characterisations. In: Aczel, P., Simmons, H., Wainer, S.S. (eds.) Proof Theory, pp. 171–193 (1992)
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)
Dershowitz N., Jouannaud J.-P.: Rewrite systems. In: Leeuwen, J. (eds) Handbook of Theoretical Computer Science, pp. 245–319. Elsevier Science, London (1990)
Dershowitz N., Manna Z.: Proving termination with multiset orderings. Commun. ACM 22(8), 465–476 (1979)
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)
Ferreira, M.C.F.: Termination of Term Rewriting. Well-Foundedness, Totality and Transformations. Ph.D. Thesis, University of Utrecht, November (1995)
Hofbauer D.: Termination proofs by multiset path orderings imply primitive recursive derivation lengths. Theor. Comput. Sci. 105, 129–140 (1992)
Jech T.: Set Theory. Springer, Heidelberg (2002)
Kirby L., Paris J.: Accessible independence results for Peano arithmetic. Bull. Lond. Math. Soc. 4, 285–293 (1982)
Lepper I.: Derivation lengths and order types of Knuth-Bendix orders. Theor. Comput. Sci. 269, 433–450 (2001)
Lepper, I.: Simplification Orders in Term Rewriting. PhD thesis, WWU Münster, 2002. http://www.math.uni-muenster.de/logik/publ/diss/9.html
Lepper I.: Simply terminating rewrite systems with long derivations. Arch. Math. Log. 43, 1–18 (2004)
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)
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)
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
Pohlers W.: Proof Theory: The First Step into Impredicativity. Universitext. Springer, Heidelberg (2008)
Takeuti G.: Proof Theory, 2nd edn. North-Holland, Amsterdam (1987)
TeReSe. Term Rewriting Systems. Cambridge Tracks in Theoretical Computer Science, vol. 55. Cambridge University Press, London (2003)
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)
Weiermann A.: Termination proofs for term rewriting systems with lexicographic path ordering imply multiply recursive derivation lengths. Theor. Comput. Sci. 139, 355–362 (1995)
Zantema H.: Termination of term rewriting: interpretation and type elimination. J. Symb. Comput. 17(1), 23–50 (1994)
Author information
Authors and Affiliations
Corresponding author
Rights 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
Received:
Revised:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s00200-009-0094-4