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

1. A Galois connection between Turing jumps and limits

Vasco Brattka.
Limit computable functions can be characterized by Turing jumps on the inputside or limits on the output side. As a monad of this pair of adjointoperations we obtain a problem that characterizes the low functions and duallyto this another problem that characterizes the functions that are computablerelative to the halting problem. Correspondingly, these two classes are thelargest classes of functions that can be pre or post composed to limitcomputable functions without leaving the class of limit computable functions.We transfer these observations to the lattice of represented spaces where itleads to a formal Galois connection. We also formulate a version of this resultfor computable metric spaces. Limit computability and computability relative tothe halting problem are notions that coincide for points and sequences, buteven restricted to continuous functions the former class is strictly largerthan the latter. On computable metric spaces we can characterize the functionsthat are computable relative to the halting problem as those functions that arelimit computable with a modulus of continuity that is computable relative tothe halting problem. As a consequence of this result we obtain, for instance,that Lipschitz continuous functions that are limit computable are automaticallycomputable relative to the halting problem. We also discuss 1-generic points asthe canonical points of continuity of limit computable functions, and we provethat restricted to these points limit computable […]

2. The principle of pointfree continuity

Tatsuji Kawai ; Giovanni Sambin.
In the setting of constructive pointfree topology, we introduce a notion ofcontinuous operation between pointfree topologies and the correspondingprinciple of pointfree continuity. An operation between points of pointfreetopologies is continuous if it is induced by a relation between the bases ofthe topologies; this gives a rigorous condition for Brouwer's continuityprinciple to hold. The principle of pointfree continuity for pointfreetopologies $\mathcal{S}$ and $\mathcal{T}$ says that any relation which inducesa 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 unitinterval and $\mathcal{T}$ is the formal topology of natural numbers, theprinciple is equivalent to spatiality of the formal Baire space and formal unitinterval, respectively. Some of the well-known connections between spatiality,bar induction, and compactness of the unit interval are recast in terms of ourprinciple of continuity. We adopt the Minimalist Foundation as our constructive foundation, andpositive topology as the notion of pointfree topology. This allows us todistinguish ideal objects from constructive ones, and in particular, tointerpret 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 appropriaterepresentation is constructed for the Moschovakis extension of its carrier(with paying attention to the cases of effective topological spaces andeffective metric spaces). Some results are presented about TTE computability inthe represented space obtained in this way. For single-valued functions, weprove, roughly speaking, the computability of any function which is absolutelyprime computable in some computable functions. A similar result holds formulti-valued functions, but with an analog of absolute prime computability. Theformulation of this result makes use of the notion of computability initerative combinatory spaces - a notion studied by the author in otherpublications.

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 forconstructive mathematics in the form of a category whose internal logicvalidates Church's Thesis. It also contains a boolean full sub-quasitopos of"assemblies" where only a restricted form of Church's Thesis survives. In thepresent paper we compare the effective topos and the quasitopos of assemblieseach as the elementary quotient completions of a Lawvere doctrine based on thepartitioned assemblies. In that way we can explain why the two forms ofChurch's Thesis each category satisfies differ by the way each is inheritedfrom specific properties of the doctrine which determines the elementaryquotient 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 showthat each lower cone in the Weihrauch degrees is characterized by such a game.These parametrized Wadge games subsume the original Wadge game, the eraser andbacktrack games as well as Semmes's tree games. In particular, we propose thatthe lower cones in the Weihrauch degrees are the answer to Andretta's questionon which classes of functions admit game characterizations. We then discuss some applications of such parametrized Wadge games. Usingmachinery from Weihrauch reducibility theory, we introduce games characterizingevery (transfinite) level of the Baire hierarchy via an iteration of a pruningderivative 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 eitherordinary or partial differential equations. From the point of view of analogcomputability, the existence of an effective way to obtain solutions of thesesystems is essential. A pioneering model of analog computation is the GeneralPurpose Analog Computer (GPAC), introduced by Shannon as a model of theDifferential Analyzer and improved by Pour-El, Lipshitz and Rubel, Costa andGraça and others. Its power is known to be characterized by the class ofdifferentially algebraic functions, which includes the solutions of initialvalue problems for ordinary differential equations. We address one of thelimitations of this model, concerning the notion of approximability, adesirable property in computation over continuous spaces that is however absentin the GPAC. In particular, the Shannon GPAC cannot be used to generatenon-differentially algebraic functions which can be approximately computed inother models of computation. We extend the class of data types using networkswith 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 ordiscrete) limit} modules which have one input and one output. We then define anL-GPAC to be a network built with $X$-stream channels and the […]

7. McShane-Whitney extensions in constructive analysis

Iosif Petrakis.
Within Bishop-style constructive mathematics we study the classicalMcShane-Whitney theorem on the extendability of real-valued Lipschitz functionsdefined on a subset of a metric space. Using a formulation similar to theformulation of McShane-Whitney theorem, we show that the Lipschitz real-valuedfunctions on a totally bounded space are uniformly dense in the set ofuniformly continuous functions. Through the introduced notion of aMcShane-Whitney pair we describe the constructive content of the originalMcShane-Whitney extension and examine how the properties of a Lipschitzfunction defined on the subspace of the pair extend to its McShane-Whitneyextensions on the space of the pair. Similar McShane-Whitney pairs andextensions are established for Hölder functions and $\nu$-continuousfunctions, where $\nu$ is a modulus of continuity. A Lipschitz version of afundamental corollary of the Hahn-Banach theorem, and the approximateMcShane-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 tapelength $\omega$. A new phenomenon is that for some countable ordinals $\alpha$,some cells cannot be halting positions of $T_\alpha$ given trivial input. Themain 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 thesupremum of $T_\alpha$-writable ordinals, i.e. those with a $T_\alpha$-writablecode of length $\alpha$. We further use the above characterizations, and an analogue to Welch'ssubmodel characterization of the ordinals $\lambda$, $\zeta$ and $\Sigma$, toshow that $\delta$ is large in the sense that it is a closure point of thefunction $\alpha \mapsto \Sigma_\alpha$, where $\Sigma_\alpha$ denotes thesupremum 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 deeplyused to control the termination and complexity of first-order term rewritesystems. This paper extends interpretation methods to a pure higher orderfunctional language. We develop a theory of higher order functions that iswell-suited for the complexity analysis of this programming language. Theinterpretation domain is a complete lattice and, consequently, we expressprogram interpretation in terms of a least fixpoint. As an application, bybounding interpretations by higher order polynomials, we characterize BasicFeasible 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 problemfor entailments of symbolic heaps in separation logic with Presburgerarithmetic and arrays. The first result is for a system with arrays andexistential quantifiers. The correctness of the decision procedure is provedunder the condition that sizes of arrays in the succedent are not existentiallyquantified. This condition is different from that proposed by Brotherston etal. in 2017 and one of them does not imply the other. The main idea is a noveltranslation from an entailment of symbolic heaps into a formula in Presburgerarithmetic. The second result is the decidability for a system with both arraysand lists. The key idea is to extend the unroll collapse technique proposed byBerdine 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 whichbinary meets distribute over countable joins. The aim of this paper is to showthat $\sigma$-frames, actually $\sigma$-locales, can be seen as a branch ofFormal Topology, that is, intuitionistic and predicative point-free topology.Every $\sigma$-frame $L$ is the lattice of Lindelöf elements (those for whicheach of their covers admits a countable subcover) of a formal topology of aspecific 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 ofcountable choice.

12. The Third Trick

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