×

Using context-sensitive rewriting for proving innermost termination of rewriting. (English) Zbl 1337.68147

Almendros-Jiménez, Jesús M (ed.), Proceedings of the 8th Spanish conference on programming and computer languages (PROLE 2008), Gijón, Spain, October 8–10, 2008. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 248, 3-17 (2009).
Summary: Computational systems based on reducing expressions usually have a predefined reduction strategy to break down the nondeterminism which is inherent to reduction relations. The innermost strategy corresponds to call by value or eager computation, that is, the computational mechanism of several programming languages like Maude, OBJ, etc. where the arguments of a function call are always evaluated before calling the function. This strategy usually fails to terminate when nonterminating computations are possible in the programs and many eager programming languages also admit the explicit specification of a particular class of strategy annotations to (try to) avoid them. Context-sensitive rewriting provides an abstract model to describe and analyze the operational behavior of such programs. This paper aims at contributing to the development of appropriate techniques and tools for the verification of program termination in the aforementioned programming languages, so we focus on termination of innermost (context-sensitive) rewriting. We adapt the notion of usable argument introduced by Fernández to prove innermost termination by proving termination of context-sensitive rewriting. Thanks to our recent developments for proving termination of (innermost) context-sensitive rewriting using dependency pairs, now we can also relax monotonicity requirements for proving innermost termination of (context-sensitive) rewriting. We have implemented these new improvements in the termination tool mu-term and evaluated the results with some benchmarks.
For the entire collection see [Zbl 1281.68014].

MSC:

68Q42 Grammars and rewriting systems
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)

Software:

