Skip to main content
SpringerLink
Log in

Proving operational termination of membership equational programs

  • Published:
Higher-Order and Symbolic Computation

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.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

References

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

    Article  MATH  Google Scholar 

  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)

    Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

  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)

    Chapter  Google Scholar 

  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(2), 187–243 (2002)

    Article  MATH  Google Scholar 

  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)

    Google Scholar 

  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)

    Google Scholar 

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

    Google Scholar 

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

    MATH  Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

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

    Article  MathSciNet  Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

  16. Giesl, J., Thiemann, R., Schneider-Kamp, P.: Proving and disproving termination of higher-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)

    Chapter  Google Scholar 

  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

    Google Scholar 

  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)

    Article  MathSciNet  MATH  Google Scholar 

  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)

    Google Scholar 

  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)

    Google Scholar 

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

    Google Scholar 

  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)

    Google Scholar 

  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)

    MathSciNet  MATH  Google Scholar 

  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/

    Google Scholar 

  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)

    Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

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

    Article  MATH  Google Scholar 

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

    Article  Google Scholar 

  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)

    Google Scholar 

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

    Google Scholar 

  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)

    Google Scholar 

  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)

    Google Scholar 

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

    MATH  Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

  37. Urbain, 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)

    Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

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

    MATH  Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

  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)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. LCC, Universidad de Málaga, Malaga, Spain

    Francisco Durán

  2. DSIC, Universidad Politécnica de Valencia, Valencia, Spain

    Salvador Lucas

  3. PCRI, LRI (CNRS UMR 8623), INRIA Futurs, Université Paris-Sud, Orsay Cedex, France

    Claude Marché

  4. CS Dept., University of Illinois at Urbana-Champaign, Urbana, USA

    José Meseguer

  5. CEDRIC, IIE, Conservatoire National des Arts et Métiers, Paris, France

    Xavier Urbain

Authors
  1. Francisco Durán
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Salvador Lucas
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Claude Marché
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. José Meseguer
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Xavier Urbain
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Salvador Lucas.

Additional information

This research was partly supported by bilateral CNRS-DSTIC/UIUC research project “Rewriting calculi, logic and behavior”, and by ONR Grant N00014-02-1-0715 and NSF Grant CCR-0234524; Francisco Durán was partially supported by the EU (FEDER) and the Spanish MEC, under grant TIN2005-09405-C02-01; Salvador Lucas was partially supported by the EU (FEDER) and the Spanish MEC, under grant TIN 2004-7943-C04-02, the Generalitat Valenciana under grant GV06/285, and the ICT for EU-India Cross-Cultural Dissemination ALA/95/23/2003/077-054 project.

Rights and permissions

Reprints and permissions

About this article

Cite this article

Durán, F., Lucas, S., Marché, C. et al. Proving operational termination of membership equational programs. Higher-Order Symb Comput 21, 59–88 (2008). https://doi.org/10.1007/s10990-008-9028-2

Download citation

  • Published:

  • Issue Date:

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

Keywords

Search

Navigation