Back to: Programme, CCC 2015 home

CCC 2015 - Abstracts

Invited Tutorials

Olivier Bournez (Palaiseau)
Continuous Time Computations

This tutorial will present some results on theories of continuous time computations. These theories are motivated both by understanding the hardness of questions related to continuous time dynamical systems and the computational power of some continuous time analog models. We will in particular focus on results relating continuous time models to particular classes of dynamical systems, and relating the computational power of continuous time models to classical computability and to computational analysis (TTE). We will in particular focus on nice recent results about the General Purpose Analog Computer (GPAC) model from Claude Shannon, and its relations to classical computability and complexity.

André Nies (Auckland)
Randomness and Analysis: a tutorial

The tutorial addresses the interactions of randomness and analysis. Randomness notions given by algorithmic tests can clarify the effective content of theorems such as Lebesgue's that a nondecreasing function is differentiable at almost every real. On the other hand, the point of view of analysis can study randomness notions. This shows invariance of randomness under the choice of a basis for the real, and leads to a better understanding of separations, such as Martin-Löf randomness versus the weaker notion defined by failure of all computable martingales.
The plan of the tutorial is as follows.
Lecture 1
Background on randomness via algorithmic tests. Constructive approaches to analysis of Bishop and Demuth, which with hindsight were the first to connect randomness with analysis.
Lectures 2 and 3
Effective versions of Lebesgues's Theorems: results of Pathak, Simpson and Rojas; Brattka Miller and Nies; results on Lipschitz functions by Freer et al. Extensions to higher dimensions by Galicki and Turetsky ; the polynomial time setting (Nies). Similar investigations in ergodic theory: V'yugin 1997; recent work by Downey, Nandakumar and Nies.
Lecture 4
We discuss the setting where the given functions are merely effective in the sense of computable enumerability. Lebesgue's density theorem for effectively closed sets; differentiability of interval-c.e. functions. An application: the recent solution of the covering problem showing that every K-trivial is below an incomplete Martin-Löf random.

Invited talks

Martín Escardó (Birmingham)
Searchable types in constructive dependent type theory

A type X is searchable if for any p:X->2 we can find x0:X such that if p(x0)=1, then p(x)=1 for all x:X. This implies that X satisfies the principle of omniscience: for any p:X->2, either we can find x:X with p(x)=0, or else p(x)=1 for all x:X. For X=N, this is LPO, the limited principle of omniscience, which is not provable or refutable in constructive type theory, which is deemed as a constructive taboo. So the searchability of the type N of natural numbers is a taboo.

However, N can be extended with a point at infinity so that it becomes searchable. Perhaps surprisingly, this doesn't rely on continuity principles (which anyway are not available in constructive type theory), but nevertheless somehow expresses the compactness of the extended natural numbers in the language of type theory. In previous work, we investigated searchable subsets of the cantor type 2^N. In this talk, we will consider more general searchable types, and ways of constructing them. Many of these searchable types are also ordinals in a constructive sense, and, for example, one can get a searchable type that corresponds to the ordinal interval [0,epsilon0] with the interval topology, a compact Hausdorff space.

In order for the talk to be as self-contained as possible, I will develop it in the language of informal/naive (but rigorous) type theory, which I will introduce as we go along. However, notice that the results have been formally developed in Agda notation, so that in particular we can run our proofs in the computer, in addition to getting reassurance that the results are formally correct.

Daniel da Silva Graça (Faro)
Computability and complexity in continuous dynamical systems

Dynamical systems are well-known to have numerous applications both in theory and in practice. Many interesting problems about dynamical systems are variations of the following questions: ``how does the system look like at time $t$?'' or ``what is the asymptotic behavior of the system when time goes to infinity?''. It is only natural to consider the following computable variants of these questions: ``can we computably tell how the system looks like at time $t$?'' or ``can we computably determine the asymptotic behavior of the system?''. The last question tends to be undecidable if we consider dynamical systems in general. However, what happens if we consider only restricted classes of dynamical systems which are still useful? In this talk we will analyze those questions and we will present some partial answers to them.

Vassilis Gregoriades (Darmstadt)
Some uniformity aspects of the class of analytic sets

It is a typical problem in descriptive set theory and computable analysis to find functions of certain complexity, which realize a given property (uniformity functions). As an example we mention the classical Luzin Separation Theorem, which states that two disjoint analytic subsets of a Polish space can be separated by a Borel set, and the Suslin-Kleene Theorem which gives a recursive (and thus continuous) function u: \mathbb{N}^\mathbb{N} \times \mathbb{N}^\mathbb{N} \to \mathbb{N}^\mathbb{N}, such that whenever \alpha and \beta code disjoint analytic sets A and B, then u(\alpha, \beta) codes a Borel set, which separates A from B. In this talk we examine the uniformity aspects of the following: (a) a separation-type result due to Dyke, which deals with the so-called positive analytic sets, and (b) the Baire property in the class of analytic sets. In (a) we show that Dyke' s result is witnessed by a recursive uniformity function. This implies that the notion of a positive Borel set has a constructive character. In (b) we show the existence of a continuous function, which realizes the required property at almost all codes, and we show that this result is optimal.

