Selected papers of the conference "Continuity, Computability, Constructivity – From Logic to Algorithms" (CCC 2015)

Editors: Ulrich Berger, Willem Fouché, Arno Pauly, Dieter Spreen, Martin A. Ziegler

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 in the Georg-Vollmar-Akademie, Schloss Aspenstein, a conference centre located in the magnificent surroundings of the Bavarian prealps, in mid September 2015.

The workshop was partially funded by the German Science Association (DFG), the Japan Society for the Promotion of Science (JSPS), as well as the European Union. It was the fifth 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 final annual meeting of the COMPUTAL project, a research network between Europe, Russia, South Africa, and Japan funded by the European Union under the FP7-IRSES programme scheme.

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 \emph{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 on non-computability one uses hierarchies, or compares them with certain well-known master problems. In many applications operators on function spaces are of central relevance. So, not only the computational complexity of functions on the reals, but also of such operators needs be investigated.

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

Ulrich Berger, Willem Fouché, Arno Pauly, Dieter Spreen, Martin Ziegler

CCC 2015 Guest Editors

1. Existence of strongly proper dyadic subbases

Yasuyuki Tsukamoto.

We consider a topological space with its subbase which induces a coding for each point. Every second-countable Hausdorff space has a subbase that is the union of countably many pairs of disjoint open subsets. A dyadic subbase is such a subbase with a fixed enumeration. If a dyadic subbase is given, then we obtain a domain representation of the given space. The properness and the strong properness of dyadic subbases have been studied, and it is known that every strongly proper dyadic subbase induces an admissible domain representation regardless of its enumeration. We show that every locally compact separable metric space has a strongly proper dyadic subbase.

2. Borel-piecewise continuous reducibility for uniformization problems

Takayuki Kihara.

We study a fine hierarchy of Borel-piecewise continuous functions, especially, between closed-piecewise continuity and $G_\delta$-piecewise continuity. Our aim is to understand how a priority argument in computability theory is connected to the notion of $G_\delta$-piecewise continuity, and then we utilize this connection to obtain separation results on subclasses of $G_\delta$-piecewise continuous reductions for uniformization problems on set-valued functions with compact graphs. This method is also applicable for separating various non-constructive principles in the Weihrauch lattice.

3. Characterization theorem for the conditionally computable real functions

Ivan Georgiev.

The class of uniformly computable real functions with respect to a small subrecursive class of operators computes the elementary functions of calculus, restricted to compact subsets of their domains. The class of conditionally computable real functions with respect to the same class of operators is a proper extension of the class of uniformly computable real functions and it computes the elementary functions of calculus on their whole domains. The definition of both classes relies on certain transformations of infinitistic names of real numbers. In the present paper, the conditional computability of real functions is characterized in the spirit of Tent and Ziegler, avoiding the use of infinitistic names.

4. First Order Theories of Some Lattices of Open Sets

Oleg Kudinov ; Victor Selivanov.

We show that the first order theory of the lattice of open sets in some natural topological spaces is $m$-equivalent to second order arithmetic. We also show that for many natural computable metric spaces and computable domains the first order theory of the lattice of effectively open sets is undecidable. Moreover, for several important spaces (e.g., $\mathbb{R}^n$, $n\geq1$, and the domain $P\omega$) this theory is $m$-equivalent to first order arithmetic.

5. Complexity theory for spaces of integrable functions

Florian Steinberg.

This paper investigates second-order representations in the sense of Kawamura and Cook for spaces of integrable functions that regularly show up in analysis. It builds upon prior work about the space of continuous functions on the unit interval: Kawamura and Cook introduced a representation inducing the right complexity classes and proved that it is the weakest second-order representation such that evaluation is polynomial-time computable. The first part of this paper provides a similar representation for the space of integrable functions on a bounded subset of Euclidean space: The weakest representation rendering integration over boxes is polynomial-time computable. In contrast to the representation of continuous functions, however, this representation turns out to be discontinuous with respect to both the norm and the weak topology. The second part modifies the representation to be continuous and generalizes it to Lp-spaces. The arising representations are proven to be computably equivalent to the standard representations of these spaces as metric spaces and to still render integration polynomial-time computable. The family is extended to cover Sobolev spaces on the unit interval, where less basic operations like differentiation and some Sobolev embeddings are shown to be polynomial-time computable. Finally as a further justification quantitative versions of the Arzelà-Ascoli and Fréchet-Kolmogorov Theorems are presented and used to argue that these representations […]

6. Localic completion of uniform spaces

Tatsuji Kawai.

We extend the notion of localic completion of generalised metric spaces by Steven Vickers to the setting of generalised uniform spaces. A generalised uniform space (gus) is a set X equipped with a family of generalised metrics on X, where a generalised metric on X is a map from the product of X to the upper reals satisfying zero self-distance law and triangle inequality. For a symmetric generalised uniform space, the localic completion lifts its generalised uniform structure to a point-free generalised uniform structure. This point-free structure induces a complete generalised uniform structure on the set of formal points of the localic completion that gives the standard completion of the original gus with Cauchy filters. We extend the localic completion to a full and faithful functor from the category of locally compact uniform spaces into that of overt locally compact completely regular formal topologies. Moreover, we give an elementary characterisation of the cover of the localic completion of a locally compact uniform space that simplifies the existing characterisation for metric spaces. These results generalise the corresponding results for metric spaces by Erik Palmgren. Furthermore, we show that the localic completion of a symmetric gus is equivalent to the point-free completion of the uniform formal topology associated with the gus. We work in Aczel's constructive set theory CZF with the Regular Extension Axiom. Some of our results also require Countable […]

7. Grilliot's trick in Nonstandard Analysis

Sam Sanders.

The technique known as Grilliot's trick constitutes a template for explicitly defining the Turing jump functional $(\exists^2)$ in terms of a given effectively discontinuous type two functional. In this paper, we discuss the standard extensionality trick: a technique similar to Grilliot's trick in Nonstandard Analysis. This nonstandard trick proceeds by deriving from the existence of certain nonstandard discontinuous functionals, the Transfer principle from Nonstandard analysis limited to $\Pi_1^0$-formulas; from this (generally ineffective) implication, we obtain an effective implication expressing the Turing jump functional in terms of a discontinuous functional (and no longer involving Nonstandard Analysis). The advantage of our nonstandard approach is that one obtains effective content without paying attention to effective content. We also discuss a new class of functionals which all seem to fall outside the established categories. These functionals directly derive from the Standard Part axiom of Nonstandard Analysis.

8. The Rice-Shapiro theorem in Computable Topology

Margarita Korovina ; Oleg Kudinov.

We provide requirements on effectively enumerable topological spaces which guarantee that the Rice-Shapiro theorem holds for the computable elements of these spaces. We show that the relaxation of these requirements leads to the classes of effectively enumerable topological spaces where the Rice-Shapiro theorem does not hold. We propose two constructions that generate effectively enumerable topological spaces with particular properties from wn--families and computable trees without computable infinite paths. Using them we propose examples that give a flavor of this class.