article

Proving operational termination of membership equational programs

Authors:

Francisco Durán,

Salvador Lucas,

Claude Marché,

José Meseguer,

Xavier UrbainAuthors Info & Claims

Higher-Order and Symbolic Computation, Volume 21, Issue 1-2

Pages 59 - 88

https://doi.org/10.1007/s10990-008-9028-2

Published: 01 June 2008 Publication History

Abstract

Reasoning about the termination of equational programs in sophisticated equational languages such as Elan , Maude , OBJ , CafeOBJ , Haskell , and so on, requires support for advanced features such as evaluation strategies, rewriting modulo, use of extra variables in conditions, partiality, and expressive type systems (possibly including polymorphism and higher-order). However, many of those features are, at best, only partially supported by current term rewriting termination tools (for instance mu-term , C i ME , AProVE , TTT , Termptation , etc.) while they may be essential to ensure termination. We present a sequence of theory transformations that can be used to bridge the gap between expressive membership equational programs and such termination tools, and prove the correctness of such transformations. We also discuss a prototype tool performing the transformations on Maude equational programs and sending the resulting transformed theories to some of the aforementioned standard termination tools.

References

[1]

Borovansky, P., Kirchner, C., Kirchner, H., Moreau, P.-E.: ELAN from a rewriting logic point of view. Theor. Comput. Sci. 285 , 155-185 (2002).

Digital Library

[2]

Borralleras, C., Lucas, S., Rubio, A.: Recursive path orderings can be context-sensitive. In: Voronkov, A. (ed.) Proc. of 18th International Conference on Automated Deduction. Lecture Notes in Artificial Intelligence, vol. 2392, pp. 314-331. Springer, Berlin (2002).

Digital Library

[3]

Bouhoula, A., Jouannaud, J.-P., Meseguer, J.: Specification and proof in membership equational logic. Theor. Comput. Sci. 236 , 35-132 (2000).

Digital Library

[4]

Bruni, R., Meseguer, J.: Generalized rewrite theories. In: Baeten, J., Lenstra, J., Parrow, J. (eds.) Proceedings of the 30th International Colloquium on Automata, Languages and Programming. Lecture Notes in Computer Science, vol. 2719, pp. 252-266. Springer, Berlin (2003).

Digital Library

[5]

Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Quesada, J.: Maude: specification and programming in rewriting logic. Theor. Comput. Sci. 285</b>(2), 187-243 (2002).

Digital Library

[6]

Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Talcott, C.: Maude Manual (Version 2.2). December 2005, http://maude.cs.uiuc.edu

[7]

CoFI Task Group on Semantics. CASL--The common algebraic specification language, version 1.0, Semantics. http://www.brics.dk/Projects/CoFI/Documents/CASL/Semantics/index.html (1999).

[8]

Contejean, E., Marché, C., Monate, B., Urbain, X.: Proving termination of rewriting with CiME. In: Rubio, A. (ed.) Proc. WST'03 (2003). http://cime.lri.fr

[9]

Durán, F., Lucas, S., Marché, C., Meseguer, J., Urbain, X.: Proving termination of membership equational programs. In: Sestoft, P., Heintze, N. (eds.) Proc. of ACM SIGPLAN 2004 Symposium PEPM'04, pp. 147-158. Assoc. Comput. Mach., New York (2004).

Digital Library

[10]

Ferreira, M.C.F., Ribeiro, A.L.: Context-sensitive AC-rewriting. In: Narendran, P., Rusinowitch, M. (eds.) Proc. RTA'99, Trento, Italy. Lecture Notes in Computer Science, vol. 1631, pp. 286-300. Springer, Berlin (1999).

Digital Library

[11]

Fissore, O., Gnaedig, I., Kirchner, H.: Cariboo: An induction based proof tool for termination with strategies. In: Kirehner, C. (ed.) Proc. PPDP'02, Pittsburgh, USA. Assoc. Comput. Mach., New York (2002).

Digital Library

[12]

Futatsugi, K., Diaconescu, R.: CafeOBJ Report. AMAST Series World Scientific, Singapore (1998).

[13]

