Abstract
A method based on dependency pairs for showing termination of functional programs on data structures generated by constructors with relations is proposed. A functional program is specified as an equational rewrite system, where the rewrite system specifies the program and the equations express the relations on the constructors that generate the data structures. Unlike previous approaches, relations on constructors can be collapsing, including idempotency and identity relations. Relations among constructors may be partitioned into two parts: (i) equations that cannot be oriented into terminating rewrite rules, and (ii) equations that can be oriented into terminating rewrite rules, in which case an equivalent convergent system for them is generated. The dependency pair method is extended to normalized rewriting, where constructor-terms in the redex are normalized first. The method has been applied to several examples, including the Calculus of Communicating Systems and the Propositional Sequent Calculus. Various refinements, such as dependency graphs, narrowing, etc., which increase the power of the dependency pair method, are presented for normalized rewriting.
Partially supported by NSF grant CCF-0541315.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Arts, T., Giesl, J.: Termination of term rewriting using dependency pairs. Theoretical Computer Science 236(1-2), 133–178 (2000)
Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998)
Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Talcott, C.: The Maude 2.0 system. In: Nieuwenhuis, R. (ed.) RTA 2003. LNCS, vol. 2706, pp. 76–87. Springer, Heidelberg (2003)
Falke, S.: Automated termination analysis for equational rewriting. Diplomarbeit, Department of Computer Science, RWTH Aachen University, Germany (2004)
Falke, S., Kapur, D.: Dependency pairs for rewriting with non-free constructors. Technical Report TR-CS-2007-07, Department of Computer Science, University of New Mexico (2007), Available at http://www.cs.unm.edu/research/
Giesl, J., Kapur, D.: Dependency pairs for equational rewriting. In: Middeldorp, A. (ed.) RTA 2001. LNCS, vol. 2051, pp. 93–108. Springer, Heidelberg (2001)
Giesl, J., Kapur, D. (ed.): Journal of Automated Reasoning, 34(2), 34(4) & 37(3), 2005-2006. Special issues on Techniques for Automated Termination Proofs
Giesl, J., Schneider-Kamp, P., Thiemann, R.: AProVE 1.2: Automatic termination proofs in the dependency pair framework. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol. 4130, pp. 281–286. Springer, Heidelberg (2006)
Giesl, J., Thiemann, R., Schneider-Kamp, P.: The dependency pair framework. In: Baader, F., Voronkov, A. (eds.) LPAR 2004. LNCS (LNAI), vol. 3452, pp. 301–331. Springer, Heidelberg (2005)
Giesl, J., Thiemann, R., Schneider-Kamp, P., Falke, S.: Mechanizing and improving dependency pairs. Journal of Automated Reasoning 37(3), 155–203 (2006)
Hirokawa, N., Middeldorp, A.: Tyrolean termination tool: Techniques and features. Information and Computation 205(4), 474–511 (2007)
Kapur, D., Sivakumar, G.: Proving associative-commutative termination using RPO-compatible orderings. In: Caferra, R., Salzer, G. (eds.) Automated Deduction in Classical and Non-Classical Logics. LNCS (LNAI), vol. 1761, pp. 40–62. Springer, Heidelberg (2000)
Kapur, D., Zhang, H.: An overview of rewrite rule laboratory (RRL). Computers & Mathematics with Applications 29(2), 91–114 (1995)
Kirchner, H., Moreau, P.-E.: Promoting rewriting to a programming language. Journal of Functional Programming 11(2), 207–251 (2001)
Kusakari, K., Nakamura, M., Toyama, Y.: Argument filtering transformation. In: Nadathur, G. (ed.) PPDP 1999. LNCS, vol. 1702, pp. 47–61. Springer, Heidelberg (1999)
Kusakari, K., Toyama, Y.: On proving AC-termination by AC-dependency pairs. IEICE Transactions on Information and Systems E84-D(5), 604–612 (2001)
Marché, C.: Normalized rewriting: An alternative to rewriting modulo a set of equations. Journal of Symbolic Computation 21(3), 253–288 (1996)
Marché, C., Urbain, X.: Modular and incremental proofs of AC-termination. Journal of Symbolic Computation 38(1), 873–897 (2004)
Peterson, G.E., Stickel, M.E.: Complete sets of reductions for some equational theories. Journal of the ACM 28(2), 233–264 (1981)
Rubio, A.: A fully syntactic AC-RPO. Information and Computation 178(2), 515–533 (2002)
Stein, C.: Das Dependency Pair Framework zur automatischen Terminierungsanalyse von Termersetzung modulo Gleichungen. Diplomarbeit, Department of Computer Science, RWTH Aachen University, Germany (in German) (2006)
Thiemann, R., Giesl, J., Schneider-Kamp, P.: Improved modular termination proofs using dependency pairs. In: Basin, D., Rusinowitch, M. (eds.) IJCAR 2004. LNCS (LNAI), vol. 3097, pp. 75–90. Springer, Heidelberg (2004)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Falke, S., Kapur, D. (2007). Dependency Pairs for Rewriting with Non-free Constructors. In: Pfenning, F. (eds) Automated Deduction – CADE-21. CADE 2007. Lecture Notes in Computer Science(), vol 4603. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-73595-3_32
Download citation
DOI: https://doi.org/10.1007/978-3-540-73595-3_32
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-73594-6
Online ISBN: 978-3-540-73595-3
eBook Packages: Computer ScienceComputer Science (R0)