Matthieu Hoyrup (Nancy)
On the information carried by programs about the objects they compute.

Finite programs can compute infinite objects. Presenting a computable object via any program for it provides at least as much information as presenting the object itself, written on an infinite tape. What additional information do programs provide? This is the problem of comparing two models of computation over infinite objects, namely Markov-computability and Type-2-computability. Many classical results provide partial answers to this problem, by Rice, Shapiro, Kreisel-Lacombe-Schoenfield, Ceitin, Friedberg and others.

We characterize the additional information to be any upper bound on the Kolmogorov complexity of the object. Hence we identify the exact relationship between Markov-computability and Type-2-computability. We then use this relationship to obtain several results characterizing the computational and topological structure of Markov-semidecidable sets.

We also prove an analog of Rice and Rice-Shapiro theorems for subrecursive classes of functions, like the primitive recursive functions or the polynomial-time computable functions, obtaining an exact characterization of the properties of functions that are decidable or semi-decidable, given a program for the function. Again Kolmogorov complexity is at the core of the characterization.

This is joint work with Cristobal Rojas.

Takayuki Kihara (UC Berkely)
Degree Theory and Infinite Dimensional Topology

The notion of degree spectrum of a structure in computable model theory is defined as the collection of all Turing degrees of presentations of the structure. We introduce the degree spectrum of a represented space as the class of collections of all Turing degrees of presentations of points in the space. The notion of point degree spectrum creates a connection among various areas of mathematics including computability theory, descriptive set theory, infinite dimensional topology and Banach space theory.

Through this new connection, for instance, we construct a family of continuum many infinite dimensional Cantor manifolds with property C in the sense of Haver/Addis-Gresham whose Borel structures at an arbitrary finite rank are mutually non-isomorphic. This provides new examples of Banach algebras of real valued Baire class two functions on metrizable compacta, and strengthen various theorems in infinite dimensional topology such as Pol's solution to Alexandrov's old problem.

To prove our main theorem, an invariant which we call degree co-spectrum, a collection of Turing ideals realized as lower Turing cones of points of a Polish space, plays a key role. The key idea is measuring the quantity of all possible Scott ideals (omega-models of WKL) realized within the degree co-spectrum (on a cone) of a given space. This is joint work with Arno Pauly.

Thomas Powell (Innsbruck)
Bar recursion over finite partial functions