Giesl, J., Arts, T.: Verification of Erlang processes by dependency pairs. Appl. Algebra Eng. Commun. Comput. 12 , 39-72 (2001).

[14]

Giesl, J., Arts, T., Ohlebusch, E.: Modular termination proofs for rewriting using dependency pairs. J. Symb. Comput. 34 (2), 21-58 (2002).

Digital Library

[15]

Giesl, J., Middleldorp, A.: Transformation techniques for context-sensitive rewrite systems. J. Funct. Program. 14 , 379-427 (2004).

Digital Library

[16]

Giesl, J., Thiemann, R., Schneider-Kamp, P.: Proving and disproving termination of higber-order functions. In: Gramlich, B. (ed.) Proc. of 5th International Workshop on Frontiers of Combining Systems, FroCoS'05, Vienna, Austria, vol. 3717, pp. 216-231. Springer, Berlin (2005).

Digital Library

[17]

Giesl, J., Thiemann, R., Schneider-Kamp, P., Falke, S.: AProVE: A system for proving termination. In: van Oostrom, V. (ed.) Rewriting Techniques and Applications. Lecture Notes in Computer Science. Springer, Berlin (2004). http://www-i2.informatik.rwth-aachen.de/AProVE

[18]

Goguen, J., Meseguer, J.: Order-sorted algebra I: Equational deduction for multiple inheritance, overloading, exceptions and partial operations. Theor. Comput. Sci. 105 , 217-273 (1992).

Digital Library

[19]

Goguen, J., Winkler, T., Meseguer, J., Futatsugi, K., Jouannaud, J.-P.: Introducing OBJ. In: Software Engineering with OBJ: Algebraic Specification in Action. Kluwer Academic, Dordrecht (2000).

[20]

Hirokawa, N., Middeldorp, A.: Tyrolean termination tool. In: Giesl, J. (ed.) Proc. RTA'05, Nara, Japan. Lecture Notes in Computer Science, vol. 3467, pp. 175-184. Springer, Berlin (2005).

Digital Library

[21]

Hudak, P., Peyton-Jones, S., Wadler, P.: Report on the functional programming language Haskell: a nonstrict, purely functional language. SIGPLAN Not. 27, 1-164 (1992).

Digital Library

[22]

Lucas, S.: Termination of context-sensitive rewriting by rewriting. In: auf der Heide, F.M., Monien, B. (eds.) Proc. of ICALP'96. Lecture Notes in Computer Science, vol. 1099, pp. 122-133. Springer, Berlin (1996).

Digital Library

[23]

Lucas, S.: Context-sensitive computations in functional and functional logic programs. J. Funct. Logic Program. 1998 (1) (1998).

[24]

Lucas, S.: Context-sensitive rewriting strategies. Inf. Comput. 178 (1), 294-343 (2002).

Digital Library

[25]

Lucas, S.: Termination of programs with strategy annotations. Technical Report DSIC-II/20/03, DSIC, Universidad Politécnica de Valencia (2003).

[26]

Lucas, S.: MU-TERM, a tool for proving termination of context-sensitive rewriting. In: van Oostrom, V. (ed.) Rewriting Techniques and Applications. Lecture Notes in Computer Science. Springer, Berlin (2004). http://www.dsic.upv.es/~slucas/csr/termination/muterm/

[27]

Lucas, S.: Polynomials for proving termination of context-sensitive rewriting. In: Walukiewicz, I. (ed.) Proc. FOSSACS'04. Lecture Notes in Computer Science, vol. 2987, pp. 318-332. Springer, Berlin (2004).

[28]

Lucas, S.: Proving termination of context-sensitive rewriting by transformation. Inf. Comput. 204 (12), 1782-1846 (2006).

Digital Library

[29]

Lucas, S., Marché, C., Meseguer, J.: Operational termination of conditional term rewriting systems. Inf. Process. Lett. 95 , 446-453 (2005).

Digital Library

[30]

Marché, C., Urbain, X.: Modular and incremental proofs of AC-termination. J. Symb. Comput. 38 , 873- 897 (2004).

[31]

