/ fb6 / tcs / projects /

 

Projekte

Die Arbeitsgruppe Mathematische Logik und Theoretische Informatik ist an zahlreichen internationalen Kooperationen beteiligt:

• Deutschland-China (2008–2011)

  Thema:

  Computability and Complexity in Analysis: Towards a Sound Foundation for Scientific Computations

  Finanzierung:

  Deutsche Forschungsgemeinschaft – Natural Science Foundation of China

  Koordinatoren:

  Prof. Dr. Dieter Spreen (Deutschland)

  Prof. Dr. Decheng Ding (China)

  Teilnehmer:

  • Auf deutscher Seite sind folgende Arbeitsgruppen beteiligt:

    Prof. Dr. Klaus Ambos-Spies (Heidelberg)

    Prof. Dr. Peter Hertling (UniBW München)

    Prof. Dr. Klaus Meer (Cottbus)

    Prof. Dr. Norbert Müller (Trier)

    Prof. Dr. Dieter Spreen (Siegen)

    Prof. Dr. Klaus Weihrauch (Hagen)

    Prof. Dr. Martin Ziegler (Darmstadt).

  • Auf chinesischer Seite nehmen teil:

    Prof. Dr. Decheng Ding (Nanjing University)

    Prof. Dr. Dianchen Lu (Jiangsu University, Zhenjiang)

    Prof. Dr. Hong Lu (Nanjing University)

    Prof. Dr. Kaile Su (Beijing University)

    Prof. Dr. Wei Wang (Sun Yat-sen University, Guangzhou)

    Prof. Dr. Yongcheng Wu (Nanjing University of Information Science and Technology)

    Prof. Dr. Daoyun Xu (Guizhou University, Guiyang)

    Prof. Dr. Liang Yu (Nanjing University)

    Prof. Dr. Xishun Zhao (Sun Yat-sen University, Guangzhou)

    Dr. Qingliang Chen (Jinan University, Guangzhou)

    Dr. Xuxin Mao (Nanjing University of Aeronautics and Astronautics)

    Dr. Yun Fan (Southeast University, Nanjing).

  Projektzusammenfassung:

  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. An important example are autopilot systems for aircrafts. 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”. They are based on the following ideas:

  In traditional analytical mathematics, points of spaces represent the “ideal (total)” result of approximations. In order to give a sound mathematical semantics to programs that have data structures representing such points, the “partial (finite)” objects used to approximate them have to be given the same status of points of a space as the total ones. From a computational view point they are even the first-class citizens, as the other—the total—ones are derived via a limiting process. This has led to new structures (e.g. “domains” in the sense of Yu.L. Ershov and D.S. Scott).

  For proving the existence of certain objects, for example the roots of polynomials or fixed points of operators, one can proceed in a purely abstract way using e.g. proofs by contradiction or compactness arguments. In applications, however, we need not only know that such objects exist, we need a concrete way to get hold of them. This can be achieved in a logic-oriented way by either using a constructive framework in the existence proof or by disclosing the constructive content of classical proofs, or by deriving an effective version of the classical existence result, i.e. by studying whether and how the postulated object can be computed. The latter approach—to a large extent developed by K. Weihrauch and his students and known as Type-Two Theory of Effectivity (TTE)—has led to extensions of traditional models used for computations on discrete objects and the study of their complexity. The full relationship of these approaches is still under investigation.

  A typical feature of computability and of the algorithms doing the computation is their deterministic rule-bounded behaviour. Opposed to this, in the physical world we often have to deal with processes the outcomes of which exhibit a “law-less” (random) behaviour. Considerable effort has been put in making this notion precise, leading among others to the development of the theory of algorithmic randomness and of algorithmic information theory. This allows new insights in such fundamental phenomena as non-computability.

  The research in this project concentrates on the following interrelated problem areas:

  1. Computability notions and models for real numbers.
  2. Effective versus constructive topology.
  3. Algorithmic randomness.
  4. Computability and complexity in higher-order and abstract spaces.
  5. Data structures and efficient algorithms.

  Das Projekt ist Nachfolgeprojekt eines entsprechenden früheren Projekts.

