TY - GEN

T1 - Correctness of context-moving transformations for term rewriting systems

AU - Sato, Koichi

AU - Kikuchi, Kentaro

AU - Aoto, Takahito

AU - Toyama, Yoshihito

N1 - Funding Information:
We are grateful to the anonymous referees for valuable comments. This research was supported by JSPS KAKENHI Grant Numbers 25330004, 25280025 and 15K00003.
Publisher Copyright:
© Springer International Publishing Switzerland 2015.

PY - 2015

Y1 - 2015

N2 - 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.

AB - 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.

KW - Inductive theorem proving

KW - Program transformation

KW - Tail-recursion

KW - Term rewriting system

UR - http://www.scopus.com/inward/record.url?scp=84952802981&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84952802981&partnerID=8YFLogxK

U2 - 10.1007/978-3-319-27436-2_20

DO - 10.1007/978-3-319-27436-2_20

M3 - Conference contribution

AN - SCOPUS:84952802981

SN - 9783319274355

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 331

EP - 345

BT - Logic-Based Program Synthesis and Transformation - 25th International Symposium, LOPSTR 2015, Revised Selected Papers

A2 - Falaschi, Moreno

PB - Springer Verlag

T2 - 25th International Symposium on Logic-Based Program Synthesis and Transformation, LOPSTR 2015

Y2 - 13 July 2015 through 15 July 2015

ER -