In this interaction the correspondence between computation and (constructive) logic will be exploited to obtain logic-based representations of data as well as an automatic method for extracting correct programs operating on these data; moreover, the correspondence will be studied in further detail.
(I) to advance the theory of realisability over abstract structures, investigate concrete applications in computable analysis, and develop a logical approach to control the computational complexity of extracted programs on infinite data;
(II) to develop fundamental results of constructive analysis in weak constructive logical systems such as the Minimalist Foundation;
(III) to originate a constructive point-free theory of probability and randomness, and to study simplified frameworks for probability theory, based on ‘constructive’ models such as toposes;
(IV) to refine and extend the connections between constructive logic, computation and topology.
Objective 3-I: The usual way first to write program code and then to verify it, has turned out being quite tedious and error-prone. An easier way is to extract the code from a constructive proof of the program specification via a realisability interpretation. By the nature of constructive logic this code satisfies the specification. Assume that A(x; y) is a formula in the language of the logic (the specification of the program we are looking for) such that we have a formal proof of the statement ∀x ∃ y A(x; y). Then a term t can be extracted from the given proof such that A(x; t(x)) is formally provable. Up to some pruning the term t corresponds to the functional program sought.
In the COMPUTAL project this approach was applied to the case of real numbers and similar infinite objects. Contrary to the TTE approach one need not deal with object representations; they are automatically generated during extraction. To achieve this, object spaces are characterised co-inductively. This representation-free approach dramatically simplifies the formalisation of proofs. The user can write specifications in normal mathematical style. Dealing with representations in concrete situations usually requires some coding which may complicate the issue. The underlying logic is only semi-constructive: quantifiers without computational content are ignored, which allows the user to reason in the way he is used to.
In earlier work a co-inductive predicate on the closed unit interval was introduced generating the infinite signed digit representation, and a nested inductive/co-inductive definition given generating a tree-like representation of uniformly continuous functions. The former has then been generalised to compact metric spaces with a finite set of covering contractions, and extended to a tree representation of the hyper-space of non-empty compact subsets.
A further intriguing open problem is the logical representation of the infinite Gray code introduced by Tsuiki. An approximative solution to the problem was found in the COMPUTAL project, which, however, does not have the appealing property of Tsuiki’s Gray code that every real number has a unique representation. Tsuiki devised the notion of an indeterministic two-head Turing machine to model his infinite Gray code. It is a challenging question whether there is a logical representation for this. The answer might require a complete overhaul of the realisability framework used so far.
Extending work in the COMPUTAL project, we will further develop the theory of realisability over abstract structures and attack some important open problems. For example, identifying computationally irrelevant inductive definitions, such as the well-founded (or accessible) part of a binary relation. Realisers of computationally irrelevant relations can be ignored which leads to simpler and more efficient programs. Another open problem is a realisability interpretation of the general form of open induction as introduced by Raoult. Open induction has been used by Berardi, Bezem and Coquand as well as Berger and Oliva to give computational interpretation of classical logic combined with the axiom of countable and dependent choice. There are strong links to the work of Escardó and Oliva on products of selection functions. Finally, we will also study realisability based on coherence spaces and linear maps, motivated by a strong link between linear maps (over coherence spaces) and uniformly continuous functions (over the real line) discovered by Terui.
In TTE there is a well-established notion of complexity of functions acting on infinite data which has recently been extended to higher types within the COMPUTAL project. On the other hand, Cook, Bellantoni and many others introduced the basic feasible functionals which lift the notion of polynomial-time computability to higher-type functionals of the natural numbers. Linearity of functionals plays an important role here. Furthermore, Schwichtenberg, Berger and Hofmann devised a calculus for the extraction of polynomial-time non-size-increasing functionals, and Leivant and others investigated subrecursion on co-algebraic data. Finally, Weihrauch studied complexity for computable metric spaces. It is our aim to bring these approaches together and make them usable for realisability on abstract structures, in particular structures in computable analysis. There are natural links to WP1 — Foundations and WP2 — Exact computation in real analysis.
Summary of this research objective: (a) attack the open problems of identifying computationally irrelevant inductive definitions and the realisability interpretation of the general form of open induction;
(b) study realisability based on coherence spaces and linear maps;
(c) apply the representation of the hyper-space of non-empty compact subsets to obtain provably correct renderings of fractals and study continuous functions on the hyper-space;
(d) investigate whether the representation of the hyper-space can be applied to model non-deterministic dynamical systems;
(e) study generalisations to spaces with multi-ary (as opposed to unary) contractions on which the hyper-space construction is a monad;
(f) attack the open question whether there is a logical representation of infinite Gray code;
(g) unify the complexity approaches for higher-type functionals and make them usable for realisability on abstract structures, in particular structures in computable analysis.
Objective 3-II: Contrary to classical logic there are various systems of constructive logic of different strengths. Modern research is particularly interested in knowing what part of analysis can be developed in systems of which strength. The ultimate goal of this part of the research is to develop fundamental results of constructive analysis in a point-free topological way and by performing proofs within logical constraints stringent enough to satisfy a range of constructivist requirements of which one is predicativity. Within this project, several of the research aims are well suited to providing case studies for testing out the power and usability of foundational systems. The main focus will be the constructive set theory called “Minimalist Foundation” developed by Sambin and Maietti. Another foundational setting to be explored, and compared with the Minimalist Foundation, is that of Arithmetic Universes (AUs). Taking its inspiration from topos theory, the AU programme already embodies techniques of point-free topology. However, unlike topos theory, it is predicative. The internal logic of an AU is finitary but has type-theoretic constructions sufficient to provide the countable disjunctions needed for point-free analysis (cf. the -frames discussed later in this WP description).
One of the historical contributors to constructive analysis was Errett Bishop with his 1967 book “Foundations of Constructive Analysis” (revised in collaboration with Bridges in 1985). He was originally concerned with real and complex analysis, including relevant portions of functional analysis.
An advantage of Bishop’s approach with respect to other constructive approaches to analysis, such as Brouwer’s intuitionistic one or Markov’s recursive one (cf. WP1 — Foundations), is that Bishop did not use any principle incompatible with classical mathematics. Hence Bishop produced an analysis of mathematical concepts that is finer than in other approaches. This was made even clearer with the development of constructive reverse mathematics, put forward by Veldman and Ishihara, where theorems are classified by means of their equivalence with well-known non-constructive principles. But to perform such an analysis one needs to adopt a suitable formal system. In the present project we plan to adopt the formal system of Minimalist Foundation to pursue constructive reverse mathematics by focusing on the predicativity of Bishop’s fundamental results in constructive analysis. However, to meet the purpose of developing constructive analysis in the Minimalist Foundation we need to deeply reformulate Bishop’s results by extracting their “point-free topological contents”. The reason is that relevant spaces used in analysis, such as that of real numbers, can be represented in the Minimalist Foundation only in a point-free way. Indeed in the Minimalist Foundation real numbers, either following Dedekind (Dedekind cuts) or Cantor (Cauchy sequences), do not form a set, but only a proper collection (and moreover these two kinds of real numbers are not equivalent due to the absence of choice principles).
A predicative approach to point-free topology, which can be carried on within the Minimalist Foundation, is offered by formal topology, introduced by Martin-Löf and Sambin. Later Sambin generalised formal topology to positive topology to include a predicative treatment of closed subsets. In this project we expect to represent Bishop’s results, starting from a point-free representation of its real numbers (a form of Cauchy real numbers), by employing formal topology and positive topology. Parts of constructive analysis have already been developed in a point-free way by scholars such as Thierry Coquand and Martin-Löf. However their results are performed in a constructive foundation that is stronger than the Minimalist Foundation and where Bishop’s real numbers form a set. An advantage of developing point-free constructive analysis in the Minimalist Foundation would be to reach compatibility with classical predicative mathematics à la Feferman, a fact that most of constructive foundations do not enjoy.
Summary of this research objective: develop fundamental results of constructive analysis in a point-free and predicative way.
Objective 3-III: Constructively, it cannot be demonstrated that random sequences exist, since it is consistent to assume that all sequences are computable. On the other hand, it would be very desirable to have a constructive theory of randomness as it would allow the extraction of computational content from proofs concerning randomness. A constructive version of Oxtoby’s Theorem (that all Polish spaces carrying non-atomic probability measures are measure-preserving homeomorphic on measure-1 subspaces), e.g., will have (a generalisation of) the arithmetic encoding method of data compression as its computational content. In this highly innovative research we will circumvent the dilemma by developing a constructive point-free theory of probability and randomness based on σ-frames, and with regard also to their possible relation to arithmetic universes. As a natural framework for such constructive developments, we shall investigate ways of extending type theory with new types for concepts concerning probability and randomness, with inhabiting terms whose computation appeals to an external source of randomness.
A further goal is to consider simplified frameworks for probability theory, based on ‘constructive’ models such as toposes. One aim is concerned with the development of Nelson’s ‘radically elementary probability theory’ in a topos. This will enable one to define many stochastic processes in these toposes and to find synthetic representations for Dirac ‘functions’ over the zero set of these processes. Another is to consider custom-built toposes defined using probabilistic concepts. For example, a topos of generalised probability spaces will allow a synthetic treatment of random variables as primitive concepts, as envisaged in Mumford’s millennium article “The Dawning of the Age of Stochasticity”. This subtheme combines the areas discussed above with topos theory, logic and non-standard analysis.
Summary of this research objective: (a) develop a framework for constructive point-free probability theory and randomness;
(b) study applications of the framework, e.g. a constructive version of Oxtoby’s theorem;
(c) investigate a type theory with primitive types for randomness and probability;
(d) develop a constructive version of Nelson’s radically elementary probability theory;
(e) understand the local time of Brownian motion from the viewpoint of such a development;
(f) investigate toposes constructed from probabilistic concepts and develop a synthetic probability theory, based on a primitive notion of random variables, valid in such models.
Objective 3-IV: There are surprising, but close connections between computability and constructive logic, as well as constructive logic and topology. Deep connections between the proof-theoretical aspects of constructive logic and computation can be seen via the Curry-Howard correspondence as well as various realisability interpretations. Computation and topology have been inextricably linked ever since D. Scott constructed models of the lambda calculus using topological spaces known as domains, and this link has gained additional strength by recent developments in the field of computable analysis. We come back full circle from topology to logic via Stone duality and its various generalisations and abstractions.
Using Stone duality, any sober topological space can be interpreted as a space of models of a particular constructive propositional logic. In particular, the lattice of open sets of the space can be viewed as the Lindenbaum algebra of some propositional theory within a particular constructive logic known as geometric logic. Conversely, the Lindenbaum algebra of a propositional geometric theory determines a sober space. This allows a nice topology-logic connection, but if the sober spaces involved are set-theoretically very large or non-constructively defined, then the corresponding geometric theory will be uncountable, and we lose our connections with computability. Recently, it was shown that the spaces that correspond to countable propositional geometric theories (i.e., countably many axioms and countably many propositional variables) are precisely the class of quasi-Polish spaces. This discovery raises many important research questions, such as better understanding the relationship between recursively axiomatised theories and effective quasi-Polish spaces. Implicit in all the above is the possibility of a constructive point-free account, as stressed earlier. The connections between quasi-Polish spaces and Vickers’ localic completion will be explored. This further suggests a possible use of arithmetic universes as a foundational setting in which to investigate the countability constraints in the above-mentioned result. Another question is how to deal with non-quasi-Polish spaces. For example, the space of rationals yields a geometric theory with uncountably many axioms, which suggests methods from computable analysis might be needed if any computational meaning can be given to this kind of theory.
Recently there is increasing interest in modelling modal logics using co-algebras. In particular, it is known that the Vietoris functor on the category of Stone spaces can be used to provide semantics of modal logics. The Vietoris functor maps a Stone space to its hyper-space of compact subsets with the Vietoris topology. A co-algebra for this functor consists of a space and a continuous function into this hyper-space. Such a co-algebra is a non-deterministic topological dynamical system, where the function defines all of the possible transitions a point can make in the next time step. The co-algebra can also be interpreted as a Kripke frame, where the function maps each “world” to the set of all other accessible “worlds”, thus providing semantics for modal logics. Similar constructions are also common in domain theory to model non-deterministic computations. Quasi-Polish spaces appear to provide a reasonable setting in which to unify these various approaches, and our goal will be to work out this theory in detail. Such a theory would provide deep connections between topological dynamical systems, intuitionistic modal logics, and semantics of non-deterministic computation, and would be general enough to include most topological spaces that occur in practise.
The third task is to investigate realisability interpretations of semi-classical logical principles in the category of represented spaces. Note that the category of represented spaces is locally Cartesian closed and therefore provides semantics for dependent type theory. Although many challenging problems still remain, the DST of represented spaces has seen much progress in recent years (cf. WP1 — Foundations). This undertaking will focus on clarifying how these developments can be interpreted within the logics that they model. There appear to be connections with work by J. van Oosten giving realisability characterisations of hyper-arithmetical functions. Furthermore, S. Hayashi and others have provided limit-computable realisability interpretations of excluded middle and other semi-classical principles for formulas of bounded arithmetical complexity. It is important to better understand how these approaches are all related.
Summary of this research objective: (a) investigate the relationship between recursively axiomatised theories and effective quasi-Polish spaces;
(b) explore the connection between quasi-Polish spaces and localic completions;
(c) unify co-algebra constructions for functors into hyper-spaces known for Stone spaces and domains on the basis of quasi-Polish spaces;
(d) study realisability interpretations of semi-classical logical principles in the category of represented spaces, and clarify their computational aspects.