• Deutschland-Russland (2005–2011)

  Thema:

  Berechnungen über nichtdiskreten Strukturen: Modelle, Semantik und Komplexität

  Finanzierung:

  Deutsche Forschungsgemeinschaft – Russian Foundation for Basic Research

  Koordinatoren:

  Prof. Dr. Dieter Spreen (Deutschland)

  Prof. Dr. Yuri L. Ershov (Russland)

  Teilnehmer:

  • Auf deutscher Seite sind folgende Arbeitsgruppen beteiligt:

    Prof. Dr. Peter Hertling (UniBw München)

    Prof. Dr. Klaus Keimel (Darmstadt)

    Prof. Dr. Ulrich Kohlenbach (Darmstadt)

    Prof. Dr. Christian Herrmann (Darmstadt)

    Prof. Dr. Helmut Schwichtenberg (LMU München)

    Prof. Dr. Dieter Spreen (Siegen)

    Prof. Dr. Thomas Streicher (Darmstadt)

    Prof. Dr. Klaus Weihrauch (Hagen)

    Prof. Dr. Martin Ziegler (Darmstadt).

  • Auf russischer Seite nehmen teil:

    Prof. Dr. Yuri L. Ershov (Novosibirsk)

    Prof. Dr. Sergei S. Goncharov (Novosibirsk)

    Prof. Dr. Andrei S. Morozov (Novosibirsk)

    Prof. Dr. Victor L. Selivanov (Novosibirsk)

    Dr. Vladimir Bashkin (Novosibirsk)

    Dr. Margarita V. Korovina (Novosibirsk)

    Dr. Alexandre Kravchenko (Novosibirsk)

    Dr. Oleg V. Kudinov (Novosibirsk)

    Dr. Vadim G. Puzarenko (Novosibirsk)

    Dr. Marina V. Semenova (Novosibirsk)

    Dr. Alexei Stukachev (Novosibirsk).

  Projektzusammenfassung:

  It appears that the intuitive notion of computability in our everyday life actually exists for a broader class of basic structures, not only for the natural numbers or other discrete structures such as the rational numbers, lists, finite strings, etc. The most important structure not in this list is the set of real numbers. Computations involving real numbers abound in engineering and the applied sciences. In these applications real numbers are identified with sequences of rational approximations (which serve as a name for the real number). The computations are done on finite parts of such approximations and produce approximations of the result. In other words, the computations are not performed on the real numbers, which are abstract mathematical entities, but on concrete objects representing them. Such concrete objects can in general be coded by sequences of natural numbers or finite words, i.e., one computes on Baire and/or Cantor space.

  In safety-sensitive areas such as aircraft control it is important that correctness of the used software is formally verified. Starting from a given program this is mostly a hard task. An appealing idea is therefore to try to extract the algorithm that has to be developed from a formal proof of its specification. This idea has first been introduced for formal systems of constructive logic, but proofs in analysis usually use clas- sical logic. Moreover, it has turned out that even in the case of constructive logic, the complexity of the extracted algorithm might be unfeasible.

  Feasibility is an important issue, not only for algorithms on the reals. In many applications such algorithms are known if one allows algorithms that have non-deterministic or probabilistic features. Other applications require the combination of discrete and continuous computations. Appropriate programming languages have to be designed for these tasks, the semantics of which must be defined in a precise way. New mathematical tools are needed to this end.

  Systems that combine discrete and continuous computations (hybrid systems) are broadly used nowadays, e.g., in electro-mechanical systems (robots), in air traffic control, in the control of automated free- ways, and in chemical process control. In many cases the discrete part of such a system uses a simple and highly effective model of computation, which is no longer Turing-complete, e.g. finite automata. Although finite automata fail to serve to solve all decidable problems, they are powerful enough in many situations and algorithms based on them are very fast. Moreover, most of the important problems for them are algorithmically decidable. Parallelism is an important feature of the algorithms used in this area. So Petri nets and similar concepts come into play very naturally.

  The research in this project concentrates on the following interrelated problem areas:

  1. Computability and complexity over topological structures.
  2. Topological models of higher type computations.
  3. Approximable functionals in type theory.
  4. Proof mining in analysis.
  5. Complexity in incomplete models of computability.

  Das Projekt hatte bereits zwei entsprechende Vorgängerprojekte.

