×

Local termination. (English) Zbl 1242.68130

Treinen, Ralf (ed.), Rewriting techniques and applications. 20th international conference, RTA 2009, Brasília, Brazil, June 29–July 1, 2009. Proceedings. Berlin: Springer (ISBN 978-3-642-02347-7/pbk). Lecture Notes in Computer Science 5595, 270-284 (2009).
Summary: The characterization of termination using well-founded monotone algebras has been a milestone on the way to automated termination techniques, of which we have seen an extensive development over the past years. Both the semantic characterization and most known termination methods are concerned with global termination, uniformly of all the terms of a term rewriting system (TRS). In this paper we consider local termination, of specific sets of terms within a given TRS.
The principal goal of this paper is generalizing the semantic characterization of global termination to local termination. This is made possible by admitting the well-founded monotone algebras to be partial. We show that our results can be applied in the development of techniques for proving local termination. We give several examples, among which a verifiable characterization of the terminating \(S\)-terms in CL.
For the entire collection see [Zbl 1165.68021].

MSC:

68Q42 Grammars and rewriting systems
03B35 Mechanization of proofs and logical operations

Software:

Coq; Haskell
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] The Coq Proof Assistant, http://coq.inria.fr/ · Zbl 1342.68280
[2] Arts, T., Giesl, J.: Termination of term rewriting using dependency pairs. Theoretical Computer Science 236, 133–178 (2000) · Zbl 0938.68051 · doi:10.1016/S0304-3975(99)00207-8
[3] Barendregt, H.P.: The Lambda Calculus, Its Syntax and Semantics. Studies in Logic and the Foundation of Mathematics, vol. 103. Elsevier, Amsterdam (1984) · Zbl 0551.03007
[4] Comon, H., Dauchet, M., Gilleron, R., Löding, C., Jacquemard, F., Lugiez, D., Tison, S., Tommasi, M.: Tree Automata Techniques and Applications (2007), http://www.grappa.univ-lille3.fr/tata
[5] Endrullis, J., Grabmayer, C., Hendriks, D., Klop, J.W., de Vrijer, R.C.: Proving Infinitary Normalization. In: Berardi, S., Damiani, F., de’Liguoro, U. (eds.) TYPES 2008. LNCS, vol. 5497, pp. 64–82. Springer, Heidelberg (2009) · Zbl 1246.68135 · doi:10.1007/978-3-642-02444-3_5
[6] Endrullis, J., Waldmann, J., Zantema, H.: Matrix interpretations for proving termination of term rewriting. Journal of Automated Reasoning (2008) · Zbl 1139.68049 · doi:10.1007/s10817-007-9087-9
[7] Geser, A., Hofbauer, D., Waldmann, J.: Match-bounded string rewriting systems. Appl. Algebra Eng., Commun. Comput. 15(3), 149–171 (2004) · Zbl 1101.68048 · doi:10.1007/s00200-004-0162-8
[8] Giesl, J., Swiderski, S., Thiemann, R., Schneider-Kamp, P.: 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) · Zbl 1151.68444 · doi:10.1007/11805618_23
[9] Hirokawa, N., Middeldorp, A.: Dependency pairs revisited. In: van Oostrom, V. (ed.) RTA 2004. LNCS, vol. 3091, pp. 249–268. Springer, Heidelberg (2004) · Zbl 1187.68275 · doi:10.1007/978-3-540-25979-4_18
[10] Koprowski, A.: Termination of Rewriting and Its Certification. PhD thesis, Eindhoven University of Technology (2008) · Zbl 1132.68431
[11] Lucas, S.: Context-Sensitive Computations in Functional and Functional Logic Programs. Journal of Functional and Logic Programming 1998(1) (1998) · Zbl 0924.68106
[12] Ohlebusch, E.: Advanced Topics in Term Rewriting. Springer, New York (2002) · Zbl 0999.68095 · doi:10.1007/978-1-4757-3661-8
[13] Panitz, S.E., Schmidt-Schauß, 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. Springer, Heidelberg (1997) · doi:10.1007/BFb0032752
[14] Raffelsieper, M., Zantema, H.: A transformational approach to prove outermost termination automatically. Technical report, RISC-Linz Report Series (2008) · Zbl 1294.68099
[15] Terese: Term Rewriting Systems. Cambridge Tracts in Theoretical Computer Science, vol. 55. Cambridge University Press, Cambridge (2003)
[16] Waldmann, J.: The combinator S. Information and Computation 159, 2–21 (2000) · Zbl 1005.03017 · doi:10.1006/inco.2000.2874
[17] Zantema, H.: Termination of term rewriting by semantic labelling. Fundamenta Informaticae 24, 89–105 (1995) · Zbl 0839.68050
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.