Paper Info
Title
Correctness of Context-Moving Transformations for Term Rewriting Systems.
Abstract
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.
Year
DOI
Venue
2015
10.1007/978-3-319-27436-2_20
LOPSTR
Keywords
Field
DocType
Tail-recursion,Program transformation,Term rewriting system,Inductive theorem proving
Initial algebra,Program transformation,Eager evaluation,Computer science,Correctness,Algorithm,Theoretical computer science,Mathematical proof,Rewriting,Confluence,Tail call
Conference
Volume
ISSN
Citations 
9527
0302-9743
0
PageRank 
References 
Authors
0.34
7
4
Name
Order
Citations
PageRank
Koichi Sato112413.87
Kentaro Kikuchi2112.51
Takahito Aoto312117.53
Yoshihito Toyama453349.60