Abstract
Rewriting is the underlying evaluation mechanism of functional programming languages. Therefore, termination analysis of term rewrite systems (TRSs) is an important technique for program verification. To capture the evaluation mechanism of a programming language one has to take care of the evaluation strategy, where we focus on the outermost strategy.
As there are only few techniques available to analyze outermost termination of TRSs directly, we introduce a new transformation such that a TRS is outermost terminating iff the transformed TRS is innermost terminating. In this way all of the several techniques that have been developed to investigate innermost termination become applicable to analyze outermost termination, too. We have implemented the transformation and successfully evaluated it on a large collection of TRSs.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
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 University Press, Cambridge (1998)
Geser, A., Hofbauer, D., Waldmann, J., Zantema, H.: On tree automata that certify termination of left-linear term rewriting systems. Information and Computation 205(4), 512–534 (2007)
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., Middeldorp, A.: Transformation techniques for context-sensitive rewrite systems. Journal of Functional Programming 14(4), 379–427 (2004)
Giesl, J., Thiemann, R., Swiderski, S., Schneider-Kamp, P.: Proving termination by bounded increase. In: Pfenning, F. (ed.) CADE 2007. LNCS, vol. 4603, pp. 443–459. Springer, Heidelberg (2007)
Giesl, J., Thiemann, R., Schneider-Kamp, P.: The dependency pair framework: Combining techniques for automated termination proofs. In: Baader, F., Voronkov, A. (eds.) LPAR 2004. LNCS, vol. 3452, pp. 301–331. Springer, Heidelberg (2005)
Giesl, J., Thiemann, R., Schneider-Kamp, P.: Proving and disproving termination of higher-order functions. In: Gramlich, B. (ed.) FroCos 2005. LNCS, vol. 3717, pp. 216–231. Springer, Heidelberg (2005)
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, vol. 4130, pp. 281–286. Springer, Heidelberg (2006)
Giesl, J., Swiderski, S., Schneider-Kamp, P., Thiemann, R.: Automated Termination Analysis for Haskell: From Term Rewriting to Programming Languages. In: Pfenning, F. (ed.) RTA 2006. LNCS, vol. 4098, pp. 297–312. Springer, Heidelberg (2006)
Giesl, J., Thiemann, R., Schneider-Kamp, P., Falke, S.: Mechanizing and improving dependency pairs. Journal of Automated Reasoning 37(3), 155–203 (2006)
Gnaedig, I., Kirchner, H.: Termination of rewriting under strategies. ACM Transactions on Computational Logic (to appear, 2008), http://tocl.acm.org/accepted/315gnaedig.ps
Hirokawa, N., Middeldorp, A.: Tyrolean Termination Tool: Techniques and features. Information and Computation 205(4), 474–511 (2007)
Lucas, S.: Context-sensitive computations in functional and functional logic programs. Journal of Functional and Logic Programming 1, 1–61 (1998)
Ohlebusch, E.: Termination of logic programs: Transformational methods revisited. Appl. Algebra in Eng., Communication and Computing 12(1-2), 73–116 (2001)
Panitz, S.E., Schmidt-Schauss, M.: TEA: Automatically proving termination of programs in a non-strict higher-order functional language. In: Van Hentenryck, P. (ed.) SAS 1997. LNCS, vol. 1302, pp. 345–360. Springer, Heidelberg (1997)
Plasmeijer, R., van Eekelen, M.: Functional Programming and Parallel Graph Rewriting. Addison-Wesley, Reading (1993)
Raffelsieper, M., Zantema, H.: A transformational approach to prove outermost termination automatically. In: Informal Proc. WRS 2008, pp. 76–89, technical report RISC-Linz 08-09 (2008), http://www.risc.uni-linz.ac.at/publications/download/risc_3452/wrs2008.pdf
Thiemann, R., Giesl, J., Schneider-Kamp, P.: Deciding innermost loops. In: Voronkov, A. (ed.) RTA 2008. LNCS, vol. 5117, pp. 366–380. Springer, Heidelberg (2008)
Zantema, H.: Termination of term rewriting by semantic labelling. Fundamenta Informaticae 24, 89–105 (1995)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Thiemann, R. (2009). From Outermost Termination to Innermost Termination. In: Nielsen, M., Kučera, A., Miltersen, P.B., Palamidessi, C., Tůma, P., Valencia, F. (eds) SOFSEM 2009: Theory and Practice of Computer Science. SOFSEM 2009. Lecture Notes in Computer Science, vol 5404. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-95891-8_48
Download citation
DOI: https://doi.org/10.1007/978-3-540-95891-8_48
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-95890-1
Online ISBN: 978-3-540-95891-8
eBook Packages: Computer ScienceComputer Science (R0)