Laboratory for Mathematical Statistical Experiments

MATH 469 Computer-Aided Proofs

Aims
This course provides students with an understanding of advanced concepts at the interface of pure mathematics and scientific computing. The aim of the course is to identify the inherent limitations of floating-point computations, and show how to overcome these by the use of a different class of algorithms. We will describe the basics of auto-validating methods, and systematically cover various problems that can successfully be handled. This course presents the theoretical foundations in the weekly lectures and provides the practical coding exercises in the weekly laboratories to familiarize you with some of the basic tools for computer-aided proofs in analysis.

Recommended Books and Lecture Notes

• Validated Numerics: A Short Introduction to Rigorous Computations, by Warwick Tucker, 2011.
• An Introduction to GCC, by Brian J. Gough, foreword by Richard M. Stallman, 2005.
• Lecture Notes Wednesday, 19-Aug-2015 14:51:57 MST
  Pick up a hard-copy of these notes from Erskine 724.

Outline of topics

• Week 01: Introduction, Motivation and Course Logistics
  • Lecture 1: Motivation, Representations of Reals in Positional Number System
• Week 02: Floating-point Numbers and their Machine-Representations
  • Lecture 1: Normal and Sub-normal Numbers and Rounding
  • Lecture 2: Rounding Error and the IEEE Standard
• Week 03: Interval Arithmetic and Analysis
  • Lecture 1: Itervals and Operations on them
  • Lecture 2: Extended interval arithmetic
• Week 04: Extensions of Reals and Interval Reals
  • Lecture 1: Including Points at Infinity
  • Lecture 2: Signed Zeros, machine intervals
• Week 05: Range Enclosures
  • Lecture 1: Enclosing Elementary Functions
  • Lecture 2: Bounding the overestimation, Mean Value Theorem
• Week 06: Automatic Differentiation
  • Lecture 1: Automatic differentiation and its interval extension
  • Lecture 2: Taylor Arithmetic
• Week 07: Complex Interval Arithmetic
  • Lecture 1: Complex numbers and intervals
  • Lecture 2: Rectangular and circular enclosures
• Week 08: Real Root-finding
  • Lecture 1: Binary Search, rigorous divide and conquer
  • Lecture 2: Newton’s Method and it’s interval extension
• Week 09: Extended Interval Newton and Rigorous Global Optimization
  • Lecture 1: Extended Interval Newton Method
  • Lecture 2: Global Optimization, Midpoint, Monotonicity and Convexity Test
• Week 10: Integration and Rigorous Quadrature
  • Lecture 1: Midpoint, Trapezoid and Simpson’s Method and naïve enclosures
  • Lecture 2: Adaptive Taylor Methods for enclosing integrals
• Week 11: ODEs/IVPs and Oral Presentations of Student Projects
  • Lecture 1: ODEs and IVPs and their first-order interval extension
  • Student Presentations 1:
• Week 12: ODEs/IVPs and Oral Presentations of Student Projects
  • Lecture 1: Interval ODEs with higher-order methods
  • Student Presentations 2:

Depending on the interests and strengths of students for 2010 we might be able to touch on extra topics such as, Linear System Solvers (Gauss Elimination and Krawczyk’s Method), computation of long periodic orbits, locating zeros of complex functions, parameter estimation via constraint propagation, multidimensional global optimization, Randomized set-valued algorithms, arithmetics for statistical data-structures, and/or partial differential equations.

Other Course Materials

• Recommended Software: C-XSC: C eXtended for Scientific Computing and C-XSC Additional Software Link.
• This course is designed from Warwick Tucker’s course in Mathematics Department of Uppsala University.
• Useful Links for the course:
  • Supplementary Materials
  • Moore’s Early Papers
• Student Presentations from 2009:
  • October 8, 2009, 1100-1125 hours, Erskine 415,
    Thomas Steinke,
    Long multiplication is too long, but complex numbers are too complex (Abstract)
  • October 8, 2009, 1125-1150 hours, Erskine 415,
    Jennifer Harlow,
    Markov Chains over Regular Subpaving Histograms (Abstract)
  • October 15, 2009, 1100-1125 hours, Erskine 415,
    Josh Collins,
    Trans-dimensional Rigourous Global Optimisation (Abstract)
  • October 15, 2009, 1125-1150 hours, Erskine 415,
    Brendan Bycroft,
    Parallelizing the Global Optimization Algorithm (Abstract)

Last modified on Thursday, 01-Sep-2016 18:35:12 MST and served on Friday, 19-Apr-2024 17:14:09 MST.