×

Dependent choice as a termination principle. (English) Zbl 1481.03040

Summary: We introduce a new formulation of the axiom of dependent choice, which can be viewed as an abstract termination principle that in particular generalises recursive path orderings, the latter being fundamental tools used to establish termination of rewrite systems. We consider several variants of our termination principle, and relate them to general termination theorems in the literature.

MSC:

03D65 Higher-type and set recursion theory
03F35 Second- and higher-order arithmetic and fragments
03B30 Foundations of classical theories (including reverse mathematics)
68Q42 Grammars and rewriting systems
PDFBibTeX XMLCite
Full Text: DOI arXiv

References:

[1] Baader, F.; Nipkow, T., Term Rewriting and All That (1998), Cambridge: Cambridge University Press, Cambridge
[2] Berger, U.: A computational interpretation of open induction. In: Proceedings of LICS 2004, pp. 326-334. IEEE Computer Society (2004)
[3] Buchholz, W., Proof-theoretic analysis of termination proofs, Ann. Pure Appl. Logic, 75, 57-65 (1995) · Zbl 0844.03031 · doi:10.1016/0168-0072(94)00056-9
[4] Coquand, T., Constructive topology and combinatorics, Construct. Comput. Sci., LNCS, 613, 159-164 (1991) · Zbl 1434.03143 · doi:10.1007/BFb0021089
[5] Dershowitz, N., Orderings for term rewriting systems, Theoret. Comput. Sci., 17, 3, 279-301 (1982) · Zbl 0525.68054 · doi:10.1016/0304-3975(82)90026-3
[6] Dershowitz, N., Termination of rewriting, J. Symbolic Comput., 3, 69-116 (1987) · Zbl 0637.68035 · doi:10.1016/S0747-7171(87)80022-6
[7] Ferreira, M.C.F., Zantema, H.: Well-foundedness of term orderings. In: N. Dershowitz (Ed.) Conditional Term Rewriting Systems (CTRS ’94), LNCS, Vol. 968, pp. 106-123
[8] Goubault-Larrecq, J.: Well-founded recursive relations. In: Computer Science Logic (CSL’01), LNCS, Vol. 2142, pp. 484-498 (2001) · Zbl 0999.68094
[9] Knuth, D.E., Bendix, P.: Simple word problems in universal algebras. In: Automation of Reasoning. Symbolic Computation, pp. 236-297. Springer (1970) · Zbl 0188.04902
[10] Kohlenbach, U.: Higher order reverse mathematics. In: Reverse Mathematics 2001, Lecture Notes in Logic, Vol. 21, pp. 281-295. ASL (2005) · Zbl 1097.03053
[11] Melliès, PA, On a duality between Kruskal and Dershowitz theorem, Proc. ICALP, LNCS, 1443, 518-529 (1998) · Zbl 0921.04001
[12] Moser, G., Powell, T.: On the computational content of termination proofs. In: Proceedings of Computability in Europe (CiE 2015), LNCS, Vol. 9136, pp. 276-285 (2015) · Zbl 1459.68093
[13] Powell, T.: On bar recursive interpretations of analysis. Ph.D. thesis, Queen Mary University of London (2013)
[14] Powell, T., The equivalence of bar recursion and open recursion, Ann. Pure Appl. Logic, 165, 11, 1727-1754 (2014) · Zbl 1354.03058 · doi:10.1016/j.apal.2014.07.003
[15] Powell, T.: A proof theoretic study of abstract termination principles (2019). To appear in: Journal of Logic and Computation · Zbl 1480.03058
[16] Powell, T.: Well quasi-orders and the functional interpretation. In: Schuster, P., Seisenberger, M., Weiermann, A. (eds.) Well-Quasi Orders in Computation, Logic, Language and Reasoning. Trends in Logic, vol. 53. Springer, pp. 221-269 (2020) · Zbl 1496.03234
[17] Seisenberger, M.: On the constructive content of proofs. Ph.D. thesis, Ludwig Maximilians Universität München (2003)
[18] Sternagel, C.: A mechanized proof of Higman’s lemma by open induction. In: Schuster, P., Seisenberger, M., Weiermann, A. (eds.) Well-Quasi Orders in Computation, Logic, Language and Reasoning. Trends in Logic, vol. 53. Springer, pp. 339-350 (2020) · Zbl 1446.68188
[19] Troelstra, AS, Metamathematical Investigation of Intuitionistic Arithmetic and Analysis (1973), Berlin: Springer, Berlin · Zbl 0275.02025
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.