Program transformation by templates based on term rewriting

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.

REFERENCES

• 1: Franz Baader , Tobias Nipkow, Term rewriting and all that, Cambridge University Press, New York, NY, 1998
• 2: A. Bouhoula, E. Kounalis, and M. Rusinowitch. Automated mathematical induction. Journal of Logic and Computation, 5(5):631--668, 1995.
• 3: H. Comon, M. Dauchet, R. Gilleron, F. Jacquemard, D. Lugiez, S. Tison, and M. Tommasi. Tree Automata Techniques and Applications. 1997.
• 4: Régis Curien , Zhenyu Qian , Hui Shi, Efficient Second-Order Matching, Proceedings of the 7th International Conference on Rewriting Techniques and Applications, p.317-331, July 27-30, 1996
• 5: O. de Moor and G. Sittampalam. Generic program transformation. In Proceedings of the 3rd International Summer School on Advanced Functional Programming, volume 1608 of LNCS, pages 116--149. Springer-Verlag, 1999.
• 6: O. de Moor and G. Sittampalam. Higher-order matching for program transformation. Theoretical Computer Science, 269:135--162, 2001.
• 7: J. Giesl, R. Thiemann, P. Schneider-Kamp, and S. Falke. Automated termination proofs with AProVE. In Proceedings of the 15th International Conference on Rewriting Techniques and Applications, volume 3091 of LNCS, pages 210--220. Springer-Verlag, 2004.
• 8: K. Hirata, K. Yamada, and M. Harao. Tractable and intractable second-order matching problems. Journal of Symbolic Computation, 37(5):611--628, 2004.
• 9: N. Hirokawa and A. Middeldorp. Tsukuba termination tool. In Proceedings of the 14th International Conference on Rewriting Techniques and Applications, volume 2706 of LNCS, pages 311--320. Springer-Verlag, 2003.
• 10: G. Huet. A unification algorithm for typed λ-calculus. Theoretical Computer Science, 1:27--57, 1975.
• 11: G. Huet and B. Lang. Proving and applying program transformations expressed with second order patterns. Acta Informatica, 11:31--55, 1978.
• 12: S. Kamin and J.-J. Lévy. Two generalizations of the recursive path ordering. Unpublished manuscript, University of Illinois, 1980.
• 13: Uday S. Reddy, Term rewriting induction, Proceedings of the tenth international conference on Automated deduction, p.162-177, July 1990, Kaiserslautern, Germany
• 14: G. Sittampalam. Higher-Order Matching for Program Transformation. PhD thesis, Magdalen College, 2001.
• 15: Terese. Term Rewriting Systems. Cambridge University Press, 2003.
• 16: Y. Toyama. Commutativity of term rewriting systems. In The Second France-Japan Artificial Intelligence and Computer Science Symposium, 1987.
• 17: Yoshihito Toyama, How to prove equivalence of term rewriting systems without induction, Theoretical Computer Science, v.90 n.2, p.369-390, Nov. 25, 1991 [doi>10.1016/0304-3975(91)90004-L ]
• 18: Eelco Visser. A survey of rewriting strategies in program transformation systems. In Workshop on Reduction Strategies in Rewriting and Programming, volume~57 of Electronic Notes in Theoretical Computer Science. Elsevier Science Publishers, 2001.
• 19: Tetsuo Yokoyama , Zhenjiang Hu , Masato Takeichi, Deterministic second-order patterns, Information Processing Letters, v.89 n.6, p.309-314, 31 March 2004 [doi>10.1016/j.ipl.2003.12.008]

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.1 Formal Definitions and Theory

Additional Classification:
  D. Software
  D.1 PROGRAMMING TECHNIQUES
      D.1.2 Automatic Programming

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.2 Grammars and Other Rewriting Systems

Keywords:
inductive theorem proving, program transformation, term rewriting, tree homomorphism