In this talk I present a new computational interpretation of classical analysis, which is achieved by replacing traditional bar recursion in the sense of Spector with a `symmetric' backward recursor that makes recursive calls over domain-theoretic extensions of partial functions. I will begin by discussing aspects of computability theory in type structures of continuous functionals, in particular demonstrating how the basic idea behind bar recursion can be extended to more complex forms recursion which are nevertheless well-founded in continuous models. I will then define the symmetric recursor and briefly explain how it can be used to give a computational interpretation to countable choice. I conclude by arguing that this new recursor performs very well in terms of efficiency, can be generalised to deal with choice principles over more abstract spaces, and has deep theoretical links to the seemingly unrelated world of learning-based realizability interpretations of classical logic.

Contributed talks

Jens Blanck (Swansea)
Use of parallelism in Haskell implementation of exact real arithmetic

There is no bound on the computation time that an exact computation may take. Computation time is no longer directly related only to the number of operations performed but also depends on the expression at hand. For benign problems exact computations stay within an order of magnitude or two of floating point computations. Although many computations are quick it is possible that some computations take large amounts of time.

Can we effectively use available parallelism to improve performance? Can it be used both for benign problems and harder problems?

Willem Fouché and Safari Mukeru (Pretoria)
Local time of algorithmically random Brownian motion

In this talk we shall discuss how the local time of a Martin-L\"of Brownian motion (an Asarin-Prokovskii ``complex oscillation") can be defined in a layerwise computable manner from an infinite binary string which is Martin-L\"of random. Along these lines we shall find new representations of the local times of Brownian motion and a representation of the inverse local time of Brownian motion, which is a stable Levy process, in the framework of algorithmic randomness.

Mizuhito Ogawa (JAIST)
Decidability and undecidability of timed devices with stopwatches

A timed automaton is a popular device for describing realtime behavior. Its reachability is decidable by digitizing to a region automaton. Some extensions preserve it, and some do not. For instance, adding one stopwatch leads to undecidability. We will briefly survey when the decidablity is violated/preserved, including the recent extensions to recursive timed devices.

Peter Schuster and Davide Rinaldi (Verona/Leeds)
Transfinite Methods as Admissible Rules

Contrapositive forms of Zorn's Lemma are often applied in concrete contexts in which the corresponding conservation theorems would suffice. Unlike the former, the latter are purely syntactical and admit proofs with finite methods only.

We show how to see this with Scott's multi-conclusion entailment relations as extending Tarskian single-conclusion consequence relations, also known as algebraic closure operators or Stone coverings. In a nutshell, the extra multi-conclusion axioms can be reduced to rules that are provable for the single-conclusion basis. Thanks to a sandwich criterion due to Scott, the method can also be proved optimal.

Apart from various rather algebraic instances involving the presence of a binary operation (Krull-Lindenbaum, Artin-Schreier), applications include extension theorems such as Szpilrajn's, and Hahn and Banach's. Related work can be found, for example, in locale theory (Mulvey-Pelletier 1991), dynamical algebra (Coste-Lombardi-Roy 2001, Lombardi 1997-8), formal topology (Cederquist-Coquand-Negri 1998) and proof theory (Coquand-Negri-von Plato 2004, Negri-von Plato 2011).

Helmut Schwichtenberg, Ulrich Berger, Kenji Miyamoto and Hideki Tsuiki (Munich/Swansea/Kyoto)
Logic for Gray code computation

Gray code is a well-known binary number system such that neighboring values differ in one digit only. Tsuiki (2002) has introduced Gray code to the field of real number computation. He assigns to each number a unique $1\bot$-sequence, i.e., a (possibly infinite) sequence of $\{-1, 1, \bot\}$ such that at most one copy of $\bot$ (meaning undefinedness) is contained in the sequence not as the last character. In this paper we take a logical and constructive approach to study real number computation based on Gray code. Instead of Tsuiki's indeterministic multihead Type-2 machine, we use pre-Gray code, which is a relaxed Gray code, to avoid the difficulty due to $\bot$ which prevents sequential access to a stream. We extract real number algorithms from proofs in an appropriate formal theory involving inductive and coinductive definitions. Examples are algorithms transforming pre-Gray code into signed digit representations of real numbers, and conversely, the average for pre-Gray code and a bounded translator from pre-Gray code into Gray code. These examples are formalized in the proof assistant Minlog.

Pedro Francisco Valencia Vizcaíno (Greifswald)
Hierarchies of Decision Problems for Real Numbers

In order to classify finitary first-order decision problems according to their level of unsolvability, one can use several models of computation and introduce hierarchies of undecidable problems similar to the classical arithmetical hierachy: Hierarchies can be defined semantically by deterministic or non-deterministic machines, and syntactically by quantified formulas. Whether these hierarchies coincide or not, is dependent on a number of factors including the model itself, and the allowed base operations. The BSS RAM's over finitary first-order structures are the result of a theoretical generalisation of the BSS model of computation (cf. [Blum et al. '89]) and allow to process all problem instances of any length uniformly. However, the demand for uniformity in the processing may be circumvented by the requirement that the underlying structures be closed under the pairing operation. This operation makes it possible to characterise---as done in [Moschovakis '69]---computable functions by means of recursions and a \nu-operator (in analogy to Kleene's \mu-operator). This characterisation is straightforward, machine-independent, and provides a projective hierarchy. Here, we will study, among other things, classes of a hierarchy that we will define by \nu-oracle machines. The \nu-oracle BSS RAM's use operators similar to Moschovakis' \nu-operator. For any finitary first-order structure A, with universe U, with at least two constants a,b in U, and any function f from the finite tuples of U to U that is computable by a usual BSS RAM over A, the \nu-operator can give, for any z1,...zn in U, some y1 in U such that there are an m and y2,..ym in U which satisfy f(z1,..,zn,y1,...ym)=a. For several ordered structures over the reals, we also consider several further operators which we call the Moschovakis operators. We will see that choosing different operators leads to different classes in the corresponding hierachies.

References

[Blum et al. '89] Blum, L., Shub, M., and Smale, S. "On a theory of computation and complexity over the real numbers: NP-completeness, recursive funcitons and universal machines"; Bulletin of the Amer. Math. Soc. 21 (1989) 1--46.

[Moschovakis '69] Moschovakis, Y. N. "Abstract first order computability. I"; Transactions of the American Mathematical Society 138 (1969), 427--464. http://dx.doi.org/10.2307/1994926

Further abstracts are available on the CCC 2015 programme website as pdfs.

CCC 2015 home