Search the Dagstuhl Website
Looking for information on the websites of the individual seminars? - Then please:
Not found what you are looking for? - Some of our services have separate websites, each with its own search option. Please check the following list:
Schloss Dagstuhl - LZI - Logo
Schloss Dagstuhl Services
Within this website:
External resources:
  • DOOR (for registering your stay at Dagstuhl)
  • DOSA (for proposing future Dagstuhl Seminars or Dagstuhl Perspectives Workshops)
Within this website:
External resources:
Within this website:
External resources:
  • the dblp Computer Science Bibliography

Dagstuhl Seminar 11411

Computing with Infinite Data: Topological and Logical Foundations

( Oct 09 – Oct 14, 2011 )

(Click in the middle of the image to enlarge)

Please use the following short url to reference this page:





In safety-critical applications it is not sufficient to produce software that is only tested for correctness: its correctness has to be formally proven. This is true as well in the area of scientific computation. The problem here is that the current mainstream approach to numerical computing uses programming languages that do not possess a sound mathematical semantics. Hence, there is no way to provide formal correctness proofs.

The reason is that on the theoretical side one deals with well-developed analytical theories based on the non-constructive concept of a real number. Implementations, on the other hand, use floating-point realizations of real numbers which do not have a well-studied mathematical structure. Ways to get out of these problems are currently promoted under the slogan "Computing with Exact Real Numbers".

Well developed practical and theoretical bases for exact real number computation and, more generally, computable analysis are provided by Scott's Domain Theory and Weihrauch's Type Two Theory of Effectivity (TTE). In both theories real numbers and similar ideal objects are represented by infinite streams of finite objects.

The seminar focused on two problem areas in the realm of computable analysis and computation on infinite streams:

  1. Algorithms for stream transforming functions with particular emphasis on (i) logical and category-theoretic methods for the synthesis of provably correct programs, (ii) topological investigations of particular stream representations supporting efficient stream algorithms.
  2. Hierarchies and reducibility relations between sets and functions of infinite data as a means of classification. Methods from topology, logic and descriptive set theory were of particular importance in this case.

Infinite streams are infinite words, So there is a close connection to the theory of omega-languages. To study these was a further aim of the seminar. In the last years much interest in the (logical and topological) structure of the infinite words used to represent continuous data as well as how they code the data space has emerged. U. Berger and others are developing a constructive theory of digital computation based on co-induction, and are applying it to computable analysis. The aim is to create a mathematical foundation for (lazy) algorithms on analytical data such as real numbers, real functions, compact sets, etc. Since co-induction admits a particularly elegant formalization, this approach is well suited for computer aided modeling and proving in computable analysis. A concrete goal is to use program extraction from proofs as a practical method for obtaining certified programs in computable analysis.

The theory is based on a category of digit spaces. A typical object in this category is a compact metric space with a set of digits, where each digit is a contracting map. A point is then an infinite sequence of function (digit) compositions and hence represented by the corresponding infinite word. Moreover, for any given finite length, the words of that length over the alphabet of digits define a covering of the given space that allows to exactly locate the points represented by infinite words of digits. The set of uniformly continuous functions between such spaces can be characterized by a combined inductive/co-inductive definition that gives rise, via program extraction, to implementations of such functions as non-wellfounded (lazy) trees. The theory of digit spaces combines known techniques for implementing and verifying stream processing functions (Edalat, Pattinson, Potts, and others) with ideas from co-induction and co-algebra (Jacobs, Rutten, Bertot, Niqui, and others).

H. Tsuiki is pursuing a similar programme, though, from a different perspective. In his case, e.g., every infinite object is represented by exactly one infinite word over { 0, 1, \bot \}, where bot represents "unknown''. It turned out that the encoded space has at most topological dimension n, exactly if there are not more than $n$ occurrences of bot in the corresponding infinite code words. Besides the problem of how to represent continuous data in an ``optimal'' way, it is as well an important task to distinguish between computable and non-computable functions and, in the last case, to estimate the degree of non-computability. Most functions are non-computable since they are not even continuous. A somewhat easier and more principal task is in fact to understand the degree of discontinuity of functions. This is mostly achieved by defining appropriate hierarchies and reducibility relations.

In classical descriptive set theory, along with the well-known hierarchies, Wadge introduced and studied an important reducibility relation on Baire space. As shown by van Engelen et al., von Stein, Weihrauch and Hertling, this reducibility of subsets of topological spaces can be generalized in various ways to a reducibility of functions on a topological space. In this way, the degrees of discontinuity of several important computational problems were classified. It turned out that these classifications refine the so called "topological complexity'' introduced in the alternative Blum-Shub-Smale approach to computability on the reals, which is used in complexity considerations in computational geometry.

Recently, reducibilities for functions on topological spaces have been used to identify computational relations between mathematical theorems. This programme, started by V. Brattka et al., can be considered as an alternative to reverse mathematics. Whereas reverse mathematics focuses on set existence axioms required to prove certain theorems, the approach pursued in computable analysis is to identify the computational power required to ``compute'' certain theorems. The approach, with contributions by M. de Brecht, G. Gherardi, A. Marcone, A. Pauly, M. Ziegler and V. Brattka, has led to deep new insights into computable analysis and has revealed close relations to reverse mathematics, but also some crucial differences. Motivated initially by decidability problems for monadic second-order logic and Church's synthesis problem for switching circuits, researchers from automata theory (Büchi, Trakhtenbrot, Rabin, Wagner and many others) developed the theory of omega-languages which provides a foundation of specification, verification and synthesis of computing systems. Topological investigations in this theory have led to several hierarchies and reducibilities of languages of infinite words and trees. Instead of being just continuous, the reduction functions are now required to be computable by automata of suitable type. The resulting hierarchies (like, for example, the Wagner hierarchy) have sometimes the advantage that their levels are decidable.

