Program transformation by templates based on term rewriting

Yuki Chiba, Takahito Aoto, Yoshihito Toyama

Research output: Chapter in Book/Report/Conference proceedingConference contribution

11 Citations (Scopus)

Abstract

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.

Original languageEnglish
Title of host publicationPPDP'05 - Proceedings of the Seventh ACM SIGPLAN Conference on Principles and Practice of Declarative Programming
Pages59-69
Number of pages11
DOIs
Publication statusPublished - 2005 Dec 1
EventPPDP'05 - 7th ACM SIGPLAN Conference on Principles and Practice of Declarative Programming - Lisbon, Portugal
Duration: 2005 Jul 112005 Jul 13

Publication series

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

Other

OtherPPDP'05 - 7th ACM SIGPLAN Conference on Principles and Practice of Declarative Programming
CountryPortugal
CityLisbon
Period05/7/1105/7/13

Keywords

  • Inductive Theorem Proving
  • Program Transformation
  • Term Rewriting
  • Tree Homomorphism

ASJC Scopus subject areas

  • Engineering(all)

Fingerprint Dive into the research topics of 'Program transformation by templates based on term rewriting'. Together they form a unique fingerprint.

  • Cite this

    Chiba, Y., Aoto, T., & Toyama, Y. (2005). Program transformation by templates based on term rewriting. In PPDP'05 - Proceedings of the Seventh ACM SIGPLAN Conference on Principles and Practice of Declarative Programming (pp. 59-69). (PPDP'05 - Proceedings of the Seventh ACM SIGPLAN Conference on Principles and Practice of Declarative Programming; Vol. 2005). https://doi.org/10.1145/1069774.1069780