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

Editors: Ulrich Berger, Pieter Collins, Mathieu Hoyrup, Victor Selivanov, Dieter Spreen, Martin A. Ziegler

The workshop was partially funded by Inria, Loria, the University of Siegen, the Japan Society for the Promotion of Science (JSPS), as well as the European Union. It was the sixth 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 first annual meeting of the new 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 Sk{\l}odowska-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 Nancy 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, Pieter Collins, Mathieu Hoyrup, Victor Selivanov, Dieter Spreen, Martin Ziegler Guest Editors for the CCC'17 Special Issue

1. A Galois connection between Turing jumps and limits

Vasco Brattka.
Limit computable functions can be characterized by Turing jumps on the input side or limits on the output side. As a monad of this pair of adjoint operations we obtain a problem that characterizes the low functions and dually to this another problem that characterizes the functions that are computable relative to the halting problem. Correspondingly, these two classes are the largest classes of functions that can be pre or post composed to limit computable functions without leaving the class of limit computable functions. We transfer these observations to the lattice of represented spaces where it leads to a formal Galois connection. We also formulate a version of this result for computable metric spaces. Limit computability and computability relative to the halting problem are notions that coincide for points and sequences, but even restricted to continuous functions the former class is strictly larger than the latter. On computable metric spaces we can characterize the functions that are computable relative to the halting problem as those functions that are limit computable with a modulus of continuity that is computable relative to the halting problem. As a consequence of this result we obtain, for instance, that Lipschitz continuous functions that are limit computable are automatically computable relative to the halting problem. We also discuss 1-generic points as the canonical points of continuity of limit computable functions, and we prove that restricted to these […]
Section: Computability and logic

2. The principle of pointfree continuity

Tatsuji Kawai ; Giovanni Sambin.
In the setting of constructive pointfree topology, we introduce a notion of continuous operation between pointfree topologies and the corresponding principle of pointfree continuity. An operation between points of pointfree topologies is continuous if it is induced by a relation between the bases of the topologies; this gives a rigorous condition for Brouwer's continuity principle to hold. The principle of pointfree continuity for pointfree topologies $\mathcal{S}$ and $\mathcal{T}$ says that any relation which induces a continuous operation between points is a morphism from $\mathcal{S}$ to $\mathcal{T}$. The principle holds under the assumption of bi-spatiality of $\mathcal{S}$. When $\mathcal{S}$ is the formal Baire space or the formal unit interval and $\mathcal{T}$ is the formal topology of natural numbers, the principle is equivalent to spatiality of the formal Baire space and formal unit interval, respectively. Some of the well-known connections between spatiality, bar induction, and compactness of the unit interval are recast in terms of our principle of continuity. We adopt the Minimalist Foundation as our constructive foundation, and positive topology as the notion of pointfree topology. This allows us to distinguish ideal objects from constructive ones, and in particular, to interpret choice sequences as points of the formal Baire space.

3. Moschovakis Extension of Represented Spaces

Dimiter Skordev.
Given a represented space (in the sense of TTE theory), an appropriate representation is constructed for the Moschovakis extension of its carrier (with paying attention to the cases of effective topological spaces and effective metric spaces). Some results are presented about TTE computability in the represented space obtained in this way. For single-valued functions, we prove, roughly speaking, the computability of any function which is absolutely prime computable in some computable functions. A similar result holds for multi-valued functions, but with an analog of absolute prime computability. The formulation of this result makes use of the notion of computability in iterative combinatory spaces - a notion studied by the author in other publications.

4. Elementary Quotient Completions, Church's Thesis, and Partioned Assemblies

Maria Emilia Maietti ; Fabio Pasquali ; Giuseppe Rosolini.
Hyland's effective topos offers an important realizability model for constructive mathematics in the form of a category whose internal logic validates Church's Thesis. It also contains a boolean full sub-quasitopos of "assemblies" where only a restricted form of Church's Thesis survives. In the present paper we compare the effective topos and the quasitopos of assemblies each as the elementary quotient completions of a Lawvere doctrine based on the partitioned assemblies. In that way we can explain why the two forms of Church's Thesis each category satisfies differ by the way each is inherited from specific properties of the doctrine which determines the elementary quotient completion.

5. Game characterizations and lower cones in the Weihrauch degrees

Hugo Nobrega ; Arno Pauly.
We introduce a parametrized version of the Wadge game for functions and show that each lower cone in the Weihrauch degrees is characterized by such a game. These parametrized Wadge games subsume the original Wadge game, the eraser and backtrack games as well as Semmes's tree games. In particular, we propose that the lower cones in the Weihrauch degrees are the answer to Andretta's question on which classes of functions admit game characterizations. We then discuss some applications of such parametrized Wadge games. Using machinery from Weihrauch reducibility theory, we introduce games characterizing every (transfinite) level of the Baire hierarchy via an iteration of a pruning derivative on countably branching trees.

6. Approximability in the GPAC

