Proving Equality of Simply Typed Term Rewriting System


Chiba et al. (2005, 2006, 2010) proposed a framework of program
transformation by templates based on term rewriting. They introduced a
notion of correct templates, which guarantee the correctness of
transformations for restricted class of term rewriting systems. 

Since their framework is based on first-order term rewriting, it is hard to
apply their method to transform higher-order programs. We propose a new
method to prove the equality of simply typed term rewriting systems
(STTRSs, for short) as an initial step to extend their framework for
higher-order setting. We modify the notion of equivalent transformation of
STTRSs and give sufficient conditions to guarantee the equality of STTRSs
based on the notion of equivalent transformation.