Recursive Euclide Algorithm

Jing-Chao Chen

Shanghai Jiaotong University

Summary.

The earlier SCM computer did not contain recursive function, so Trybulec and Nakamura proved the correctness of the Euclid's algorithm only by way of an iterative program. However, the recursive method is a very important programming method, furthermore, for some algorithms, for example Quicksort, only by employing a recursive method (note push-down stack is essentially also a recursive method) can they be implemented. The main goal of the article is to test the recursive function of the SCMPDS computer by proving the correctness of the Euclid's algorithm by way of a recursive program. In this article, we observed that the memory required by the recursive Euclide algorithm is variable but it is still autonomic. Although the algorithm here is more complicated than the non-recursive algorithm, its focus is that the SCMPDS computer will be able to implement many algorithms like Quicksort which the SCM computer cannot do.

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

MML Identifier: SCMP_GCD

Contents (PDF format)

1. Preliminaries
2. The Construction of Recursive Euclide Algorithm
3. The Computation of Recursive Euclide Algorithm
4. The Correctness of Recursive Euclide Algorithm
5. The Autonomy of Recursive Euclide Algorithm

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] Czeslaw Bylinski. Functions and their basic properties. Journal of Formalized Mathematics, 1, 1989.

[4] 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.

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

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

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

[8] Jing-Chao Chen. A small computer model with push-down stack. Journal of Formalized Mathematics, 11, 1999.

[9] Rafal Kwiatek and Grzegorz Zwara. The divisibility of integers and integer relatively primes. Journal of Formalized Mathematics, 2, 1990.

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

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

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

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

[14] Wojciech A. Trybulec. Groups. Journal of Formalized Mathematics, 2, 1990.

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