Abstract
The dependency pair technique is a powerful modular method for automated termination proofs of term rewrite systems (TRSs). We present two important extensions of this technique: First, we show how to prove termination of higher-order functions using dependency pairs. To this end, the dependency pair technique is extended to handle (untyped) applicative TRSs. Second, we introduce a method to prove non-termination with dependency pairs, while up to now dependency pairs were only used to verify termination. Our results lead to a framework for combining termination and non-termination techniques for first- and higher-order functions in a very flexible way. We implemented and evaluated our results in the automated termination prover AProVE.
Supported by the Deutsche Forschungsgemeinschaft DFG under grant GI 274/5-1.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Aoto, T., Yamada, T.: Termination of simply typed term rewriting systems by translation and labelling. In: Nieuwenhuis, R. (ed.) RTA 2003. LNCS, vol. 2706, pp. 380–394. Springer, Heidelberg (2003)
Aoto, T., Yamada, T.: Termination of simply typed applicative term rewriting systems. In: Proc. HOR 2004, Report AIB-2004-03, RWTH, pp. 61–65 (2004)
Aoto, T., Yamada, T.: Dependency pairs for simply typed term rewriting. In: Giesl, J. (ed.) RTA 2005. LNCS, vol. 3467, pp. 120–134. Springer, Heidelberg (2005)
Arts, T., Giesl, J.: Termination of term rewriting using dependency pairs. Theoretical Computer Science 236, 133–178 (2000)
Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge (1998)
Bird, R.: Introduction to Functional Prog. using Haskell. Prentice-Hall, Englewood Cliffs (1998)
Blanqui, F.: A type-based termination criterion for dependently-typed higher-order rewrite systems. In: van Oostrom, V. (ed.) RTA 2004. LNCS, vol. 3091, pp. 24–39. Springer, Heidelberg (2004)
Borralleras, C., Rubio, A.: A monotonic higher-order semantic path ordering. In: Nieuwenhuis, R., Voronkov, A. (eds.) LPAR 2001. LNCS (LNAI), vol. 2250, pp. 531–547. Springer, Heidelberg (2001)
Contejean, E., Marché, C., Monate, B., Urbain, X.: CiME, http://cime.lri.fr
Dershowitz, N.: Termination of rewriting. J. Symb. Comp. 3, 69–116 (1987)
Drosten, K.: Termersetzungssysteme: Grundlagen der Prototyp-Generierung algebraischer Spezifikationen. Springer, Heidelberg (1989)
Giesl, J., Arts, T.: Verification of Erlang processes by dependency pairs. Appl. Algebra in Engineering, Communication and Computing 12(1,2), 39–72 (2001)
Giesl, J., Arts, T., Ohlebusch, E.: Modular termination proofs for rewriting using dependency pairs. Journal of Symbolic Computation 34(1), 21–58 (2002)
Giesl, J., Thiemann, R., Schneider-Kamp, P., Falke, S.: Improving dependency pairs. In: Y. Vardi, M., Voronkov, A. (eds.) LPAR 2003. LNCS (LNAI), vol. 2850, pp. 165–179. Springer, Heidelberg (2003)
Giesl, J., Thiemann, R., Schneider-Kamp, P., Falke, S.: Automated termination proofs with AProVE. In: van Oostrom, V. (ed.) RTA 2004. LNCS, vol. 3091, pp. 210–220. Springer, Heidelberg (2004)
Giesl, J., Thiemann, R., Schneider-Kamp, P.: The DP framework: Combining techniques for autom. termination proofs. 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.: Proving and disproving termination of higher-order functions. Technical Report AIB-2005-03, RWTH Aachen (2005), Available from http://aib.informatik.rwth-aachen.de
Hirokawa, N., Middeldorp, A.: Automating the DP method. In: Baader, F. (ed.) CADE 2003. LNCS (LNAI), vol. 2741, pp. 32–46. Springer, Heidelberg (2003)
Hirokawa, N., Middeldorp, A.: Tyrolean Termination Tool. In: Giesl, J. (ed.) RTA 2005. LNCS, vol. 3467, pp. 175–184. Springer, Heidelberg (2005)
Jouannaud, J.-P., Rubio, A.: Higher-order recursive path orderings. In: Proc. LICS 1999, pp. 402–411 (1999)
Kapur, D., Musser, D., Narendran, P., Stillman, J.: Semi-unification. Theoretical Computer Science 81(2), 169–187 (1991)
Kennaway, R., Klop, J.W., Sleep, R., de Vries, F.-J.: Comparing curried and uncurried rewriting. Journal of Symbolic Computation 21(1), 15–39 (1996)
Kusakari, K., Nakamura, M., Toyama, Y.: Argument filtering transformation. In: Nadathur, G. (ed.) PPDP 1999. LNCS, vol. 1702, pp. 48–62. Springer, Heidelberg (1999)
Kusakari, K.: On proving termination of term rewriting systems with higher-order variables. IPSJ Transactions on Programming,42(SIG 7 (PRO 11)), 35–45 (2001)
Lifantsev, M., Bachmair, L.: An LPO-based termination ordering for higher-order terms without λ-abstraction. In: Grundy, J., Newey, M. (eds.) TPHOLs 1998. LNCS, vol. 1479, pp. 277–293. Springer, Heidelberg (1998)
Mycroft, A.: The theory and practice of transforming call-by-need into call-by-value. In: Robinet, B. (ed.) Programming 1980. LNCS, vol. 83, pp. 269–281. Springer, Heidelberg (1980)
Oliart, A., Snyder, W.: A fast algorithm for uniform semi-unification. In: Kirchner, C., Kirchner, H. (eds.) CADE 1998. LNCS, vol. 1421, pp. 239–253. Springer, Heidelberg (1998)
Plaisted, D.A.: A simple non-termination test for the Knuth-Bendix method. In: Siekmann, J.H. (ed.) CADE 1986. LNCS, vol. 230, pp. 79–88. Springer, Heidelberg (1986)
van de Pol. J.: Termination of higher-order rewrite systems. PhD, Utrecht (1996)
Sakai, M., Watanabe, Y., Sakabe, T.: An extension of dependency pair method for proving termination of higher-order rewrite systems. IEICE Transactions on Information and Systems E84-D(8), 1025–1032 (2001)
Sakai, M., Kusakari, K.: On dependency pair method for proving termination of higher-order rewrite systems. IEICE Trans. on Inf. & Sys. (2005) (To appear)
Thiemann, R., Giesl, J., Schneider-Kamp, P.: Improved modular termination proofs using dependency pairs. In: Basin, D., Rusinowitch, M. (eds.) IJCAR 2004. LNCS, vol. 3097, pp. 75–90. Springer, Heidelberg (2004)
Toyama, Y.: Termination of S-expression rewriting systems: Lexicographic path ordering for higher-order terms. In: van Oostrom, V. (ed.) RTA 2004. LNCS, vol. 3091, pp. 40–54. Springer, Heidelberg (2004)
TPDB. web page, http://www.lri.fr/~marche/termination-competition/
Wadler, P., Hughes, J.: Projections for strictness analysis. In: Kahn, G. (ed.) FPCA 1987. LNCS, vol. 274, pp. 385–407. Springer, Heidelberg (1987)
Waldmann, J.: Matchbox: A tool for match-bounded string rewriting. In: van Oostrom, V. (ed.) RTA 2004. LNCS, vol. 3091, pp. 85–94. Springer, Heidelberg (2004)
Zantema, H.: TORPA: Termination of string rewriting proved automatically. Journal of Automated Reasoning (2005) (To appear)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Giesl, J., Thiemann, R., Schneider-Kamp, P. (2005). Proving and Disproving Termination of Higher-Order Functions. In: Gramlich, B. (eds) Frontiers of Combining Systems. FroCoS 2005. Lecture Notes in Computer Science(), vol 3717. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11559306_12
Download citation
DOI: https://doi.org/10.1007/11559306_12
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-29051-3
Online ISBN: 978-3-540-31730-2
eBook Packages: Computer ScienceComputer Science (R0)