Diogo Poças ; Jeffery Zucker.
Most of the physical processes arising in nature are modeled by either ordinary or partial differential equations. From the point of view of analog computability, the existence of an effective way to obtain solutions of these systems is essential. A pioneering model of analog computation is the General Purpose Analog Computer (GPAC), introduced by Shannon as a model of the Differential Analyzer and improved by Pour-El, Lipshitz and Rubel, Costa and Graça and others. Its power is known to be characterized by the class of differentially algebraic functions, which includes the solutions of initial value problems for ordinary differential equations. We address one of the limitations of this model, concerning the notion of approximability, a desirable property in computation over continuous spaces that is however absent in the GPAC. In particular, the Shannon GPAC cannot be used to generate non-differentially algebraic functions which can be approximately computed in other models of computation. We extend the class of data types using networks with channels which carry information on a general complete metric space $X$; for example $X=C(R,R)$, the class of continuous functions of one real (spatial) variable. We consider the original modules in Shannon's construction (constants, adders, multipliers, integrators) and we add \emph{(continuous or discrete) limit} modules which have one input and one output. We then define an L-GPAC to be a network built with $X$-stream channels and […]

7. McShane-Whitney extensions in constructive analysis

Iosif Petrakis.
Within Bishop-style constructive mathematics we study the classical McShane-Whitney theorem on the extendability of real-valued Lipschitz functions defined on a subset of a metric space. Using a formulation similar to the formulation of McShane-Whitney theorem, we show that the Lipschitz real-valued functions on a totally bounded space are uniformly dense in the set of uniformly continuous functions. Through the introduced notion of a McShane-Whitney pair we describe the constructive content of the original McShane-Whitney extension and examine how the properties of a Lipschitz function defined on the subspace of the pair extend to its McShane-Whitney extensions on the space of the pair. Similar McShane-Whitney pairs and extensions are established for Hölder functions and $\nu$-continuous functions, where $\nu$ is a modulus of continuity. A Lipschitz version of a fundamental corollary of the Hahn-Banach theorem, and the approximate McShane-Whitney theorem are shown.

8. Reachability for infinite time Turing machines with long tapes

Merlin Carl ; Benjamin Rin ; Philipp Schlicht.
Infinite time Turing machine models with tape length $\alpha$, denoted $T_\alpha$, strengthen the machines of Hamkins and Kidder [HL00] with tape length $\omega$. A new phenomenon is that for some countable ordinals $\alpha$, some cells cannot be halting positions of $T_\alpha$ given trivial input. The main open question in [Rin14] asks about the size of the least such ordinal $\delta$. We answer this by providing various characterizations. For instance, $\delta$ is the least ordinal with any of the following properties: (a) For some $\xi<\alpha$, there is a $T_\xi$-writable but not $T_\alpha$-writable subset of $\omega$. (b) There is a gap in the $T_\alpha$-writable ordinals. (c) $\alpha$ is uncountable in $L_{\lambda_\alpha}$. Here $\lambda_\alpha$ denotes the supremum of $T_\alpha$-writable ordinals, i.e. those with a $T_\alpha$-writable code of length $\alpha$. We further use the above characterizations, and an analogue to Welch's submodel characterization of the ordinals $\lambda$, $\zeta$ and $\Sigma$, to show that $\delta$ is large in the sense that it is a closure point of the function $\alpha \mapsto \Sigma_\alpha$, where $\Sigma_\alpha$ denotes the supremum of the $T_\alpha$-accidentally writable ordinals.

9. Theory of higher order interpretations and application to Basic Feasible Functions

Emmanuel Hainry ; Romain Péchoux.
Interpretation methods and their restrictions to polynomials have been deeply used to control the termination and complexity of first-order term rewrite systems. This paper extends interpretation methods to a pure higher order functional language. We develop a theory of higher order functions that is well-suited for the complexity analysis of this programming language. The interpretation domain is a complete lattice and, consequently, we express program interpretation in terms of a least fixpoint. As an application, by bounding interpretations by higher order polynomials, we characterize Basic Feasible Functions at any order.

10. Decidability for Entailments of Symbolic Heaps with Arrays

Daisuke Kimura ; Makoto Tatsuta.
This paper presents two decidability results on the validity checking problem for entailments of symbolic heaps in separation logic with Presburger arithmetic and arrays. The first result is for a system with arrays and existential quantifiers. The correctness of the decision procedure is proved under the condition that sizes of arrays in the succedent are not existentially quantified. This condition is different from that proposed by Brotherston et al. in 2017 and one of them does not imply the other. The main idea is a novel translation from an entailment of symbolic heaps into a formula in Presburger arithmetic. The second result is the decidability for a system with both arrays and lists. The key idea is to extend the unroll collapse technique proposed by Berdine et al. in 2005 to arrays and arithmetic as well as double-linked lists.

11. $\sigma$-locales in Formal Topology

Francesco Ciraulo.
A $\sigma$-frame is a poset with countable joins and finite meets in which binary meets distribute over countable joins. The aim of this paper is to show that $\sigma$-frames, actually $\sigma$-locales, can be seen as a branch of Formal Topology, that is, intuitionistic and predicative point-free topology. Every $\sigma$-frame $L$ is the lattice of Lindelöf elements (those for which each of their covers admits a countable subcover) of a formal topology of a specific kind which, in its turn, is a presentation of the free frame over $L$. We then give a constructive characterization of the smallest (strongly) dense $\sigma$-sublocale of a given $\sigma$-locale, thus providing a "$\sigma$-version" of a Boolean locale. Our development depends on the axiom of countable choice.

12. The Third Trick

Hannes Diener ; Matthew Hendtlass.
We prove a result, similar to the ones known as Ishihara's First and Second Trick, for sequences of functions.