The Hydra battle and Cichon’s principle. (English) Zbl 1181.68163
Summary: 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.
Keywords:
term rewrite systemReferences:
| [1] | Arts T., Giesl J.: Termination of term rewriting using dependency pairs. Theor. Comput. Sci. 236, 133–178 (2000) · Zbl 0938.68051 · doi:10.1016/S0304-3975(99)00207-8 |
| [2] | Baader F., Nipkow T.: Term Rewriting and All That. Cambridge University Press, London (1998) · Zbl 0948.68098 |
| [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) · Zbl 0844.03031 · doi:10.1016/0168-0072(94)00056-9 |
| [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) · Zbl 0812.03023 · doi:10.1002/malq.19940400212 |
| [7] | Buss, S.-R. (eds): Handbook of Proof Theory, vol. 137. Elsevier Science, London (1998) · Zbl 0898.03001 |
| [8] | Cichon, E.-A.: Termination orderings and complexity characterisations. In: Aczel, P., Simmons, H., Wainer, S.S. (eds.) Proof Theory, pp. 171–193 (1992) · Zbl 0793.03057 |
| [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) · Zbl 0900.68283 |
| [11] | Dershowitz N., Manna Z.: Proving termination with multiset orderings. Commun. ACM 22(8), 465–476 (1979) · Zbl 0431.68016 · doi:10.1145/359138.359142 |
| [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) · Zbl 1181.68161 |
| [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) · Zbl 0759.68045 · doi:10.1016/0304-3975(92)90289-R |
| [15] | Jech T.: Set Theory. Springer, Heidelberg (2002) · Zbl 0419.03028 |
| [16] | Kirby L., Paris J.: Accessible independence results for Peano arithmetic. Bull. Lond. Math. Soc. 4, 285–293 (1982) · Zbl 0501.03017 · doi:10.1112/blms/14.4.285 |
| [17] | Lepper I.: Derivation lengths and order types of Knuth-Bendix orders. Theor. Comput. Sci. 269, 433–450 (2001) · Zbl 0983.68087 · doi:10.1016/S0304-3975(01)00015-9 |
| [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 · Zbl 1024.03037 |
| [19] | Lepper I.: Simply terminating rewrite systems with long derivations. Arch. Math. Log. 43, 1–18 (2004) · Zbl 1113.68060 · doi:10.1007/s00153-003-0190-2 |
| [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) · Zbl 1165.68391 |
| [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 · Zbl 1038.68069 |
| [23] | Pohlers W.: Proof Theory: The First Step into Impredicativity. Universitext. Springer, Heidelberg (2008) · Zbl 1153.03001 |
| [24] | Takeuti G.: Proof Theory, 2nd edn. North-Holland, Amsterdam (1987) · Zbl 0609.03019 |
| [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) · Zbl 1113.68419 |
| [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) · Zbl 0874.68156 · doi:10.1016/0304-3975(94)00135-6 |
| [28] | Zantema H.: Termination of term rewriting: interpretation and type elimination. J. Symb. Comput. 17(1), 23–50 (1994) · Zbl 0810.68087 · doi:10.1006/jsco.1994.1003 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
