|
Abstract
Abstract Stone Duality is a revolutionary paradigm for general topology
that describes computable continuous functions directly,
without using set theory, infinitary lattice theory or
a prior theory of discrete computation.
Every expression in the calculus denotes both a continuous function
and a program, and the reasoning looks remarkably like
a sanitised form of that in classical topology.
This is an introduction to ASD for the general mathematician,
with application to elementary real analysis.
This language is applied to the Intermediate Value Theorem:
the solution of equations for continuous functions on the real line.
As is well known from both numerical and constructive considerations,
the equation cannot be solved if the function "hovers" near 0,
whilst tangential solutions will never be found.
In ASD, both of these failures and the general method of finding
solutions of the equation when they exist
are explained by the new concept of overtness.
The zeroes are captured, not as a set,
but by higher-type modal operators.
Unlike the Brouwer degree, these are defined and (Scott) continuous
across singularities of a parametric equation.
Expressing topology in terms of continuous functions rather
than sets of points leads to treatments of open and closed concepts
that are very closely lattice- (or de Morgan-) dual,
without the double negations that are found in intuitionistic approaches.
In this, the dual of compactness is overtness.
Whereas meets and joins in locale theory are asymmetrically
finite and infinite,
they have overt and compact indices in ASD.
Overtness replaces metrical properties such as total boundedness,
and cardinality conditions such as having a countable dense subset.
It is also related to locatedness in constructive analysis
and recursive enumerability in recursion theory.
History This paper was presented at
@inproceedings{TaylorP:lamcra,
author = {Taylor, Paul},
title = {A Lambda Calculus for Real Analysis},
pages = {227--266},
booktitle = {Computability and Complexity in Analysis},
editor = {Grubba, Tanja and Hertling, Peter and
Tsuiki, Hideki and Weihrauch, Klaus},
year = 2005,
number = 326,
series = {Informatik Berichte},
publisher = {FernUniversit\"at in Hagen},
note = {revised version at
www.PaulTaylor.EU/ASD/lamcra/}}
Acknowledgements As I was a reluctant analyst, this work would never have been done without the persistent (but friendly) cajoling of Graham White and Andrej Bauer. I would like to express my warmest appreciation for the ongoing encouragement that they have both given me. In particular, during my visit to Ljubljana in November 2004, Andrej provided the construction of the supremum of a compact overt subspace in Section 12 using Dedekind cuts that is the keystone of this paper. I am grateful to Peter Hertling and the CCA programme committee for the indulgence of allowing me to occupy altogether 80 pages of their proceedings. The paper that you see here is the fruit of illuminating discussions with numerous people since the conference. I would particularly also like to thank Vasco Brattka, Douglas Bridges, Robin Cockett, Thierry Coquand, Nicola Gambino, André Joyal, Achim Jung, Norbert Müller, Petrus Potgieter, Pino Rosolini, Giovanni Sambin, Peter Schuster, Anton Setzer and Bas Spitters for their interest and encouragement in this project. The top-level HTML pages on this site (including this one) were translated from LATEX using TTH, whilst Hevea was used for the content of this paper. |
Download the paper to print it
PDF,
DVI,
compressed PostScript or
A5 booklet.
Table of contents and the HTML version Introduction An overview of the sections of the paper. 1. The constructive intermediate value theorem The constructive critique of this classical theorem and some mis-understandings; stable zeroes. 2. Stable zeroes and straddling intervals Straddling intervals; the < > operator; it preserves joins; compact subpaces and []; the modal laws; singular and non-singular cases. 3. The Scott topology Some background in non-Hausdorff general topology: the Scott topology; the ascending and descending reals; semicontinuous functions; the constructive least upper bound principle; the Sierpinski space Σ and open and closed subspaces; directed unions and relations; uniformity; function-spaces; local compactness; analogy with computation; the Phoa principle. 4. Introducing the calculus Algebra, order and induction on N, Q and R; propositions (terms of type Σ) and statements (equations thereof); discrete and Hausdorff spaces. 5. Formal reasoning Contexts, judgements, rules and proofs; functions and denotation; monotonicity, Phoa and Gentzen rules; properties of equality and inequality; the existential quantifier. 6. Numbers from logic Definition by description; general recusion; the existence property and computation; Dedekind completeness; the Archimedean principle; evaluating real-valed expressions; Cauchy completeness; representability of computable continuous functions. 7. Open and general subspaces The λ-calculus and set-theoretic notation used for these. 8. Abstract compact subspaces The familiar results that link compact and closed subspaces of Hausdorff spaces; compact spaces; the universal quantifier; occupied compact (sub)spaces; direct images; compact open subspaces; compact subspaces of non-Hausdorff spaces. 9. Compactness and uniformity Scott continuity; directed relations; uniformity; compact intervals; boundedness; supremum of a compact subspace of R is a descending real; categories without these axioms. 10. Continuity on the real line Every member of an open subspace is in its interior; ε-δ continuity; uniform continuity; definitions of the Riemann integral and derivative as Dedekind cuts. 11. Overt subspaces A dual treatment to that in Section 8; accumulation points; compact overt subspaces; emptiness is decidable. 12. Compact overt subspaces Any compact overt subspace of R either is empty or has a maximum element; finding it; the singular case. 13. Connectedness Classical, constructive = overt and compact binary definitions; approximate intermediate value theorems; [0,1] is connected in all senses, with the classical proof; R is overt connected; compact connected subspaces of R are intervals. 14. The intermediate value theorem The proofs in ASD of the results in Sections 1-2; in the bounded non-singular case, there is a maximum zero; the singular case. 15. Some counterexamples Classical and constructive connectedness; compact subspaces that are not overt; ascending reals with no descending partner; failure of overtness for hovering functions; the singular case. 16. Local connectedness Connected open subspaces; finitary overt connectedness; every open equivalence relation ∼ on [0,1] has 0 ∼ 1; this fails in Bishop's theory; the categorical (infinitary) definition; occupied compact intervals are connected. References |
This is www.PaulTaylor.EU/ASD/lamcra/index.html and it was derived from ASD/lamcra.tex which was last modified on 9 December 2009.