 |
 |
Special Festschrift Issue in Honor of Dieter Spreen
The workshop *Continuity, Computability, Constructivity - From Logic to Algorithms (CCC 2012)* was held in Trier (Germany) from May 29 to June 2, 2012. It was the second in a series of workshops which are part of the EU project *Computable Analysis - theoretical and applied aspects (COMPUTAL)*. This special issue of *Logical Methods in Computer Science* contains nine selected contributions of workshop participants. The workshop as well as this special issue were dedicated to *Dieter Spreen*, the leader of the COMPUTAL project and founder of the CCC workshop series, to honour his numerous contributions to the field. Dieter Spreen's pioneering work on effective topological spaces revealed the intimate connection between continuity and computability. His result on the continuity of total effective operations (*On effective topological spaces, The Journal of Symbolic Logic 63, 185-221, 1998*) is one of the most powerful generalization of the Kreisel-Lacombe-Shoenfield Theorem and constitutes, together with its partial counterparts, Rice's Theorem and the Rice-Shapiro Theorem, one of the pillars for research on topological aspects of computability with far reaching consequences in current research areas such as Domain Theory, Computable Analysis, Constructive Mathematics and Proof Theory. Dieter Spreen scientific contributions are complemented by his tireless and very successful activities to promote and foster these research areas and to support young researches. He organized many Dagstuhl seminars and initiated and led successful large EU network grant applications and projects with associated workshops, to give some examples. The articles in this special issue cover a wide spectrum of research that is being carried out under the umbrella of the COMPUTAL project: Intuitionistic Logic (Hajime Ishihara), Algorithmic Randomness, Brownian Motion, Fourier Spectra (Willem Louw Fouch@eacute;, Safari Mukeru and George Davie), Realizability, Higher-Type Functionals, Computable Analysis (Dag Normann), Domain Representations, Computable Analysis (Hideki Tsuiki and Yasuyuki Tsukamoto), Topology, Domain-theory, Functional Analysis (Klaus Keimel), Constructive Analysis (Douglas Bridges, James Dent, Maarten McKubre-Jordens), Infinitary Combinatorics, Proof Theory, Program Extraction (Josef Berger and Helmut Schwichtenberg), Co-analytic Sets, Quasi-Polish Spaces (Matthew de Brecht), Computable Solutions of Partial Differential Equations (Svetlana Selivanova and Victor Selivanov). All papers were refereed according to the usual standards of *Logical Methods in Computer Science*. Ulrich Berger, Hannes Diener, Norbert Müller CCC 2012 Guest Editors Editors: Ulrich Berger, Hannes Diener, Norbert Müller
1. Fourier spectra of measures associated with algorithmically random Brownian motion
In this paper we study the behaviour at infinity of the Fourier transform of Radon measures supported by the images of fractal sets under an algorithmically random Brownian motion. We show that, under some computability conditions on these sets, the Fourier transform of the associated measures have, relative to the Hausdorff dimensions of these sets, optimal asymptotic decay at infinity. The argument relies heavily on a direct characterisation, due to Asarin and Pokrovskii, of algorithmically random Brownian motion in terms of the prefix free Kolmogorov complexity of finite binary sequences. The study also necessitates a closer look at the potential theory over fractals from a computable point of view.
2. Classical propositional logic and decidability of variables in intuitionistic propositional logic
We improve the answer to the question: what set of excluded middles for propositional variables in a formula suffices to prove the formula in intuitionistic propositional logic whenever it is provable in classical propositional logic.
3. The extensional realizability model of continuous functionals and three weakly non-constructive classical theorems
We investigate wether three statements in analysis, that can be proved classically, are realizable in the realizability model of extensional continuous functionals induced by Kleene's second model $K_2$. We prove that a formulation of the Riemann Permutation Theorem as well as the statement that all partially Cauchy sequences are Cauchy cannot be realized in this model, while the statement that the product of two anti-Specker spaces is anti-Specker can be realized.
4. Domain Representations Induced by Dyadic Subbases
We study domain representations induced by dyadic subbases and show that a proper dyadic subbase S of a second-countable regular space X induces an embedding of X in the set of minimal limit elements of a subdomain D of $\{0,1,\perp\}\omega$. In particular, if X is compact, then X is a retract of the set of limit elements of D.
5. Weak upper topologies and duality for cones
In functional analysis it is well known that every linear functional defined on the dual of a locally convex vector space which is continuous for the weak topology is the evaluation at a uniquely determined point of the given vector space. M. Schroeder and A. Simpson have obtained a similar result for lower semicontinuous linear functionals on the cone of all Scott-continuous valuations on a topological space endowed with the weak upper topology, an asymmetric version of the weak topology. This result has given rise to several proofs, originally by the Schroeder and Simpson themselves and, more recently, by the author of these Notes and by J. Goubault-Larrecq. The proofs developed from very technical arguments to more and more conceptual ones. The present Note continues on this line, presenting a conceptual approach inspired by classical functional analysis which may prove useful in other situations.
6. Z-stability in Constructive Analysis
We introduce Z-stability, a notion capturing the intuition that if a function f maps a metric space into a normed space and if the norm of f(x) is small, then x is close to a zero of f. Working in Bishop's constructive setting, we first study pointwise versions of Z-stability and the related notion of good behaviour for functions. We then present a recursive counterexample to the classical argument for passing from pointwise Z-stability to a uniform version on compact metric spaces. In order to effect this passage constructively, we bring into play the positivity principle, equivalent to Brouwer's fan theorem for detachable bars, and the limited anti-Specker property, an intuitionistic counterpart to sequential compactness. The final section deals with connections between the limited anti-Specker property, positivity properties, and (potentially) Brouwer's fan theorem for detachable bars.
7. A bound for Dickson's lemma
We consider a special case of Dickson's lemma: for any two functions $f,g$ on the natural numbers there are two numbers $i<j$ such that both $f$ and $g$ weakly increase on them, i.e., $f_i\le f_j$ and $g_i \le g_j$. By a combinatorial argument (due to the first author) a simple bound for such $i,j$ is constructed. The combinatorics is based on the finite pigeon hole principle and results in a descent lemma. From the descent lemma one can prove Dickson's lemma, then guess what the bound might be, and verify it by an appropriate proof. We also extract (via realizability) a bound from (a formalization of) our proof of the descent lemma. Keywords: Dickson's lemma, finite pigeon hole principle, program extraction from proofs, non-computational quantifiers.
8. Computing Solution Operators of Boundary-value Problems for Some Linear Hyperbolic Systems of PDEs
We discuss possibilities of application of Numerical Analysis methods to proving computability, in the sense of the TTE approach, of solution operators of boundary-value problems for systems of PDEs. We prove computability of the solution operator for a symmetric hyperbolic system with computable real coefficients and dissipative boundary conditions, and of the Cauchy problem for the same system (we also prove computable dependence on the coefficients) in a cube $Q\subseteq\mathbb R^m$. Such systems describe a wide variety of physical processes (e.g. elasticity, acoustics, Maxwell equations). Moreover, many boundary-value problems for the wave equation also can be reduced to this case, thus we partially answer a question raised in Weihrauch and Zhong (2002). Compared with most of other existing methods of proving computability for PDEs, this method does not require existence of explicit solution formulas and is thus applicable to a broader class of (systems of) equations.
9. A generalization of a theorem of Hurewicz for quasi-Polish spaces
We identify four countable topological spaces $S_2$, $S_1$, $S_D$, and $S_0$ which serve as canonical examples of topological spaces which fail to be quasi-Polish. These four spaces respectively correspond to the $T_2$, $T_1$, $T_D$, and $T_0$-separation axioms. $S_2$ is the space of rationals, $S_1$ is the natural numbers with the cofinite topology, $S_D$ is an infinite chain without a top element, and $S_0$ is the set of finite sequences of natural numbers with the lower topology induced by the prefix ordering. Our main result is a generalization of Hurewicz's theorem showing that a co-analytic subset of a quasi-Polish space is either quasi-Polish or else contains a countable $\Pi^0_2$-subset homeomorphic to one of these four spaces.