OBJ3; Maude; MU-TERM
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Alarcón, B.; Gutiérrez, R.; Iborra, J.; Lucas, S., Proving Termination of Context-Sensitive Rewriting with MU-TERM, Electronic Notes in Theoretical Computer Science, 188, 105-115 (2007) · Zbl 1278.68113
[2] Alarcón, B.; Gutiérrez, R.; Lucas, S., Context-Sensitive Dependency Pairs, (Arun-Kumar, S.; Garg, N., Proc. of the 26th Conference on Foundations of Software Technology and Theoretical Computer Science. Proc. of the 26th Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS’06. Proc. of the 26th Conference on Foundations of Software Technology and Theoretical Computer Science. Proc. of the 26th Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS’06, LNCS, 4337 (2006), Springer-Verlag: Springer-Verlag Berlin), 297-308 · Zbl 1177.68133
[3] Alarcón, B.; Gutiérrez, R.; Lucas, S., Improving the Context-Sensitive Dependency Graph, Electronic Notes in Theoretical Computer Science, 188, 91-103 (2007) · Zbl 1278.68114
[4] B. Alarcón, R. Gutiérrez, and S. Lucas. Context-Sensitive Dependency Pairs. Technical Report DSIC II/10/08 (72 pages); B. Alarcón, R. Gutiérrez, and S. Lucas. Context-Sensitive Dependency Pairs. Technical Report DSIC II/10/08 (72 pages) · Zbl 1177.68133
[5] Alarcón, B.; Lucas, S., Termination of Innermost Context-Sensitive Rewriting Using Dependency Pairs, (Konev, B.; Wolter, F., Proc. of 6th International Symposium on Frontiers of Combining Systems. Proc. of 6th International Symposium on Frontiers of Combining Systems, FroCoS’07. Proc. of 6th International Symposium on Frontiers of Combining Systems. Proc. of 6th International Symposium on Frontiers of Combining Systems, FroCoS’07, LNAI, 4720 (2007), Springer-Verlag: Springer-Verlag Berlin), 73-87 · Zbl 1148.68463
[6] Arts, T.; Giesl, J., Termination of Term Rewriting Using Dependency Pairs, Theoretical Computer Science, 236, 133-178 (2000) · Zbl 0938.68051
[7] Clavel, M.; Durán, F.; Eker, S.; Lincoln, P.; Martí-Oliet, N.; Meseguer, J.; Talcott, C., All About Maude - A High-Performance Logical Framework, LNCS, 4350 (2007) · Zbl 1115.68046
[8] Durán, F.; Lucas, S.; Meseguer, J.; Marché, C.; Urbain, X., Proving Operational Termination of Membership Equational Programs, Higher-Order and Symbolic Computation, 21, 1-2, 59-88 (2008) · Zbl 1192.68154
[9] Fernández, M. L., Relaxing monotonicity for innermost termination, Information Processing Letters, 93, 3, 117-123 (2005) · Zbl 1173.68543
[10] Fernández, M. L.; Godoy, G.; Rubio, A., Orderings Innermost Termination, (Giesl, J., Proc. 16th Int. Conf. on Rewriting Techniques and Applications Proc. of RTA’05. Proc. 16th Int. Conf. on Rewriting Techniques and Applications Proc. of RTA’05, LNCS, 3467 (2005), Springer-Verlag: Springer-Verlag Berlin), 17-31 · Zbl 1078.68060
[11] Futatsugi, K.; Goguen, J.; Jouannaud, J.-P.; Meseguer, J., Principles of OBJ2, (Conference Record of the 12th Annual ACM Symposium on Principles of Programming Languages. Conference Record of the 12th Annual ACM Symposium on Principles of Programming Languages, POPL’85 (1985), ACM Press), 52-66
[12] Futatsugi, K., and A. Nakagawa. An Overview of CAFEProc. of 1st International Conference on Formal Engineering Methods; Futatsugi, K., and A. Nakagawa. An Overview of CAFEProc. of 1st International Conference on Formal Engineering Methods
[13] Giesl, J.; Middeldorp, A., Innermost termination of context-sensitive rewriting, (Ito, M.; Toyama, M., Proc. of 6th International Conference on Developments in Language Theory. Proc. of 6th International Conference on Developments in Language Theory, DLT’02. Proc. of 6th International Conference on Developments in Language Theory. Proc. of 6th International Conference on Developments in Language Theory, DLT’02, LNCS, 2450 (2003), Springer-Verlag: Springer-Verlag Berlin), 231-244 · Zbl 1015.68106
[14] Giesl, J.; Middeldorp, A., Transformation techniques for context-sensitive rewrite systems, Journal of Functional Programming, 14, 4, 379-427 (2004) · Zbl 1104.68056
[15] Giesl, J.; Thiemann, R.; Schneider-Kamp, P.; Falke, S., Mechanizing and Improving Dependency Pairs, Journal of Automated Reasoning, 37, 3, 155-203 (2006), Springer-Verlag · Zbl 1113.68088
[16] 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)
[17] Hirokawa, N.; Middeldorp, A., Automating the dependency pair method, Information and Computation, 199, 172-199 (2005) · Zbl 1081.68038
[18] Lucas, S., Context-sensitive computations in functional and functional logic programs, Journal of Functional and Logic Programming, 1998, 1, 1-61 (1998) · Zbl 0924.68106
[19] Lucas, S., Termination of Rewriting With Strategy Annotations, (Nieuwenhuis, R.; Voronkov, A., Proc. of 8th International Conference on Logic for Programming, Artificial Intelligence and Reasoning. Proc. of 8th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, LPAR’01. Proc. of 8th International Conference on Logic for Programming, Artificial Intelligence and Reasoning. Proc. of 8th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, LPAR’01, LNAI, 2250 (2001), Springer-Verlag: Springer-Verlag Berlin), 669-684 · Zbl 1275.68084
[20] Lucas, S., Termination of on-demand rewriting and termination of OBJ programs, (Proc. of 3rd International Conference on Principles and Practice of Declarative Programming, Proc. of PPDP’01 (2001), ACM Press), 82-93
[21] Lucas, S., Context-sensitive rewriting strategies, Information and Computation, 178, 1, 293-343 (2002) · Zbl 1012.68095
[22] Lucas, S., MU-TERM: A Tool for Proving Termination of Context-Sensitive Rewriting, (van Oostrom, V., Proc. of 15h International Conference on Rewriting Techniques and Applications. Proc. of 15h International Conference on Rewriting Techniques and Applications, RTA’04. Proc. of 15h International Conference on Rewriting Techniques and Applications. Proc. of 15h International Conference on Rewriting Techniques and Applications, RTA’04, LNCS, 3091 (2004), Springer-Verlag: Springer-Verlag Berlin), 200-209, Available at
[23] Lucas, S., Proving termination of context-sensitive rewriting by transformation, Information and Computation, 204, 12, 1782-1846 (2006) · Zbl 1171.68514
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.