Verifying the Correctness of Tupling Transformations based on Conditional Rewriting

ABSTRACT. Chiba et al.\ (2010) proposed a framework of program transformation by templates based on term rewriting. Their framework can deal with tupling, which improve efficiency of programs. Outputs of their framework, however, may not always more efficient than inputs. In this paper, we propose a technique to show the correctness of tupling based on conditional term rewriting. We give an extended equational logic in order to add conditional rules.