Computing constructor forms with non terminating rewrite programs

ABSTRACT

In the context of the study of rule-based programming, we focus in this paper on the property of C-reducibility, expressing that every term reduces to a constructor term on at least one of its rewriting derivations. This property implies completeness of function definitions, and enables to stop evaluations of a program on a constructor form, even if the program is not terminating. We propose an inductive procedure proving C-reducibility of rewriting. The rewriting relation on ground terms is simulated through an abstraction mechanism and narrowing. The induction hypothesis allows assuming that terms smaller than the starting terms rewrite into a constructor term. The existence of the induction ordering is checked during the proof process, by ensuring satisfiability of ordering constraints. The proof is constructive, in the sense that the branch leading to a constructor term can be computed from the proof trees establishing C-reducibility for every term

REFERENCES

• 1: P. Borovanský, C. Kirchner, H. Kirchner, P.-E. Moreau, and C. Ringeissen. An Overview of ELAN. In C. Kirchner and H. Kirchner, editors, Proceedings of the 2nd International Workshop on Rewriting Logic and its Applications, Electronic Notes in Theoretical Computer Science, Pont-à-Mousson (France), Sept. 1998. Elsevier Science Publishers B. V. (North-Holland).
• 2: Adel Bouhoula, Using induction and rewriting to verify and complete parameterized specifications, Theoretical Computer Science, v.170 n.1-2, p.245-276, Dec. 1996 [doi>10.1016/S0304-3975(96)00005-9 ]
• 3: A. Bouhoula and F. Jaquemard. Automatic verification of. sufficient completeness for. specifications of complex data structures. Technical Report RR-LSV-05-17, INRIA, 2005.
• 4: Anne-Cécile Caron , Jean-Luc Coquidé , Max Dauchet, Encompassment Properties and Automata with Constraints, Proceedings of the 5th International Conference on Rewriting Techniques and Applications, p.328-342, June 16-18, 1993
• 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: H Comon, Sufficient completeness, term rewriting systems and “anti-unification”, Proc. of the 8th international conference on Automated deduction, p.128-140, August 1986, Oxford, United Kingdom
• 7: H. Comon. Inductionless induction. In A. Robinson and A. Voronkov, editors, Handbook of Automated Reasoning, volume I, chapter 14, pages 913--962. Elsevier Science, 2001.
• 8: Hubert Comon , Florent Jacquemard, Ground Reducibility is EXPTIME-complete, Proceedings of the 12th Annual IEEE Symposium on Logic in Computer Science, p.26, June 29-July 02, 1997
• 9: E. Contejean, C. Marché, B. Monate, and X. Urbain. CiME version 2, 2000. http://cime.lri.fr/.
• 10: N. Dershowitz. Orderings for term-rewriting systems. Theoretical Computer Science, 17:279--301, 1982.
• 11: N. Dershowitz and J.-P. Jouannaud. Handbook of Theoretical Computer Science, volume B, chapter 6: Rewrite Systems, pages 244--320. Elsevier Science Publishers B. V. (North-Holland), 1990. Also as: Research report 478, LRI.
• 12: 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 ]
• 13: 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 B. V. (North-Holland), 2001.
• 14: O. Fissore, I. Gnaedig, and H. Kirchner. Outermost ground termination. In Proceedings of the 4th International Workshop on Rewriting Logic and Its Applications, volume 71 of Electronic Notes in Theoretical Computer Science, Pisa, Italy, September 2002. Elsevier Science Publishers B. V. (North-Holland).
• 15: O. Fissore, I. Gnaedig, and H. Kirchner. A proof of weak termination providing the right way to terminate. In 1st International Colloquium on THEORETICAL ASPECTS OF COMPUTING, volume 3407 of Lecture Notes in Computer Science, pages 356--371, Guiyang, China, September 2004. Springer-Verlag.
• 16: O. Fissore, I. Gnaedig, and H. Kirchner. Proving weak termination also provides the right way to terminate - Extended version. Technical report, LORIA, Nancy (France), March 2004. Available at http://www.loria.fr/~gnaedig/PAPERS/REPORTS/wt-extended-2004.ps.
• 17: 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
• 18: J. Giesl, R. Thiemann, P. Schneider-Kamp, and S. Falke. Improving dependency pairs. In Proceedings of the 10th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR '03), volume 2850 of Lecture Notes in Artificial Intelligence, pages 165--179, Almaty, Kazakhstan, 2003. Springer-Verlag.
• 19: I. Gnaedig and H. Kirchner. Computing Constructor Forms with Non Terminating Rewrite Programs - Extended version. Technical report, LORIA, Nancy (France), 2006. Available at http://www.loria.fr/~gnaedig/PAPERS/REPORTS/comp-extended-2006.pdf.
• 20: I. Gnaedig, H. Kirchner, and O. Fissore. Induction for innermost and outermost ground termination. Technical Report A01-R-178, LORIA, Nancy (France), September 2001.
• 21: G. Huet and J.-M. Hullot. Proofs by induction in equational theories with constructors. Journal of Computer and System Sciences, 25(2):239--266, Oct. 1982. Preliminary version in Proceedings 21st Symposium on Foundations of Computer Science, IEEE, 1980.
• 22: Jean-Pierre Jouannaud , Emmanuel Kounalis, Automatic proofs by induction in theories without constructors, Information and Computation, v.82 n.1, p.1-33, July 1989 [doi>10.1016/0890-5401(89)90062-X]
• 23: D Kapur , P Narendran , H Zhang, Proof by induction using test sets, Proc. of the 8th international conference on Automated deduction, p.99-117, August 1986, Oxford, United Kingdom
• 24: D. Kapur, P. Narendran, and H. Zhang. On sufficient completeness and related properties of term rewriting systems. Acta Informatica, 24:395--415, 1987.
• 25: 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]
• 26: Emmanuel Kounalis, Completeness in Data Type Specifications, Research Contributions from the European Conference on Computer Algebra-Volume 2, p.348-362, April 01-03, 1985
• 27: Emmanuel Kounalis, Testing for the ground (co-)reducibility property in term-rewriting systems, Theoretical Computer Science, v.106 n.1, p.87-117, Nov. 1992
• 28: A. Lazrek , P. Lescanne , J. J. Thiel, Tools for proving inductive equalities, relative completeness, and &ohgr;-completeness, Information and Computation, v.84 n.1, p.47-70, Jan. 1990 [doi>10.1016/0890-5401(90)90033-E]
• 29: P.-E. Moreau, C. Ringeissen, and M. Vittek. A Pattern Matching Compiler for Multiple Target Languages. In G. Hedin, editor, 12th Conference on Compiler Construction, Warsaw (Poland), volume 2622 of LNCS, pages 61--76. Springer-Verlag, May 2003.
• 30: Tobias Nipkow , Gerhard Weikum, A decidability result about sufficient-completeness of axiomatically specified abstract data types, Proceedings of the 6th GI-Conference on Theoretical Computer Science, p.257-268, January 05-07, 1983
• 31: D. Plaisted. Semantic confluence tests and completion methods. Information and Control, 65:182--215, 1985.

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Logics of programs

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Correctness proofs; Formal methods; Validation
  D.3 PROGRAMMING LANGUAGES
      D.3.1 Formal Definitions and Theory

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Mechanical verification; Specification techniques
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.2 Grammars and Other Rewriting Systems
      F.4.3 Formal Languages
          Subjects: Algebraic language theory

  I. Computing Methodologies
  I.1 SYMBOLIC AND ALGEBRAIC MANIPULATION
      I.1.3 Languages and Systems
  I.2 ARTIFICIAL INTELLIGENCE
      I.2.3 Deduction and Theorem Proving
          Subjects: Mathematical induction; Deduction (e.g., natural, rule-based); Inference engines

General Terms:
Algorithms, Languages, Verification

Keywords:
abstraction, constructor, narrowing, ordering constraint, sufficient completeness, termination