The Construction and Computation of for-loop Programs for SCMPDS

Jing-Chao Chen

Shanghai Jiaotong University

Piotr Rudnicki

University of Alberta

Summary.

This article defines two for-loop statements for SCMPDS. One is called for-up, which corresponds to ``for (i=x; i$<$0; i+=n) S'' in C language. Another is called for-down, which corresponds to ``for (i=x; i$>$0; i-=n) S''. Here, we do not present their unconditional halting (called parahalting) property, because we have not found that there exists a useful for-loop statement with unconditional halting, and the proof of unconditional halting is much simpler than that of conditional halting. It is hard to formalize all halting conditions, but some cases can be formalized. We choose loop invariants as halting conditions to prove halting problem of for-up/down statements. When some variables (except the loop control variable) keep undestroyed on a set for the loop invariant, and the loop body is halting for this condition, the corresponding for-up/down is halting and computable under this condition. The computation of for-loop statements can be realized by evaluating its body. At the end of the article, we verify for-down statements by two examples for summing.

This research is partially supported by the National Natural Science Foundation of China Grant No. 69873033.

MML Identifier: SCMPDS_7

Contents (PDF format)

1. Preliminaries
2. The Construction of for-up loop Program
3. The Computation of for-up loop Program
4. The Construction of for-down loop Program
5. The Computation of for-down loop Program
6. Two Examples for Summing

Bibliography

[1] Grzegorz Bancerek. Cardinal numbers. Journal of Formalized Mathematics, 1, 1989.

[2] Grzegorz Bancerek. The fundamental properties of natural numbers. Journal of Formalized Mathematics, 1, 1989.

[3] Grzegorz Bancerek. Joining of decorated trees. Journal of Formalized Mathematics, 5, 1993.

[4] Grzegorz Bancerek and Krzysztof Hryniewiecki. Segments of natural numbers and finite sequences. Journal of Formalized Mathematics, 1, 1989.

[5] Grzegorz Bancerek and Piotr Rudnicki. Development of terminology for \bf scm. Journal of Formalized Mathematics, 5, 1993.

[6] Grzegorz Bancerek and Andrzej Trybulec. Miscellaneous facts about functions. Journal of Formalized Mathematics, 8, 1996.

[7] Czeslaw Bylinski. Functions and their basic properties. Journal of Formalized Mathematics, 1, 1989.

[8] Czeslaw Bylinski. A classical first order language. Journal of Formalized Mathematics, 2, 1990.

[9] Czeslaw Bylinski. The modification of a function by a function and the iteration of the composition of a function. Journal of Formalized Mathematics, 2, 1990.

[10] Jing-Chao Chen. Computation and program shift in the SCMPDS computer. Journal of Formalized Mathematics, 11, 1999.

[11] Jing-Chao Chen. Computation of two consecutive program blocks for SCMPDS. Journal of Formalized Mathematics, 11, 1999.

[12] Jing-Chao Chen. The construction and computation of conditional statements for SCMPDS. Journal of Formalized Mathematics, 11, 1999.

[13] Jing-Chao Chen. The construction and shiftability of program blocks for SCMPDS. Journal of Formalized Mathematics, 11, 1999.

[14] Jing-Chao Chen. Recursive Euclide algorithm. Journal of Formalized Mathematics, 11, 1999.

[15] Jing-Chao Chen. The SCMPDS computer and the basic semantics of its instructions. Journal of Formalized Mathematics, 11, 1999.

[16] Andrzej Kondracki. The Chinese Remainder Theorem. Journal of Formalized Mathematics, 9, 1997.

[17] Yatsuka Nakamura and Andrzej Trybulec. A mathematical model of CPU. Journal of Formalized Mathematics, 4, 1992.

[18] Yatsuka Nakamura and Andrzej Trybulec. On a mathematical model of programs. Journal of Formalized Mathematics, 4, 1992.

[19] Jan Popiolek. Some properties of functions modul and signum. Journal of Formalized Mathematics, 1, 1989.

[20] Yasushi Tanaka. On the decomposition of the states of SCM. Journal of Formalized Mathematics, 5, 1993.

[21] Andrzej Trybulec. Enumerated sets. Journal of Formalized Mathematics, 1, 1989.

[22] Andrzej Trybulec. Tarski Grothendieck set theory. Journal of Formalized Mathematics, Axiomatics, 1989.

[23] Andrzej Trybulec. Subsets of real numbers. Journal of Formalized Mathematics, Addenda, 2003.

[24] Andrzej Trybulec and Yatsuka Nakamura. Some remarks on the simple concrete model of computer. Journal of Formalized Mathematics, 5, 1993.

[25] Michal J. Trybulec. Integers. Journal of Formalized Mathematics, 2, 1990.

[26] Edmund Woronowicz. Relations and their basic properties. Journal of Formalized Mathematics, 1, 1989.