Computing with Infinite Data: Program Extraction from Proofs in a Constructive Logic Extended by (Co-)Inductive Definitions, Its Computational Power, and Applications

• Applicant: Professor Dr. Dieter Spreen
• Subject Area: Theoretical Computer Science ; Mathematics
• Term: since 2024
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 549144494

Computability with finite objects such as the natural numbers is a well-developed subject with first investigations dating back to the first half of the last century. In contrast, interest in computing with infinite objects is much younger. A prime example for infinite data is provided by the real numbers, most commonly conceived as infinite sequences of digits. Since the reals are fundamental in mathematics, any attempt to compute objects of mathematical interest has to be based on an implementation of real numbers. Applications in science and engineering usually substitute the reals with floating point numbers of fixed finite precision. However, this number set is not even closed under the basic arithmetic operations. Consequently, one has to deal with problems arising from the rounding of calculation results and the associated errors. The approach in this project is different: exact real numbers form a basic data type and while any computation can only exploit a finite portion of its input in finite time, increased precision is always available by continuing the computation process. The dissociation between the mathematical theory and its implementation in computer programs is even more a problem when the correctness of software in scientific computations is required to be formally proven, which is particularly the case in the increasing number of engineering applications in safety-critical areas. The proposed project aims to extend the scope of calculations with infinite data and thus expand the scope of applications. It will address fundamental problems that need to be solved to obtain algorithms that are at the same time efficient and formally proven to be correct. A major topic will be computability on high-dimensional spaces and a continuation of the approach to computations on the space of compact sets developed by the applicant. Earlier work on program extraction from inductive and co-inductive proofs will be extended to deal with these problems and guarantee the correctness of the algorithms obtained. The issue of efficiency will be addressed by integrating linear logic, which permits a control of resources, as well as Taylor models that are particularly well-suited to deal with high-dimensional computation problems.

• DFG Programme: Research Grants
• International Connection: France, United Kingdom
• Cooperation Partners: Dr. Ulrich Berger; Dr. Jules Chouquet