×

Dependency pairs for proving termination properties of conditional term rewriting systems. (English) Zbl 1353.68155

Summary: The notion of operational termination provides a logic-based definition of termination of computational systems as the absence of infinite inferences in the computational logic describing the operational semantics of the system. For Conditional Term Rewriting Systems we show that operational termination is characterized as the conjunction of two termination properties. One of them is traditionally called termination and corresponds to the absence of infinite sequences of rewriting steps (a horizontal dimension). The other property, that we call V-termination, concerns the absence of infinitely many attempts to launch the subsidiary processes that are required to perform a single rewriting step (a vertical dimension). We introduce appropriate notions of dependency pairs to characterize termination, \(V\)-termination, and operational termination of Conditional Term Rewriting Systems. This can be used to obtain a powerful and more expressive framework for proving termination properties of Conditional Term Rewriting Systems.

MSC:

68Q42 Grammars and rewriting systems
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Arts, T.; Giesl, J., Termination of term rewriting using dependency pairs, Theor. Comput. Sci., 236, 1-2, 133-178 (2000) · Zbl 0938.68051
[2] Alarcón, B.; Gutiérrez, R.; Lucas, S., Context-sensitive dependency pairs, Inf. Comput., 208, 8, 922-968 (2010) · Zbl 1206.68158
[3] Alarcón, B.; Gutiérrez, R.; Lucas, S.; Navarro-Marset, R., Proving termination properties with MU-TERM, (Johnson, M.; Pavlovic, D., Proc. of the 13th International Conference on Algebraic Methodology and Software Technology. Proc. of the 13th International Conference on Algebraic Methodology and Software Technology, AMAST’10. Proc. of the 13th International Conference on Algebraic Methodology and Software Technology. Proc. of the 13th International Conference on Algebraic Methodology and Software Technology, AMAST’10, Lect. Notes Comput. Sci., vol. 6486 (2011)), 201-208 · Zbl 1308.68068
[4] Alarcón, B.; Lucas, S.; Meseguer, J., A dependency pair framework for \(A \vee C\)-termination, (Ölveczky, P. C., Proc. of the 8th International Workshop on Rewriting Logic and its Applications. Proc. of the 8th International Workshop on Rewriting Logic and its Applications, WRLA’10. Proc. of the 8th International Workshop on Rewriting Logic and its Applications. Proc. of the 8th International Workshop on Rewriting Logic and its Applications, WRLA’10, Lect. Notes Comput. Sci., vol. 6381 (2010)), 35-51 · Zbl 1306.68060
[5] Baader, F.; Nipkow, T., Term Rewriting and All That (1998), Cambridge University Press
[6] Bergstra, J. A.; Klop, J. W., Conditional rewrite rules: confluence and termination, J. Comput. Syst. Sci., 32, 323-362 (1986) · Zbl 0658.68031
[7] Borovanský, P.; Kirchner, C.; Kirchner, H.; Moreau, P.-E.; Ringeissen, C., An overview of ELAN, (Kirchner, C.; Kirchner, H., Proc. of the 2nd International Workshop on Rewriting Logic and its Applications. Proc. of the 2nd International Workshop on Rewriting Logic and its Applications, WRLA’98. Proc. of the 2nd International Workshop on Rewriting Logic and its Applications. Proc. of the 2nd International Workshop on Rewriting Logic and its Applications, WRLA’98, Electron. Notes Theor. Comput. Sci., vol. 15 (1998)), 1-16
[8] van den Brand, M. G.J.; Heering, J.; Klint, P.; Olivier, P. A., Compiling language definitions: the ASF+SDF compiler, ACM Trans. Program. Lang. Syst., 24, 4, 334-368 (2002)
[9] Clavel, M.; Durán, F.; Eker, S.; Lincoln, P.; Martí-Oliet, N.; Meseguer, J.; Talcott, C., All About Maude - A High-Performance Logical Framework, Lect. Notes Comput. Sci., vol. 4350 (2007), Springer-Verlag · Zbl 1115.68046
[10] Dershowitz, N., Termination by abstraction, (Demoen, B.; Lifschitz, V., Proc. of the 20th International Conference on Logic Programming. Proc. of the 20th International Conference on Logic Programming, ICLP’04. Proc. of the 20th International Conference on Logic Programming. Proc. of the 20th International Conference on Logic Programming, ICLP’04, Lect. Notes Comput. Sci., vol. 3132 (2004)), 1-18 · Zbl 1104.68373
[11] Dershowitz, N.; Okada, M., A rationale for conditional equational programming, Theor. Comput. Sci., 75, 111-138 (1990) · Zbl 0702.68034
[12] Durán, F.; Lucas, S.; Meseguer, J., MTT: the Maude Termination Tool (system description), (Armando, A.; Baumgartner, P.; Dowek, G., Proc. of the 4th International Joint Conference on Automated Reasoning. Proc. of the 4th International Joint Conference on Automated Reasoning, IJCAR’08. Proc. of the 4th International Joint Conference on Automated Reasoning. Proc. of the 4th International Joint Conference on Automated Reasoning, IJCAR’08, LNAI, vol. 5195 (2008)), 313-319 · Zbl 1165.68360
[13] Durán, F.; Lucas, S.; Meseguer, J.; Marché, C.; Urbain, X., Proving termination of membership equational programs, (Sestoft, P.; Heintze, N., Proc. of the ACM SIGPLAN 2004 Symposium on Partial Evaluation and Program Manipulation. Proc. of the ACM SIGPLAN 2004 Symposium on Partial Evaluation and Program Manipulation, PEPM’04 (2004)), 147-158
[14] Durán, F.; Lucas, S.; Marché, C.; Meseguer, J.; Urbain, X., Proving operational termination of membership equational programs, High.-Order Symb. Comput., 21, 1-2, 59-88 (2008) · Zbl 1192.68154
[15] Futatsugi, K.; Diaconescu, R., CafeOBJ Report, AMAST Ser. Comput., vol. 6 (1998), World Scientific · Zbl 0962.68115
[16] Giesl, J.; Thiemann, R.; Schneider-Kamp, P., The dependency pair framework: combining techniques for automated termination proofs, (Baader, F.; Voronkov, A., Proc. of the 11th International Conference on Logic for Programming Artificial Intelligence and Reasoning. Proc. of the 11th International Conference on Logic for Programming Artificial Intelligence and Reasoning, LPAR’04. Proc. of the 11th International Conference on Logic for Programming Artificial Intelligence and Reasoning. Proc. of the 11th International Conference on Logic for Programming Artificial Intelligence and Reasoning, LPAR’04, LNAI, vol. 3452 (2004)), 301-331 · Zbl 1108.68477
[17] 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
[18] Giesl, J.; Schneider-Kamp, P.; Thiemann, R., AProVE 1.2: automatic termination proofs in the dependency pair framework, (Furbach, U.; Shankar, N., Proc. of the 3rd International Joint Conference on Automated Reasoning. Proc. of the 3rd International Joint Conference on Automated Reasoning, IJCAR’06. Proc. of the 3rd International Joint Conference on Automated Reasoning. Proc. of the 3rd International Joint Conference on Automated Reasoning, IJCAR’06, LNAI, vol. 4130 (2006)), 281-286
[19] Goguen, J. A.; Winkler, T.; Meseguer, J.; Futatsugi, K.; Jouannaud, J.-P., Introducing OBJ, (Goguen, J.; Malcolm, G., Software Engineering with OBJ: Algebraic Specification in Action (2000), Kluwer)
[20] Gutiérrez, R.; Lucas, S., Proving termination in the context-sensitive depedency pairs framework, (Ölveczky, P. C., Proc. of the 8th International Workshop on Rewriting Logic and its Applications. Proc. of the 8th International Workshop on Rewriting Logic and its Applications, WRLA’10. Proc. of the 8th International Workshop on Rewriting Logic and its Applications. Proc. of the 8th International Workshop on Rewriting Logic and its Applications, WRLA’10, Lect. Notes Comput. Sci., vol. 6381 (2010)), 19-35
[21] Hirokawa, N.; Middeldorp, A., Dependency pairs revisited, (van Oostrom, V., Proc. of the 15th International Conference on Rewriting Techniques and Applications. Proc. of the 15th International Conference on Rewriting Techniques and Applications, RTA’04. Proc. of the 15th International Conference on Rewriting Techniques and Applications. Proc. of the 15th International Conference on Rewriting Techniques and Applications, RTA’04, Lect. Notes Comput. Sci., vol. 3091 (2004)), 249-268 · Zbl 1187.68275
[22] Hirokawa, N.; Middeldorp, A., Tyrolean termination tool: techniques and features, Inf. Comput., 205, 474-511 (2007) · Zbl 1111.68048
[23] Hudak, P.; Peyton-Jones, S. J.; Wadler, P., Report on the functional programming language Haskell: a non-strict, purely functional language, SIGPLAN Not., 27, 5, 1-164 (1992)
[24] Kaplan, S., Conditional rewrite rules, Theor. Comput. Sci., 33, 175-193 (1984) · Zbl 0577.03013
[25] Lucas, S., Context-sensitive computations in functional and functional logic programs, J. Funct. Logic Program., 1998, 1, 1-61 (1998) · Zbl 0924.68106
[26] Lucas, S.; Marché, C.; Meseguer, J., Operational termination of conditional term rewriting systems, Inf. Process. Lett., 95, 446-453 (2005) · Zbl 1185.68374
[27] Lucas, S.; Meseguer, J., Order-sorted dependency pairs, (Antoy, S., Proc. of the 10th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming. Proc. of the 10th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming, PPDP’08 (2008)), 108-119
[28] Lucas, S.; Meseguer, J., 2D dependency pairs for proving operational termination of CTRSs, (Escobar, S., Proc. of the 10th International Workshop on Rewriting Logic and its Applications. Proc. of the 10th International Workshop on Rewriting Logic and its Applications, WRLA’14. Proc. of the 10th International Workshop on Rewriting Logic and its Applications. Proc. of the 10th International Workshop on Rewriting Logic and its Applications, WRLA’14, Lect. Notes Comput. Sci., vol. 8663 (2014)), 195-212 · Zbl 1367.68145
[29] Lucas, S.; Meseguer, J., Normal forms and normal theories in conditional rewriting, J. Log. Algebr. Methods Program., 85, 67-97 (2016) · Zbl 1356.68124
[30] Lucas, S.; Meseguer, J.; Gutiérrez, R., Extending the 2D DP framework for CTRSs, (Proietti, M.; Seki, H., Selected Papers of the 24th International Symposium on Logic-Based Program Synthesis and Transformation LOPSTR’14. Selected Papers of the 24th International Symposium on Logic-Based Program Synthesis and Transformation LOPSTR’14, Lect. Notes Comput. Sci., vol. 8981 (2015)), 113-130
[31] Marchiori, M., Unravelings and ultra-properties, (Hanus, M.; Rodríguez-Artalejo, M., Proc. of the 5th International Conference on Algebraic and Logic Programming. Proc. of the 5th International Conference on Algebraic and Logic Programming, ALP’96. Proc. of the 5th International Conference on Algebraic and Logic Programming. Proc. of the 5th International Conference on Algebraic and Logic Programming, ALP’96, Lect. Notes Comput. Sci., vol. 1039 (1996)), 107-121 · Zbl 1355.68142
[32] Meseguer, J., General logics, (Ebbinghaus, H.-D.; etal., Logic Colloquium’87 (1989), North-Holland), 275-329
[33] Meseguer, J., Membership algebra as a logical framework for equational specification, (Parisi-Presicce, F., Proc. of the 12th International Workshop on Recent Trends in Algebraic Development Techniques. Proc. of the 12th International Workshop on Recent Trends in Algebraic Development Techniques, WADT’97. Proc. of the 12th International Workshop on Recent Trends in Algebraic Development Techniques. Proc. of the 12th International Workshop on Recent Trends in Algebraic Development Techniques, WADT’97, Lect. Notes Comput. Sci., vol. 1376 (1998)), 18-61 · Zbl 0903.08009
[34] Nakamura, M.; Ogata, K.; Futatsugi, K., On proving operational termination incrementally with modular conditional dependency pairs, Int. J. Comput. Sci., 40, 2 (2013)
[35] Nishida, N.; Sakai, M.; Sakabe, T., Soundness of unravelings for conditional term rewriting systems via ultra-properties related to linearity, Log. Methods Comput. Sci., 8, 3, 1-49 (2012) · Zbl 1252.68161
[36] Ohlebusch, E., Advanced Topics in Term Rewriting (2002), Springer-Verlag · Zbl 0999.68095
[37] Schernhammer, F.; Gramlich, B., Characterizing and proving operational termination of deterministic conditional term rewriting systems, J. Log. Algebraic Program., 79, 659-688 (2010) · Zbl 1206.68163
[38] Schernhammer, F.; Gramlich, B., VMTL - a modular termination laboratory, (Treinen, R., Proc. of the 20th International Conference on Rewriting Techniques and Applications. Proc. of the 20th International Conference on Rewriting Techniques and Applications, RTA’09. Proc. of the 20th International Conference on Rewriting Techniques and Applications. Proc. of the 20th International Conference on Rewriting Techniques and Applications, RTA’09, Lect. Notes Comput. Sci., vol. 5595 (2009)), 285-294
[39] Serbanuta, T.; Rosu, G., Computationally equivalent elimination of conditions, (Pfenning, F., Proc. of the 17th International Conference on Rewriting Techniques and Applications. Proc. of the 17th International Conference on Rewriting Techniques and Applications, RTA’06. Proc. of the 17th International Conference on Rewriting Techniques and Applications. Proc. of the 17th International Conference on Rewriting Techniques and Applications, RTA’06, Lect. Notes Comput. Sci., vol. 4098 (2006)), 19-34 · Zbl 1151.68438
[40] Sternagel, C.; Thiemann, R., Signature extensions preserve termination. An alternative proof via dependency pairs, (Dawar, A.; Veith, H., Proc. of Computer Science Logic, 24th International Workshop, CSL 2010, 19th Annual Conference of the EACSL. Proc. of Computer Science Logic, 24th International Workshop, CSL 2010, 19th Annual Conference of the EACSL, Lect. Notes Comput. Sci., vol. 6247 (2010)), 514-528 · Zbl 1287.03032
[41] (TeReSe, Term Rewriting Systems (2003), Cambridge University Press) · Zbl 1030.68053
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.