[ The Types Forum (announcements only),
http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]
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.
