#	Pagina
attuale pagina	/open-h2020/projects/207017/results.html

Report

Teaser, summary, work performed and final results

Periodic Reporting for period 1 - CID (Computing with Infinite Data)

Teaser

Summary

The joint research in this programme will study important aspects---both theoretical as well as applied---of computing with infinite objects such as decimal fractions, to mention a key example. A central aim is laying the grounds for the generation of efficient and verified software in engineering applications.

More and more applications require the use of computers, but in many situations computer programs can present inaccuracies due to, for example, rounding errors. However software inaccuracies can create vulnerabilities which can have unexpected consequences. For example, the first Ariadne 5 launch (a rocket used by the European Space Agency) failed due to that kind of inaccuracies. We want to develop tools which can help resolve these inaccuracies. The problem is that there is a dissociation between the mathematical theory and its implementation in computer programs.

At the same time we would like to develop a possibility to formally prove the correct functioning of engineering applications: The autopilot in an aircraft must work flawlessly, also the software of control and monitoring systems in railway traffic. Even with autonomous cars, human life depends on the technology being correct at all times. Software is usually tested against a variety of possible scenarios. However, this often does not guarantee that the software is completely safe since vulnerabilities can still exist and can have unintended consequences, either due to accidents or to malicious behaviour. Using infinite-precision data it should be possible in future to develop tools which can help to formally prove that programs function according to their respective requirements. This would eliminate the need for testing, since we would be sure that the software works correctly.

In another part of the investigation we would like to understand which problems are inherently difficult or even impossible to solve with the help of computers, and how do they fundamentally differ from easier problems. For some problems there are simply no simple algorithms because of their complexity. This knowledge is valuable for software developers, since they do no longer need to spend their time for searching for alternatives in such cases.

Work performed

\"On the applied side much work was done to improve and extend existing software packages using infinite-precision data. Moreover, a programming language for such computations has been devised that supports formal specification and verification of programs.

As is well-known, programs satisfying a specification can be extracted from a formal proof of the specification in calculi of constructive logic. Work on using this property in the development of efficient certified programs using infinite-precision data was carried on. A uniform approach with a wide range of applications was developed allowing dealing with various kinds of infinitary data appearing in engineering applications. A limitation of this approach is that the programs obtained will not contain concurrent features. To overcome this restriction logic was extended appropriately. It was successfully used to extract programs using infinitary Gray code notation for infinite objects like real numbers and certain sets of such. Moreover, an operational small-step semantics for infinite data was developed and an adequacy result proved which says that through successive small-step computations finite approximations are computed that in the limit are equal to the full (infinitary) value of a program. Different proof assistants, that is program systems that allow for the interactive development of formal proofs, have been extended by the new features and test programs extracted.

Another strand of investigations has been dealing with the classification of problems. The classifications refine the distinction between non-computable and computable. In case of non-computability, Descriptive Set Theory was used for such purposes. It classifies problems according to the complexity of their logical description. However, it was developed under assumptions that are not satisfied in the case of structures used in modern program semantics. Much work has been invested to remedy this problem. Quasi-Polish spaces were introduced and it seemed that they form the largest class of sets of infinitary objects to which essential parts of the theory could be extended. Quite recently, however, examples of spaces not belonging to this class were found to which the theory could nicely be extended as well. The examples belong to the class of coPolish spaces, which is now investigated.

Note that the extension of descriptive set theory to quasi-Polish spaces has been achieved by using classical logical reasoning which is not always computationally meaningful. First studies to obtain a computationally meaningful notion of a quasi-Polish space have been done.

Much work has been done for computable problems. First of all, the computability of certain dynamical systems has been studied. A typical example of a \"\"chaotic\"\" attractor arising on systems that have a very complex behaviour and sensitive dependence on initial conditions, which appear in the context of many applications like meteorology, e.g., is the Lorenz attractor. The computability of geometric Lorenz attractors and their physical measured was derived.

Computable problems are classified according to the space and/or time resources necessarily needed for in their computation. The behaviour of further dynamical systems was studied in this respect. It was shown that attractors can be typically computed in an efficient manner but, for some pathological parameters, the cost of computing can be arbitrarily high.

Further highlights in this research are:

- A restriction of the famous 3-Body Problem is computable in polynomial time on average. The 3-body problem features prominently in astronomy, e.g. when the motion of a space shuttle under the gravitational pull of, say, the earth and the moon should be computed.
- One-soliton and two-soliton solutions to the Korteweg-de Vries partial differential equation for shallow water waves are computable in polynomial-time.\"

Final results

As mentioned, an extension of constructive logic was found that allows extracted program to use concurrent computations. This as well as the adequacy theorem for an operational small-step semantics for infinite data which could be derived in this context constitutes a milestone in this kind of research and pushes the frontier far beyond what was known so far. There are numerous situations where the new technique can be applied.

The computability result for geometric Lorenz attractors and their physical measures was a further such achievement. Before this result Lorenz\' research was mainly based on non-rigorous (i.e. truncation-error prone) numerical simulations, and an existence proof for Lorenz attractor was elusive.

As said, in research on extending descriptive set theory to larger classes of spaces quasi-Polish spaces played an eminent role so far. A major discovery was the identification of four spaces which can serve as canonical examples of spaces failing to be quasi-Polish. This result has a strong impact on further research.