Top > JACIII > Design of Nondeterministic Program Termination Based on the Eq ...

single-jc.php

JACIII Vol.10 No.3 pp. 349-361
doi: 10.20965/jaciii.2006.p0349
(2006)

Paper:

Views over last 60 days: 596

Design of Nondeterministic Program Termination Based on the Equivalent Transformation Computation Model

Itaru Takarajima*, Kiyoshi Akama**, Ikumi Imani***,
and Hiroshi Mabuchi****

*Department of Commerce, Nagoya Gakuin University, 1350 Kami-Shinano, Seto, Aichi 480-1298, Japan

**Information Initiative Center, Hokkaido University, Sapporo, Japan

***Department of Foreign Studies, Nagoya Gakuin University, Seto, Japan

****Faculty of Software and Information Science, Iwate Prefectural University, Iwate, Japan

Received:
February 22, 2005
Accepted:
December 21, 2005
Published:
May 20, 2006
Creative Commons License
Keywords:
termination, nondeterministic program, equivalent transformation
Abstract
We studied the termination of nondeterministic programs, which play an important, basic role in program synthesis, and provide a foundation for proving program termination. The class of programs we consider here is based on the equivalent transformation (ET) computation model. Computation with this model involves the succesive application of rules to sets of clauses. Since the ET model has more expressive terms and rules than other programming languages, program termination is difficult to prove: we must take into account all possible changes of terms made by various rules. We propose a sufficient condition of ET program termination that proves termination by checking each rule in a given program. We also provide an algorithm for this check.
Cite this article as:
I. Takarajima, K. Akama, I. Imani, and H. Mabuchi, “Design of Nondeterministic Program Termination Based on the Equivalent Transformation Computation Model,” J. Adv. Comput. Intell. Intell. Inform., Vol.10 No.3, pp. 349-361, 2006.
Data files:
References
  1. [1] K. Akama, T. Shimizu, and E. Miyamoto, “Solving Problems by Equivalent Transformation of Declarative Programs,” J. Japanese Society for Artificial Intelligence, 13(6): pp. 944-952, 1998.
  2. [2] K. Akama, E. Nantajeewarawat, and H. Koike, “Program Synthesis Based on the Equivalent Transformation Computation Model,” Proc. 12th International Workshop on Logic Based Program Development and Transformation, pp. 285-304, 2002.
  3. [3] K. Akama, and E. Nantajeewarawat, “Formalization of Computation Models in View of Program Synthesis,” Proc. of the 4th International Conference on Intelligent Technologies (InTech’03), pp. 507-516, 2003.
  4. [4] K. Akama, and E. Nantajeewarawat, “Formalization Of The Equivalent Transformation Computations Model,” Proc. of the 5th International Conference on Intelligent Technologies (InTech’04), pp. 190-199, 2004.
  5. [5] K. Akama, and E. Nantajeewarawat, “State-Transition Computation Models and Program Correctness Thereon,” The 6th International Conference on Intelligent Technologies (InTech’05), under review.
  6. [6] C. S. Lee, N. D. Jones, and A. M. Ben-Amram, “The size-change principle for program termination,” Proc. of POPL, pp. 81-92, 2001.
  7. [7] S. Decorte, and D. De Schreya, “Termination of logic programs: the never-ending story,” J. of Logic Programming, 19-20: pp. 199-260, 1994.
  8. [8] K. Doets, “From Logic to Logic Programming,” MIT Press, 1994.
  9. [9] T. Frühwirth, “Theory and Practice of Constraint Handling Rules,” Journal of Logic Programming, Special Issue on Constraint Logic Programming, 37(1-3): pp. 95-138, 1998.
  10. [10] H. Anderson, and S.-C. Khoo, “Affine-Based Size-Change Termination,” Proc. of APLAS, pp. 122-140, 2003.
  11. [11] J. Jaffar, and J.-L. Lassez, “Constraint Logic Programming,” Proc. 14th Ann. ACM Symp. Principles of Programming Languages, pp. 111-119, 1987.
  12. [12] J. Jaffar, and M. Maher, “Constraint Logic Programming: A Survey,” J. of Logic Programming, 19,20: pp. 503-581, 1994.
  13. [13] J. W. Klop, “Term Rewriting Systems,” Handbook of Logic in Computer Science, 2: pp. 1-116, Oxford University Press, New York, 1992.
  14. [14] H. Koike, K. Akama, T. Tsuji, and H. Mabuchi, “Computation Mechanism for Set Expressions,” World Multiconference on Systemics, Cybernetics and Informatics, Volume VII, Computer Science and Engineering: part I, pp. 29-34, 2001.
  15. [15] J. W. Lloyd, “Foundations of Logic Programming,” Second Edition, p. 212, Springer-Verlag, 1987.
  16. [16] H. Ogasawara, K. Akama, H. Koike, H. Mabuchi, and Y. Saito, “Parallel Processing Method based on Equivalent Transformation,” 9th International Conference on Intelligent Engineering Systems 2005, to appear.
  17. [17] C. A. Petri, “Nets, Time and Space,” Theoretical Computer Science, 153: pp. 3-48, 1996.
  18. [18] E. Tsang, “Foundations of Constraint Satisfaction,” Academic Press, 1993.
  19. [19] P. van Hentenryck, H. Simonis, and M. Dincbas, “Constraint satisfaction using constraint logic programming,” Artificial Intelligence, 58: pp. 113-159, 1992.

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. 22, 2024