projects

International Research Cooperations

The Laboratory for Mathematical Logic and Theoretical Computer Science is partaking in several international research cooperations:

• EU-Projekt CORCON (2014-2017)
• EU-Projekt COMPUTAL (2012–2015)
• Germany-China (2008–2011)
• Germany-Russia (2005–2011)
• Germany-South Africa (2007–2011)

EU-Projekt CORCON (2014-2017)

Topic:

Correctness by Construction

Funding:

EU-FP7-Programme IRSES

Coordinator:

Dr. Peter Schuster (Leeds)

Participating groups and institutions:

Australia:

• Dr. Pattinson (Canberra, ANU)

Germany:

• Prof. Dr. Schwichtenberg (Munich, LMU)
• Dr. Diener, Prof. Dr. Spreen (Siegen)

United Kingdom:

• Dr. Schuster, Dr. Beyersdorff, Prof. Rathjen, Dr. Stell (Leeds)
• Prof. Gani (Glasgow, U Strathclyde)
• Drs. Berger, Blanck, Seisenberger, Setzer (Swansea)

India:

• Prof. Mahajan (Chennai, Inst. Mathematical Sci.)

Italy:

• Dr. Benini (Varese, U della Insubria)
• Profs. Moggi, Rosolini (Genua)
• Prof. Sambin (Padua)

Japan:

• Prof. Ishihara (Nomi, Ishikawa, Japan Inst. Science and Technology)

South Korea:

• Prof. Lee (Anseong-si, Hankyong Nat. U)

New Zealand:

• Prof. Bridges (Christchurch, U Canterbury)

Sweden:

• Profs. Martin-Löf, Palmgren (Stockholm)

USA:

• Profs. Awodey, Avigad, Harper, Sieg (Pittsburgh, CMU)

Associated partners:

• Profs. Tsuiki, Sato (Kyoto)
• Prof. Tatsuta (Tokyo, Nat. Inst. Informatics)
• Prof. Tanaka (Sendai, Tohoku U)
• Profs. Coquand, Dybjer (U Gotheburg)
• Prof. Bauer (Ljubljana)

Project summary:

As software becomes ever more ubiquitous in our lives, the need to ensure it runs without error becomes ever more important. Restarting a phone is a simple, if inconvenient task; restarting an aeroplane in mid-flight is not an option! Correct by construction programming offers a revolutionary approach to program verification where programs can contain not just computations as is normal, but also logical proofs of the correctness of these computations. The simple fact that such programs compile provides formal, i.e. mathematical, guarantees of the correctness of the program. In particular, there is no need for post-hoc testing of software etc. Fundamental to the implicit marriage of computation and logic inherent within correct by construction programming is the choice of the right logical systems and concepts upon which programming languages ought to be built. This reflects the symbiotic relationship between logic, programming, and the design of programming languages—any attempt to sever this connection will diminish each component. This proposal brings together internationally leading researchers from both inside Europe and outside Europe to work on exactly what logical structures are needed for correct by construction programming and how those logical structures can then by turned into concrete programming artefacts. In order to produce fundamental work which stands the test of time, we work not with specific programming languages but with mathematical abstractions of them. The recent development of dependently typed programming languages capable of supporting correct by construction programming makes this a very timely proposal, while the billions spent on software every year makes the potential impact of this proposal very significant.

EU-Projekt COMPUTAL (2012–2015)

Topic:

Computable Analysis

Funding:

EU-FP7-Programmschema IRSES

Coordinator:

Prof. Dr. Dieter Spreen (Siegen)

Participating groups and institutions:

Germany:

• Prof. Dr. Peter Hertling (Uni Federal Forces Munich)
• Prof. Dr. Dieter Spreen (Siegen)
• Prof. Dr. Norbert Müller (Trier)
• Prof. Dr. Martin Ziegler (Darmstadt)

UK:

• Dr. Ulrich Berger (Swansea)
• Prof. Anuj Dawar (Cambridge)

Japan:

• Prof. Hajime Ishihara (Japan Advanced Institute ofScience and Technology, Nomi, Ishikawa)

Russia:

• Prof. Victor Selivanov (A.P. Ershov Instituteof Informatics Systems, SBRAS, Novosibirsk)

Slovenia:

• Prof. Dr. Andrej Bauer (Ljubljana)

South Africa:

