Correctness of context-moving transformations for term rewriting systems

Koichi Sato, Kentaro Kikuchi, Takahito Aoto, Yoshihito Toyama

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

1 Citation (Scopus)


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.

Original languageEnglish
Title of host publicationLogic-Based Program Synthesis and Transformation - 25th International Symposium, LOPSTR 2015, Revised Selected Papers
EditorsMoreno Falaschi
PublisherSpringer Verlag
Number of pages15
ISBN (Print)9783319274355
Publication statusPublished - 2015
Event25th International Symposium on Logic-Based Program Synthesis and Transformation, LOPSTR 2015 - Siena, Italy
Duration: 2015 Jul 132015 Jul 15

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Conference25th International Symposium on Logic-Based Program Synthesis and Transformation, LOPSTR 2015


  • Inductive theorem proving
  • Program transformation
  • Tail-recursion
  • Term rewriting system


Dive into the research topics of 'Correctness of context-moving transformations for term rewriting systems'. Together they form a unique fingerprint.

Cite this