<title>Abstract</title>Infinite-dimensional Newton methods can be effectively used to derive numerical proofs of the existence of solutions to partial differential equations (PDEs). In computer-assisted proofs of PDEs, the original problem is transformed into the infinite-dimensional Newton-type fixed point equation <inline-formula><alternatives><tex-math>$$w = - {\mathcal {L } }^{-1} {\mathcal {F } }(\hat{u}) + {\mathcal {L } }^{-1} {\mathcal {G } }(w)$$</tex-math><mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML">
<mml:mrow>
<mml:mi>w</mml:mi>
<mml:mo>=</mml:mo>
<mml:mo>-</mml:mo>
<mml:msup>
<mml:mrow>
<mml:mi>L</mml:mi>
</mml:mrow>
<mml:mrow>
<mml:mo>-</mml:mo>
<mml:mn>1</mml:mn>
</mml:mrow>
</mml:msup>
<mml:mi>F</mml:mi>
<mml:mrow>
<mml:mo>(</mml:mo>
<mml:mover>
<mml:mi>u</mml:mi>
<mml:mo>^</mml:mo>
</mml:mover>
<mml:mo>)</mml:mo>
</mml:mrow>
<mml:mo>+</mml:mo>
<mml:msup>
<mml:mrow>
<mml:mi>L</mml:mi>
</mml:mrow>
<mml:mrow>
<mml:mo>-</mml:mo>
<mml:mn>1</mml:mn>
</mml:mrow>
</mml:msup>
<mml:mi>G</mml:mi>
<mml:mrow>
<mml:mo>(</mml:mo>
<mml:mi>w</mml:mi>
<mml:mo>)</mml:mo>
</mml:mrow>
</mml:mrow>
</mml:math></alternatives></inline-formula>, where <inline-formula><alternatives><tex-math>$${\mathcal {L } }$$</tex-math><mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML">
<mml:mi>L</mml:mi>
</mml:math></alternatives></inline-formula> is a linearized operator, <inline-formula><alternatives><tex-math>$${\mathcal {F } }(\hat{u})$$</tex-math><mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML">
<mml:mrow>
<mml:mi>F</mml:mi>
<mml:mo>(</mml:mo>
<mml:mover>
<mml:mi>u</mml:mi>
<mml:mo>^</mml:mo>
</mml:mover>
<mml:mo>)</mml:mo>
</mml:mrow>
</mml:math></alternatives></inline-formula> is a residual, and <inline-formula><alternatives><tex-math>$${\mathcal {G } }(w)$$</tex-math><mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML">
<mml:mrow>
<mml:mi>G</mml:mi>
<mml:mo>(</mml:mo>
<mml:mi>w</mml:mi>
<mml:mo>)</mml:mo>
</mml:mrow>
</mml:math></alternatives></inline-formula> is a nonlinear term. Therefore, the estimations of <inline-formula><alternatives><tex-math>$$\Vert {\mathcal {L } }^{-1} {\mathcal {F } }(\hat{u}) \Vert $$</tex-math><mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML">
<mml:mrow>
<mml:mrow>
<mml:mo>‖</mml:mo>
</mml:mrow>
<mml:msup>
<mml:mrow>
<mml:mi>L</mml:mi>
</mml:mrow>
<mml:mrow>
<mml:mo>-</mml:mo>
<mml:mn>1</mml:mn>
</mml:mrow>
</mml:msup>
<mml:mi>F</mml:mi>
<mml:mrow>
<mml:mo>(</mml:mo>
<mml:mover>
<mml:mi>u</mml:mi>
<mml:mo>^</mml:mo>
</mml:mover>
<mml:mo>)</mml:mo>
</mml:mrow>
<mml:mrow>
<mml:mo>‖</mml:mo>
</mml:mrow>
</mml:mrow>
</mml:math></alternatives></inline-formula> and <inline-formula><alternatives><tex-math>$$\Vert {\mathcal {L } }^{-1}{\mathcal {G } }(w) \Vert $$</tex-math><mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML">
<mml:mrow>
<mml:mrow>
<mml:mo>‖</mml:mo>
</mml:mrow>
<mml:msup>
<mml:mrow>
<mml:mi>L</mml:mi>
</mml:mrow>
<mml:mrow>
<mml:mo>-</mml:mo>
<mml:mn>1</mml:mn>
</mml:mrow>
</mml:msup>
<mml:mrow>
<mml:mi>G</mml:mi>
<mml:mrow>
<mml:mo>(</mml:mo>
<mml:mi>w</mml:mi>
<mml:mo>)</mml:mo>
</mml:mrow>
<mml:mo>‖</mml:mo>
</mml:mrow>
</mml:mrow>
</mml:math></alternatives></inline-formula> play major roles in the verification procedures . In this paper, using a similar concept to block Gaussian elimination and its corresponding ‘Schur complement’ for matrix problems, we represent the inverse operator <inline-formula><alternatives><tex-math>$${\mathcal {L } }^{-1}$$</tex-math><mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML">
<mml:msup>
<mml:mrow>
<mml:mi>L</mml:mi>
</mml:mrow>
<mml:mrow>
<mml:mo>-</mml:mo>
<mml:mn>1</mml:mn>
</mml:mrow>
</mml:msup>
</mml:math></alternatives></inline-formula> as an infinite-dimensional operator matrix that can be decomposed into two parts: finite-dimensional and infinite-dimensional. This operator matrix yields a new effective realization of the infinite-dimensional Newton method, which enables a more efficient verification procedure compared with existing Nakao’s methods for the solution of elliptic PDEs. We present some numerical examples that confirm the usefulness of the proposed method. Related results obtained from the representation of the operator matrix as <inline-formula><alternatives><tex-math>$${\mathcal {L } }^{-1}$$</tex-math><mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML">
<mml:msup>
<mml:mrow>
<mml:mi>L</mml:mi>
</mml:mrow>
<mml:mrow>
<mml:mo>-</mml:mo>
<mml:mn>1</mml:mn>
</mml:mrow>
</mml:msup>
</mml:math></alternatives></inline-formula> are presented in the “Appendix”.

This paper is concerned with an explicit value of the embedding constant from W-1,W- q(Omega) to L-p(Omega) for a domain Omega subset of R-N (N is an element of N), where 1 &lt;= q &lt;= p &lt;=infinity. We previously proposed a formula for estimating the embedding constant on bounded and unbounded Lipschitz domains by estimating the norm of Stein's extension operator. Although this formula can be applied to a domain Omega that can be divided into a finite number of Lipschitz domains, there was room for improvement in terms of accuracy. In this paper, we report that the accuracy of the embedding constant is significantly improved by restricting Omega to a domain dividable into bounded convex domains.

A fast numerical verification method is proposed for evaluating the accuracy of numerical solutions for symmetric saddle point linear systems whose diagonal blocks of the coefficient matrix are semidefinite matrices. The method is based on results of an algebraic analysis of a block diagonal preconditioning. Some numerical experiments are present to illustrate the usefulness of the method.

This paper focuses on blow-up solutions of ordinary differential equations (ODEs). We present a method for validating blow-up solutions and their blow-up times, which is based on compactifications and the Lyapunov function validation method. The necessary criteria for this construction can be verified using interval arithmetic techniques. Some numerical examples are presented to demonstrate the applicability of our method. (C) 2016 Elsevier B.V. All rights reserved.

In this paper, we propose a verified numerical method for obtaining a sharp inclusion of the best constant for the embedding H-0(1)(Omega) hooked right arrow L-p (Omega) on a bounded convex domain in R-2. We estimate the best constant by computing the corresponding extremal function using a verified numerical computation. Verified numerical inclusions of the best constant on a square domain are presented. (C) 2016 Elsevier B.V. All rights reserved.

In this study, we examine the accurate matrix multiplication in floating-point arithmetic. We demonstrate the error-free transformations of matrix multiplication using high performance basic linear algebra subprograms. These transformations can be applied to accurately compute the product of two matrices using floating-point entries. A key technique for this calculation is error-free splitting in floating-point matrices. In this study, we improve upon our previous method by a posteriori validation using floating-point exception. In the method, we utilize the presence of overflow in a positive manner for detecting whether rounding error occurs. If overflow occurs, the result contains some exceptional values such as +/- and NaN, that is, the method fails by necessity. Otherwise, we can confirm that no rounding error occurs in the process. Therefore, reducing the possibility of overflow is important. The numerical results suggest that the proposed algorithm provides more accurate results compared with the original algorithm. Moreover, for the product of n x n matrices, when n5000, the new algorithm reduces the computing time for error-free transformation by an average of 20 % and up to 30 % compared with the original algorithm. Furthermore, the new algorithm can be used when matrix multiplication is performed using divide-and-conquer methods. Copyright (c) 2016 John Wiley & Sons, Ltd.

This paper is concerned with floating-point filters for a two dimensional orientation problem which is a basic problem in the field of computational geometry. If this problem is only approximately solved by floating-point arithmetic, then an incorrect result may be obtained due to accumulation of rounding errors. A floating-point filter can quickly guarantee the correctness of the computed result if the problem is well-conditioned. In this paper, a simple semi-static floating-point filter which handles floating-point exceptions such as overflow and underflow by only one branch is developed. In addition, an improved fully-static filter is developed.

In this paper, we propose a method for estimating the Sobolev-type embedding constant from W-1,W-q(Omega) to L-p(Omega) on a domain Omega subset of R-n (n = 2,3, ... ) with minimally smooth boundary (also known as a Lipschitz domain), where p is an element of(n/(n - 1), infinity) and q = np/(n + p). We estimate the embedding constant by constructing an extension operator from W-1,W-q(Omega) to W-1,W-q(R-n) and computing its operator norm. We also present some examples of estimating the embedding constant for certain domains.

Recently, new algorithms for accurate matrix multiplication have been developed by the authors. A characteristic of the algorithms is a high dependency on level-3 BIAS routines, which are highly optimized for several architectures. An error-free splitting for floating-point matrices is a key technique in the algorithms. In this paper, an improvement of the error-free splitting is focused on. It is shown by numerical examples that the accuracy of computed results of matrix products can be improved by the modified error-free splitting, compared to that by the previous algorithms. (C) 2015 Elsevier B.V. All rights reserved.

This paper is concerned with real interval arithmetic. We focus on interval matrix multiplication. Well-known algorithms for this purpose require the evaluation of several point matrix products to compute one interval matrix product. In order to save computing time we propose a method that modifies such known algorithm by partially using low-precision floating-point arithmetic. The modified algorithms work without significant loss of tightness of the computed interval matrix product but are about 30% faster than their corresponding original versions. The negligible loss of accuracy is rigorously estimated.

Improved componentwise error bounds for approximate solutions of linear systems are derived in the case where the coefficient of a given linear system is an H-matrix. One of the error bounds presented in this paper proves to be tighter than the existing error bound, which is effective especially for ill-conditioned cases. Numerical experiments are performed to illustrate the effect of the improvements.

