Correctness of Context-Moving Transformations for Term Rewriting Systems

  • Koichi Sato
  • Kentaro KikuchiEmail author
  • Takahito Aoto
  • Yoshihito Toyama
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 9527)


Proofs by induction are often incompatible with functions in tail-recursive form as the accumulator changes in the course of unfolding the definitions. Context-moving and context-splitting (Giesl, 2000) for functional programs transform tail-recursive programs into non tail-recursive ones which are more suitable for proofs by induction and thus for verification. In this paper, we formulate context-moving and context-splitting transformations in the framework of term rewriting systems, and prove their correctness with respect to both eager evaluation semantics and initial algebra semantics under some conditions on the programs to be transformed. The conditions for the correctness with respect to initial algebra semantics can be checked by automated methods for inductive theorem proving developed in the field of term rewriting systems.


Tail-recursion Program transformation Term rewriting system Inductive theorem proving 



We are grateful to the anonymous referees for valuable comments. This research was supported by JSPS KAKENHI Grant Numbers 25330004, 25280025 and 15K00003.


  1. 1.
    Aoto, T.: Designing a rewriting induction prover with an increased capability of non-orientable equations. In: Proceedings of 1st SCSS, volume 08–08 of RISC Technical report, pp. 1–15 (2008)Google Scholar
  2. 2.
    Aoto, T.: Sound lemma generation for proving inductive validity of equations. In: Proceedings of 28th FSTTCS, LIPIcs, vol. 2, pp. 13–24. Schloss Dagstuhl (2008)Google Scholar
  3. 3.
    Bouhoula, A., Kounalis, E., Rusinowitch, M.: Automated mathematical induction. J. Logic Comput. 5(5), 631–668 (1995)MathSciNetCrossRefzbMATHGoogle Scholar
  4. 4.
    Giesl, J.: Context-moving transformations for function verification. In: Bossi, A. (ed.) LOPSTR 1999. LNCS, vol. 1817, pp. 293–312. Springer, Heidelberg (2000) CrossRefGoogle Scholar
  5. 5.
    Giesl, J.: Induction proofs with partial functions. J. Autom. Reasoning 26(1), 1–49 (2001)MathSciNetCrossRefzbMATHGoogle Scholar
  6. 6.
    Kapur, D., Narendran, P., Zhang, H.: On sufficient-completeness and related properties of term rewriting systems. Acta Informatica 24(4), 395–415 (1987)MathSciNetCrossRefzbMATHGoogle Scholar
  7. 7.
    Reddy, U.S.: Term rewriting induction. In: Stickel, M.E. (ed.) CADE 1990. LNCS, vol. 449, pp. 162–177. Springer, Heidelberg (1990) CrossRefGoogle Scholar
  8. 8.
    Sato, K., Kikuchi, K., Aoto, T., Toyama, Y.: Automated inductive theorem proving using transformations of term rewriting systems. JSSST Comput. Softw. 32(1), 179–193 (2015). In JapaneseGoogle Scholar
  9. 9.
    Shimazu, S., Aoto, T., Toyama, Y.: Automated lemma generation for rewriting induction with disproof. JSSST Comput. Softw. 26(2), 41–55 (2009). In JapaneseGoogle Scholar
  10. 10.
    Stratulat, S.: A general framework to build contextual cover set induction provers. J. Symbolic Comput. 32, 403–445 (2001)MathSciNetCrossRefzbMATHGoogle Scholar
  11. 11.
    Urso, P., Kounalis, E.: Sound generalizations in mathematical induction. Theor. Comput. Sci. 323, 443–471 (2004)MathSciNetCrossRefzbMATHGoogle Scholar
  12. 12.
    Walsh, T.: A divergence critic for inductive proof. J. Artif. Intell. Res. 4, 209–235 (1996)MathSciNetzbMATHGoogle Scholar

Copyright information

© Springer International Publishing Switzerland 2015

Authors and Affiliations

  • Koichi Sato
    • 1
  • Kentaro Kikuchi
    • 1
    Email author
  • Takahito Aoto
    • 1
  • Yoshihito Toyama
    • 1
  1. 1.RIEC, Tohoku UniversitySendaiJapan

Personalised recommendations