Marchiori, M.: Unravelings and ultra-properties. In: Hanus, M., Rodríguez-Artalejo, M. (eds.) Proc. of ALP'96. Lecture Notes in Computer Science, vol. 1039, pp. 107-121. Springer, Berlin (1996).

Digital Library

[32]

Meseguer, J.: General logics, In: Logic Colloquium'87, pp. 275-329. North-Holland, Amsterdam (1989).

[33]

Meseguer, J.: Membership algebra as a logical framework for equational specification. In: Parisi-Presicce, F. (ed.) Proceedings WADT'97. Lecture Notes in Computer Science, vol. 1376, pp. 18-61. Springer, Berlin (1998).

Digital Library

[34]

Meseguer, J., Goguen, J.: Initiality, induction and computability. In: Nivat, M., Reynolds, J. (eds.) Algebraic Methods in Semantics, pp. 459-541. Cambridge University Press, Cambridge (1985).

Digital Library

[35]

Ohlebusch, E.: Advanced Topics in Term Rewriting. Springer, Berlin (2002).

Digital Library

[36]

Ohlebusch, E.: Hierarchical termination revisited. Inf. Process. Lett. 84 (4), 207-214 (2002).

Digital Library

[37]

Urbaln, X.: Automated incremental termination proofs for hierarchically defined term rewriting systems. In: Goré, R., Leitsch, A., Nipkow, T. (eds.) Proc. IJCAR'01, Siena, Italy. Lecture Notes in Artificial Intelligence, vol. 2083, pp. 485-498. Springer, Berlin (2001).

Digital Library

[38]

Urbain, X.: Modular and incremental automated termination proofs. J. Automat. Reason. 32 , 315-355 (2004).

[39]

Van Deursen, A., Heering, J., Klint, P: Language Prototyping: An Algebraic Specification Approach. World Scientific, Singapore (1996).

Digital Library

[40]

Viry, P.: Equational rules for rewriting logic. Theor. Comput. Sci. 285 , 487-517 (2002).

Digital Library

[41]

Zantema, H.: Termination of context-sensitive rewriting. In: Comon, H. (ed.) Proc. RTA'97, Sitges, Spain. Lecture Notes in Computer Science, vol. 1232, pp. 172-186. Springer, Berlin (1997)

Digital Library

Cited By

Lucas S(2020)Using Well-Founded Relations for Proving Operational TerminationJournal of Automated Reasoning10.1007/s10817-019-09514-264:2(167-195)Online publication date: 1-Feb-2020
https://dl.acm.org/doi/10.1007/s10817-019-09514-2
Aguirre LMartí-Oliet NPalomino MPita I(2018)Sentence-Normalized Conditional Narrowing Modulo in Rewriting Logic and MaudeJournal of Automated Reasoning10.1007/s10817-017-9417-560:4(421-463)Online publication date: 1-Apr-2018
https://dl.acm.org/doi/10.1007/s10817-017-9417-5
Aguirre LMartí-Oliet NPalomino MPita IVanhoof WPientka B(2017)Conditional narrowing modulo SMT and axiomsProceedings of the 19th International Symposium on Principles and Practice of Declarative Programming10.1145/3131851.3131856(17-28)Online publication date: 9-Oct-2017
https://dl.acm.org/doi/10.1145/3131851.3131856
Show More Cited By

Index Terms

Proving operational termination of membership equational programs
1. Software and its engineering
  1. Software notations and tools
    1. General programming languages
      1. Language types
        Constraint and logic languages
2. Theory of computation
  1. Logic
  2. Semantics and reasoning
    1. Program reasoning

Recommendations

Operational Termination of Membership Equational Programs: the Order-Sorted Way

Our main goal is automating termination proofs for programs in rewriting-based languages with features such as: (i) expressive type structures, (ii) conditional rules, (iii) matching modulo axioms, and (iv) context-sensitive rewriting. Specifically, we ...
Proving termination of membership equational programs
PEPM '04: Proceedings of the 2004 ACM SIGPLAN symposium on Partial evaluation and semantics-based program manipulation

Advanced typing, matching, and evaluation strategy features, as well as very general conditional rules, are routinely used in equational programming languages such as, for example, ASF+SDF, OBJ, CafeOBJ, Maude, and equational subsets of ELAN and CASL. ...
Operational Termination of Conditional Rewriting with Built-in Numbers and Semantic Data Structures

