A lambda calculus for real analysisPaul Taylor |
|
This paper is an introduction to Abstract Stone Duality and its in particular its application to real analysis that is indended for the general mathematician. It was published in the Journal of Logic and Analysis 2(5) 1–115 on 18 August 2010 (BibTeX).
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
More than 1500 distinct non-robot sites downloaded this paper between September 2007 and June 2010, including over 150 universities.
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. This work was presented at Computability and Complexity in Analysis in Kyoto in August 2005, and I am grateful to Peter Hertling and the CCA programme committee for the indulgence of allowing me to occupy altogether 80 pages of their (pre-conference) 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 Jeremy Avigad, Vasco Brattka, Douglas Bridges, Robin Cockett, Thierry Coquand, Martín Escardó, Nicola Gambino, André Joyal, Achim Jung, Norbert Müller, Erik Palmgren, Petrus Potgieter, Pino Rosolini, Giovanni Sambin, Peter Schuster, Anton Setzer, Bas Spitters and Steve Vickers for their interest and encouragement in this project. Finally, I would like to thank the anonymous referees for their care. Lengthy technical papers are not so uncommon, but in this case someone from well outside my usual circle was obliged to make a seismic shift in his entire understanding of the way in which mathematics is done. I deeply appreciate the grace with which he was willing and able to do this. @article{TaylorP:lamcra,
author = {Taylor, Paul},
title = {A Lambda Calculus for Real Analysis},
journal = {Journal of Logic and Analysis},
year = 2010, month = {August},
volume = 2, number = 5, pages = {1--115},
doi = {10.4115/jla.2010.2.5},
url = {PaulTaylor.EU/ASD/lamcra}}
@inproceedings{TaylorP:lamcra-,
author = {Taylor, Paul},
title = {A Lambda Calculus for Real Analysis},
booktitle = {Computability and Complexity in Analysis},
editor = {Grubba, Tanja and Hertling, Peter and
Tsuiki, Hideki and Weihrauch, Klaus},
year = 2005, month = {July},
series = {Informatik Berichte},
volume = 326, pages = {227--266},
publisher = {FernUniversit\"at in Hagen},
note = {Proccedings of the second international conference,
Kyoto, Japan, August 25--29, 2005}}
|
Download the paper to print it PDF, DVI, compressed PostScript or A5 booklet.
Table of contents and the HTML version An overview of the sections of the paper.
The constructive critique of this classical theorem and some mis-understandings; stable zeroes.
Straddling intervals; the ◊ operator; it preserves joins; compact subpaces and ▫; the modal laws; singular and non-singular cases. 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. Algebra, order and induction on ℕ, ℚ and ℝ; propositions (terms of type Σ) and statements (equations thereof); discrete and Hausdorff spaces. Contexts, judgements, rules and proofs; functions and denotation; monotonicity, Phoa and Gentzen rules; properties of equality and inequality; the existential quantifier. 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. The λ-calculus and set-theoretic notation used for these. 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. Scott continuity; directed relations; uniformity; compact intervals; boundedness; supremum of a compact subspace of ℝ is a descending real; categories without these axioms.
Every member of an open subspace is in its interior; є–δ continuity; uniform continuity; definitions of the Riemann integral and derivative as Dedekind cuts. A dual treatment to that in Section 8; accumulation points; compact overt subspaces; emptiness is decidable. Any compact overt subspace of ℝ either is empty or has a maximum element; finding it; the singular case. Classical, constructive = overt and compact binary definitions; approximate intermediate value theorems; [0,1] is connected in all senses, with the classical proof; ℝ is overt connected; compact connected subspaces of ℝ are intervals.
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. 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. 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.
|
This document was translated from LATEX by HEVEA.