 |
 |
Selected papers of the conference "Continuity, Computability, Constructivity – From Logic to Algorithms" (CCC 2018)
Editors: Daniel Graça, Mathieu Hoyrup, Dieter Spreen, Hideki Tsuiki, Martin A. Ziegler
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
1. Constructive Domains with Classical Witnesses
We develop a constructive theory of continuous domains from the perspective of program extraction. Our goal that programs represent (provably correct) computation without witnesses of correctness is achieved by formulating correctness assertions classically. Technically, we start from a predomain base and construct a completion. We then investigate continuity with respect to the Scott topology, and present a construction of the function space. We then discuss our main motivating example in detail, and instantiate our theory to real numbers that we conceptualise as the total elements of the completion of the predomain of rational intervals, and prove a representation theorem that precisely delineates the class of representable continuous functions.
2. Overlap Algebras: a Constructive Look at Complete Boolean Algebras
The notion of a complete Boolean algebra, although completely legitimate in constructive mathematics, fails to capture some natural structures such as the lattice of subsets of a given set. Sambin's notion of an overlap algebra, although classically equivalent to that of a complete Boolean algebra, has powersets and other natural structures as instances. In this paper we study the category of overlap algebras as an extension of the category of sets and relations, and we establish some basic facts about mono-epi-isomorphisms and (co)limits; here a morphism is a symmetrizable function (with classical logic this is just a function which preserves joins). Then we specialize to the case of morphisms which preserve also finite meets: classically, this is the usual category of complete Boolean algebras. Finally, we connect overlap algebras with locales, and their morphisms with open maps between locales, thus obtaining constructive versions of some results about Boolean locales.
3. A syntactic approach to continuity of T-definable functionals
We give a new proof of the well-known fact that all functions $(\mathbb{N} \to \mathbb{N}) \to \mathbb{N}$ which are definable in Gödel's System T are continuous via a syntactic approach. Differing from the usual syntactic method, we firstly perform a translation of System T into itself in which natural numbers are translated to functions $(\mathbb{N} \to \mathbb{N}) \to \mathbb{N}$. Then we inductively define a continuity predicate on the translated elements and show that the translation of any term in System T satisfies the continuity predicate. We obtain the desired result by relating terms and their translations via a parametrized logical relation. Our constructions and proofs have been formalized in the Agda proof assistant. Because Agda is also a programming language, we can execute our proof to compute moduli of continuity of T-definable functions.
4. On the incomputability of computable dimension
Using an iterative tree construction we show that for simple computable subsets of the Cantor space Hausdorff, constructive and computable dimensions might be incomputable.
5. The Sierpinski Object in the Scott Realizability Topos
We study the Sierpinski object $\Sigma$ in the realizability topos based on Scott's graph model of the $\lambda$-calculus. Our starting observation is that the object of realizers in this topos is the exponential $\Sigma ^N$, where $N$ is the natural numbers object. We define order-discrete objects by orthogonality to $\Sigma$. We show that the order-discrete objects form a reflective subcategory of the topos, and that many fundamental objects in higher-type arithmetic are order-discrete. Building on work by Lietz, we give some new results regarding the internal logic of the topos. Then we consider $\Sigma$ as a dominance; we explicitly construct the lift functor and characterize $\Sigma$-subobjects. Contrary to our expectations the dominance $\Sigma$ is not closed under unions. In the last section we build a model for homotopy theory, where the order-discrete objects are exactly those objects which only have constant paths.
6. Direct spectra of Bishop spaces and their limits
We apply fundamental notions of Bishop set theory (BST), an informal theory that complements Bishop's theory of sets, to the theory of Bishop spaces, a function-theoretic approach to constructive topology. Within BST we develop the notions of a direct family of sets, of a direct spectrum of Bishop spaces, of the direct limit of a direct spectrum of Bishop spaces, and of the inverse limit of a contravariant direct spectrum of Bishop spaces. Within the extension of Bishop's informal system of constructive mathematics BISH with inductive definitions with rules of countably many premises, we prove the fundamental theorems on the direct and inverse limits of spectra of Bishop spaces and the duality principle between them.
7. Logic for exact real arithmetic
Continuing earlier work of the first author with U. Berger, K. Miyamoto and H. Tsuiki, it is shown how a division algorithm for real numbers given as a stream of signed digits can be extracted from an appropriate formal proof. The property of being a real number represented as a stream is formulated by means of coinductively defined predicates, and formal proofs involve coinduction. The proof assistant Minlog is used to generate the formal proofs and extract their computational content as terms of the underlying theory, a form of type theory for finite or infinite data. Some experiments with running the extracted term are described, after its translation to Haskell.
8. Computable analysis and notions of continuity in Coq
We give a number of formal proofs of theorems from the field of computable analysis. Many of our results specify executable algorithms that work on infinite inputs by means of operating on finite approximations and are proven correct in the sense of computable analysis. The development is done in the proof assistant Coq and heavily relies on the Incone library for information theoretic continuity. This library is developed by one of the authors and the paper can be used as an introduction to the library as it describes many of its most important features in detail. While the ability to have full executability in a formal development of mathematical statements about real numbers and the like is not a feature that is unique to the Incone library, its original contribution is to adhere to the conventions of computable analysis to provide a general purpose interface for algorithmic reasoning on continuous structures. The results that provide complete computational content include that the algebraic operations and the efficient limit operator on the reals are computable, that certain countably infinite products are isomorphic to spaces of functions, compatibility of the enumeration representation of subsets of natural numbers with the abstract definition of the space of open subsets of the natural numbers, and that continuous realizability implies sequential continuity. We also formalize proofs of non-computational results that support the correctness of our definitions. These […]
9. A realizability semantics for inductive formal topologies, Church's Thesis and Axiom of Choice
We present a Kleene realizability semantics for the intensional level of the Minimalist Foundation, for short mtt, extended with inductively generated formal topologies, Church's thesis and axiom of choice. This semantics is an extension of the one used to show consistency of the intensional level of the Minimalist Foundation with the axiom of choice and formal Church's thesis in previous work. A main novelty here is that such a semantics is formalized in a constructive theory represented by Aczel's constructive set theory CZF extended with the regular extension axiom.