This paper is concerned with factorization of symmetric and positive definite matrices which are extremely ill-conditioned. Following the results by Rump (1990), Oishi et al. (2007, 2009) and Ogita (2010), Ogita and Oishi (2012) derived an iterative algorithm for an accurate inverse matrix factorization based on Cholesky factorization for such ill-conditioned matrices. We analyze the behavior of the algorithm in detail and give reasons for convergency by the use of numerical error analysis. Main analysis is that each iteration reduces the condition number of a preconditioned matrix by a factor around the relative rounding error unit until convergence. This behavior is consistent with the numerical results.

This paper proposes a verified numerical method of proving the invertibility of linear elliptic operators. This method also provides a verified norm estimation for the inverse operators. This type of estimation is important for verified computations of solutions to elliptic boundary value problems. The proposed method uses a generalized eigenvalue problem to derive the norm estimation. This method has several advantages. Namely, it can be applied to two types of boundary conditions: the Dirichlet type and the Neumann type. It also provides a way of numerically evaluating lower and upper bounds of target eigenvalues. Numerical examples are presented to show that the proposed method provides effective estimations in most cases.

早稲田大学基幹理工学部に応用数理学科を設立して7年経過した．これは工学と数学を半分づつ学ぶ学科である．3年生に回路理論を工学系の中心的な必修科目として設置した．電気回路基礎から電子回路（アナログ電子回路もディジタル電子回路も含む）までを30回の90分講義で教える科目である．この科目を2012年度と2013年度の2年間担当した．講義の準備に当たって，回路理論を数学的な論理性を保って講義することができるかを考えた．講義開始前の数か月と講義開始後の8か月ぐらいの約1年間でこのことに対する思索（とそれに必要な歴史的な文献調査，外国の教科書の調査，現在の技術動向調査が含まれる）を巡らし，その結果をコロナ社から回路理論として出版した．結果的にこの本はマクスウェルの方程式を公理として仮定し，素子特性は数理モデルとして与えられていると考えて回路理論を数学的な論理性を保つように展開することを志した．教科書とするために，数学的道具立ては制限した部分が多く，また，原稿も半分程度に圧縮したが，回路理論の論理的展開のためにいろいろな講義展開法についての試行を行い，我が国の定石の講義法とかなり異なっている部分も多い．2年目には講義の前半は理論，後半は実験という形で講義を展開した．2年目は回路理論を論理的に捉えるだけでなく，実験により回路の実在をどう捉えるか考えさせた．これらの思索と実践について報告する．

This paper describes the emergence of two characteristic notions, nondegenerate Peano continuum and Cantor set, by the exploration of the essence of the existence of primitive chaos from a topological viewpoint. The primitive chaos is closely related to vital problems in physics itself and leads to chaotic features under natural conditions. The nondegenerate Peano continuum represents an ordinarily observed space, and the existence of a single nondegenerate Peano continuum guarantees the existence of infinite varieties of the primitive chaos leading to the chaos. This result provides an explanation of the reason why we are surrounded by diverse chaotic behaviors. Also, the Cantor set is a general or universal notion different from the special set, the Cantor middle-third set, and the existence of a single Cantor set guarantees infinite varieties of the primitive chaos leading to the chaos. This analogy implies the potential of the Cantor set for the method of new recognizing physical phenomena.

An efficient format and fast algorithms of basic operations for 4-fold working precision are proposed. The proposed format is an unevaluated sum of four double precision numbers, capable of representing at least 203 bits of mantissa. Hence, it is slightly less accurate than quad-double format proposed by Hida et. al. [1], however presented algorithms based on the format are faster than those algorithms. By numerical experiments it is shown that the proposed algorithms are efficient.

This paper presents an algorithm of identifying parameters satisfying a sufficient condition of Plum's Newton-Kantorovich like theorem. Plum's theorem yields a numerical existence test of solutions for nonlinear partial differential equations. The sufficient condition of Plum's theorem is given by the nonemptiness of a region defined by one dimensional nonlinear inequalities. The aim of this paper is to develop a systematic method of constructing an inner inclusion of this region. If $\underline\rho \in {\mathbb R}^+$ is the minimum included in this region, $\underline\rho$ gives the minimum of the error bounds. Moreover, if $\overline\rho \in {\mathbb R}^+$ is the maximum included in this region, then $\overline\rho$ gives the maximum radius of a ball in which the exact solution is unique. In this paper, an algorithm is developed for finding $\rho_e$ and $\rho_u$ such that they belong to this region and become close approximations of $\underline\rho$ and $\overline\rho$, respectively. Finally, to illustrate features of Plum's theorem with our proposed algorithm, some numerical results compared with results by Plum's theorem with the Newton method are presented. In addition to this, Plum's theorem with our algorithm is also compared with Newton-Kantorovich's theorem. One of the most important facts found in this paper is that, for some examples, $\rho_e$ become smaller than error bounds obtained by Newton-Kantorovich's theorem. Moreover, also for these examples, $\rho_u$ become greater than regions indicating uniqueness of the exact solution derived by Newton-Kantorovich's theorem. This implies that Plum's theorem can be seen as a modification of Newton-Kantorovich's theorem.

For Poisson's equation over a polygonal domain of general shape, the solution of which may have a singularity around re-entrant corners, we provide an explicit a priori error estimate for the approximate solution obtained by finite element methods of high degree. The method used herein is a direct extension of the one developed in preceding paper of the second and third listed authors, which provided a new approach to deal with the singularity by using linear finite elements. In the present paper, we also give a detailed discussion of the dependency of the convergence order on solution singularities, mesh sizes and degrees of the finite element method used.

In this paper, a numerical verification method is presented for second-order semilinear elliptic boundary value problems on arbitrary polygonal domains. Based on the Newton-Kantorovich theorem, our method can prove the existence and local uniqueness of the solution in the neighborhood of its approximation. In the treatment of polygonal domains with an arbitrary shape, which gives a singularity of the solution around the re-entrant corner, the computable error estimate of a projection into the finite-dimensional function space plays an essential role. In particular, the lack of smoothness of the solution makes classical error estimates fail on nonconvex domains. By using the Hyper-circle equation, an alternative error estimate of the projection has been proposed. Additionally, a new residual evaluation method based on the mixed finite element method works well. It yields more accurate evaluation than the existing method. The efficiency of our method is shown through illustrative numerical results on several polygonal domains.

This paper is concerned with verification methods for numerical solutions of linear systems. Many methods for the verification require switches of rounding modes defined by the IEEE 754 standard. However, the switches cannot be supported in several computational environments. In such cases, Ogita-Rump-Oishi's method can work on such environments. Recently, Rump developed new error estimates of floating-point summation and dot product. The aim of this paper is to improve Ogita-Rump-Oishi's error estimates by using the error estimates by Rump. In addition, the computational cost of our method is comparable to that of Ogita-Rump-Oishi's method.

This paper is concerned with accurate numerical algorithms for matrix multiplication. Recently, an error-free transformation from a product of two floating-point matrices into an unevaluated sum of floating-point matrices has been developed by the authors. Combining this technique and accurate summation algorithms, new algorithms for accurate matrix multiplication could be investigated. In this paper, it is mentioned that the previous work is not the unique way to achieve an error-free transformation and the constraint of the error-free transformation is clarified. For the application, a new algorithm is developed reducing the number of matrix products compared to the previous algorithm.

The authors recently published a paper on some properties of the solution curves for the last n-1 equations of F(x)+Ax=b where x=[x1,x2,...,xn]T is a variable, F(x):Rn → Rn is a nonlinear function of which the first and second derivatives are strictly positive, A ∈ Rn × n is an Ω-matrix, and b ∈ Rn is a constant vector. In that paper, the authors showed that any solution curve possesses neither maximal points nor inflection points with respect to x1, by making use of a fundamental property of Ω-matrices, which is expressed in the form of inequality. However, the proof was a little unclear as shown in Introduction. The objective of this paper is to give an explicit proof for the property of Ω-matrices, which makes the author's previous result more rigorous.

The finite element method (FEM) is applied to bound leading eigenvalues of the Laplace operator over polygonal domains. Compared with classical numerical methods, most of which can only give concrete eigenvalue bounds over special domains of symmetry, our proposed algorithm can provide concrete eigenvalue bounds for domains of arbitrary shape, even when the eigenfunction has a singularity. The problem of eigenvalue estimation is solved in two steps. First, we construct a computable a priori error estimation for the FEM solution of Poisson's problem, which holds even for nonconvex domains with reentrant corners. Second, new computable lower bounds are developed for the eigenvalues. Because the interval arithmetic is implemented throughout the computation, the desired eigenvalue bounds are expected to be mathematically correct. We illustrate several computation examples, such as the cases of an L-shaped domain and a crack domain, to demonstrate the efficiency and flexibility of the proposed method.

We consider an explicit estimation for error constants from two basic constant interpolations on triangular finite elements. The problem of estimating the interpolation constants is related to the eigenvalue problems of the Laplacian with certain boundary conditions. By adopting the Lehmann-Goerisch theorem and finite element spaces with a variable mesh size and polynomial degree, we succeed in bounding the leading eigenvalues of the Laplacian and the error constants with high precision. An online demo for the constant estimation is also available at http://www.xfliu.org/onlinelab/.

Since the chaos was discovered, it has been recognized that we are surrounded by diverse chaotic behaviors. The purpose of this study is to reconsider the implication of this fact through the notion of a primitive chaos. Under natural conditions, each primitive chaos leads to apparent chaotic features, such as the existence of a nonperiodic orbit, the existence of the periodic point whose prime period is n for any n is an element of N, the existence of a dense orbit, the density of periodic points, sensitive dependence on initial conditions, and topological transitivity, while infinite varieties of the primitive chaos are guaranteed by a nondegenerate Peano continuum.

