Top > JACIII > Expanding Transformation: A Basis for Correctness Verification ...

single-jc.php

JACIII Vol.11 No.5 pp. 478-490
doi: 10.20965/jaciii.2007.p0478
(2007)

Paper:

Views over last 60 days: 465

Expanding Transformation: A Basis for Correctness Verification of Rewriting Rules

Ekawit Nantajeewarawat*, Kiyoshi Akama**, and Hidekatsu Koike***

*Computer Science Program, Sirindhorn International Institute of Technology, Thammasat University, Rangsit Campus, P.O. Box 22, Thammasat-Rangsit Post Office, Pathumthani 12121, Thailand

**Division of Large-Scale Computational Systems, Information Initiative Center, Hokkaido University, Kita 11 Nishi 5, Kita-ku, Sapporo, Hokkaido 060-0811, Japan

***Faculty of Social Information, Sapporo Gakuin University, 11 Bunkyodai, Ebetsu, Hokkaido 060-8555, Japan

Received:
November 21, 2006
Accepted:
March 2, 2007
Published:
June 20, 2007
Creative Commons License
Keywords:
expanding transformation, rule-based equivalent transformation, rewriting rules, metacomputation, correctness verification
Abstract
Unfolding transformation has long been used for computation and program transformation both in functional programming and logic programming paradigms. In this paper, we clarify that an unfolding step can be regarded as the composition of two simpler operations, i.e., expanding transformation and unification, and show that expanding transformation, rather than unfolding transformation, is a suitable basis for verifying the correctness of rewriting rules by pattern manipulation, which in turn provides a basis for systematically generating rewriting rules from a given problem description. We verify the correctness of expanding transformation and demonstrate the correctness of a basic class of rewriting rules, called general rewriting rules, based on expanding transformation. Applying expanding transformation and its correctness result, we demonstrate correctness verification of a larger class of rewriting rules, called expanding-based rewriting rules, by transformation of clause patterns.
Cite this article as:
E. Nantajeewarawat, K. Akama, and H. Koike, “Expanding Transformation: A Basis for Correctness Verification of Rewriting Rules,” J. Adv. Comput. Intell. Intell. Inform., Vol.11 No.5, pp. 478-490, 2007.
Data files:
References
  1. [1] R. Bird, “Introduction to Functional Programming,” second edition, Prentice Hall, 1998.
  2. [2] R. M. Burstall and J. Darlington, “A Transformation System for Developing Recursive Programs,” Journal of the ACM, Vol.24, No.1, pp. 44-67, 1977.
  3. [3] D. Sands, “Total Correctness by Local Improvement in the Transformation of Functional Programs,” ACM Transactions on Programming Languages and Systems, Vol.18, No.2, pp. 175-234, 1996.
  4. [4] J. A. Robinson, “A Machine-Oriented Logic Based on the Resolution Principle,” Journal of the ACM, Vol.12, pp. 23-41, 1965.
  5. [5] D. De Schreye, R. Glück, J. Jørgensen, M. Leuschel, B. Martens, and M. H. Sørensen, “Conjunctive Partial Deduction: Foundations, Control, Algorithms, and Experiments,” Journal of Logic Programming, Vol.41, pp. 231-277, 1999.
  6. [6] A. Pettorossi and M. Proietti, “Transformation of Logic Programs,” in D. M. Gabbay, C. J. Hogger, and J. A. Robinson (Eds.), Handbook of Logic in Artificial Intelligence and Logic Programming, Vol.5, Oxford University Press, pp. 697-787, 1998.
  7. [7] A. Pettorossi and M. Proietti, “Synthesis and Transformation of Logic Programs using Unfold/fold Proofs,” Journal of Logic Programming, Vol.41, pp. 197-230, 1999.
  8. [8] K. Tamaki and T. Sato, “Unfold/Fold Transformation of Logic Programs,” in Proc. the 2nd International Conference on Logic Programming, Uppsala, Sweden, pp. 127-138, 1984.
  9. [9] K. Akama, Y. Kawaguchi, and E. Miyamoto, “Solving Logical Problems by Equivalent Transformation – Limitations of SLD Resolution,” Journal of the Japanese Society for Artificial Intelligence, Vol.13, pp. 936-943, 1998.
  10. [10] K. Akama, E. Nantajeewarawat, and H. Koike, “A Class of Rewriting Rules and Reverse Transformation for Rule-Based Equivalent Transformation,” Electronic Notes in Theoretical Computer Science, Vol.59, No.4, pp. 1-16, 2001.
  11. [11] K. Akama, E. Nantajeewarawat, and H. Koike, “Program Generation in the Equivalent Transformation Computation Model Using the Squeeze Method,” Lecture Notes in Computer Science, Vol.4378, pp. 41-54, 2007. (A revised and extended paper from the Sixth International Conference on Perspectives of System Informatics, Novosibirsk, Russia, September 2006.)
  12. [12] J. W. Lloyd, “Foundations of Logic Programming,” second, extended edition, Springer-Verlag, 1987.
  13. [13] K. Akama, T. Shimizu, and E. Miyamoto, “Solving Problems by Equivalent Transformation of Declarative Programs,” Journal of the Japanese Society for Artificial Intelligence, Vol.13, pp. 944-952, 1998.
  14. [14] K. Akama and E. Nantajeewarawat, “Formalization of the Equivalent Transformation Computation Model,” Journal of Advanced Computational Intelligence and Intelligent Informatics, Vol.10, No.3, pp. 245-259, 2006.
  15. [15] K. Akama, Y. Nomura, and E. Miyamoto, “Semantic Interpretation of Natural Language Descriptions by Program Transformation,” Computer Software, Vol.12, No.5, pp. 45-62, 1995.
  16. [16] V. Wuwongse, C. Anutariya, K. Akama, and E. Nantajeewarawat, “XML Declarative Description: A Language for the Semantic Web,” IEEE Intelligent Systems, Vol.16, No.3, pp. 54-65, 2001.
  17. [17] V. Wuwongse, K. Akama, C. Anutariya, and E. Nantajeewarawat, “A Data Model for XML Databases,” Journal of Intelligent Information Systems, Vol.20, No.1, pp. 63-80, 2003.
  18. [18] C. Anutariya, V. Wuwongse, K. Akama, and E. Nantajeewarawat, “RDF Declarative Description (RDD): A Language for Metadata,” Journal of Digital Information, Vol.2, No.2, 2001.
  19. [19] E. Nantajeewarawat, V. Wuwongse, C. Anutariya, K. Akama, and S. Thiemjarus, “Toward Reasoning with Unified Modeling Language Diagrams Based-on Extensible Markup Language Declarative Description Theory,” International Journal of Intelligent Systems, Vol.19, pp. 89-98, 2004.
  20. [20] E. Nantajeewarawat and V. Wuwongse, “Knowledge-Based Inconsistency Detection in UML Models,” in S. K. Chang (Ed.), Handbook of Software Engineering & Knowledge Engineering, Vol.3, World Scientific Publishing, pp. 177-201, 2005.
  21. [21] H. Koike, K. Akama, and E. Boyd, “Program Synthesis by Generating Equivalent Transformation Rules,” in Proc. the 2nd International Conference on Intelligent Technologies, Bangkok, Thailand, pp. 250-259, 2001.
  22. [22] K. Akama, E. Nantajeewarawat, and H. Koike, “Componentwise Program Construction: Requirements and Solutions,” WSEAS Transactions on Information Science and Applications, Vol.3, No.7, pp. 1214-1221, 2006.
  23. [23] L. Sterling and E. Shapiro, “The Art of Prolog,” MIT Press, 1986.

Creative Commons License  This article is published under a Creative Commons Attribution-NoDerivatives 4.0 Internationa License.

*This site is desgined based on HTML5 and CSS3 for modern browsers, e.g. Chrome, Firefox, Safari, Edge, Opera.

Last updated on Apr. 19, 2024