This issue of Logical Methods in Computer Science is composed of selected papers submitted by participants of the Workshop Continuity, Computability, Constructivity: From Logic to Algorithms, held at the University of the Algarve in Faro, Portugal in the second half of September 2018.
The workshop was partially funded by the University of the Algarve, the Japan Society for the Promotion of Science (JSPS), as well as the European Union. It was the seventh in a series of workshops aimed at bringing together researchers from exact real number computation, computable analysis, effective descriptive set theory, constructive analysis, and related fields. The overall objective is to apply logical methods in these disciplines to provide a sound foundation for obtaining exact and correct algorithms. At the same time, the conference was the annual meeting of the CID project, a research network between Europe, Chile, Japan, New Zealand, Russia, Singapore, South Africa, South Korea, and the USA. The project has received funding from the European Union's Horizon 2020 research and innovation programme under the Marie Sklodowska-Curie grant agreement No. 731143.
A central aim for the project collaboration has been laying the grounds for the generation of efficient and verified software in engineering applications. A pivotal problem in current scientific computations is still the dissociation between the mathematical theory and its implementation in computer programs: Implementations of the reals use floating-point numbers of fixed finite precision, whereas proofs of program properties are given on the basis of the classical theory of the real number field.
Ways out of this problem are promoted under the slogan Exact Real Arithmetic in which real numbers are taken as first-class citizens. 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.
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. In both theories real numbers and similar ideal objects are represented by infinite streams of finite objects. They can locally be manipulated by Turing machines. In contrast to the theory of computing with finite data, the study of computing with infinite data crucially depends on topological and measure-theoretic considerations.
A related approach is pursued in constructive analysis by using intuitionistic logic. As is well known, proofs of existential statements in this logic allow the extraction of algorithms computing the object that is stated to exist. By their nature these algorithms are correct. Many important problems are either inherently difficult to compute, or even not computable at all. To measure their computational hardness or the degree of non-computability one uses hierarchies, or compares them with certain well-known master problems.
The present issue contains contributions to all these areas.
As usual, there are many people to be thanked. This is in particular true for the organising committee of the Faro meeting. They did a wonderful job. Moreover, we want to thank the referees for having taken the burden of carefully reading and commenting the submissions. Last, but not least, we are very grateful to the Editor-in-Chief of Logical Methods in Computer Science for the opportunity to publish in this issue of the journal. The papers have undergone a rigorous reviewing process in accordance with the standards set by Logical Methods in Computer Science.
Daniel Graça, Mathieu Hoyrup, Dieter Spreen, Hideki Tsuiki, Martin Ziegler CCC 2018 Guest Editors