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 <= q <= p <=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.

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.

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.

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 'verification methods'. 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'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'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's and Ogita-Oishi'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.

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 < u kappa(A) < 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.

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 <= x <= 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) < x(1)(v) < ... < 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) -> 0 as v -> 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 >= v(0), the inverse A(v)(-1) = (g(ij)(v)) exists and vertical bar g(ij)(v)vertical bar <= M, for all(i,j) with a constant M > 0 independent of h(v). (iii) For sufficiently large v >= (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 <= (M) over cap, for all(i,j) with a constant (M) over cap > 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 <= i <= 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 <= x <= 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) < x(1)(v) < ... < 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) -> 0 as v -> 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 >= v(0), the inverse A(v)(-1) = (g(ij)(v)) exists and vertical bar g(ij)(v)vertical bar <= M, for all(i,j) with a constant M > 0 independent of h(v). (iii) For sufficiently large v >= (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 <= (M) over cap, for all(i,j) with a constant (M) over cap > 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 <= i <= 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 <= x <= b, alpha(0)u(a) - alpha(1)u'(a) = alpha, beta(0)u(b) + beta(1)u'(b) = beta, alpha(i) >= 0, beta(i) >= 0, i = 0, 1, alpha(0)+alpha(1) > 0, beta(0)+beta(1) > 0, alpha(0)+beta(0) > 0. Under the assumption inf f(u) > - 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 <= x <= 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 >= 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の方程式を公理として仮定し,素子特性は数理モデルとして与えられていると考えて回路理論を数学的な論理性を保つように展開することを志した。回路理論の論理的展開のためにいろいろな講義展開法についての試行を行い,我が国の定石の講義法とかなり異なっている部分も多い。これらの思索と実践について報告する。

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積分方程式の精度保証付き数値計算を実現した(村重

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