[TYPES/announce] CID: information on a new research project

[Dieter Spreen]

Dear moderator please forward this information about a new collaboration programme.


CID — Computing with Infinite Data

cid.uni-trier.de <http://cid.uni-trier.de/>


CID is a new international research project with about 20 participating institutions, mainly from Europe, but also from Chile, Japan, New Zealand, Russia, Singapore, South Africa, South Korea, and the USA. It is funded by the European Union as well as several national funding organisations, and is running for four years.

The joint research will study important aspects - both theoretical as well as applied - of computing with infinite objects. A central aim is laying the grounds for the generation of efficient and verified software in engineering applications. 

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. While most applications in science and engineering substitute the reals with floating point numbers of fixed finite precision and thus have to deal with truncation and rounding errors, the approach in this project is different: exact real numbers are taken as first-class citizens 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. We will refer to this mode of computing with real numbers as exact real arithmetic or ERA. These ideas are greatly generalised in Weihrauch’s type-two theory of effectivity which aims to represent infinite data of any kind as streams of finite data. This project aims to bring together the expertise of specialists in mathematics, logic, and computer science to push the frontiers of our theoretical and practical understanding of computing with infinite objects. Three overarching motivations drive the collaboration:  

Representation and representability. Elementary cardinality considerations tell us that it is not possible to represent arbitrary mathematical objects in a way that is accessible to computation. We will enlist expertise in topology, logic, and set theory, to address the question of which objects are representable and how they can be represented most efficiently.
Constructivity. Working in a constructive mathematical universe can greatly enhance our understanding of the link between computation and mathematical structure. Not only informs us which are the objects of relevance, it also allows us to devise algorithms from proofs.
Efficient implementation. The project also aims to make progress on concrete implementations. Theoretical insights from elsewhere will thus be tested in actual computer systems, while obstacles encountered in the latter will inform the direction of mathematical investigation.

The specific research objectives of this project are grouped together in three work packages:

WP1 — Foundations

This foundational study has two aims: (I) to compare two major models for computations with infinite objects, Markov computability and type-two theory of effectivity, and to obtain a better understanding of the first one in structural terms; and (II) to extend (effective) descriptive theory of sets and functions beyond its classical scope of Polish spaces.

A specific goal of (I) is to develop a characterisation of Markov computability in terms of Kolmogorov complexity. Objective II aims at extending Descriptive Set Theory to a Cartesian closed subcategory of Schroeder-Simpson-qcb-spaces, large enough to also contain non-countably based spaces, in particular, at devising specific (descriptive) complexity notions for qcb-spaces so to allow singling out a sufficiently large class of simply enough spaces. Further sub-goals are finding interesting well quasi-ordered substructures of the structure of Weihrauch degrees of multi-valued functions and exploring the interactions between the various notions of effectively presented spaces so as to identify the adequate ones.

WP2 — Exact computation in real analysis

In this investigation the connection between computability and important areas of applied mathematics such as dynamical systems, stochastic processes as well as differential equations will be explored. Moreover, the problem of algorithmic efficiency and computer realisations will be considered.

Research objectives are (I) to determine which long-term (asymptotic) properties of a dynamical system can be computed, at least in theory, and in a more refined manner, which ones can be computed given reasonable amount of resources such as time or memory; (II) to study in how much the theory of Kolmogorov complexity and algorithmic randomness applied to Brownian motion and other stochastic processes may help in understanding the complexity of computational problems over such processes; (III) to measure the computational hardness of problems such as root finding or solving differential equations; and (IV) to improve and extend existing software packages in ERA.

WP3 — Logical representation of data

The goal of this interaction is to exploit the correspondence between computation and (constructive) logic to obtain logic-based representations of data as well as an automatic method  for extracting correct programs operating on these data; moreover, the correspondence will be studied in further detail.

Research objectives are (I) to advance the theory of realisability over abstract structures, investigate concrete applications in computable analysis, and develop a logical approach to control the computational complexity of extracted programs on infinite data; (II) to develop fundamental results of constructive analysis in weak constructive logical systems such as the Minimalist Foundation; (III) to originate a constructive point-free theory of probability and randomness, and to study simplified frameworks for probability theory, based on ‘constructive’ models such as toposes; and (IV) to refine and extend the connections between constructive logic, computation and topology.

A more detailed exposition can be found on the project web page.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.seas.upenn.edu/pipermail/types-announce/attachments/20170413/317432e7/attachment.html>