Proving termination of membership equational programs

ABSTRACT

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. Proving termination of equational programs having such expressive features is important but nontrivial, because some of those features may not be supported by standard termination methods and tools, such as muterm, CiME, AProVE, TTT, Termptation, etc. Yet, use of the features may be essential to ensure termination. We present a sequence of theory transformations that can be used to bridge the gap between expressive equational programs and termination tools, prove the correctness of such transformations, and discuss a prototype tool performing the transformations on Maude equational programs and sending the resulting transformed theories to some of the aforementioned tools.

REFERENCES

• 1: Jürgen Giesl , Thomas Arts , Enno Ohlebusch, Modular termination proofs for rewriting using dependency pairs, Journal of Symbolic Computation, v.34 n.1, p.21-58, July 2002 [doi>10.1006/jsco.2002.0541]
• 2: Peter Borovanský , Claude Kirchner , Hélène Kirchner , Pierre-Etienne Moreau, ELAN from a rewriting logic point of view, Theoretical Computer Science, v.285 n.2, p.155-185, 28 August 2002 [doi>10.1016/S0304-3975(01)00358-9 ]
• 3: Cristina Borralleras , Salvador Lucas , Albert Rubio, Recursive Path Orderings Can Be Context-Sensitive, Proceedings of the 18th International Conference on Automated Deduction, p.314-331, July 27-30, 2002
• 4: C. Borralleras and A. Rubio. Termptation. In Rubio {27}, pages 61--63. Technical Report DSIC II/15/03, Universidad Politécnica de Valencia, Spain.
• 5: Adel Bouhoula , Jean-Pierre Jouannaud , José Meseguer, Specification and proof in membership equational logic, Theoretical Computer Science, v.236 n.1-2, p.35-132, April 6, 2000 [doi>10.1016/S0304-3975(99)00206-6 ]
• 6: R. Bruni and J. Meseguer. Generalized rewrite theories. In J. Baeten, J. Lenstra, J. Parrow, and G. Woeginger, editors, Proceedings of the 30th International Colloquium on Automata, Languages and Programming, volume 2719 of LNCS, pages 252--266, 2003.
• 7: M. Clavel , F. Durán , S. Eker , P. Lincoln , N. Martí-Oliet , J. Meseguer , J. F. Quesada, Maude: specification and programming in rewriting logic, Theoretical Computer Science, v.285 n.2, p.187-243, 28 August 2002 [doi>10.1016/S0304-3975(01)00359-0 ]
• 8: 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, July 1999.
• 9: E. Contejean, C. Marché, B. Monate, and X. Urbain. Proving termination of rewriting with CiME. In Rubio {27}. http://cime.lri.fr.
• 10: Maria C. F. Ferreira , A. L. Ribeiro, Context-Sensitive AC-Rewriting, Proceedings of the 10th International Conference on Rewriting Techniques and Applications, p.286-300, July 02-04, 1999
• 11: Olivier Fissore , Isabelle Gnaedig , Hélène Kirchner, System Presentation -- CARIBOO: An induction based proof tool for termination with strategies, Proceedings of the 4th ACM SIGPLAN international conference on Principles and practice of declarative programming, p.62-73, October 06-08, 2002, Pittsburgh, PA, USA [doi>10.1145/571157.571164]
• 12: K. Futatsugi and R. Diaconescu. CafeOBJ Report. World Scientific, AMAST Series, 1998.
• 13: Jürgen Giesl , Aart Middeldorp, Transformation techniques for context-sensitive rewrite systems, Journal of Functional Programming, v.14 n.4, p.379-427, July 2004 [doi>10.1017/S0956796803004945]
• 14: J. Giesl, R. Thiemann, P. Schneider-Kamp, and S. Falke. AProVE: A system for proving termination. In Rubio {27}. http://www-i2.informatik.rwth-aachen.de/AProVE.
• 15: J. Goguen, T. Winkler, J. Meseguer, K. Futatsugi, and J.-P. Jouannaud. Introducing OBJ. In Software Engineering with OBJ: Algebraic Specification in Action. Kluwer, 2000.
• 16: N. Hirokawa and A. Middeldorp. Tsukuba termination tool. In R. Nieuwenhuis, editor, 14th International Conference on Rewriting Techniques and Applications, volume 2706 of LNCS, pages 311--320, Valencia, Spain, June 2003. Springer-Verlag.
• 17: Salvador Lucas, Termination of Context-Sensitive Rewriting by Rewriting, Proceedings of the 23rd International Colloquium on Automata, Languages and Programming, p.122-133, July 08-12, 1996
• 18: S. Lucas. Context-sensitive computations in functional and functional logic programs. Journal of Functional and Logic Programming, 1998(1), January 1998.
• 19: Salvador Lucas, Context-sensitive rewriting strategies, Information and Computation, v.178 n.1, p.294-343, October 10, 2002 [doi>10.1016/S0890-5401(02)93176-7 ]
• 20: S. Lucas. Termination of programs with strategy annotations. Technical Report DSIC-II/20/03, DSIC, Universidad Politécnica de Valencia, September 2003.
• 21: S. Lucas. mu-term, a tool for proving termination of context-sensitive rewriting. In V. van Oostrom, editor, 15th International Conference on Rewriting Techniques and Applications, LNCS, Aachen, Germany, June 2004. Springer-Verlag. http://www.dsic.upv.es/~slucas/csr/termination/muterm/.
• 22: S. Lucas. Polynomials for proving termination of context-sensitive rewriting. In I. Walukiewicz, editor, Proc. of 7th International Conference on Foundations of Software Science and Computation Structures, FOSSACS'04, volume 2987 of LNCS, pages 318--332. Springer-Verlag, 2004.
• 23: C. Marché and X. Urbain. Modular & incremental proofs of AC-termination. Journal of Symb. Comp., 2004.
• 24: José Meseguer, Membership algebra as a logical framework for equational specification, Selected papers from the 12th International Workshop on Recent Trends in Algebraic Development Techniques, p.18-61, July 01, 1997
• 25: E. Ohlebusch. Advanced Topics in Term Rewriting. Springer-Verlag, Apr. 2002.
• 26: Enno Ohlebusch, Hierarchical termination revisited, Information Processing Letters, v.84 n.4, p.207-214, 30 November 2002 [doi>10.1016/S0020-0190(02)00272-7 ]
• 27: A. Rubio, editor. 6th International Workshop on Termination, WST'03, June 2003. Technical Report DSIC II/15/03, Universidad Politécnica de Valencia, Spain.
• 28: Xavier Urbain, Automated Incremental Termination Proofs for Hierarchically Defined Term Rewriting Systems, Proceedings of the First International Joint Conference on Automated Reasoning, p.485-498, June 18-23, 2001
• 29: X. Urbain. Modular and incremental automated termination proofs. Journal of Automated Reasoning, 2004.
• 30: Arie Van Deursen , Jan Heering , Paul Klint, Language Prototyping: An Algebraic Specification Approach: Vol. V, World Scientific Publishing Co., Inc., River Edge, NJ, 1996
• 31: H. Zantema, Termination of term rewriting: interpretation and type elimination, Journal of Symbolic Computation, v.17 n.1, p.23-50, Jan. 1994 [doi>10.1006/jsco.1994.1003 ]
• 32: Hans Zantema, Termination of Context-Sensitive Rewriting, Proceedings of the 8th International Conference on Rewriting Techniques and Applications, p.172-186, June 02-05, 1997

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification

Additional Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Mechanical verification

General Terms:
Languages, Theory, Verification

Keywords:
membership equational logic, program transformation, term rewriting, termination