×

Relative termination via dependency pairs. (English) Zbl 1410.68190

Summary: A term rewrite system is terminating when no infinite reduction sequences are possible. Relative termination generalizes termination by permitting infinite reductions as long as some distinguished rules are not applied infinitely many times. Relative termination is thus a fundamental notion that has been used in a number of different contexts, like analyzing the confluence of rewrite systems or the termination of narrowing. In this work, we introduce a novel technique to prove relative termination by reducing it to dependency pair problems. To the best of our knowledge, this is the first significant contribution to Problem #106 of the RTA List of Open Problems. We first present a general approach that is then instantiated to provide a concrete technique for proving relative termination. The practical significance of our method is illustrated by means of an experimental evaluation.

MSC:

68Q42 Grammars and rewriting systems
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Alarcón, B., Lucas, S., Meseguer, J.: A dependency pair framework for A \[\vee ∨C\]-termination. In: WRLA 2010, LNCS, vol. 6381, pp. 36-52. Springer (2010) · Zbl 1270.68135
[2] Arts, T., Giesl, J.: Termination of term rewriting using dependency pairs. Theor. Comput. Sci. 236(1-2), 133-178 (2000) · Zbl 0938.68051 · doi:10.1016/S0304-3975(99)00207-8
[3] Arts, T., Giesl, J.: A collection of examples for termination of term rewriting using dependency pairs. Technical report AIB-2001-09, RWTH Aachen (2001) · Zbl 0938.68051
[4] Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998) · Zbl 0948.68098 · doi:10.1017/CBO9781139172752
[5] Bachmair, L., Dershowitz, N.: Critical pair criteria for completion. J. Symb. Comput. 6, 1-18 (1988) · Zbl 0651.68030 · doi:10.1016/S0747-7171(88)80018-X
[6] Bonacina, M., Hsiang, J.: On fairness of completion-based theorem proving strategies. In: RTA 1991, LNCS, vol. 488, pp. 348-360. Springer (1991) · Zbl 1503.03016
[7] Dershowitz, N.: Termination of rewriting. J. Symb. Comput. 3(1&2), 69-115 (1987) · Zbl 0637.68035 · doi:10.1016/S0747-7171(87)80022-6
[8] 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 · doi:10.1007/s10817-007-9087-9
[9] Geser, A.: Relative Termination. Dissertation, Fakultät für Mathematik und Informatik. Universität Passau, Germany (1990)
[10] Giesl, J., Kapur, D.: Dependency pairs for equational rewriting. In: RTA 2001, LNCS, vol. 2051, pp. 93-107. Springer (2001) · Zbl 0981.68063
[11] Giesl, J., Schneider-Kamp, P., Thiemann, R.: AProVE 1.2: automatic termination proofs in the dependency pair framework. In: IJCAR 2006, LNCS, vol. 4130, pp. 281-286. Springer (2006)
[12] Giesl, J., Thiemann, R., Schneider-Kamp, P., Falke, S.: Mechanizing and improving dependency Pairs. J. Autom. Reason. 37(3), 155-203 (2006) · Zbl 1113.68088 · doi:10.1007/s10817-006-9057-7
[13] Hirokawa, N., Middeldorp, A.: Dependency pairs revisited. In: RTA 2004, LNCS, vol. 3091, pp. 249-268. Springer (2004) · Zbl 1187.68275
[14] Hirokawa, N., Middeldorp, A.: Polynomial interpretations with negative coefficients. In: AISC 2004, LNAI, vol. 3249, pp. 185-198. Springer (2004) · Zbl 1109.68501
[15] Hirokawa, N., Middeldorp, A.: Tyrolean termination tool: techniques and features. Inf. Comput. 205(4), 474-511 (2007) · Zbl 1111.68048 · doi:10.1016/j.ic.2006.08.010
[16] Hirokawa, N., Middeldorp, A.: Decreasing diagrams and relative termination. J. Autom. Reason. 47(4), 481-501 (2011) · Zbl 1243.68199 · doi:10.1007/s10817-011-9238-x
[17] Hullot, J.M.: Canonical forms and unification. In: CADE 1980, LNCS, vol. 87, pp. 318-334. Springer (1980) · Zbl 0441.68108
[18] Iborra, J., Nishida, N., Vidal, G.: Goal-directed and relative dependency pairs for proving the termination of narrowing. In: LOPSTR 2009, LNCS, vol. 6037, pp. 52-66. Springer (2010) · Zbl 1284.68186
[19] Iborra, J., Nishida, N., Vidal, G., Yamada, A.: Reducing relative termination to dependency pair problems. In: CADE-25, LNAI, vol. 9195, pp. 163-178. Springer (2015) · Zbl 1465.68120
[20] Kamin, S., Lévy, J.J.: Two generalizations of the recursive path ordering (1980). Unpublished note · Zbl 1139.68049
[21] Klop, J.W.: Term rewriting systems: a tutorial. Bull. Eur. Assoc. Theor. Comput. Sci. 32, 143-183 (1987) · Zbl 0666.68025
[22] Koprowski, A.: TPA: termination proved automatically. In: RTA 2006, LNCS, vol. 4098, pp. 257-266. Springer (2006) · Zbl 1151.68635
[23] Koprowski, A., Zantema, H.: Proving liveness with fairness using rewriting. In: FroCoS 2005, LNCS, vol. 3717, pp. 232-247. Springer (2005) · Zbl 1171.68513
[24] Korp, M., Sternagel, C., Zankl, H., Middeldorp, A.: Tyrolean termination tool 2. In: RTA 2009, LNCS, vol. 5595, pp. 295-304. Springer (2009) · Zbl 0839.68050
[25] Kusakari, K., Toyama, Y.: On proving AC-termination by AC-dependency pairs. IEICE Trans. Inf. Syst. E84-D(5), 439-447 (2001)
[26] Lankford, D.: Canonical algebraic simplification in computational logic. Technical report ATP-25, University of Texas (1975)
[27] Marché, C., Urbain, X.: Modular and incremental proofs of AC-termination. J. Symb. Comput. 38(1), 873-897 (2004) · Zbl 1137.68419 · doi:10.1016/j.jsc.2004.02.003
[28] Nishida, N., Sakai, M., Sakabe, T.: Narrowing-based simulation of term rewriting systems with extra variables. ENTCS 86(3), 52-69 (2003) · Zbl 1270.68135
[29] Nishida, N., Vidal, G.: Termination of narrowing via termination of rewriting. Appl. Algebra Eng. Commun. Comput. 21(3), 177-225 (2010) · Zbl 1197.68049 · doi:10.1007/s00200-010-0122-4
[30] Ohlebusch, E.: Advanced Topics in Term Rewriting. Springer, London (2002) · Zbl 0999.68095 · doi:10.1007/978-1-4757-3661-8
[31] Slagle, J.: Automated theorem-proving for theories with simplifiers commutativity and associativity. J. ACM 21(4), 622-642 (1974) · Zbl 0296.68092 · doi:10.1145/321850.321859
[32] Thiemann, R., Allais, G., Nagele, J.: On the formalization of termination techniques based on multiset orderings. In: RTA 2012, LIPIcs, vol. 15, pp. 339-354. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2012) · Zbl 1437.68088
[33] Vidal, G.: Termination of narrowing in left-linear constructor systems. In: FLOPS 2008, LNCS, vol. 4989, pp. 113-129. Springer (2008) · Zbl 1137.68420
[34] Yamada, A., Kusakari, K., Sakabe, T.: Nagoya termination tool. In: RTA-TLCA 2014, LNCS, pp. 466-475. Springer (2014) · Zbl 1416.68183
[35] Yamada, A., Kusakari, K., Sakabe, T.: A unified ordering for termination proving. Sci. Comput. Program. 111, 110-134 (2015) · doi:10.1016/j.scico.2014.07.009
[36] Zantema, H.: Termination of term rewriting by semantic labelling. Fundam. Inf. 24(1/2), 89-105 (1995) · Zbl 0839.68050
[37] Zantema, H.: Termination. In: Bezem, M., Klop, J. W., de Vrijer, R. (eds.) Term Rewriting Systems, Cambridge Tracts in Theoretical Computer Science, chap. 6, vol. 55, pp. 181-259. Cambridge University Press, Cambridge (2003)
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.