This paper concerns a robust algorithm for the 2D orientation problem which is one of the basic tasks in computational geometry. Recently, a fast and accurate floating-point summation algorithm is investigated by Rump, Ogita and Oishi in [S.M. Rump, T. Ogita, S. Oishi, Accurate floating-point summation. Part I: Faithful rounding, SIAM J. Sci. Comput. 31 (1) (2008) 189-2241, in which a new kind of an error-free transformation of floating-point numbers is used. Based on it, a new algorithm of error-free determinant transformation for the 2D orientation problem is proposed, which gives a correct result. Numerical results are presented for illustrating that the proposed algorithm has some advantage over preceding algorithms in terms of measured computing time. (C) 2012 Elsevier Inc. All rights reserved.

This paper is concerned with accurate matrix multiplication in floating-point arithmetic. Recently, an accurate summation algorithm was developed by Rump et al. (SIAM J Sci Comput 31(1):189-224, 2008). The key technique of their method is a fast error-free splitting of floating-point numbers. Using this technique, we first develop an error-free transformation of a product of two floating-point matrices into a sum of floating-point matrices. Next, we partially apply this error-free transformation and develop an algorithm which aims to output an accurate approximation of the matrix product. In addition, an a priori error estimate is given. It is a characteristic of the proposed method that in terms of computation as well as in terms of memory consumption, the dominant part of our algorithm is constituted by ordinary floating-point matrix multiplications. The routine for matrix multiplication is highly optimized using BLAS, so that our algorithms show a good computational performance. Although our algorithms require a significant amount of working memory, they are significantly faster than 'gemmx' in XBLAS when all sizes of matrices are large enough to realize nearly peak performance of 'gemm'. Numerical examples illustrate the efficiency of the proposed method.

We discuss several methods for real interval matrix multiplication. First, earlier studies of fast algorithms for interval matrix multiplication are introduced: naive interval arithmetic, interval arithmetic by midpoint-radius form by Oishi-Rump and its fast variant by Ogita-Oishi. Next, three new and fast algorithms are developed. The proposed algorithms require one, two or three matrix products, respectively. The point is that our algorithms quickly predict which terms become dominant radii in interval computations. We propose a hybrid method to predict which algorithm is suitable for optimizing performance and width of the result. Numerical examples are presented to show the efficiency of the proposed algorithms. (C) 2011 Elsevier B.V. All rights reserved.

This paper is concerned with an accurate computing for matrix multiplication. We show that matrix multiplication can be transformed into a summation of floating-point matrices by mainly using level 3 operations in BLAS. We call it 'error-free transformation of matrix multiplication'. By combining this error-free transformation and accurate summation algorithms for floating-point numbers, we can obtain an accurate result of matrix multiplication. Numerical examples are presented to illustrate the efficiency of the proposed algorithm.

In this paper, an algorithm for an accurate matrix factorization based on Cholesky factorization for extremely ill-conditioned matrices is proposed. The Cholesky factorization is widely used for solving a system of linear equations whose coefficient matrix is symmetric and positive definite. However, it sometimes breaks down by the presence of an imaginary root due to the accumulation of rounding errors, even if the matrix is actually positive definite. To overcome this, a completely stable algorithm named inverse Cholesky factorization is investigated, which never breaks down as long as the matrix is symmetric and positive definite. The proposed algorithm consists of standard numerical algorithms and an accurate algorithm for dot products. Moreover, it is shown that the algorithm can also verify the positive definiteness of a given real symmetric matrix. Numerical results are presented for illustrating the performance of the proposed algorithms.

In this paper we study the generation of an ill-conditioned integer matrix A=[aij] with |aij|≤µ for some given constant µ. Let n be the order of A. We first give some upper bounds of the condition number of A in terms of n and µ. We next propose new methods to generate extremely ill-conditioned integer matrices. These methods are superior to the well-known method by Rump in some respects, namely, the former has a simple algorithm to generate a larger variety of ill-conditioned matrices. In particular we propose a method to generate ill-conditioned matrices with a choice of desirable singular value distributions as benchmark matrices.

This paper is concerned with the tight enclosure of matrix multiplication AB for two floating-point matrices A and B. The aim of this paper is to compute component-wise upper and lower bounds of the exact result C of the matrix multiplication AB by floating-point arithmetic. Namely, an interval matrix enclosing C is obtained. In this paper, new algorithms for enclosing C are proposed. The proposed algorithms are designed to mainly exploit the level 3 operations in BLAS. Although the proposed algorithms take around twice as much costs as a standard algorithm promoted by Oishi and Rump, the accuracy of the result by the proposed algorithms is better than that of the standard algorithm. At the end of this paper, we present numerical examples showing the efficiency of the proposed algorithms. Copyright (C) 2010 John Wiley & Sons, Ltd.

Several methods have been proposed to calculate a rigorous error bound of an approximate solution of a linear system by floating-point arithmetic. These methods are called &apos;verification methods&apos;. Applicable range of these methods are different. It depends mainly on the condition number and the dimension of the coefficient matrix whether such methods succeed to work or not. In general, however, the condition number is not known in advance. If the dimension or the condition number is large to some extent, then Oishi-Rump&apos;s method, which is known as the fastest verification method for this purpose, may fail. There are more robust verification methods whose computational cost is larger than the Oishi-Rump&apos;s one. It is not so efficient to apply such robust methods to well-conditioned problems. The aim of this paper is to choose a suitable verification method whose computational cost is minimum to succeed. First in this paper, four fast verification methods for linear systems are briefly reviewed. Next, a compromise method between Oishi-Rump&apos;s and Ogita-Oishi&apos;s one is developed. Then, an algorithm which automatically and efficiently chooses an appropriate verification method from five verification methods is proposed. The proposed algorithm does as much work as necessary to calculate error bounds of approximate solutions of linear systems. Finally, numerical results are presented.

This paper is concerned with interval arithmetic, especially, an enclosure of a matrix product is focused on. Using level 3 operations of matrix computations, an algorithm outputting a tight enclosure for matrix multiplication is proposed. Most of the algorithms for this purpose require switches of rounding modes defined in the IEEE standard 754. However some programing enviroments have not supported them. Our proposed method demands only rounding-to-nearest mode, so that it is very portable.

Present authors have presented with Takayuki Kubo at University of Tsukuba a method of a computer assisted proof for the existence and uniqueness of solutions to two-point boundary value problems of nonlinear ordinary differential equations in the paper submitted for NOLTA, IEICE. This method uses piecewise linear finite element base functions and sometimes requires fine mesh. To overcome this difficulty, in this paper, an improved method is presented for the norm estimation of the residual to the operator equation. In this refined formulation, piecewise quadratic finite element base functions are used. A kind of the residual technique works sophisticatedly well. It is stated that the estimation of the residual can be expected smaller than that of the previous method. Finally, four examples are presented. Each result demonstrates that a remarkable improvement is achieved in accuracy of the guaranteed error estimation.

It is well known that it is an ill-posed problem to decide whether a function has a multiple root. For example, an arbitrarily small perturbation of a real polynomial may change a double real root into two distinct real or complex roots. In this paper we describe a computational method for the verified computation of a complex disc to contain exactly k roots of a univariate nonlinear function. The function may be given by some program. Computational results using INTLAB, the Matlab toolbox for reliable computing, demonstrate properties and limits of the method.

Given a vector pi of floating-point numbers with exact sum s, we present a new algorithm with the following property: Either the result is a faithful rounding of s, or otherwise the result has a relative error not larger than epsKcond(∑pi) for K to be specified. The statements are also true in the presence of underflow, the computing time does not depend on the exponent range, and no extra memory is required. Our algorithm is fast in terms of measured computing time because it allows good instruction-level parallelism. A special version for K=2, i.e., quadruple precision is also presented. Computational results show that this algorithm is more accurate and faster than competitors such as XBLAS.

A fast verified automatic integration algorithm is proposed for calculating univariate integrals over finite intervals. This algorithm is based on the double exponential formula proposed by Takahasi and Mori. The double exponential formula uses a certain trapezoidal rule. This trapezoidal rule is determined by fixing two parameters, the width h of a subdivision of a finite interval and the number n of subdivision points of this subdivision. A theorem is presented for calculating h and n as a function of a given tolerance of the verified numerical integration of a definite integral. An efficient a priori method is also proposed for evaluating function calculation errors including rounding errors of floating point calculations. Combining these, a fast algorithm is proposed for verified automatic integration. Numerical examples are presented for illustrating effectiveness of the proposed algorithm.

In this paper, a numerical method is presented for verifying the existence and uniqueness of solutions to two-point boundary value problems of nonlinear ordinary differential equations. Taking into account every error of numerical computations such as the discretization error and the rounding error, this method also provides mathematically guaranteed error bounds between approximations obtained by numerical computations and the exact solution whose existence is proven by the numerical existence theorem, which is based on the Newton-Kantorovich theorem. Finally, illustrative numerical results are presented for showing the usefulness of the method.

A verified automatic integration algorithm is proposed for calculating contour integration over complex field using numerical computations. The proposed algorithm is based on trapezoidal rule for angle. The error analysis of the method have been presented by several authors, however, these investigations are done basically for examining the rates of convergence, and several constants in these error formula were left unevaluated. In order to construct verified numerical integrator using the algorithm, the error formula is presented. To construct efficient verified numerical integrator, an efficient a priori method of evaluating function calculation errors is adopted. Combining these, a verified automatic integration algorithm is proposed. Numerical examples are presented for illustrating effectiveness of the proposed algorithm.

This paper treats a linear equation
Av = b,
where A is an element of F(nxn) and b is an element of F(n). Here, F is a set of floating point numbers. Let u be the unit round-off of the working precision and kappa(A) = parallel to A parallel to(infinity)parallel to A(-1)parallel to(infinity) be the condition number of the problem. In this paper, ill-conditioned problems with
1 &lt; u kappa(A) &lt; infinity
are considered and an iterative refinement algorithm for the problems is proposed. In this paper, the forward and backward stability will be shown for this iterative refinement algorithm.

This paper is concerned with a robust geometric predicate for the 2D orientation problem. Recently, a fast and accurate floating-point summation algorithm is investigated by Rump, Ogita and Oishi, which provably outputs a result faithfully rounded from the exact value of the summation of floating-point numbers. We optimize their algorithm for applying it to the 2D orientation problem which requires only a correct sign of a determinant of a 3 x 3 matrix. Numerical results illustrate that our algorithm works fairly faster than the state-of-the-art algorithm in various cases.

This paper aims to survey fast methods of verifying the accuracy of a numerical solution of a linear system. For the last decade, a number of fast verification algorithms have been proposed to obtain an error bound of a numerical solution of a dense or sparse linear system. Such fast algorithms rely on the verified numerical computation using floating-point arithmetic defined by IEEE standard 754. Some fast verification methods for dense and sparse linear systems are reviewed together with corresponding numerical results to show the practical use and efficiency of the verified numerical computation as much as possible.

This paper concerns with the following linear programming problem: \[ \mbox{Maximize } c^tx, \mbox{ subject to } Ax \leqq b \mbox{ and } x\geqq 0, \] where $A \in \F^{m\times n}$, $b \in \F^m$ and $c, x \in \F^n$. Here, $\F$ is a set of floating point numbers. The aim of this paper is to propose a numerical method of including an optimum point of this linear programming problem provided that a good approximation of an optimum point is given. The proposed method is base on Kantorovich's theorem and the continuous Newton method. Kantorovich's theorem is used for proving the existence of a solution for complimentarity equation and the continuous Newton method is used to prove feasibility of that solution. Numerical examples show that a computational cost to include optimum point is about 4 times than that for getting an approximate optimum solution.

Parallel algorithms for accurate summation and dot product are proposed, They are parallelized versions of fast and accurate algorithms of calculating sum and dot product using error-free transformations which are recently proposed by Ogita et al. [T. Ogita, S.M. Rump, S. Oishi, Accurate sum and dot product, SIAM J. Sci. Comput. 26 (6) (2005) 1955-1988]. They have shown their algorithms are fast in terms of measured computing time. However, due to the strong data dependence in the process of their algorithms, it is difficult to parallelize them. Similarly to their algorithms, the proposed parallel algorithms in this paper are designed to achieve the results as if computed in K-fold working precision with keeping the fastness of their algorithms. Numerical results are presented showing the performance of the proposed parallel algorithm of calculating dot product. (C) 2008 Elsevier B.V. All rights reserved.

筆者は1976 年の卒論より研究をスタートしました。すでに32 年間研究に携わってきたことになります。筆者が精度保証付き数値計算の研究に移ったのは1990年のことです。以来本分野で研究を続けてきました。精度保証付き数値計算の研究の研究に移ったのは筆者なりの必然性があります。1990年当時の精度保証付き数値計算の研究は実用的ではないと考えられていたような気がします。実際、数百次元の連立一次方程式の精度保証が精一杯の感じでありました。現在では特殊な構造を持つ方程式であれば一億次元の連立一次方程式でも精度保証できるようになり、精度保証付き数値計算は実用の段階に至っていると思っています。筆者の研究がこのようなブレークスルーに貢献できたと考えておりますが、本稿ではこのような精度保証付き数値計算の研究の発展と筆者の研究の個人史の交錯を描かせていただきました。

In Part II of this paper we first refine the analysis of error-free vector transformations presented in Part I. Based on that we present an algorithm for calculating the rounded-to-nearest result of s := Sigma pi for a given vector of floating-point numbers pi, as well as algorithms for directed rounding. A special algorithm for computing the sign of s is given, also working for huge dimensions. Assume a floating-point working precision with relative rounding error unit eps. We define and investigate a K-fold faithful rounding of a real number r. Basically the result is stored in a vector Res(nu) of K nonoverlapping floating-point numbers such that Sigma Res(nu) approximates r with relative accuracy eps(K), and replacing Res(K) by its floating-point neighbors in Sigma Res(nu) forms a lower and upper bound for r. For a given vector of floating-point numbers with exact sum s, we present an algorithm for calculating a K-fold faithful rounding of s using solely the working precision. Furthermore, an algorithm for calculating a faithfully rounded result of the sum of a vector of huge dimension is presented. Our algorithms are fast in terms of measured computing time because they allow good instruction-level parallelism, they neither require special operations such as access to mantissa or exponent, they contain no branch in the inner loop, nor do they require some extra precision. The only operations used are standard floating-point addition, subtraction, and multiplication in one working precision, for example, double precision. Certain constants used in the algorithms are proved to be optimal.

Consider the boundary value problem Lu equivalent to -(pu ')' + qu ' + ru = f, a &lt;= x &lt;= b, u(a) = u(b) = 0. Let H(v)A(v)U = f and (A) over cap U-v = (f) over cap be its finite difference equations and piecewise linear finite element equations on partitions Delta(v) : a = x(0)(v) &lt; x(1)(v) &lt; ... &lt; x(nv+1)(v) = b, v = 1, 2.... with h(i)(v) = x(i)(v) - x(i-1)(v), h(v) = max(i)h(i)(v) -&gt; 0 as v -&gt; infinity, where H-v, are n(v) x n(v) diagonal matrices and A(v) as well as (A) over cap (v) are n(v) x n(v) tridiagonal. It is shown that the following three conditions are equivalent: (i) The boundary value problem has a unique solution u is an element of C-2[a, b]. (ii) For sufficiently large v &gt;= v(0), the inverse A(v)(-1) = (g(ij)(v)) exists and vertical bar g(ij)(v)vertical bar &lt;= M, for all(i,j) with a constant M &gt; 0 independent of h(v). (iii) For sufficiently large v &gt;= (v) over cap (0), (A(v)) over cap (-1) = ((g(ij)) over cap)(v) exists and vertical bar(g(ij)) over cap (v)vertical bar &lt;= (M) over cap, for all(i,j) with a constant (M) over cap &gt; 0 independent of h(v). It is also shown by a numerical example that the finite difference method with uniform nodes x(i+1) = x(i) + h, 0 &lt;= i &lt;= n, h = (b - a)/(n + 1) applied to the boundary value problem with no solution gives a ghost solution for every n.

Given a vector of floating-point numbers with exact sum s, we present an algorithm for calculating a faithful rounding of s, i.e., the result is one of the immediate floating-point neighbors of s. If the sum s is a floating-point number, we prove that this is the result of our algorithm. The algorithm adapts to the condition number of the sum, i.e., it is fast for mildly conditioned sums with slowly increasing computing time proportional to the logarithm of the condition number. All statements are also true in the presence of underflow. The algorithm does not depend on the exponent range. Our algorithm is fast in terms of measured computing time because it allows good instruction-level parallelism, it neither requires special operations such as access to mantissa or exponent, it contains no branch in the inner loop, nor does it require some extra precision: The only operations used are standard floating-point addition, subtraction, and multiplication in one working precision, for example, double precision. Certain constants used in the algorithm are proved to be optimal.

Given a vector of floating-point numbers with exact sum s, we present an algorithm for calculating a faithful rounding of s, i.e., the result is one of the immediate floating-point neighbors of s. If the sum s is a floating-point number, we prove that this is the result of our algorithm. The algorithm adapts to the condition number of the sum, i.e., it is fast for mildly conditioned sums with slowly increasing computing time proportional to the logarithm of the condition number. All statements are also true in the presence of underflow. The algorithm does not depend on the exponent range. Our algorithm is fast in terms of measured computing time because it allows good instruction-level parallelism, it neither requires special operations such as access to mantissa or exponent, it contains no branch in the inner loop, nor does it require some extra precision: The only operations used are standard floating-point addition, subtraction, and multiplication in one working precision, for example, double precision. Certain constants used in the algorithm are proved to be optimal.

Consider the boundary value problem Lu equivalent to -(pu ')' + qu ' + ru = f, a &lt;= x &lt;= b, u(a) = u(b) = 0. Let H(v)A(v)U = f and (A) over cap U-v = (f) over cap be its finite difference equations and piecewise linear finite element equations on partitions Delta(v) : a = x(0)(v) &lt; x(1)(v) &lt; ... &lt; x(nv+1)(v) = b, v = 1, 2.... with h(i)(v) = x(i)(v) - x(i-1)(v), h(v) = max(i)h(i)(v) -&gt; 0 as v -&gt; infinity, where H-v, are n(v) x n(v) diagonal matrices and A(v) as well as (A) over cap (v) are n(v) x n(v) tridiagonal. It is shown that the following three conditions are equivalent: (i) The boundary value problem has a unique solution u is an element of C-2[a, b]. (ii) For sufficiently large v &gt;= v(0), the inverse A(v)(-1) = (g(ij)(v)) exists and vertical bar g(ij)(v)vertical bar &lt;= M, for all(i,j) with a constant M &gt; 0 independent of h(v). (iii) For sufficiently large v &gt;= (v) over cap (0), (A(v)) over cap (-1) = ((g(ij)) over cap)(v) exists and vertical bar(g(ij)) over cap (v)vertical bar &lt;= (M) over cap, for all(i,j) with a constant (M) over cap &gt; 0 independent of h(v). It is also shown by a numerical example that the finite difference method with uniform nodes x(i+1) = x(i) + h, 0 &lt;= i &lt;= n, h = (b - a)/(n + 1) applied to the boundary value problem with no solution gives a ghost solution for every n.

In this paper, the problem of inverting regular matrices with arbitrarily large condition number is treated in double precision defined by IEEE 754 floating point standard. In about 1984, Rump derived a method for inverting arbitrarily ill-conditioned matrices. The method requires the possibility to calculate a dot product in higher precision. Rump's method is of theoretical interest. Rump made it clear that inverting an arbitrarily ill-conditioned matrix in single or double precision does not produce meaningless numbers, but contains a lot of information in it. Rump's method uses such inverses as preconditioners. Numerical experiments exhibit that Rump's method converges rapidly for various matrices with large condition numbers. Why Rump's method is so efficient for inverting arbitrarily ill-conditioned matrices is a little mysterious. Thus, to prove its convergence is an interesting problem in numerical error analysis. In this article, a convergence theorem is presented for a variant of Rump's method. (C) 2006 Elsevier B.V. All rights reserved.

Recent development of Java's optimization techniques makes Java one of the most useful programming languages for numerical computations. This paper proposes a numerical method of obtaining verified approximate solutions of linear systems. Usual methods for verified computations use switches of rounding modes defined in IEEE standard 754. However, such switches of rounding modes have not been supported in Java. This method avoids using directed rounding, so that it is implementable on a wide range of programming languages including Java. Numerical experiments using Java illustrate that the method can give a very accurate error bound for an approximate solution of a linear system with almost same computational cost as that for calculating an approximate inverse by the Gaussian elimination. (c) 2005 Elsevier B.V. All rights reserved.

This paper is concerned with semilinear tow-point boundary value problems of the form -(p(x)u')'+ f (x, u) = 0, a &lt;= x &lt;= b, alpha(0)u(a) - alpha(1)u'(a) = alpha, beta(0)u(b) + beta(1)u'(b) = beta, alpha(i) &gt;= 0, beta(i) &gt;= 0, i = 0, 1, alpha(0)+alpha(1) &gt; 0, beta(0)+beta(1) &gt; 0, alpha(0)+beta(0) &gt; 0. Under the assumption inf f(u) &gt; - lambda(1), where lambda(1) is the smallest eigenvalue of Lu = -(pu')' with the boundary conditions, unique existence theorems of solution for the continuous problem and a discretized. system with not necessarily uniform nodes are given as well as error estimates. The results generalize three theorems of Lees for u" = f (x, u), 0 &lt;= x &lt;= 1, u(0) = alpha, u(1) = beta.

This paper is concerned with interval matrix multiplication.New algorithms are proposed to calculate an inclusion of the product of interval matrices using rounding mode controlled computation. Thecomputational cost of the proposed algorithms is almost the same as that for calculating an inclusion of the product of point matrices.Numerical results are presented to illustrate that the new algorithms are much faster than the conventional algorithms and that the guaranteed accuracies obtained by the proposed algorithms are comparable to those of the conventional algorithms. © Springer 2005.

A fast verification algorithm of calculating guaranteed error bounds for all approximate eigenvalues of a real symmetric matrix is proposed. In the proposed algorithm, Rump's and Wilkinson's bounds are combined. By introducing Wilkinson's bound, it is possible to improve the error bound obtained by the verification algorithm based on Rump's bound with a small additional cost. Finally, this paper includes some numerical examples to show the efficiency of the proposed algorithm.

Algorithms for summation and dot product of floating-point numbers are presented which are fast in terms of measured computing time. We show that the computed results are as accurate as if computed in twice or K-fold working precision, K &gt;= 3. For twice the working precision our algorithms for summation and dot product are some 40% faster than the corresponding XBLAS routines while sharing similar error estimates. Our algorithms are widely applicable because they require only addition, subtraction, and multiplication of floating-point numbers in the same working precision as the given data. Higher precision is unnecessary, algorithms are straight loops without branch, and no access to mantissa or exponent is necessary.

This paper proposes the method of numerical verification of solutions of a periodic integral equation with a logarithmic singular kernel, which is typically found in some two-dimensional potential problems. The verification method utilizes a property of the singular integral for trigonometric polynomials, the periodic Sobolev space and Schauder's fixed point theorem.

This paper describes numerical verification of a double turning point of a nonlinear system using an extended system. To verify the existence of a double turning point, we need to prove that one of the solutions of the extended system corresponds to the double turning point. For that, we propose an extended system with an additional condition. As an example, for a finite dimensional problem, we verify the existence and local uniqueness of a double turning point numerically using the extended system and a verification method based on the Banach fixed point theorem.

As interval analysis-based reliable computations find wider application, more software is becoming available. Simultaneously. the applications for which this software is designed are becoming more diverse. Because of this, the software itself takes diverse forms, ranging from libraries for application development to fully interactive systems. The target applications range from fairly general to specialized.
Here, we describe the design of four freely available software systems providing validated computations. Oishi provides Slab, a complete, high-performance system for validated linear algebra whose user interface mimics both Matlab's M-files and a large subset of Matlab's command-line functions. In contrast, CADNA (Fabien Rico) is a C++ library designed to give developers of embedded systems access to validated numeric computations. Addressing global constrained optimization and validated solution of nonlinear algebraic systems, Kearfott's GlobSol focuses on providing the most practical such system possible without specifying non-general problem structure, Kearfott's system has a Fortran-90 interface. Finally, Neher provides a mathematically sound stand-alone package ACETAF with an intuitive graphical user interface for computing complex Taylor coefficients and their bounds, radii of convergence, etc.
Overviews of each package's capabilities, use, and instructions for obtaining and installing appear.

This paper is concerned with the problem of verifying the accuracy of approximate solutions of systems of linear equations. Recently, fast algorithms for calculating guaranteed error bounds of computed solutions of system's of linear equations have been proposed using the rounding mode controlled verification method and the residual iterative verification method. In this paper, a new verification method for systems of linear equations is proposed. Using this verification method, componentwise verified error bounds of approximate solutions of systems of linear equations can be calculated. Numerical results are presented to illustrate that it is possible to get very sharp error bounds of computed solutions of systems of linear equations whose coefficient matrices are symmetric and positive definite.

In this paper. we are concerned with a matrix equation
Ax = b
where A is an a x n real matrix and x and b are n-vectors. Assume that an approximate solution (x) over tilde is given together with an approximate LU decomposition. We will present fast algorithms for proving nonsingularity of A and for calculating rigorous error bounds for parallel toA(-1)b-(x) over tilde parallel to(infinity), The emphasis is on rigour of the bounds. The purpose of this paper is to propose different algorithms, the fastest with 2/3n(3) flops computational cost for the verification step, the same as for the LU decomposition. The presented algorithms exclusively use library routines for LU decomposition and for all other matrix and vector operations.

This paper is concerned with the validation of simple turning points of two-point boundary value problems of nonlinear ordinary differential equations. Usually it is hard to validate approximate solutions of turning points numerically because of it's singularity. In this paper, it is pointed out that applying the infinite dimensional Krawcyzk-based interval validation method to enlarged system, the existence of simple turning points can be verified. Taking an example, the result of validation is also presented.

Synchronous distributed timing clocks are the basic building blocks in digital communication systems. Conventional systems mainly employ a tree-like network of cascaded timing clocks for synchronous clocking. On the other hand, decentralized synchronous networks of timing clocks, which have been proposed from a very early stage of the digital communication, are gaining attention in the consumer communication networks and also recently in large, high-performance digital systems (such as multiprocessors) clocking. In this paper, we present a theoretical study of synchronous networks of timing clocks consisting of locally connected second order phase-locked loops (PLLs). We find a close connection between the stability properties of the first and second order networks. The particular examples of one way and two way nearest neighbor coupling, with a lag-lead filter and a triangular phase detector (PD) are analyzed in detail. Both the synchronized in-phase solution and the wave-like ''mode-lock'' solution are examined. A criterion is found for the stability of the one-way coupled network while the two-way coupled network is found to be always stable.

We analyze the collective behavior of a set of coupled damped driven pendula with finite (large) inertia, and show that the synchronization of the oscillators exhibits a first order phase transition synchronization onset, substantially different from the second order transition obtained in the case of no inertia. There is hysteresis between two macroscopic states, a weakly and a strongly coherent synchronized state, depending on the coupling and the initial state of the oscillators. A self-consistent theory is shown to determine these cooperative phenomena and to predict the observed numerical data in specific examples.

We analyze a large system of nonlinear phase oscillators with sinusoidal nonlinearity, uniformly distributed natural frequen cies and global all-to-all coupling, which is an extension of Kuramoto's model to second-order systems. For small coupling, the system evolves to an incoherent state with the phases of all the oscillators distributed uniformly. As the coupling is increased, the system exhibits a discontinuous transition to the coherently synchronized state at a pinning threshold of the coupling strength, or to a partially synchronized oscillation coherent state at a certain threshold below the pinning threshold. if the coupling is decreased from a strong coupling with all the oscillators synchronized coherently, this coherence can persist until the depinning threshold which is less than the pinning threshold, resulting in hysteretic synchrony depending on the initial configuration of the oscillators. We obtain analytically both the pinning and depinning threshold and also explain the discontinuous transition at the thresholds for the underdamped case in the large system size limit. Numerical exploration shows the oscillatory partially coherent state bifurcates at the depinning threshold and also suggests that this state persists independent of the system size. The system studied here provides a simple model for collective behaviour in damped driven high-dimensional Hamiltonian systems which can explain the synchronous firing of certain fireflies or neural oscillators with frequency adaptation and may also be applicable to interconnected power systems.

Dynamical properties such as lock-in or out-of-lock condition of mutually coupled phase-locked loops (PLL's) are problems of practical interest, The present paper describes a study of such dynamical properties for mutually coupled PLL's incorporating lag filters and triangular phase detectors, The fourth-order ordinary differential equation (ODE) governing the mutually coupled PLL's is reduced to the equivalent third-order ODE due to the symmetry, where the system is analyzed in the context of nonlinear dynamical system theory, An understanding as to how and when lock-in can be obtained or out-of-lock behavior persists, is provided by the geometric structure of the invariant manifolds generated in the vector field from the third-order ODE. In addition, a connection to the recently developed theory on chaos and bifurcations from degenerated homoclinic points is also found to exist. The two-parameter diagrams of the one-homoclinic orbit are obtained by graphical solution of a set of nonlinear (finite dimensional) equations. Their graphical results useful in determining whether the system undergoes lock-in or continues out-of-lock behavior, are verified by numerical simulations.

早稲田大学基幹理工学部に応用数理学科を設立して7年経過した。その3年生に回路理論は必修科目で電気回路基礎から電子回路までを30回の90分講義で教える科目である。この科目を2012年度と2013年度の2年間担当した。講義の準備に当たって,回路理論を数学的な論理性を保って講義することができるかを考えた。その結果をコロナ社から回路理論として出版した。結果的にこの本はMaxwellの方程式を公理として仮定し,素子特性は数理モデルとして与えられていると考えて回路理論を数学的な論理性を保つように展開することを志した。回路理論の論理的展開のためにいろいろな講義展開法についての試行を行い,我が国の定石の講義法とかなり異なっている部分も多い。これらの思索と実践について報告する。

数値計算結果を非常に効率的に精度保証する技術が高度に発展してきている.特に,線形計算や多項式計算については,このような精度保証付き数値計算法は倍精度浮動小数点数計算による近似計算の数倍の手間で,完全に正しい結果を与える.ここでは信頼性の技術に対して精度保証付き数値計算の技術がどのように関わるかを展望したい.

In this paper, we describe how to calculate the Bessel functions J_0(x) and J_1(x) with guaranteed error bound. We shall further present similar arguments for the Hankel functions H_0^<(1)>(x) and H_1^<(1)>(x).

数値シミュレーションは，膨大な数値計算の結果の上に成り立っている．そのような数値計算の結果を数学的に厳密な誤差限界と共に与えることを精度保証付き数値計算という．近年の著者らの成果により，精度保証付き数値計算は，線形計算については近似解を求めるのと比べて数倍の手間で実行できることが多いことが示された．さらに，数値計算自身も必要な精度の計算を適応的にかつ必要な計算の手間で行えることが示された．たとえば，連立一次方程式の数値解を倍精度浮動小数点演算で求めても，その精度が10進数換算で16桁（倍精度での最大）はほぼ常に出せる計算方式が実現できる．しかも，問題の難しさ（条件数）に応じた計算量で高速に実行できる．このように，数値線形代数の問題については，精度保証付き数値計算の技術は多くの場合，数値シミュレーションを支える技術として，実に驚くべき進展を遂げた．本稿では，このような現状について概観する．具体的には，著者らの研究により確立しつつある高速精度保証付き数値計算技術と無誤差数値計算技術についてサーベイを行う．

In this paper, we will present an accurate Cholesky decomposition algorithm. For the purpose, we develope multiple precision algorithms for the four basic arithmetic operations and the square root operation. Let A=[A_1, A_2, …, A_K] and B=[B_1, B_2, …, B_L] are K-tuple and L-tuple numbers. Here, A_i∈F for i=1, 2, …, K and B_i∈F for i=1, 2, …, L. For simplicity, we assume that K=max(K, L) Then, the following becomes multiple precision addition with K-fold accuracy :

IEEE standard 754 is widely used as a standard of floating-point arithmetic. Most of CPUs in today's computers support IEEE standard 754. Using double precision arithmetic following IEEE standard 754, the authors have proposed fast methods of verifying the accuracy of a numerical solution of a linear system. In this paper, an accurate and fast verification method for a linear system is developed using residual iteration method. The residual iteration requires the availability of high precision computation. Up to now, extended precision, i.e. multiple precision and quadruple precision are used for the accurate computation of the residual. However, such higher precision arithmetic systems are not necessarily available on all computers. Therefore, the residual iteration using such systems does not have the portability. In this paper, an accurate, fast and portable method for a linear system using the fact that an algorithm of accurate dot product can portably be implemented and applied to the residual iteration. Finally, numerical results are presented showing the effectiveness of the proposed verification method.

In this paper, new verification methods for verifying the accuracy of a numerical solution of a linear system with a dense coefficient matrix are proposed. The proposed methods are based on a verification method which uses an approximate inverse of the coefficient matrix. It is possible to reduce the computational memory space for the verification drastically without slowing down its computational speed seriously. Numerical results are presented to illustrate that the proposed methods become more effective in larger problem size.

Programming techniques for numerical computation with guaranteed accuracy are surveyed. In particular, a programming library on Scilab is described in detail. Fast verification method is also described.

非線形理論とその応用の分野は学際的な極めて広い範囲をカバーする学問分野である. そのため一大学では, 本分野全般をカバーするカリキュラムを構成することは難しい. そこで全国の大学等が共同して, 各地に分散する学生を教育する可能性について論議する. マルチメディアや合宿など様々な手段を利用することやカリキュラム体系を提案する.

有限次元非線形方程式 f(x)=0,f:R^n→R^n の特異解を精度保証付で計算するための一つの方法を提案する。非線形方程式の解を精度保証付で計算するためにKrawczyk法は大変有効である。しかし、特異解に対してKrawczyk法は常に失敗する。一方、方程式をより高次の空間に埋め込んで特異性を解消する方法が、多く提案されている。以下、この方法を方法(*)と呼ぶことにする。しかし、この方法(*)によって得られた解が元の方程式の特異解であることを数値的に保証することは、不可能であると考えられる。それは、方法(*)が方程式に微小な摂動を加えることによって特異性を解消しているので、摂動を加える前の方程式が特異解を持っていたかは分からない。分かることは、元の方程式にある摂動を加えることによって生成された方程式が特異解を持つということである。そこで、本報告では、新たに近似的特異解という概念を導入し、この近似的特異解を精度保証付で計算することを考える。この概念は方法(*)の欠点を逆手にとったもので、方程式にある微小な摂動を加えた時に特異解となるような点を近似的特異解と定義する。この定義によって、方法(*)によって求められた数値は、近似的特異解として意味のあるものになると考えられる。方法にはもう一つの大きな問題がある。それは、方程式の持つ異なる特異性に対して異なる方程式をたてねばならないことである。しかし、求める解の特異性が予め分かっていることは不自然であり、実際の方法(*)の適用は、考えられL特異性に対するそれぞれの方程式を片端から試していくことになりそうである。そこで本報告では、単一の方程式によって、全ての異なる特性を持つ解を求めることのできる方法を提案する。

複素数解を持つ有限次元非線形方程式の求解問題を解くために, 複素数演算を行なえる精度保証付数値計算システムについて考える. 本報告では, 区間演算とKrawczykの方法を用いて解の精度保証を行なうために, 複素区間, の定義を行ない, 複本領域に対してKrawczyk法を用いて, 複素解を持つ非線形方程式の解の精度保証を行なう.

Krawczyk法を用いることによって有限次元非線形方程式f(χ)=0,f:R^<n+1>&xrarr;R^n (1)の解曲線が唯一存在する領域を保証しながら解曲線追跡を行う方法が提案されている。従来の方法は解曲線上の離散的な点を出力するものであったのにたいして、この方法は解曲線自体を捉えるものである。その結果、この方法は正則解に対して必ず成功するものである。本報告では、この考えを関数方程式に拡張することによって、一パラメータ依存非線形常微分方程式の境界値問題F_0(χ(t),λ):=dχ(t)/(dt)-f(χ(t),t,λ)=0,(2)g_0(χ)=0,(3)χ&isins;C[-1,1],λ&isins;R (4)の解を、ある既知解(χ_1(t),λ_1)から、区間を用いて追跡することを考える。ここで準備として常微分方程式にの境界値問題に対するKrawczyk法を概観する。方程式F_0(χ(t))&colone;dχ(t)/(dt)-f(χ(t),t)=0,g0(χ)=0の近似解c(t)に対して、区間関数Τ(t)とKrawczyk作用素K(Τ)を定義し、[numerical fomula]の成立によって、Τ(t)内に唯一解の存在を保証する。ただし、[numerical fomula]である。

非線形方程式の分岐点を求める場合、特異性を解消するため正則な拡大方程式を作り、その方程式を解くことによって分岐点を求める方法が一般的である。微分方程式の境界値問題に対しても、上記方法によって折り返し点を求める手法が提案されている。この方法に対し文献[2]の数値的存在検証法を適用し、2点境界値問題の単純折り返し点の存在を精度保証付き数値計算により検証できることを示す。

カオス理論は力学系理論、エルゴード理論など枠組みとして非常にきれいに整備されている。しかし、現実の系をモデル化した方程式に適用するに当たって、枠組みを適用する前提が成立するか否か厳密に証明するの極めて困難なことが多い。精度保証付き数値計算に基ずく計算機援用証明は力学系の不変集合の存在証明などに応用が試みられている。ここでは、その例として常微分方程式のコネクティングオービット(ホモクリニック軌道、ヘテロクリニック軌道の総称)の存在証明の数値的検証例を示す。コネクティングオービットの存在証明はカオス理論の最も基本的な問題の一つであるが、極めて困難な問題で現実的な系において数学的に厳密に実行された例は極めて少ないと思われる。

本文では次のパラメタを含む非線形力学系を考える:dx/(dt)= f(x,λ),x(t)∈R^n,λ∈R^p (1)ただし,f(x,λ)はn-次元ベクトル値連続関数とする.(1)のλ=λ^*における解x(t)^*,-∞<t<∞,で極限x_-=lim__<t→-∞> x(t),x_+=lim__<t→∞>x(t) (2)が存在するものは危点x_-,x_+間のコネクティングオービットと呼ばれる.x_-,x_+はfの危点となるからである:f(x_-,λ^*)=0,f(x_+,λ^*)=0. (3)コネクティングオービットはx_-=x_+のときはホモクリニックオービット,x_-&bne;x_+のときはヘテロクリニックオービットとなる.コネクティングオービットは力学系の大域的な性質を決定する上で重要な役割をはたすため,その数値計算法は1990年代になって活発に提案されるようになってきた.また,それらの数値計算法の安定性,収束性の証明も示されている.ここでは,コネクティングオービットの数値的存在検証法を,精度保証付き数値計算を基に,与えることを目的とする.具体的には,コネクティングオービットの数値的存在検証の問題が多点境界値問題に帰着し,これが著者の提案した非線形境界値問題の解の数値的存在検証法によって解かれることを指摘する.この数値的存在検証法は従来のコネクティングオービットの数値計算法を補完するもので,コネクティングオービットの近似とそれが発生する固有値(これをコネクティングオービット対と呼ぶ)の近似c=(x_a(t),λ_a)が与えられたとき,cの近くに(1)の真のコネクティングオービット対が存在するための十分条件の成立を精度保証付き数値計算により検証するものである.存在検証に成功したときには,同時に,cと真のコネクティングオービット対との間のシャープな誤差評価も与えられる.

Duffing方程式の周期解の分岐集合を精度保証付き数値計算により実用的な時間内で数値的に存在検証できることを示す.具体的には,Tuning Point、Non-odd symmetric解の発生、1, 2分数調波解の発生などについて論じる。実際の数値検証結果についても示す。

本報告では,有限次元非線形方程式に対する精度保証のアルゴリズムを提案する.まず最初に,与えられた近似解を用いて真の解を含むような区間を得るアルゴリズムを示す.この方法は区間演算を利用し,方程式の表現誤差を考慮に入れたものである.次に,その区間を任意に小さく縮小できるような区間反復法を示す.ここでは有理数演算が用いられ,また有理数の丸めが効果的に使用されている.最後に,このアルゴリズムを計算機上への試作と,幾つかの数値例について報告する.

Duffing方程式の周期解を実用的な時間的で数値内に存在検証できることを示す.また,任意の精度で真の周期解を数値的に与えられることを示す.実際にこのような精度保証付き数値計算ができることを,数値シミュレーションを実際に行うことによって示す.

1はしがきソリトンやカオス等の新たな非線形現象の発見や、VLSI等の発展により、非線形システムの解析は益々重要性を加え、そのより精緻な新しい解析手法の開発が要望されている。本研究は、非線形システムの構造とダイナミックスに関し、本研究者等が開発した新しい解析手法によって徹底的な検討を加え、その基本的性質を明らかにして、具体的諸問題への応用の基礎を築くことを目的として、三年間に渡って遂行された。2研究成果本研究では、近代数学が生み出した新しい概念による数学的手法を開発しつつ、非線形システムの構造とダイナミックスに関する基本的な諸性質を解明する理論を展開し、その結果、実際的諸問題への応用の基礎を与えた。具体的には、そのための創造的・効果的な手法として、新たに(1)非決定性作用素に関する関数解析的手法(2)ホモトピー法や分割解法に基づく非線形システムの数値解析技法(3)ソリトン等の非線形波動を解明する新しい方法論を開発・展開して、一般的な非線形システムを解析する方法論を論ずると共に、(4)電子回路における非周期アトラクタの実験による観測とシミュレーションによる検証およびカオス的であることの理論的証明(5)送風機およびMultibodyシステムのダイナミックスの解析とそのモデリング(6)光伝送系や生体系でのカオス現象モデルの解析を行って、その基本的性質を解明した。本研究は所期の成果を得て、その目的を達成したと考えられる

昭和63年度は本研究のまとめの年として以下の事項について総括的な検討を加え、実用システムのプロトタイプを製作した。1.図画・文書の電子ファイルシステム対象図画として、地図・文書・一般図画をとり上げ、各々を図面解析し書式等を自動的に認識し生成するシステムのプロトタイプを作成した。これらはCCITT及びISOで検討されているドキュメントプーキテクチャの概念にのっとったものである。特に新聞紙面の自動解析技術においては、図面としてのレイアウトストラクチャからロジカルストラクチャを抽出する限界について深く検討した。その他、地図図面や他の図画についてのドキュメントアーキテクチャを検討し、これら文書・図面などはドキュメントアーキテクチャの思想の基に共通のデータ構造として表現できることがわかった。2.高詳細画像の電子ファイル化システム高詳細な画像データ及び動画などを、ディジタルストレージメディアあるいは高速のパケット網に伝送するデータ構造を提案した。この方式によれば論理的な共通方式のもとに画像情報、とりわけ動画情報を伝送することができる。またこの方式をドキュメントアーキテクチャの一構成要素としてとり込むことも可能であり、その為のコンテントアーキテクチャの整備を今後の課題として残している。3.文書図形・画像情報伝送におけるセキュリティ対策文書図形・画像情報特有の性質を利用した、ディジタル透かし方式を提案した。本方式は従来の情報暗号化方式とは性質を異なったもので、文書図形・画像情報をその構成要素と変換関数としてとらえ、この変換関数を他のものに変えて伝送する方式で、ドキュメント管理センタをおくことで、より安全性の高い情報伝送ができる

本年度は、(1)相互情報量に基づく音韻性抽出、(2)非定常態を対象とした特徴抽出、(3)生成モデルに基づいた特徴抽出、(4)聴覚における時系列信号の特徴抽出、(5)音響的特徴の音韻環境依存性、(6)深い意味理解に必要な音響的特徴の抽出精度、の6点をテーマとして研究を行なった。(1)では、個々のフレームにおける音響的情報を多角的に把握し、それらを用いて音韻コンテキストを考慮した音韻性の特徴抽出を実現するために、特徴量相互の情報量を基準とした音韻性抽出手法について検討した。ここでは、複数の音響的特徴量を階層的に用いることにより、音響的類似性に基づいた分類、時系列的な出現パタンによる分類を行い、音韻性の記述は、まずフレーム単位に音韻候補及びその確からしさを示しさらに確実性のある音韻候補情報を用いて不確実な音韻候補の修正を行うことで実現した。(2)では、有声音を対象として、非定常波形の分析・特徴抽出を行なう構造モデルについて検討した。二連インパルス応答からなる非定常波形にPSE分析を適用したとき現われるFMスペクトルにスペクトル(ホルマント)の変化の方向性の情報が折り込まれていることが示された。(3)では、AbS型の調音パラメタ推定法を対象としてアルゴリズムの並列化を行なった。(4)では、人工内耳の基礎研究から、モルモットおよび重度難聴者の聴神経における時系列刺激の応答を調べ、人工喉頭の基礎研究から母音波形のゆらぎが音声の自然性にどのように寄与しているかを明確にした。(5)では、音響的特徴量が前後の音韻コンテキストから受ける影響について、数量化理論を非線形に拡張したモデルを用いて検討した。(6)では、地口の解釈を含む「深い意味理解」を実現するという高度な枠組みの中で必要とされる音響的特徴の抽出精度について検討した

本研究ではシステムダイナミックの独創的で応用範囲の広い方法論を確立することを目標とした。本研究の成果は以下の通りである。I.非線形ダイナミックシステムの非線形関数解析に基づくシステム変動の解析及び無限次元システムの数値解析手法に関する研究非決定性作用素論を用いて非線形システムの不確定的動揺の許容性に関する理論を展開・総合化し,非線形システム変動の関数解析手法を確立した。また,無限次元ホモトピ-法と事後誤差評価に基づく数値誤差制御法を開発し,無限次元システムを含む非線形システムの大域的かつ誤差の制御ができる数値解析技法を確立した。II.電子回路の局所及び大域分岐現象に関する研究幾つかの単純な非線形回路の分岐現象を実験,シミュレ-ションおよび厳密解析の3方面から詳細に検討した。その結果,興味深い大域的分岐現象を幾つか発見した。また,区分線形系を扱うことにより,その区分線形性を巧みに利用し,数値積分公式では不可能であった諸現象をシミュレ-ションにより観測する手法を与えた。III.非線形ダイナミックシステムの数値解析技法に関する研究非線形ダイナミックスシステムの数値解析技法の効率化に関して,非線形写像の分離性を利用する立場から研究を行った。特に非線形回路解析,非線形計画問題,通信路容量の計算問題,周期振動解の分岐問題,非線形方程式の全ての解を求める問題などに対して効率のよい解法を与えた。IV.ダイナミカルシステムのモデリングとその多体系への応用ボンドグラフに基づくダイナミカルシステムのモデリング手法を用いてダイナミクスの定式化を行い,記号処理言語により運動方程式の自動導出アルゴリズムを構築した。これを元に,柔軟多体動力学系等の効果的モデリング・数値積分手法を開発した

1.自然語文や図形の意味を総合的に取り扱いうる認識表現の研究、及び自然語文・図形の解析と認識表現の生成を行うシステムの研究についてこれまでに構築したプロトタイプシステムの拡張のために、画像データ処理部についてアルゴリズムの再検討を行い、その結果に基いて図形処理ツールの拡張を行った。2.自然語文・図形の理解と問題解決プロセスに関する研究について本年度は特に、(1)数学文章題を解くシステム(2)高校化学の問題演習型知的CAIシステム(3)高校経済の教科書や新聞記事を読んで文章を理解するシステム 等を題材として、文章理解・対話制御・問題解決に関する諸問題の検討を行った。(1)については、数学の問題を解くために必要な知識を整理し、教師の助言を受け付ながら問題を解くシステムのプロトタイプを構築した。(2)については、特に教育への利用の便宜を考慮しつつ化学の教材知識について整理し、また問題解決プロセスについて検討した。更にこの求解結果を用いて対話指導を行う手法について考察し、以下の2つの能力を実現する対話制御手法を提案した。(1)外界からの情報を常時取り込み、得られた情報を直ちに行動に反映させる事が可能(2)状況に応じて多様な教授方法を実行可能これらの成果に基づいて問題演習型知的CAIシステムの問題解決部及び対話部を構築した。(3)については、人間が文章を読み取る際に生じるイメージをモデル化し、計算機が文章を読み取りながらこの様なイメージを構築することによって、概念間関係の推定や指示語の同定などを行って文章を理解する手法について検討した。また、この手法に基づいて新聞記事を読み取る文章理解システムのプロトタイプを構築した

本年度は、昨年度に引続き高校化学を対象とする知的CAIシステムと学生の対話を題材として、人間-機械間のコミュニケ-ションに関する基礎的検討を行った。特に、学生に知識を効果的に伝授するための教師の発話内容と、そのような発話能力の実現方法について検討した。問題演習を通じて、学生により本質的な理解をさせるためには、求解に利用される知識がどの様な理由で成立するかを教える必要がある。ここではこの理由を知識の成立原理と呼ぶ、知識の成立原理を説明する能力を実現するため、まず高校化学の計算問題で利用される知識を分類した。さらに各タイプの知識毎に、その成立原理を説明するためにシステムが把握すべき事柄について整理した。その結果、利用される知識は数量間関係の知識、化学現象の知識、物質・物体に固有な構造・属性についての知識等に分類され、知識の成立原理として、問題で扱う系の各時点での状態(実体概念の属性値や実体概念間の位置関係、接続関係、包含関係等)、系に働く作用、系に生じる変化、及びそれらの相互関係等が重要な役割を果たす事が明らかになった。これらり事柄を教育システムが把握するためには、系の状態を、系に働く作用や、それによって生じる変化を考慮してシミュレ-トし、化学現象に関するモデルを構築する機構を持つ必要がある。そこで化学現象モデルについて検討を行い、具体的なモデル表現手法を提案した。提案されたモデルは、(1)演修問題を解くための知識と関係づけられており、その知識の成立原理を説明する際に利用できる、(2)系の状態・作用・変化の関係を陽に記述できる,等の特長を持つ。以上の成果をもとに,ワ-クステ-ション上に演習問題求解システムを構築し、昨年度の成果である対話システムと接続して、知識の成立原理を説明できる対話型教育システムを実現した

近年,非線形性を本格的に活用したシステムや技術の研究が飛躍的な発展を遂げている。光ファイバにおけるソリトン通信やニューラルネットワーク,ファジイシステム,アナログVLSIなどがその例である.しかしVLSIに代表されるように,これらの非線形システムは大規模化,高精度化が進み,既存の方法ではもはや解析が不可能で,非線形効果を十分に活用するための効率的なモデリング及びシミュレーション技法の開発が緊急の課題となっている.また,このような非線形システムの計算機援用設計において,計算結果の精度保証を行うことが多くの分野で重要視されている.例えばVLSI設計では,モデリング及びシミュレーションの精度を各プロセスで確認できれば,設計機関とコストを短縮させることが可能となる.本研究では非線形システムのモデリングの精度を考慮し,更にそのモデリングを用いたシミュレーションの精度を保証することによって,非線形システムのシミュレーションプロセス全体の精度保証を行う方法を確立した.同時に,本申請者らが開発した独自の理論を導入することにより,計算速度を向上させ,大規模システムへの適用の可能性を切り開いた.本年度は,前年度までに確立した理論,アルゴリズム,及びシステムを更に発展させ,様々な工学的問題に対する実用的解法とするための検討を行った.1.昨年度までに開発したファジイ写像によるモデリング理論の有効性をシミュレーションによって確認した.2.常微分方程式一般に対する自動的な精度保証技法を開発し,過渡解析における厳密な手法を確立した.3.全解探索法で用いられた技法を発展させ,集合値写像の解集合の包み込み技術を開発し,精度保証付きモデリング技法と併せてより厳密なシステム解析技法を与えた

本総合研究に関し都合6回の会合をもち、研究状況の報告、情報交換及び研究討論を行なった。また、シンポジウム等で多数の発表を行なった。主な結果を列挙すると以下の通りである。1.本研究に直接関係する従来の多数の研究発表の整理を行ない、現状の解析手法の分析を行った。2.分布定数回路の特性インピーダンスZ_0(s)を有理正実関数近似する必要性を示すとともに、有理関数近似の一方法を与え、従来法よりも優れた結果を得た。3.多相・多分岐伝送回路網の過渡解析法に対し新提案を行い、シミュレーションによりその有効性を確認した。4.数値計算法全般に関する問題として、精度保証つき計算法の計算精度を高める方法を提案した。5.非線形回路解析の基本的問題として、区分線形方程式の効率的全解探索法を提案し、またKazenelson型の新しいアルゴリズムを与えるともにその2次収束性を証明した。6.分布定数形(配線)の周波数域でのシミュレーションと集中定数系(理論ゲート)の時間域でのシミュレーション結果とを波形緩和法で統合して回路全体の過渡波形を求める方法について検討した。7.汎用回路解析アルゴリズムを並列化し、並列コンピュータにインプリメントを行なった。さらに、統合回路シミュレーションプログラムの基本的な部分を開発し、インプリメントを行なった。誘電体フィルタに対する分布・集中混在モデルを提案し、実験結果とのフィッティングを行ない、従来法よりも広帯域で一致することを示した

研究期間の前半においては、基礎理論の確立と計算機援用ソフトウェアの構成要素の作成を目標として進められ、研究計画通りの進展が見られた。具体的には、(1)非線形解析の基礎となる不動点定理について、系の不確定性をモデル化したファジィ写像の不動点定理を示した。(2)非線形常微分方程式の境界値問題や一般的な非線形作用素方程式の解の数値的な存在検証に適した理論を構築した。これは、Newton法の収束定理を計算機により自動的に検証する方法である。(3)C++言語及び有理数演算を実行できるオブジェクト指向言語をもとに、区間演算、自動微分、関数展開などに付随する様々なオブジェクトを柔軟に扱い得るオブジェクト指向ソフトウェアのプロトタイプ3種類構築した。このソフトウェアにおいて、非線形計算解機解析用のソフトウェアライブラリの作成を進めた。(4)分岐現象の数値的検証が可能となるような方程式系を拡張することによって、特異点を解消するための理論の構築を進めた。また、構築した理論をサドル-ノード分岐、Hopf分岐、対称性破壊分岐などに適用し、実際にこれらの分岐現象の存在が数値的に検証可能なことを示した。(5)ホモクリニック軌道、ヘテロクリニック軌道の存在を数値的に検証するための一般理論を展開し、実際にホモクリニック分岐の存在検証を、適当な例に対して行った。(6)有限次元方程式の有界領域の全ての解の存在を数値的に証明するためのアルゴリズムを作成し、適当な条件下でその有限時間停止性を示した。(7)VLSI回路の方程式などセパラブル性を持つ方程式に対し、上記のアルゴリズムを高速化するための手法を開発した。これは、解の存在しない領域を線形計画法を有効に援用して、高速に見出す方法に基づく。研究期間の後半においては、前半に確立した理論を、作成した非線形計算解析用のソフトウェアのプロタイプに組み込み、総合化、洗練化することによりしなやかな非線形計算援用解析ソフトウェアシステム実現の組織的研究を行った。具体的には、(1)区間演算ソフトウェアの計算速度を区間演算の精度に応じて可変とし、精度が要求されない場合には超高速に、高い精度が必要な場合にも高速に計算できる方式を確立した。これと自動微分など各種オブジェクトに対する演算時間の高速化をはかり、プロトタイプソフトウェアの高速化及び柔軟化を達成した。(2)前半に確立した精度保証付き数値計算技法をプロトタイプソフトウェア上で実現し、各種の具体的な非線形関数方程式に適用して実現性を向上させつつ、有用性を検証した。特に、分岐現象の計算機解析を回路系、化学系の非線形方程式に適用して研究を進めた。(3)精度がそれほど要求されない場合の手法と高精度解法を融合し、与えられた精度に応じて、その精度の解を高速に求める手法を確立した。また、その手法をプロトタイプソフトウェア上で実現し、回路方程式を例にとってその解の高速求解が達成されることを検証した。(4)以上のような組織的研究を総合して、改めて問題の変更や精度の変更などに柔軟に対応できるしなやかな非線形計算機援用ソフトウェアのプロタイプを作成し、その有用性を回路系の非線形問題に適用して検証した

個別の問題によらない共通的精度保証方式の開発および従来方式の拡張・改良を計る、液体の流れ問題などの自然界における具体的現象に即した個別問題の精度保証、および関連数値解析技法の検討を行った。研究を進めるに際しては、代表者(中尾)が全体をとりまとめつつ、各研究分担者と関連研究者の協力を得て恒常的に検討を進めた。主な研究実績は以下の通りである。・共通的精度保証方式1.中尾、山本野人、渡部は共同して偏微分方程式の解に対する精度保証方式について検討し、具体的計算アルゴリズムの開発について研究を進め、楕円型境界値問題に対する従来方式の拡張として以下の成果を得た。(1)非線形楕円型方程式の球対称解の分岐曲線の包み込み(2)2階楕円型作用素の固有値の精度保証の定式化とその実現(3)変分方程式の解に対する数値的検証法の定式化と数値例(4)Stokes方程式の有限要素解に対する構成的a posteriori/a priori誤差評価(5)定常Navier-Stokes方程式の解に対する数値的検証アルゴリズムとその数値例2.大石は高速精度保証アルゴリズムの基本的な方法を確立し実際的なアルゴリズムを実現した。3.菊地は電磁場問題の有限要素法に関する誤差解析について、理論的・数値的知見を得た。4.酒井は主に常微分方程式の近似解のスプライン関数による表現法について研究を進めた。5.藤野は全根同時反復の加速法、および並列計算機上での高速化技法の研究を進めた。6.三井は常微分方程式の初期値問題の解に対する精度保証方式について検討した。7.山本哲朗はDirichlet問題に対するShortley-Weller型差分析の誤差精度の理論的・数値実験的検討を進めた。・個別問題に対する精度保証に関する研究1.田端は流体方程式に対する有限要素法による数値計算の誤差精度に関する考察を行った。2.西田は流体方程式系の解空間の構造を解析するために、計算機援用証明法の研を行った。3.西田は流体方程式系の解空間の構造を解析するために、計算機援用証明法の研究開発を進めた。4.室田は構造工学の分野における計算の信頼性に関し、群論的分岐理論を用いた考察を行った

本研究は精度保証付き数値計算の高速化に関する研究成果をまとめたものである。以下、本研究の目的と研究成果について述べる。1.本研究の目的と必要性浮動小数点演算による計算には(a)丸め誤差、(b)方程式を近似する離散化誤差、(c)反復解法を有限回で停止する打切り誤差が生じる。精度保証付き数値計算はすべての誤差を厳密にかつタイトに評価することを目的とする。本拠点形成においては、各種の計算システムの効率的でユニバーサルな精度保証方式を開発することを目標としている。特に、数値計算の基礎となる、線形計算において、近似解を求めるのとほぼ同じ計算量で精度保証することを目的としている。この目標は画期的なもので、従来は近似解を求める計算時間の1万倍に及ぶ計算量が精度保証に必要であった。2.研究成果著者はベクトルや行列の加減算と行列の乗算に対する区間演算が丸めの方向の指定を2回行うだけで実行でき、また、行列の加減算と乗算のライブラリをそのまま用いて実行できることを示した(ベクトル区間演算の提案)。また、近似計算の各ステップを区間演算に置き換えるのではなく、近似解を普通に計算した後、その近似解に対し、摂動定理などの事後誤差定理により、精度を計算する手法を採用した。これにより、近似解の計算時間の9倍の計算時間で精度保証できることを示した。更に、後退誤差解析を発展させた理論により、近似解を求めるのとほぼ同じ時間で連立一次方程式の数値解の精度保証ができることを示した。従来比、1000倍から10000倍の高速化である。また、IEEE754規格に従う各種計算機に適用できるユニバーサルな方式であり、PCクラスターにより蜜行列で3万次元、疎行列では数百万次元まで実際に扱えることを実証し、精度保証が一気に実用段階に達した

平成13および14年度とも、個別の問題によらない共通的精度保証方式の開発および従来方式の拡張・改良をはかるとともに、流体力学や振動問題などの具体的問題に依存した応用解析学上の問題に対する、計算機援用証明を行った。また、精度保証に関連する数値解析技法の検討を行った。主な研究実績は以下の通りである。・共通的精度保証方式(1)楕円型境界値問題の解の数値的検証に関し従来方式の拡張改良として以下の成果を得た。(i)微分項を含む方程式に対する解の検証において、有限次元部分の計算法の効率化を行い検証対象の拡大を計ることに成功した(中尾、渡部)(ii)重複または近接固有値をもつ楕円型固有値問題の精度保証を実現した(中尾、渡部)(iii)double turning pointの検証定式化とそのperturbed Gelfand方程式への適用を行った(皆本)(iv)非線形楕円型方程式の厳密解で線形化した固有値問題の精度保証付き計算(中尾、長藤)(2)周期解を持つDuffingタイプの非線形発展方程式の分岐点自体の存在に対する検証を定式化し、その具体的検証例を与えた(川中子)(3)第2種変分不等式の解に対する数値的検証方式を定式化し、その具体例を与えた(中尾)(4)非線形方程式、連立一次方程式の解の高速精度保証のアルゴリズムを検討し、その効率化を行った(大石、陳、藤野)(5)有限要素解の近似能力を精度保証付きで検証するために、任意メッシュ上での最良apriori誤差評価定数の精度保証付き計算法について検討した(山本野人)(6)高精度多倍長演算方式の検討とその具体的応用例を与えた(今井、磯)(7)adaptiveなメッシュによる差分解法の収束性について検討し2点境界値問題の特異解に対する適用性に対する知見を得た(山本哲朗)・個別問題に対する精度保証に関する研究(1)理論的証明の困難な熱対流問題の分岐解に対し計算機援用方法による数値的証明を行った(中尾、西田、渡部)(2)Kolmogorov問題について計算機援用証明を行いaspect比と安定性の関係に対する知見を得た(長藤)(3)Orr-Sommerfeld方程式の固有値問題の精度保証により不安定解の存在を数値的に検証した(中尾、渡部)(4)電気回路問題に現れる非線形方程式の解の精度保証付き計算(奥村

研究期間中、各分担者とも、個別の問題によらない無限次元・有限次元の共通的精度保証付き数値計算およびその関連数値計算方式の開発に対して恒常的に取り組み、その改良・拡張と、新たな方式の検討を行った。また、実際の現象に即した問題に対する、数値的検証の実例も与えその有効性の実証に努めた。また、内外の研究集会に参加し、講演討論を行い、研究成果の発信を行うとともに活発な研究情報を交換し、新たな研究の進展を図った。主な研究実績は以下の通りである。1.共通的数値検証理論とその実装(1)任意領域における楕円型方程式、定常Navier-Stokes方程式の解に対する数値的検証のために、Poisson方程式、および2次元重調和方程式の有限要素解に対する構成的事前誤差評価について検討し、十分な実用性をもつ評価定数の算定を行った。(中尾、山本、田端、土屋)(2)非線形楕円型方程式のdouble-turning-pointの数値検証を定式化しその実例を与えた(皆本)(3)1階微分項を持つ2階楕円型方程式の数値検証の効率化について検討した(中尾、渡部)(4)線形化作用素の逆作用素ノルムを直接評価し、それを用いた無限次元Newton法にもとづく新しい検証方式の検討を行い、その適用による有効性を確認した。(中尾)(5)有限次元一次相補性問題の解の精度保証付き計算について検討しその方式を定式化した(陳)(6)連立一次方程式の解の高速精度保証について検討しその大幅な改良を得た(大石)(7)多培長演算ソフトウェアを実装し超高精度近似解の計算を可能とした(今井)(8)非線形振動問題に関する計算機援用可能な分岐理論を定式化しその応用例を与えた(川中子)2.個別問題の解に対する数値的検証方式とその適用(1)2次元熱対流問題の大域的分岐解の検証付き追跡および分岐点の存在検証を行い、さらに3次元問題に対してもその拡張を図った(西田、中尾、渡部)(2)線形化Navier-Stokes作用素の固有値問題であるKolmogorov固有値問題の精度保証付き数値計算によりトーラス上の流れの安定性を検証した(長藤)(3)水面波の数学モデルであるNekrasov積分方程式の精度保証付き数値計算を実現した(村重

非線形偏微分方程式に対する解の数値的検証法の開発とその適用を中心として研究を進め、特に、これまでほとんど研究例を見ない非線形発展方程式に対し、十分有効な数値的検証原理を見出すことに成功した。また、従来から蓄積してきた楕円型方程式の解に対する解の検証方式に新たな知見を加え、その拡張・改良を行うとともに、流体方程式をはじめ理論解析が困難な実際問題に適用して数値的証明を行い、その有効性を実証した