While ordinary conditional rewrite systems are more elegant than unconditional ones, they still have limited expressive power since semantic data structures, such as sets or multisets, cannot be modeled elegantly. Extending our work presented at RTA ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Higher-Order and Symbolic Computation

Higher-Order and Symbolic Computation Volume 21, Issue 1-2

June 2008

233 pages

ISSN:1388-3690

Issue’s Table of Contents

Copyright © Copyright © 2008 Springer Science+Business Media, LLC.

Publisher

Kluwer Academic Publishers

United States

Publication History

Published: 01 June 2008

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

23
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 12 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Lucas S(2020)Using Well-Founded Relations for Proving Operational TerminationJournal of Automated Reasoning10.1007/s10817-019-09514-264:2(167-195)Online publication date: 1-Feb-2020
https://dl.acm.org/doi/10.1007/s10817-019-09514-2
Aguirre LMartí-Oliet NPalomino MPita I(2018)Sentence-Normalized Conditional Narrowing Modulo in Rewriting Logic and MaudeJournal of Automated Reasoning10.1007/s10817-017-9417-560:4(421-463)Online publication date: 1-Apr-2018
https://dl.acm.org/doi/10.1007/s10817-017-9417-5
Aguirre LMartí-Oliet NPalomino MPita IVanhoof WPientka B(2017)Conditional narrowing modulo SMT and axiomsProceedings of the 19th International Symposium on Principles and Practice of Declarative Programming10.1145/3131851.3131856(17-28)Online publication date: 9-Oct-2017
https://dl.acm.org/doi/10.1145/3131851.3131856
Meseguer J(2017)Strict coherence of conditional rewriting modulo axiomsTheoretical Computer Science10.1016/j.tcs.2016.12.026672:C(1-35)Online publication date: 11-Apr-2017
https://dl.acm.org/doi/10.1016/j.tcs.2016.12.026
Durán FMoreno-Delgado AÁlvarez-Palomo J(2016)Statistical Model Checking of e-Motions Domain-Specific Modeling LanguagesProceedings of the 19th International Conference on Fundamental Approaches to Software Engineering - Volume 963310.1007/978-3-662-49665-7_18(305-322)Online publication date: 2-Apr-2016
https://dl.acm.org/doi/10.1007/978-3-662-49665-7_18
Cholewa AEscobar SMeseguer J(2015)Constrained narrowing for conditional equational theories modulo axiomsScience of Computer Programming10.1016/j.scico.2015.06.001112:P1(24-57)Online publication date: 15-Nov-2015
https://dl.acm.org/doi/10.1016/j.scico.2015.06.001
Gutiérrez RMeseguer JRocha C(2015)Order-sorted equality enrichments modulo axiomsScience of Computer Programming10.1016/j.scico.2014.07.00399:C(235-261)Online publication date: 1-Mar-2015
https://dl.acm.org/doi/10.1016/j.scico.2014.07.003
Lucas SMeseguer JChitil OKing ADanvy O(2014)Proving Operational Termination of Declarative Programs in General LogicsProceedings of the 16th International Symposium on Principles and Practice of Declarative Programming10.1145/2643135.2643152(111-122)Online publication date: 8-Sep-2014
https://dl.acm.org/doi/10.1145/2643135.2643152
Gutiérrez RMeseguer JRocha C(2012)Order-Sorted equality enrichments modulo axiomsProceedings of the 9th international conference on Rewriting Logic and Its Applications10.1007/978-3-642-34005-5_9(162-181)Online publication date: 24-Mar-2012
https://dl.acm.org/doi/10.1007/978-3-642-34005-5_9
Alarcón BLucas SMeseguer J(2010)A dependency pair framework for A∨C-terminationProceedings of the 8th international conference on Rewriting logic and its applications10.5555/1927806.1927812(35-51)Online publication date: 20-Mar-2010
https://dl.acm.org/doi/10.5555/1927806.1927812
Show More Cited By

View Options

View options

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Issue’s Table of Contents