• Deutschland-Südafrika (2007–2011)

  Thema:

  Von der Stetigkeit zur Berechenbarkeit

  Finanzierung:

  Deutsche Forschungsgemeinschaft – National Research Foundation of South Africa

  Koordinatoren:

  Prof. Dr. Dieter Spreen (Deutschland)

  Prof. Dr. Vasco Brattka (Südafrika)

  Teilnehmer:

  • Auf deutscher Seite sind folgende Arbeitsgruppen beteiligt:

    Prof. Dr. Peter Hertling (UniBW München)

    Prof. Dr. Klaus Keimel (Darmstadt)

    Prof. Dr. Ulrich Kohlenbach (Darmstadt)

    Prof. Dr. Norbert Th. Müller (Trier)

    Prof. Dr. Helmut Schwichtenberg (LMU München)

    Prof. Dr. Dieter Spreen (Siegen)

    Prof. Dr. Thomas Streicher (Darmstadt)

    Prof. Dr. Klaus Weihrauch (Hagen)

    Prof. Dr. Martin Ziegler (Darmstadt).

  • Auf südafrikanischer Seite nehmen teil:

    Prof. Dr. Vasco Brattka (University of Cape Town)

    Prof. Dr. Willem Fouché (University of South Africa, Pretoria)

    Prof. Dr. Hans-Peter Künzi (University of Cape Town)

    Prof. Dr. Petrus H. Potgieter (University of South Africa, Pretoria)

    Dr. George Davie (University of South Africa, Pretoria)

    Dr. Paul Potgieter (University of South Africa, Pretoria).

  Projektzusammenfassung:

  It appears that our intuitive notion of computability makes sense not only for discrete structures as natural numbers, rational numbers, lists, finite strings etc., but for a much broader class of non-discrete structures like real numbers and other spaces. Computations with real numbers abound in engineering and in the applied sciences. In these applications, real numbers are identified with sequences of rational approximations and computations are executed on finite parts of such approximations and produce approximations of the result.

  In traditional topology, points of spaces represent the “ideal (total)” results of approximations. For the verification of procedures that compute such objects, the “partial (finite)” objects used to approximate them have to be given the same status of points of a space as the total ones. This has led to new structures (e.g. “domains” in the sense of Yu.L. Ershov and D.S. Scott) and a new branch of topology: “asymmetric topology”.

  For proving the existence of certain objects, for example roots of polynomials or fixed points of operators, one can proceed in a purely abstract way using e.g. proofs by contradiction or compactness arguments. In applications, however, we not only need to know that such objects exist, we need a concrete way to get hold of them. This can be achieved in a logic-oriented way by either using a constructive framework in the existence proofs or by disclosing the constructive content of classical proofs, or by deriving an effective version of the classical existence result, i.e., by studying whether and how the postulated object can be computed (computable analysis). Obviously, these approaches are closely related.

  A typical feature of computability and of the algorithms doing the computation is their deterministic rule-bounded behaviour. Opposed to this, in the physical world we often have to deal with random processes. Considerable effort has been put in the development of a notion of algorithmic randomness and of algorithmic information theory. This allows new insights in such fundamental phenomena as non-computability.

  The research in this project concentrates on the following interrelated problem areas:

  1. Computability over topological structures: computable analysis and topology.
  2. Constructive ways to topology and mathematics.
  3. Topological models of computability: domains and asymmetric spaces.
  4. Approximable functionals in type theory.
  5. Proof mining in analysis, hyperbolic geometry and geometric group theory: obtaining uniform effective bounds.
  6. Kolmogorov complexity, Brownian motion, randomness, dynamical systems.

• EU-Projekt COMPUTAL (2012–2015)

  Thema:

  Computable Analysis

  Finanzierung:

  EU-FP7-Programmschema IRSES

  Koordinator:

  Prof. Dr. Dieter Spreen (Siegen)

  Teilnehmende Arbeitsgruppen und Institutionen:

  Deutschland:

  Prof. Dr. Peter Hertling (UniBW München)

  Prof. Dr. Dieter Spreen (Siegen)

  Prof. Dr. Norbert Müller (Trier)

  Prof. Dr. Martin Ziegler (Darmstadt)

  Großbritannien:

  Dr. Ulrich Berger (Swansea)

  Prof. Anuj Dawar (Cambridge)

  Japan:

  Prof. Hajime Ishihara

  (Japan Advanced Institute of Science and Technology, Nomi, Ishikawa)

  Russland:

  Prof. Victor Selivanov

  (A.P. Ershov Institute of Informatics Systems, SB RAS, Novosibirsk)

  Slowenien:

  Prof. Dr. Andrej Bauer (Ljubljana)

  Südafrika:

  Prof. Vasco Brattka (University of Cape Town)

  Prof. Hans-Peter Künzi (University of Cape Town

  Prof. Willem Fouché (University of South Africa, Pretoria)

  Assoziierte Partner:

  Prof. Hideki Tsuiki (Kyoto University)

  Prof. Dr. Klaus Weihrauch (Fernuniversität Hagen)

  PD. Dr. Robert Rettinger (Fernuniversität Hagen)

  Projektzusammenfassung:

  The programme of this interaction focusses on the following related topics: computable analysis, domain theory, topology, and exact real number computation, hereby dealing with both theoretical and applied aspects.

  A major motivation for undertaking this research is the fact that 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 also true in Scientific Computing. 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 realisations 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 certain applications also other computational models are used. Moreover, strengthening the underlying logic has been suggested. The full relationship of these approaches is still under investigation.

  Weihrauch’s TTE is based on Turing machines that by computing infinitely long transform infinite strings. The study of such computations is important also for other branches of theoretical computer science including specification, verification and synthesis of reactive systems as well as stream computability. In contrast to the theory of finite computations, the study of infinite computations crucially depends on topological considerations.