Note that even the study of automata on finite words now involves topological methods in the classical form of profinite topology. Recently, deep relations of profinite topology to Stone and Priestly spaces were discovered by Pippenger and developed by Gehrke, Grigorieff and Pin. Again, suitable versions of the Wadge reducibility seem to play an important role in development of this field.

The seminar attracted 51 participants representing 15 countries and 5 continents, and working in fields such as computable analysis, descriptive set theory, exact real number computation, formal language theory, logic and topology, among them 10 young researchers working on their PhD or having just finished it. The atmosphere was very friendly, but discussions were most lively. During the breaks and until late into night, participants gathered in small groups for continuing discussions, communicating new results and exchanging ideas. The seminar led to new research contacts and collaborations. The participants are invited to submit a full paper for a special issue of Mathematical Structures in Computer Science. At least one submission deals with a problem posted in the discussions following a talk. The great success of the seminar is not only due to the participants, but also to the staff, both in Saarbrücken and Dagstuhl, who always do a great job in making everything run efficient and smoothly. Our thanks extend to both groups!

  • Andrej Bauer (University of Ljubljana, SI) [dblp]
  • Veronica Becher (University of Buenos Aires, AR) [dblp]
  • Ulrich Berger (Swansea University, GB) [dblp]
  • Jens Blanck (Swansea University, GB) [dblp]
  • Vasco Brattka (Universität der Bundeswehr - München, DE) [dblp]
  • Matthew de Brecht (ATR - Kyoto, JP) [dblp]
  • Hannes Diener (Universität Siegen, DE) [dblp]
  • Martín H. Escardó (University of Birmingham, GB) [dblp]
  • Willem L. Fouché (UNISA - Pretoria, ZA) [dblp]
  • Sy David Friedman (Universität Wien, AT) [dblp]
  • Stefano Galatolo (University of Pisa, IT)
  • Guido Gherardi (University of Bologna, IT) [dblp]
  • Vassilios Gregoriades (TU Darmstadt, DE) [dblp]
  • Serge Grigorieff (University of Paris VII, FR) [dblp]
  • Peter G. Hancock (University of Strathclyde, GB)
  • Reinhold Heckmann (AbsInt - Saarbrücken, DE) [dblp]
  • Peter Hertling (Universität der Bundeswehr - München, DE) [dblp]
  • Tie Hou (Swansea University, GB)
  • Hajime Ishihara (JAIST - Ishikawa, JP) [dblp]
  • Akitoshi Kawamura (University of Tokyo, JP) [dblp]
  • Takayuki Kihara (Tohoku University, JP) [dblp]
  • Anton Konovalov (A. P. Ershov Institute - Novosibirsk, RU)
  • Margarita Korovina (Manchester University, GB) [dblp]
  • Alexander P. Kreuzer (TU Darmstadt, DE) [dblp]
  • Hans-Peter Albert Künzi (University of Cape Town, ZA) [dblp]
  • Stéphane Le Roux (TU Darmstadt, DE) [dblp]
  • Luca Motto Ros (Universität Freiburg, DE) [dblp]
  • Norbert T. Müller (Universität Trier, DE) [dblp]
  • Damian Niwinski (University of Warsaw, PL) [dblp]
  • Fredrik Nordvall Forsberg (Swansea University, GB)
  • Dag Normann (University of Oslo, NO)
  • Paulo Oliva (Queen Mary University of London, GB) [dblp]
  • Arno Pauly (University of Cambridge, GB) [dblp]
  • Jean-Eric Pin (University of Paris VII, FR) [dblp]
  • Robert Rettinger (FernUniversität in Hagen, DE) [dblp]
  • Carsten Roesnick (TU Darmstadt, DE)
  • Nazanin Roshandel Tavana (Amir Kabir University of Technology - Teheran, IR) [dblp]
  • Jan Rutten (CWI - Amsterdam, NL) [dblp]
  • Matthias Schröder (Universität der Bundeswehr - München, DE) [dblp]
  • Peter M. Schuster (University of Leeds, GB) [dblp]
  • Helmut Schwichtenberg (LMU München, DE) [dblp]
  • Victor Selivanov (A. P. Ershov Institute - Novosibirsk, RU) [dblp]
  • Svetlana Selivanova (Sobolev Institute of Mathematics - Novosibirsk, RU) [dblp]
  • Anton Setzer (Swansea University, GB)
  • Dieter Spreen (Universität Siegen, DE) [dblp]
  • Ludwig Staiger (Martin-Luther-Universität Halle-Wittenberg, DE)
  • Wolfgang Thomas (RWTH Aachen, DE) [dblp]
  • Hideki Tsuiki (Kyoto University, JP)
  • Bill Wadge (University of Victoria, CA) [dblp]
  • Klaus Weihrauch (FernUniversität in Hagen, DE) [dblp]
  • Martin Ziegler (TU Darmstadt, DE) [dblp]

  • Data structures / algorithms / complexity
  • Semantics / formal methods
  • Verification / logic
  • Stream computation
  • Computability in analysis
  • Languages of infinite words
  • Dynamical systems

  • Exact real number computation
  • stream computation
  • infinite computations
  • computability in analysis
  • hierarchies
  • reducibility
  • topological complexity
  • dynamical systems
  • languages of infinite words