Journal of Formalized Mathematics
Volume 11, 1999
University of Bialystok
Copyright (c) 1999
Association of Mizar Users
Definitions of Radix-$2^k$ Signed-Digit Number and its Adder Algorithm
-
Yoshinori Fujisawa
-
Shinshu University, Nagano
-
Yasushi Fuwa
-
Shinshu University, Nagano
Summary.
-
In this article, a radix-$2^k$ signed-digit number (Radix-$2^k$ SD number)
is defined and based on it a high-speed adder algorithm is discussed. \par
The
processes of coding and encoding for public-key cryptograms require a
great deal of addition operations of natural number of many figures.
This results in a~long time for the encoding and decoding processes. It
is possible to reduce the processing time using the high-speed adder
algorithm.\par
In the first section of this article, we prepared some useful theorems
for natural
numbers and integers. In the second section, we defined the concept
of radix-$2^k$, a set named $k$-SD and proved some properties about
them.
In the third section, we provide some important functions for
generating Radix-$2^k$ SD numbers from natural numbers and natural numbers
from Radix-$2^k$ SD numbers. In the fourth section, we defined the carry
and data components of addition with Radix-$2^k$ SD numbers and some
properties about them. In the fifth section, we defined a theorem for
checking whether or not a natural number can be expressed as $n$ digits
Radix-$2^k$ SD number. \par
In the last section, a high-speed adder algorithm
on Radix-$2^k$ SD numbers is proposed and we provided some properties.
In this algorithm, the carry of each digit has an effect on only the
next digit. Properties of the relationships of the results of this
algorithm to the operations of natural numbers are also given.
MML Identifier:
RADIX_1
The terminology and notation used in this paper have been
introduced in the following articles
[8]
[11]
[9]
[1]
[4]
[7]
[3]
[10]
[6]
[2]
[5]
-
Some Useful Theorems
-
Definition for Radix-$2^k$, $k$-SD
-
Functions for Generating Radix-$2^k$ SD Numbers from Natural Numbers
and Natural Numbers from Radix-$2^k$ SD Numbers
-
Definition for Carry and Data Components of Addition
-
Definition for Checking whether or not a Natural Number can be Expressed
as n Digits Radix-$2^k$ SD Number
-
Definition for Addition Operation for a High-Speed Adder Algorithm
on Radix-$2^k$ SD Number
Bibliography
- [1]
Grzegorz Bancerek.
The fundamental properties of natural numbers.
Journal of Formalized Mathematics,
1, 1989.
- [2]
Grzegorz Bancerek.
Joining of decorated trees.
Journal of Formalized Mathematics,
5, 1993.
- [3]
Grzegorz Bancerek and Krzysztof Hryniewiecki.
Segments of natural numbers and finite sequences.
Journal of Formalized Mathematics,
1, 1989.
- [4]
Czeslaw Bylinski.
Functions and their basic properties.
Journal of Formalized Mathematics,
1, 1989.
- [5]
Andrzej Kondracki.
The Chinese Remainder Theorem.
Journal of Formalized Mathematics,
9, 1997.
- [6]
Takaya Nishiyama and Yasuho Mizuhara.
Binary arithmetics.
Journal of Formalized Mathematics,
5, 1993.
- [7]
Konrad Raczkowski and Andrzej Nedzusiak.
Real exponents and logarithms.
Journal of Formalized Mathematics,
2, 1990.
- [8]
Andrzej Trybulec.
Tarski Grothendieck set theory.
Journal of Formalized Mathematics,
Axiomatics, 1989.
- [9]
Michal J. Trybulec.
Integers.
Journal of Formalized Mathematics,
2, 1990.
- [10]
Wojciech A. Trybulec.
Pigeon hole principle.
Journal of Formalized Mathematics,
2, 1990.
- [11]
Zinaida Trybulec.
Properties of subsets.
Journal of Formalized Mathematics,
1, 1989.
Received September 7, 1999
[
Download a postscript version,
MML identifier index,
Mizar home page]