TY - GEN

T1 - Program transformation by templates based on term rewriting

AU - Chiba, Yuki

AU - Aoto, Takahito

AU - Toyama, Yoshihito

PY - 2005/12/1

Y1 - 2005/12/1

N2 - Huet and Lang (1978) presented a framework of automated program transformation based on lambda calculus in which programs are transformed according to a given program transformation template. They introduced a second-order matching algorithm of simply-typed lambda calculus to verify whether the input program matches the template. They also showed how to validate the correctness of the program transformation using the denotational semantics. We propose in this paper a framework of program transformation by templates based on term rewriting. In our new framework, programs are given by term rewriting systems. To automate our program transformation, we introduce a term pattern matching problem and present a sound and complete algorithm that solves this problem. We also discuss how to validate the correctness of program transformation in our framework. We introduce a notion of developed templates and a simple method to construct such templates without explicit use of induction. We then show that in any program transformation by developed templates the correctness of the transformation can be verified automatically. In our framework the correctness of the program transformation is discussed based on the operational semantics. This is a sharp contrast to Huet and Lang's framework.

AB - Huet and Lang (1978) presented a framework of automated program transformation based on lambda calculus in which programs are transformed according to a given program transformation template. They introduced a second-order matching algorithm of simply-typed lambda calculus to verify whether the input program matches the template. They also showed how to validate the correctness of the program transformation using the denotational semantics. We propose in this paper a framework of program transformation by templates based on term rewriting. In our new framework, programs are given by term rewriting systems. To automate our program transformation, we introduce a term pattern matching problem and present a sound and complete algorithm that solves this problem. We also discuss how to validate the correctness of program transformation in our framework. We introduce a notion of developed templates and a simple method to construct such templates without explicit use of induction. We then show that in any program transformation by developed templates the correctness of the transformation can be verified automatically. In our framework the correctness of the program transformation is discussed based on the operational semantics. This is a sharp contrast to Huet and Lang's framework.

KW - Inductive Theorem Proving

KW - Program Transformation

KW - Term Rewriting

KW - Tree Homomorphism

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

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

U2 - 10.1145/1069774.1069780

DO - 10.1145/1069774.1069780

M3 - Conference contribution

AN - SCOPUS:33746037594

SN - 1595930906

SN - 9781595930903

T3 - PPDP'05 - Proceedings of the Seventh ACM SIGPLAN Conference on Principles and Practice of Declarative Programming

SP - 59

EP - 69

BT - PPDP'05 - Proceedings of the Seventh ACM SIGPLAN Conference on Principles and Practice of Declarative Programming

T2 - PPDP'05 - 7th ACM SIGPLAN Conference on Principles and Practice of Declarative Programming

Y2 - 11 July 2005 through 13 July 2005

ER -