Journal of Formalized Mathematics
Volume 11, 1999
University of Bialystok
Copyright (c) 1999
Association of Mizar Users
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.
The terminology and notation used in this paper have been
introduced in the following articles
[15]
[3]
[13]
[2]
[4]
[10]
[11]
[12]
[8]
[7]
[5]
[1]
[6]
[14]
[9]
-
Preliminaries
-
The Construction of Recursive Euclide Algorithm
-
The Computation of Recursive Euclide Algorithm
-
The Correctness of Recursive Euclide Algorithm
-
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.
Received June 15, 1999
[
Download a postscript version,
MML identifier index,
Mizar home page]