|
News (February 2011): New research programme on
Equideductive Topology,
whose leading concrete model is the category of all sober topological spaces
(not just locally compact ones), with three draft papers.
What is Abstract Stone Duality? It is a revolutionary theory of topological spaces and continuous functions that treats them directly, just as traditional geometry was about lines and circles, without smashing the continuum into dust. ASD provides a natural language for real analysis that describes the solution-space of an equation continuously in its parameters, even across singularities. Since it is presented syntactically, in a way that generalises ordinary algebraic notation, it is inherently computable. It was inpired by Marshall Stone's study of the categorical duality between topology and algebra, taking his slogan "always topologize" seriously by topologising the topology. It also exploits the analogy between continuous and computable functions, on which Dana Scott built the theory of denotational semantics of programming languages. ASD also has a very strong lattice duality. Any open subspace U of a space X is the inverse image of the open point of the Sierpinksi space (here called T ∈ Σ) under a unique continuous function φ:X→Σ. We write membership a ∈ U logically, as the predicate φ(a), so ∧, ∨ and ∃ mean intersection, union and infinite union of open subspaces. Since the same is true of any closed subspace and the closed point ⊥ ∈ Σ, these symbols also mean union, intersection and infinite intersection of closed subspaces. The correspondence between open and closed subspaces arises from their common relationship to a continuous map φ:X→Σ, not by set-theoretic complementation. This logic is valid constructively, but as it applies equally to open and closed subspaces, it often looks like classical logic, and is free of the ubiquitous double negations of intuitionism. For example, in a Hausdorff space H, the diagonal subspace is closed, so it has a continuous map H×H→Σ that we call ≠ . In particular, inequality in R is computationally observable, whilst equality is not. Dually, discrete spaces such as N and Q have =, because their diagonals are open. The topology (lattice of open subspaces) of a space X is another space, called ΣX or X→Σ. We need this in order to say when K is a compact space, namely if it has a continuous map ∀:ΣK→Σ. Logically, this obeys the rules of predicate calculus, and topologically the Heine-Borel "finite open sub-cover" property. However, it is much stronger than saying that "every point" of K is in U, as there are not enough computably representable points for this to be a valid mode of reasoning. Similarly, a compact subspace K ⊂ X is described by a necessity operator []:ΣX→Σ, where []φ means that the open subspace corresponding to φ covers K. The duality between open and closed ideas in ASD is so close that it is often very fruitful to turn definitions and theorems "up-side down". In particular, the dual of compactness is overtness, which is defined using the symbols ∃ and < > . This concept is invisible in classical topology, because there all spaces are overt, but similar ideas have turned up in other constructive disciplines. Its role is played by locatedness and total boundedness in Bishop's Constructive Analysis, but these are metrical ideas, whereas overtness is topological. Its strongest relationship is to recursive enumerability in recursion theory, and it legitimises the idea that the topology of N consists of the RE subsets. In real analysis, the stable zeroes of a function (those where the function takes values of opposite sign arbitrarily closely on opposite sides of the zero) form an overt subspace, whose < > operator is directly related to algorithms for solving the equation. The re-axiomatisation of topology requires more than the exponential objects ΣX and their associated λ-calculus. In particular, the three-way extensional correspondence amongst open and closed subspaces and continuous maps X→Σ depends on the equation
However, we need a further idea to justify definition by description, Dedekind completeness and compactness of [0,1] ⊂ R. These are all consequences of the wild speculation in category theory from which ASD began, namely the principle that the dual of the category of spaces is algebraic over the category of spaces itself, where we express infinitary algebra my means of a monad in category theory. |
Introduction - the papers on real analysis
[J] A Lambda Calculus for Real Analysis
(for a general mathematical audience).
[K] Interval Analysis Without Intervals
(for programmers).
[I] The Dedekind Reals in ASD, with
Andrej Bauer
(for theoretical computer scientists),
Mathematical Structures in Computer Science,
19 (2009) 757-838.
Efficient Computation with Dedekind Reals, by
Andrej Bauer (for actual computation).
The core theory for locally compact spaces [O] Foundations for Computable Topology surveys of the development of ASD, including the methodology behind it and an overview of the components of the theory that are described more fully in the following papers. [A] Sober Spaces and Continuations. Theory and Applications of Categories 10 (2002) 248-299. [B] Subspaces in ASD. Theory and Applications of Categories 10 (2002) 300-366. [C] Geometric and Higher Order Logic in terms of ASD, Theory and Applications of Categories 7 (2000) 284-338. [D] Non-Artin Gluing in Recursion Theory and Lifting in ASD, 2000. [E] Inside every model of ASD lies an Arithmetic Universe, Electronic Notes in Theoretical Computer Science 122 (2005) 247-296. [G] Computably Based Locally Compact Spaces, Logical Methods in Computer Science, 2 (2006) 1-70. Other papers on locally compact spaces [F] Scott Domains in ASD, 2002. [G-] Local Compactness and the Baire Category Theorem in ASD: a feasibility study, Electronic Notes in Theoretical Computer Science 69 (2003). [L] Tychonov's Theorem in ASD, 2004. Beyond local compactness There are two ideas for extending ASD beyond locally compact spaces. One is equideductive logic, which is a predicate calculus whose object language is the sober lambda calculus, and has the category of all sober topological spaces as its leading model. It is motivated by the way in which this category (and others, such as that of affine varieties) lies nicely within a cartesian closed extension, and a new construction of such an extension is given. The other is the "underlying set functor", which makes the full subcategory of overt discrete spaces into a topos and enables the characterisation of the categories of sober spaces and of locales. Synthetic domain theory This is the theory out of which ASD originally grew. Its view of the world is a topos, i.e. a specially constructed model of intuitionistic set theory. Topological spaces or domains are special sets, but all functions between them are continuous and computable. [-] The Synthetic Plotkin Powerdomain, with Wesley Phoa, 1990. [-] The Fixed Point Property in Synthetic Domain Theory, Logic in Computer Science 6 (1991). [-] Stone Duality in Synthetic Domain Theory, with Giuseppe Rosolini, 1997. |
This is www.PaulTaylor.EU/ASD/index.php and it was derived from ASD/index-080630.tex which was last modified on 20 February 2011.