Abstract A uniform approach to computing with infinite objects like real numbers, tuples of these, compacts sets and uniformly continuous maps is presented. In the work of Berger, it was shown how to extract certified algorithms working with the signed digit representation from constructive proofs. Berger and the present author generalised this approach to complete metric spaces and showed how to deal with compact sets. Here, we unify this work and lay the foundations for doing a similar thing for the much more comprehensive class of compact Hausdorff spaces occurring in applications. The approach is of the same computational power as Weihrauch’s Type-Two Theory of Effectivity.

This issue of Mathematical Structures in Computer Science is composed mainly of papers submitted by participants of the Workshop ‘Continuity, Computability, Constructivity: From Logic to Algorithms,’ held in Gregynog, a conference centre of the University of Wales located in the beautiful nature of Mid Wales, in the last week of June 2013. In addition, several colleagues accepted our invitation to contribute to this volume.

The continuity problem, i.e., the question whether effective maps between effectively given topological spaces are effectively continuous, is reconsidered. In earlier work, it was shown that this is always the case, if the effective map also has a witness for non-inclusion. The extra condition does not have an obvious topological interpretation. As is shown in the present paper, it appears naturally where in the classical proof that sequentially continuous maps are continuous, the Axiom of Choice is used. The question is therefore whether the witness condition appears in the general continuity theorem only for this reason, i.e., whether effective operators are effectively sequentially continuous. For two large classes of spaces covering all important applications, it is shown that this is indeed the case. The general question, however, remains open. Spaces in this investigation are in general not required to be Hausdorff. They only need to satisfy the weaker T 0 separation condition

This special issue of Mathematical Structures in Computer Science is composed mainly of papers submitted by participants of the Dagstuhl Seminar on Computing with Infinite Data: Topological and Logical Foundations. The workshop took place in the Schloss Dagstuhl - Leibniz Center for Informatics in the first half of October 2011.

Abstract If one wants to compute with infinite objects like real numbers or data streams, continuity is a necessary requirement: better and better (finite) approximations of the input are transformed into better and better (finite) approximations of the output. In case the objects are constructively generated, they can be represented by a finite description of the generating procedure. By effectively transforming such descriptions for the generation of the input (respectively, their codes) into (the code of) a description for the generation of the output another type of computable operation is obtained. Such operations are also called effective. The relationship of both classes of operations has always been a question of great interest. In this paper the setting is extended to the case of multifunctions. Various ways of coding (indexing) sets are discussed and their relationship is investigated. Moreover, effective versions of several continuity notions for multifunctions are introduced. For each of these notions an indexing system for sets is exhibited so that the multifunctions that are effective with respect to this indexing system are exactly the multifunction which are effectively continuous with respect to the continuity notion under consideration. Mostly, in addition to being effective the multifunctions need also possess certain witnessing functions. Important special cases are discussed where such witnessing functions always exist.

This paper addresses a conjecture of Smyth that says that if -algebraic cpo, and computable maps as morphisms. This is indeed the case: the category of constructive SFP domains is the largest constructively Cartesian closed weakly indexed effectively full subcategory of the category of constructive domains that have a completeness test and satisfy a further effectivity requirement.

Minimization operators of different strengths have been studied in the framework of "predicative (safe) recursion." In this paper, a modification of these operators is presented. By adding the new operator to those used by Bellantoni--Cook and Leivant to characterize the polynomial-time computable functions, one obtains a characterization of the nondeterministic polynomial-time computable multifunctions. Thus the generation of the nondeterministic polytime multifunctions from the deterministic polytime functions parallels the generation of the computable functions from the primitive recursive ones.

Abstract In examples like the total recursive functions or the computable real numbers the canonical indexings are only partial maps. It is even impossible in these cases to find an equivalent total numbering. We consider effectively given topologicalT0-spaces and study the problem in which cases the canonical numberings of such spaces can be totalized,i.e., have an equivalent total indexing. Moreover, we show under very natural assumptions that such spaces can effectively and effectively homeomorphically be embedded into a totally indexed algebraic partial order that is closed under the operation of taking least upper bounds of enumerable directed subsets.

Abstract Starting with D. Scott's work on the mathematical foundations of programming language semantics, interest in topology has grown up in theoretical computer science, under the slogan ‘open sets are semidecidable properties’. But whereas on effectively given Scott domains all such properties are also open, this is no longer true in general. In this paper a characterization of effectively given topological spaces is presented that says which semidecidable sets are open. This result has important consequences. Not only follows the classical Rice-Shapiro Theorem and its generalization to effectively given Scott domains, but also a recursion theoretic characterization of the canonical topology of effectively given metric spaces. Moreover, it implies some well known theorems on the effective continuity of effective operators such as P. Young and the author's general result which in its turn entails the theorems by Myhill-Shepherdson, Kreisel-Lacombe-Shoenfield and Ceĭtin-Moschovakis, and a result by Eršov and Berger which says that the hereditarily effective operations coincide with the hereditarily effective total continuous functionals on the natural numbers.