×

Beyond polynomials and Peano arithmetic – automation of elementary and ordinal interpretations. (English) Zbl 1315.68168

Summary: L. Kirby and J. Paris [Bull. Lond. Math. Soc. 14, 285–293 (1982; Zbl 0501.03017)] proved in a celebrated paper that a theorem of R. L. Goodstein [J. Symb. Log. 9, 33–41 (1944; Zbl 0060.02306)] cannot be established in Peano arithmetic. We present an encoding of Goodstein’s theorem as a termination problem of a finite rewrite system. Using a novel implementation of algebras based on ordinal interpretations, we are able to automatically prove termination of this system, resulting in the first automatic termination proof for a system whose derivational complexity is not multiple recursive. Our method can also cope with the encoding by H. Touzet [Lect. Notes Comput. Sci. 1450, 267–276 (1998; Zbl 1113.68419)] of the battle of Hercules and Hydra as well as a (corrected) encoding by L. Beklemishev [“Representing worms as term rewriting systems”, Oberwolfach Rep. 3, No. 4, 3093–3095 (2006)] of the Worm battle, two further systems which have been out of reach for automatic tools, until now. Based on our ideas of implementing ordinal algebras we also present a new approach for the automation of elementary interpretations for termination analysis.

MSC:

68Q42 Grammars and rewriting systems
03B35 Mechanization of proofs and logical operations

Software:

