Interval Analysis and Constructive Mathematics (16w5099)

Arriving in Oaxaca, Mexico Sunday, November 13 and departing Friday November 18, 2016

Organizers

Helmut Schwichtenberg (University of Munich)

(University of Canterbury)

(University of Canterbury)

(University of Louisiana at Lafayette)

(University of Texas at El Paso)

(Tijuana Institute of Technology)

(University of Canterbury)

Objectives

We aim to bring together about 40 leading researchers from two major research groups: one working in interval arithmetic (IA), the other in various aspects of constructive mathematics (CM). As outlined in the workshop description, opportunities to bring these fields together seldom arise, but will undoubtedly shape the direction of both fields for some time. It is expected that considerable cross-fertilisation of research will occur across the groups. The interaction of these areas is increasingly in demand within the global research community as both computers and mathematics evolve. The proposed workshop begins to address this need.

The central theme will be to apply ideas and methods used by each group to the research of the other---for example, to develop the interval-analytic constructive theory of the real numbers in such a way that it could have serious practical application in numerical analysis, or to use notions traditionally bound to IA to provide insight into more general issues of computability. From the current state of the art, we expect the following emerging topics will play an important role in the workshop:
  • exact real number arithmetic;
  • issues of convergence and confirmation of computability;
  • unifying approaches---combining the a priori methods of constructive proofs with the a posteriori approach of interval arithmetic;
  • program verification and extraction from proofs, which has many open problems and an impressive emerging track record.


Problems in these areas are spurring approaches previously overlooked, and we hope to make big steps in both disciplines. Specific goals include:

  1. extraction of IA algorithms from constructive proofs;

  2. determining the constructive content of IA algorithms;

  3. using constructive proofs to provide convergence rates for IA algorithms;

  4. the constructive development of interval analysis.



Promising progress towards these goals already exists---for example: W. Tucker's interval arithmetic proof that the Lorenz attractor is, in fact, an attractor (can this proof give insight into a constructive version?); and U. Berger's investigations into algorithm extraction from classical proofs. There is accelerating progress in each of these areas, and the emergence of new connections and applications partially drives this proposal. Past experience tells us that a focused workshop is the perfect setting for meeting these aims. The group size is large enough to bring together experienced and acknowledged leaders in the field as well as emerging researchers, yet small enough to foster productive collaboration and new interaction. Participants have been carefully selected to maximize benefit for both research communities. Furthermore, the workshop will provide an opportunity for selected early-career researchers to interact with, and learn from, experienced colleagues in both IA and CM. We expect that the outcome of this interaction will be a tremendous boost to both fields, and have an important impact in the scientific community.

Another tangible benefit of the workshop will be the fostering of cutting-edge research in Mexico, and the formation of a global research network of interval- and constructive-analysts. Also, the workshop will promote dialogue and continue the formation of a growing network of mathematicians to share experience and solutions, and partnerships both inside and outside of academia. Given the importance of practical applications (from accurate robotics to biological simulations) and the increasing importance and acceptance of computer-aided proofs, this workshop is poised to provide a wide range of benefits for the North American research community and society as a whole.