II

Size: px

Start display at page:

Download "II"

こうじいなくら
5 years ago
Views:

1 II

2 computer-assisted proof 1 / 64

3 Siegfried M. Rump : [1] I,, 14:3 (2004), pp [2] II,, 14:4 (2004), pp / 64

4 Risch 18 3 / 64

5 M n = 2 n 1 (n = 1, 2,... ) , , Bryant Tuckerman, IBM Thomas J. Watson Center 2 74,207, , GIMPS: Great Internet Mersenne Prime Search 4 / 64

6 Figure 1: IBM Thomas J. Watson Center GIMPS Lucas-Lehmer 3,000 US ,000 US 5 / 64

7 / 64

8 1976 Kenneth Appel Wolfgang Haken Figure 2: 7 / 64

9 Risch = e x2 dx e x2 dx = 1 π erf( 1 x) + C 2 erf(x) := 2 π x 0 e u2 du 8 / 64

10 Johannes Kepler π % Thomas C. Hales = 9 / 64

11 Figure 3: 10 / 64

12 11 / 64

13 = 12 / 64

14 Frank N. Cole AMS Cole = 13 / 64

15 Frank N. Cole AMS Cole = / 64

16 Frank N. Cole AMS Cole = 15 / 64

17 Frank N. Cole AMS Cole = / 64

18 Frank N. Cole AMS Cole = = = / 64

19 Mathematica Maple 18 / 64

20 Mathematica Maple 19 / 64

21 20 / 64

22 21 / 64

23 22 / 64

24 N 0 N 2 23 / 64

25 / 64

26 25 / 64

27 1980 UNIVAC = IBM S/360 William M. Kahan 26 / 64

28 wrap-around x 127 k = 0 k 1 k k + 1 (demo) = = = = = / 64

29 / 64

30 = = / 64

31 ESA = x = 30 / 64

32 31 / 64

33 32 / 64

34 / 64

35 1. IEEE / 64

36 (i) (ii) (iii) (ii),(iii) 35 / 64

37 IEEE IEEE Kahan xxxxxx / 64

38 IEEE / 64

39 IEEE 754 semimorphism IEEE / 64

40 R F r R R F : R F (r) r f F + : R F (r) f r f F r : R F (r) f r f F r : R F (r) f r 0 f r f F r 39 / 64

41 ÊÓÙÒ Ò ØÓ ½ ÊÓÙÒ Ò ØÓ ½ Öµ Öµ Ê Ó Ø Ò ¹ÔÓ ÒØ ÒÙÑ Ö Ö Figure 4: 40 / 64

42 a, b F {,,, } + a b = (a + b) 41 / 64

43 IEEE 754 a, b F (a + b) a + b (a + b) a + b (a + b) = 42 / 64

44 IEEE 754 IEEE 754 = 43 / 64

45 = = = 44 / 64

46 Rump 2 45 / 64

47 Rump 46 / 64

48 1980 S. M. Rump [6] f(x, y) = y 6 + x 2 (11x 2 y 2 y 6 121y 4 2) + 5.5y 8 + x 2y a = 77617, b = f(a, b) IBM S/ : f(a, b) : f(a, b) : f(a, b) IEEE 754 ( x 2 )y 6 + x 2 (11x 2 y 2 121y 4 2) + 5.5y 8 + x/(2y) [5] 47 / 64

49 f(a, b) = / 64

50 2 Ax = b [4] ( ) ( ) A =, b = A ( ) x = A 1 b = IEEE 754 x ( ) x = / 64

51 x r r = (0, 0) T x (demo) MATLAB b = (1, 1) T >> A=[ , ; , ]; >> b=[1; 1]; >> x=a\b, r=b-a*x >> xs=sym(a)\sym(b) % Symbolic Math Toolbox 50 / 64

52 Ax = b x r := b A x r x = 51 / 64

53 A x b A x A x u (1) LINPACK b A x b (demo) 52 / 64

54 W. M. Kahan Significant discrepancies (between the computed and the true result) are very rare, too rare to worry about all the time, yet not rare enough to ignore. 53 / 64

55 [9] Smale 14 [1] 400 Double Bubble [2] / 64

56 π 1 N P N N Q N Q N π P N 2N P 2N = 2P NQ N P N + Q N 2N Q 2N = P 2N Q N 55 / 64

57 π / 64

58 1 P 6 = 2 3 Q 6 = 3 3 [ , ] P6 [ , ] π [Q 6, P 6 ] = [3, ] P 12 = 2P 6Q 6 P 6 + Q 6 [ , ] Q 12 = P 12 Q 6 [ , ] π [Q 12, P 12 ] = [ , ] π [Q 96, P 96 ] = [ , ] π / 64

59 = IGA = = n = = 58 / 64

60 A: n, b: x = e n IGA x x x max 1 i n (x i x i )/2 59 / 64

61 J. H. Wilkinson Wilkinson [10] This does not imply that interval arithmetic is useless, but it does place severe restrictions on the way it can be applied. In general it is best in algebraic computations to leave the use of interval arithmetic as late as possible so that it effectively becomes an a posteriori weapon. = 60 / 64

62 1. IEEE / 64

63 References [1] T. C. Hales: A proof of the Kepler conjecture, Annals of Mathematics, 162 (2005), [2] J. Hass, M. Hutchings, R. Schlafly: The double bubble conjecture, Electron. Res. Announc. Amer. Math. Soc. 1 (1995), [3] W. M. Kahan: The Regrettable Failure of Automated Error Analysis, A Mini-Course prepared for the conference at MIT on Computers and Mathematics, [4] U. W. Kulisch, W. L. Miranker: The Arithmetic of the 62 / 64

64 Digital Computer: A New Approach, SIAM Review, 28 (1986), [5] E. Loh, G. W. Walster: Rump s example revisited, Reliable Computing, 8 (2002), [6] S. M. Rump: Algorithms for Verified Inclusions: Theory and Practice, Reliability in Computing: The Role of Interval Methods in Scientific Computing (R. E. Moore ed.), Academic Press, Boston, 1988, [7] S. M. Rump: Computer-assisted Proofs and Self-validating Methods, Accuracy and Reliability in Scientific Computing (Chapter 10), SIAM, Philadelphia, PA, / 64

65 [8] T. Sunaga: Theory of an interval algebra and its application to numerical analysis, RAAG Memoirs, 2 (1958), [9] W. Tucker: The Lorenz attractor exists, C. R. Acad. Sci. Paris Sér. I Math., 328 (1999), [10] J. H. Wilkinson: Modern error analysis, SIAM Review, 13 (1971), / 64

kokyuroku.dvi

kokyuroku.dvi On Applications of Rigorous Computing to Dynamical Systems (Zin ARAI) Department of Mathematics, Kyoto University email: arai@math.kyoto-u.ac.jp 1 [12, 13] Lorenz 2 Lorenz 3 4 2 Lorenz 2.1 Lorenz E. Lorenz