• Prof. Vasco Brattka (University of CapeTown)
• Prof. Hans-Peter Künzi (University of CapeTown
• Prof. Willem Fouché (University of SouthAfrica, Pretoria)

Associated partners:

• Prof. Hideki Tsuiki (Kyoto University)
• Prof. Dr. Klaus Weihrauch (Fernuniversität Hagen)
• PD. Dr. Robert Rettinger (Fernuniversität Hagen)

Project summary:

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.

Germany-China (2008–2011)

Topic:

Computability andComplexity in Analysis: Towards a Sound Foundationfor Scientific Computations

Funding:

German Science Association(DFG) – Natural Science Foundation of China

Coordinators:

Prof. Dr. Dieter Spreen(Germany)

Prof. Dr. Decheng Ding(China)

Participants:

• On the German side thefollowing groups are participating:

  Prof. Dr. Klaus Ambos-Spies(Heidelberg)

  Prof. Dr. Peter Hertling (Uni FederalForces Munich)

  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).

• The Chineseparticipants are:

  Prof. Dr. Decheng Ding (NanjingUniversity)

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

  Prof. Dr. Hong Lu(Nanjing University)

  Prof. Dr. Kaile Su (BeijingUniversity)

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

  Prof. Dr. Yongcheng Wu

  (Nanjing University of Information Science andTechnology)

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

  Prof. Dr. LiangYu (Nanjing University)

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

  Dr. Qingliang Chen (Jinan University, Guangzhou)

  Dr. Xuxin Mao (Nanjing University ofAeronautics and Astronautics)

  Dr. Yun Fan(Southeast University, Nanjing).

Project summary:

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. Datastructures and efficient algorithms.

The project is a follow-up of a similar earlier one.

Germany-Russia (2005–2011)

Topic:

Computations overnon-discrete structures: models, semantics and complexity

Funding:

German Science Association(DFG) – Russian Foundation for Basic Research

Coordinators:

Prof. Dr. Dieter Spreen(Germany)

Prof. Dr. Yuri L. Ershov (Russia)

Participants:

• On the German side the following groups are participating:

  Prof. Dr. PeterHertling (Uni FederalForces Munich)

  Prof. Dr. Klaus Keimel (Darmstadt)

  Prof. Dr. UlrichKohlenbach (Darmstadt)

  Prof. Dr. Christian Herrmann (Darmstadt)

  Prof. Dr. Helmut Schwichtenberg (LMUMunich)

  Prof. Dr. Dieter Spreen (Siegen)

  Prof. Dr. Thomas Streicher (Darmstadt)

  Prof. Dr. Klaus Weihrauch (Hagen)

  Prof. Dr. Martin Ziegler (Darmstadt).

• The Russianparticipants are:

  Prof. Dr. YuriL. 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. OlegV. Kudinov (Novosibirsk)

  Dr. Vadim G. Puzarenko (Novosibirsk)

  Dr. Marina V. Semenova (Novosibirsk)

  Dr. Alexei Stukachev (Novosibirsk).

Project summary:

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 overtopological structures.
2. Topological models of higher typecomputations.
3. Approximable functionals in typetheory.
4. Proofmining in analysis.
5. Complexity in incomplete models ofcomputability.

The Project is a follow-up of two similar ones.

Germany-South Africa (2007–2011)

Topic:

From continuity tocomputability

Finanzierung:

DeutscheForschungsgemeinschaft – National ResearchFoundation of South Africa

Coordinators:

Prof. Dr. Dieter Spreen(Germany)

Prof. Dr. Vasco Brattka(South Africa)

Participants:

• On the German side thefollowing groups are participating:

  Prof. Dr. PeterHertling (Uni FederalForces Munich)

  Prof. Dr. KlausKeimel (Darmstadt)

  Prof. Dr. UlrichKohlenbach (Darmstadt)

  Prof. Dr. NorbertTh. Müller(Trier)

  Prof. Dr. HelmutSchwichtenberg (LMUMunich)

  Prof. Dr. DieterSpreen (Siegen)

  Prof. Dr. ThomasStreicher (Darmstadt)

  Prof. Dr. KlausWeihrauch (Hagen)

  Prof. Dr. MartinZiegler (Darmstadt).

• The South Africanparticipants are:

  Prof. Dr. VascoBrattka (University of CapeTown)

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

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

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

  Dr. George Davie (University of SouthAfrica, Pretoria)

  Dr. Paul Potgieter (University ofSouth Africa,Pretoria).

Project summary:

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 andmathematics.
3. Topological models of computability:domains and asymmetric spaces.
4. Approximable functionals in typetheory.
5. Proofmining in analysis, hyperbolic geometry andgeometric group theory: obtaining uniformeffective bounds.
6. Kolmogorov complexity, Brownian motion,randomness, dynamical systems.