Formalized Mathematics    (ISSN 1898-9934 (Online), ISSN 1426-2630 (Print))
Volume 11, Number 2 (2003): pdf, ps, dvi.
  1. Masaaki Niimura, Yasushi Fuwa. Improvement of Radix-$2^k$ Signed-Digit Number for High Speed Circuit, Formalized Mathematics 11(2), pages 133-137, 2003. MML Identifier: RADIX_3
    Summary: In this article, a new radix-$2^k$ signed-digit number (Radix-$2^k$ sub signed-digit number) is defined and its properties for hardware realization are discussed. \par Until now, high speed calculation method with Radix-$2^k$ signed-digit numbers is proposed, but this method used ``Compares With 2" to calculate carry. ``Compares with 2'' is a very simple method, but it needs very complicated hardware especially when the value of $k$ becomes large. In this article, we propose a subset of Radix-$2^k$ signed-digit, named Radix-$2^k$ sub signed-digit numbers. Radix-$2^k$ sub signed-digit was designed so that the carry calculation use ``bit compare'' to hardware-realization simplifies more.\par In the first section of this article, we defined the concept of Radix-$2^k$ sub signed-digit numbers and proved some of their properties. In the second section, we defined the new carry calculation method in consideration of hardware-realization, and proved some of their properties. In the third section, we provide some functions for generating Radix-$2^k$ sub signed-digit numbers from Radix-$2^k$ signed-digit numbers. In the last section, we defined some functions for generation natural numbers from Radix-$2^k$ sub signed-digit, and we clarified its correctness.
  2. Masaaki Niimura, Yasushi Fuwa. High Speed Adder Algorithm with Radix-$2^k$ Sub Signed-Digit Number, Formalized Mathematics 11(2), pages 139-141, 2003. MML Identifier: RADIX_4
    Summary: In this article, a new adder algorithm using Radix-$2^k$ sub signed-digit numbers is defined and properties for the hardware-realization is discussed.\par Until now, we proposed Radix-$2^k$ sub signed-digit numbers in consideration of the hardware realization. In this article, we proposed High Speed Adder Algorithm using this Radix-$2^k$ sub signed-digit numbers. This method has two ways to speed up at hardware-realization. One is 'bit compare' at carry calculation, it is proposed in another article. Other is carry calculation between two numbers. We proposed that $n$ digits Radix-$2^k$ signed-digit numbers is expressed in $n+1$ digits Radix-$2^k$ sub signed-digit numbers, and addition result of two $n+1$ digits Radix-$2^k$ sub signed-digit numbers is expressed in $n+1$ digits. In this way, carry operation between two Radix-$2^k$ sub signed-digit numbers can be processed at $n+1$ digit adder circuit and additional circuit to operate carry is not needed.\par In the first section of this article, we prepared some useful theorems for operation of Radix-$2^k$ numbers. In the second section, we proved some properties about carry on Radix-$2^k$ sub signed-digit numbers. In the last section, we defined the new addition operation using Radix-$2^k$ sub signed-digit numbers, and we clarified its correctness.
  3. Jing-Chao Chen, Yatsuka Nakamura. The Underlying Principle of Dijkstra's Shortest Path Algorithm, Formalized Mathematics 11(2), pages 143-152, 2003. MML Identifier: GRAPH_5
    Summary: A path from a source vertex $v$ to a target vertex $u$ is said to be a shortest path if its total cost is minimum among all $v$-to-$u$ paths. Dijkstra's algorithm is a classic shortest path algorithm, which is described in many textbooks. To justify its correctness (whose rigorous proof will be given in the next article), it is necessary to clarify its underlying principle. For this purpose, the article justifies the following basic facts, which are the core of Dijkstra's algorithm. \begin{itemize} \itemsep-3pt \item A graph is given, its vertex set is denoted by $V.$ Assume $U$ is the subset of $V,$ and if a path $p$ from $s$ to $t$ is the shortest among the set of paths, each of which passes through only the vertices in $U,$ except the source and sink, and its source and sink is $s$ and in $V,$ respectively, then $p$ is a shortest path from $s$ to $t$ in the graph, and for any subgraph which contains at least $U,$ it is also the shortest. \item Let $p(s,x,U)$ denote the shortest path from $s$ to $x$ in a subgraph whose the vertex set is the union of $\{s,x\}$ and $U,$ and cost $(p)$ denote the cost of path $p(s,x,U),$ cost$(x,y)$ the cost of the edge from $x$ to $y.$ Give $p(s,x,U),$ $q(s,y,U)$ and $r(s,y,U \cup \{x\})$. If ${\rm cost}(p) = {\rm min} \{{\rm cost}(w): w(s,t,U) \wedge t \in V\}$, then we have $${\rm cost}(r) = {\rm min} ({\rm cost}(p)+{\rm cost}(x,y),{\rm cost}(q)).$$ \end{itemize} \noindent This is the well-known triangle comparison of Dijkstra's algorithm.
  4. Adam Grabowski. On the Hausdorff Distance Between Compact Subsets, Formalized Mathematics 11(2), pages 153-157, 2003. MML Identifier: HAUSDORF
    Summary: In \cite{WEIERSTR.ABS} the pseudo-metric ${\rm dist}^{\rm max}_{\rm min}$ on compact subsets $A$ and $B$ of a topological space generated from arbitrary metric space is defined. Using this notion we define the Hausdorff distance (see e.g. \cite{Csaszar}) of $A$ and $B$ as a maximum of the two pseudo-distances: from $A$ to $B$ and from $B$ to $A$. We justify its distance properties. At the end we define some special notions which enable to apply the Hausdorff distance operator ${\rm ``HausDist"}$ to the subsets of the Euclidean topological space~$\calE^n_T.$
  5. Freek Wiedijk. Chains on a Grating in Euclidean Space, Formalized Mathematics 11(2), pages 159-167, 2003. MML Identifier: CHAIN_1
    Summary: Translation of pages 101, the second half of 102, and 103 of \cite{Newman51}.
  6. Hiroshi Yamazaki, Yasunari Shidama, Yatsuka Nakamura. Bessel's Inequality, Formalized Mathematics 11(2), pages 169-173, 2003. MML Identifier: BHSP_5
    Summary: In this article we defined the operation of a set and proved Bessel's inequality. In the first section, we defined the sum of all results of an operation, in which the results are given by taking each element of a set. In the second section, we defined Orthogonal Family and Orthonormal Family. In the last section, we proved some properties of operation of set and Bessel's inequality.
  7. Hisayoshi Kunimune, Yatsuka Nakamura. A Representation of Integers by Binary Arithmetics and Addition of Integers, Formalized Mathematics 11(2), pages 175-178, 2003. MML Identifier: BINARI_4
    Summary: In this article, we introduce the new concept of 2's complement representation. Natural numbers that are congruent mod $n$ can be represented by the same $n$ bits binary. Using the concept introduced here, negative numbers that are congruent mod $n$ also can be represented by the same $n$ bit binary. We also show some properties of addition of integers using this concept.
  8. Kanchun , Yatsuka Nakamura. The Inner Product of Finite Sequences and of Points of $n$-dimensional Topological Space, Formalized Mathematics 11(2), pages 179-183, 2003. MML Identifier: EUCLID_2
    Summary: First, we define the inner product to finite sequences of real value. Next, we extend it to points of $n$-dimensional topological space ${\calE}^{n}_{\rmT}$. At the end, orthogonality is introduced to this space.
  9. Xiquan Liang. Solving Roots of Polynomial Equation of Degree 4 with Real Coefficients, Formalized Mathematics 11(2), pages 185-187, 2003. MML Identifier: POLYEQ_2
    Summary: In this paper, we describe the definition of the fourth degree algebraic equations and their properties. We clarify the relation between the four roots of this equation and its coefficient. Also, the form of these roots for various conditions is discussed. This solution is known as the Cardano solution.
  10. Artur Kornilowicz. Morphisms Into Chains. Part I, Formalized Mathematics 11(2), pages 189-195, 2003. MML Identifier: WAYBEL35
    Summary: This work is the continuation of formalization of \cite{CCL}. Items from 2.1 to 2.8 of Chapter 4 are proved.
  11. Shunichi Kobayashi. Propositional Calculus for Boolean Valued Functions. Part VII, Formalized Mathematics 11(2), pages 197-199, 2003. MML Identifier: BVFUNC25
    Summary: In this paper, we proved some elementary propositional calculus formulae for Boolean valued functions.
  12. Markus Moschner. Basic Notions and Properties of Orthoposets, Formalized Mathematics 11(2), pages 201-210, 2003. MML Identifier: OPOSET_1
    Summary: Orthoposets are defined. The approach is the standard one via order relation similar to common text books on algebra like \cite{Gratzer}.