Tyrolean
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Baader, F.; Nipkow, T., Term Rewriting and All That (1998), Cambridge University Press: Cambridge University Press Cambridge
[2] Beklemishev, L., Representing Worms as term rewriting systems, (Proc. Mini-Workshop: Logic, Combinatorics and Independence Results. Proc. Mini-Workshop: Logic, Combinatorics and Independence Results, Oberwolfach Rep., vol. 3(4) (2006), European Mathematical Society), 3093-3095
[3] Buchholz, W., An independence result for \((\pi_1^1 - CA) + BI\), Ann. Pure Appl. Log., 33, 131-155 (1987) · Zbl 0636.03052
[4] Buchholz, W., Another rewrite system for the standard Hydra battle, (Proc. Mini-Workshop: Logic, Combinatorics and Independence Results. Proc. Mini-Workshop: Logic, Combinatorics and Independence Results, Oberwolfach Rep., vol. 3(4) (2006), European Mathematical Society), 3099-3102
[5] Cichon, E., A short proof of two recently discovered independence results using recursion theoretic methods, Proc. Am. Math. Soc., 87, 4, 704-706 (1983) · Zbl 0512.03028
[6] Contejean, E.; Marché, C.; Tomás, A.-P.; Urbain, X., Mechanically proving termination using polynomial interpretations, J. Autom. Reason., 34, 4, 325-363 (2005) · Zbl 1108.03017
[7] Dershowitz, N., Trees, ordinals, and termination, (TAPSOFT. TAPSOFT, Lect. Notes Comput. Sci., vol. 668 (1993)), 243-250 · Zbl 1497.68140
[8] Dershowitz, N.; Jouannaud, J.-P., Rewrite systems, (Handbook of Theoretical Computer Science. Volume B: Formal Models and Semantics (1990), Elsevier), 243-320 · Zbl 0900.68283
[9] Dershowitz, N.; Moser, G., The Hydra battle revisited, (Rewriting, Computation and Proof, Essays Dedicated to Jean-Pierre Jouannaud on the Occasion of His 60th Birthday. Rewriting, Computation and Proof, Essays Dedicated to Jean-Pierre Jouannaud on the Occasion of His 60th Birthday, Lect. Notes Comput. Sci., vol. 4600 (2007)), 1-27 · Zbl 1181.68161
[10] Endrullis, J.; Waldmann, J.; Zantema, H., Matrix interpretations for proving termination of term rewriting, J. Autom. Reason., 40, 2-3, 195-220 (2008) · Zbl 1139.68049
[11] Fleischer, R., Die another day, Theory Comput. Syst., 44, 2, 205-214 (2009) · Zbl 1175.91038
[12] Fuhs, C.; Giesl, J.; Middeldorp, A.; Schneider-Kamp, P.; Thiemann, R.; Zankl, H., SAT solving for termination analysis with polynomial interpretations, (SAT. SAT, Lect. Notes Comput. Sci., vol. 4501 (2007)), 340-354 · Zbl 1214.68352
[13] Gentzen, G., Die Widerspruchsfreiheit der reinen Zahlentheorie, Math. Ann., 122, 493-565 (1936) · JFM 62.0044.01
[14] Goodstein, R. L., On the restricted ordinal theorem, J. Symb. Log., 9, 2, 33-41 (1944) · Zbl 0060.02306
[15] Hamano, M.; Okada, M., A relationship among Gentzen’s proof-reduction, Kirby-Paris’ Hydra game and Buchholz’s Hydra game, Math. Log. Q., 43, 103-120 (1997) · Zbl 0872.03038
[16] Hirokawa, N.; Middeldorp, A., Polynomial interpretations with negative coefficients, (AISC. AISC, Lect. Notes Comput. Sci., vol. 3249 (2004)), 185-198 · Zbl 1109.68501
[17] Hofbauer, D.; Lautemann, C., Termination proofs and the length of derivations (preliminary version), (RTA. RTA, Lect. Notes Comput. Sci., vol. 355 (1989)), 167-177 · Zbl 1503.68116
[18] Hong, H.; Jakuš, D., Testing positiveness of polynomials, J. Autom. Reason., 21, 1, 23-38 (1998) · Zbl 0916.68084
[19] Just, W.; Weese, M., Discovering Modern Set Theory. I: The Basics (1996), American Mathematical Society · Zbl 0854.04001
[20] Kirby, L.; Paris, J., Accessible independence results for Peano arithmetic, Bull. Lond. Math. Soc., 14, 285-325 (1982) · Zbl 0501.03017
[21] Korp, M.; Sternagel, C.; Zankl, H.; Middeldorp, A., Tyrolean termination tool 2, (Proc. of the 20th RTA. Proc. of the 20th RTA, Lect. Notes Comput. Sci., vol. 5595 (2009)), 295-304
[22] Kovács, L.; Moser, G.; Voronkov, A., On transfinite Knuth-Bendix orders, (CADE. CADE, Lect. Notes Comput. Sci., vol. 6803 (2011)), 384-399 · Zbl 1341.68194
[23] Lepper, I., Derivation lengths and order types of Knuth-Bendix orders, Theor. Comput. Sci., 269, 1-2, 433-450 (2001) · Zbl 0983.68087
[24] Lepper, I., Simply terminating rewrite systems with long derivations, Arch. Math. Log., 43, 1, 1-18 (2004) · Zbl 1113.68060
[25] Lescanne, P., Termination of rewrite systems by elementary interpretations, Form. Asp. Comput., 7, 1, 77-90 (1995) · Zbl 0817.68095
[26] Lucas, S., Automatic proofs of termination with elementary interpretations, (Proc. of the 9th PROLE. Proc. of the 9th PROLE, Electron. Notes Theor. Comput. Sci., vol. 258 (2009)), 41-61 · Zbl 1294.68058
[27] Manolios, P.; Vroon, D., Ordinal arithmetic: algorithms and mechanization, J. Autom. Reason., 34, 4, 387-423 (2005) · Zbl 1108.03020
[28] Moser, G., The Hydra battle and Cichon’s principle, Appl. Algebra Eng. Commun. Comput., 20, 2, 133-158 (2009) · Zbl 1181.68163
[29] Moser, G.; Schnabl, A., The derivational complexity induced by the dependency pair method, Log. Methods Comput. Sci., 7, 3 (2011) · Zbl 1237.68109
[30] Schnabl, A., Derivational complexity analysis revisited (2012), University of Innsbruck, Ph.D. thesis
[31] TeReSe, Term Rewriting Systems, Camb. Tracts Theor. Comput. Sci., vol. 55 (2003), Cambridge University Press
[32] Touzet, H., Encoding the Hydra battle as a rewrite system, (MFCS. MFCS, Lect. Notes Comput. Sci., vol. 1450 (1998)), 267-276 · Zbl 1113.68419
[33] Turing, A., Checking a large routine, (Report of a Conference on High Speed Automatic Calculating Machines (1949)), 67-68
[34] Urban, C.; Miné, A., An abstract domain to infer ordinal-valued ranking functions, (Proc. of the 23rd European Symposium on Programming. Proc. of the 23rd European Symposium on Programming, ESOP 2014. Proc. of the 23rd European Symposium on Programming. Proc. of the 23rd European Symposium on Programming, ESOP 2014, Lect. Notes Comput. Sci., vol. 8410 (2014)), 412-431 · Zbl 1405.68094
[35] Weiermann, A., Termination proofs for term rewriting systems by lexicographic path orderings imply multiply recursive derivation lengths, Theor. Comput. Sci., 139, 1-2, 355-362 (1995) · Zbl 0874.68156
[36] Winkler, S.; Middeldorp, A., Termination tools in ordered completion, (IJCAR. IJCAR, Lect. Notes Comput. Sci., vol. 6173 (2010)), 518-532 · Zbl 1291.68376
[37] Winkler, S.; Zankl, H.; Middeldorp, A., Ordinals and Knuth-Bendix orders, (LPAR. LPAR, Lect. Notes Comput. Sci., vol. 7180 (2012)), 420-434 · Zbl 1352.03018
[38] Winkler, S.; Zankl, H.; Middeldorp, A., Beyond Peano arithmetic—automatically proving termination of the Goodstein sequence, (RTA. RTA, Leibniz Int. Proc. Inform., vol. 21 (2013)), 335-351 · Zbl 1356.68206
[39] Zankl, H.; Middeldorp, A., Satisfiability of non-linear (ir)rational arithmetic, (LPAR. LPAR, Lect. Notes Comput. Sci., vol. 6355 (2010)), 481-500 · Zbl 1310.68126
[40] Zankl, H.; Winkler, S.; Middeldorp, A., Automating ordinal interpretations, (WST (2012)), 94-98
[41] Zantema, H., The termination hierarchy for term rewriting, Appl. Algebra Eng. Commun. Comput., 12, 1-2, 3-19 (2001) · Zbl 0973.68099
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.