System Presentation -- CARIBOO: An induction based proof tool for termination with strategies

ABSTRACT

We describe Cariboo, the implementation of an inductive process recently proposed to prove termination of rewriting under strategies on ground term algebras. The method is based on an abstraction mechanism, introducing variables that represent ground terms in normal form, and on narrowing, schematizing reductions on ground terms. It applies in particular to non-terminating systems which are terminating with innermost or local strategies. The narrowing process, well known to easily diverge, is controlled by using appropriate abstraction constraints. The abstraction mechanism lies on satisfiability of ordering constraints. Thanks to the power of induction, these ordering constraints are often simple and automatically solved by our system. Otherwise, they can be treated by the user or any external automatic solver. On many examples, Cariboo even enables to succeed without considering any constraint at all ; the process is then completely automatic. Cariboo offers a graphical view of the proof process. It is implemented in ELAN, a rule based programming environment, and so can be used for proving termination of ELAN programs.

REFERENCES

• 1: Thomas Arts , Jürgen Giesl, Proving Innermost Normalisation Automatically, Proceedings of the 8th International Conference on Rewriting Techniques and Applications, p.157-171, June 02-05, 1997
• 2: T. Arts and J. Giesl. A collection of examples for termination of term rewriting using dependency pairs. Technical Report AIB-2001-09, RWTH Aachen, Germany, September 2001.
• 3: P. Borovanský, C. Kirchner, H. Kirchner, P.-E. Moreau, and Ch. Ringeissen. An Overview of ELAN. In C. Kirchner and H. Kirchner, editors, Proc. Second Intl. Workshop on Rewriting Logic and its Applications, Electronic Notes in Theoretical Computer Science, Pont-à-Mousson (France), September 1998. Elsevier.
• 4: Peter Borovanský, Claude Kirchner, Hélène Kirchner, Pierre-Etienne Moreau, and Christophe Ringeissen. An overview of ELAN. In Claude Kirchner and Hélène Kirchner, editors, Proceedings of the second International Workshop on Rewriting Logic and Applications, volume 15, http://www.elsevier.nl/locate/entcs/volume15.html, Pont-à-Mousson (France), September 1998. Electronic Notes in Theoretical Computer Science. Report LORIA 98-R-316.
• 5: M. Clavel, S. Eker, P. Lincoln, and J. Meseguer. Principles of Maude. In J. Meseguer, editor, Proceedings of the 1st International Workshop on Rewriting Logic and its Applications, volume 5 of Electronic Notes in Theoretical Computer Science, Asilomar, Pacific Grove, CA, USA, September 1996. North Holland.
• 6: Evelyne Contejean, Claude Marché, Ana-Paula Tomás, and Xavier Urbain. Solving termination constraints via finite domain polynomial interpretations. Unpublished draft, 2000.
• 7: S. Eker. Term rewriting with operator evaluation strategies. In C Kirchner and H. Kirchner, editors, Proceedings of the 2nd International Workshop on Rewriting Logic and its Applications, Pont-à-Mousson, France, September 1998.
• 8: Benjamin Monate et Xavier Urbain Evelyne Contejean, Claude Marché. Cime version 2, 2000. Version préliminaire disponible à http://cime.lri.fr/.
• 9: O. Fissore, I. Gnaedig, and H. Kirchner. Termination of rewriting with local strategies. In M. P. Bonacina and B. Gramlich, editors, Selected papers of the 4th International Workshop on Strategies in Automated Deduction, volume 58 of Electronic Notes in Theoretical Computer Science. Elsevier Science Publishers, 2001. Also available as Technical Report A01-R-177, LORIA, Nancy, France.
• 10: O. Fissore, I. Gnaedig, and H. Kirchner. CARIBOO : An induction based proof tool for termination with strategies - Extended version. Technical Report A02-R-077, LORIA, Nancy, France, 2002. Available at http://www.loria.fr/~gnaedig/INDO/CARIBOO/cari-boo-extended.ps.
• 11: K. Futatsugi , A. Nakagawa, An overview of CAFE specification environment-an algebraic approach for creating, verifying, and maintaining formal specifications over networks, Proceedings of the 1st International Conference on Formal Engineering Methods, p.170, November 12-14, 1997
• 12: Jürgen Giesl , Aart Middeldorp, Transforming Context-Sensitive Rewrite Systems, Proceedings of the 10th International Conference on Rewriting Techniques and Applications, p.271-287, July 02-04, 1999
• 13: Jurgen Giesl. Polo -- a system for termination proofs using polynomial orderings. Technical Report IBN 95/24, Technische Hochschule Darmstadt, 1995.
• 14: I. Gnaedig, H. Kirchner, and O. Fissore. Induction for innermost and outermost ground termination. Technical Report A01-R-178, LORIA, Nancy, France, 2001.
• 15: J. Goguen, T. Winkler, J. Meseguer, K. Futatsugi, and J.P. Jouannaud. Introducing OBJ3. Technical report, Computer Science Laboratory, SRI International, march 1992.
• 16: P. Klint, A meta-environment for generating programming environments, ACM Transactions on Software Engineering and Methodology (TOSEM), v.2 n.2, p.176-201, April 1993 [doi>10.1145/151257.151260]
• 17: M. R. K. Krishna Ras, Some characteristics of strong innermost normalization, Theoretical Computer Science, v.239 n.1, p.141-164, May 17, 2000 [doi>10.1016/S0304-3975(99)00215-7 ]
• 18: Salvador Lucas, Termination of Rewriting With Strategy Annotations, Proceedings of the Artificial Intelligence on Logic for Programming, p.669-684, December 03-07, 2001
• 19: 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:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.6 Programming Environments
          Subjects: Integrated environments
  D.3 PROGRAMMING LANGUAGES
      D.3.2 Language Classifications
          Subjects: Constraint and logic languages

  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Mechanical theorem proving

  I. Computing Methodologies
  I.1 SYMBOLIC AND ALGEBRAIC MANIPULATION
      I.1.3 Languages and Systems
          Subjects: Evaluation strategies

General Terms:
Algorithms, Languages, Theory, Verification

Keywords:
ELAN, constraint, innermost, local strategy, narrowing, ordering, rewriting, rule based language induction, termination