|
|
PDF (818 kb) DVI (654 kb) PostScript (compressed) (471 kb) A5 PS booklet (compressed) (445 kb) What are these? [19 Aug 2010] |
Presented at
This paper is intended for the general mathematician. It introdes the ASD axioms above for R and applies them to elementary real analysis. In particular, it studies the Intermediate Value Theorem, i.e. the solution of equations f x=0 for continuous f:R→R, and the notion of connectedness that is abstracted from it. In classical real analysis thie theorem holds for general continuous functions. However, it is well known from both numerical and constructive considerations that the equation cannot be solved if f "hovers" near 0, whilst tangential solutions will never be found. The paper begins with a summary of the constructive critique, but goes on to throw new light on the cases that constructivists usually dismiss. 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 operators [] and < > that remain (Scott) continuous across singularities of a parametric equation. Expressing topology in terms of continuous functions rather than sets of points leads to a very closely dual treatment of open and closed subspaces, without the double negations of intuitionistic approaches. In this, the dual of compactness is overtness, and 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. As a further application of connectedness, we also show that every open set of the line is uniquely expressible as a countable union of intervals, in a suitable constructive sense, which is not the case in Bishop's theory. The characterisation of open subsets of R as countable unions of disjoint open intervals, and some counterexamples, were added in April 2007; these are in (the present) Sections 13, 15 and 16. In this, the January 2008 version, Sections 3, 5, 6, 7, 9 and 10 have been completely (re)written to provide a brief Òneed to knowÓ account of various foundational disciplines that underlie this work. |
|
PDF (764 kb) DVI (550 kb) PostScript (compressed) (447 kb) A5 PS booklet (compressed) (425 kb) What are these? [03 Jun 2009] |
with Andrej Bauer.
Mathematical Structures in Computer Science,
19 (2009) 757-838.
Presented at Computability and Complexity in Analysis, Kyoto, 25-29 August 2005,
using these slides.
Also presented at
Foundational Methods in Computer Science,
Kananaskis, Canadian Rockies, 7-9 June 2006,
using these improved slides.
Abstract Stone Duality (ASD) is a direct axiomatisation of general topology, in contrast to the traditional and all other contemporary approaches, which rely on a prior notion of discrete set, type or object of a topos. ASD reconciles mathematical and computational viewpoints, providing an inherently computable calculus that does not sacrifice key properties of real analysis such as compactness of the closed interval. Previous theories of recursive analysis failed to do this because they were based on points; ASD succeeds because, like locale theory, it is founded on the algebra of open subspaces. ASD is presented as a λ-calculus, of which this paper provides a self-contained summary, as the foundational background has been investigated in earlier work. The core of the paper constructs the real line using two-sided Dedekind cuts. We show that the closed interval is compact and overt, these concepts being defined in ASD using quantifiers. Further topics, such as the Intermediate Value Theorem, are presented in a separate paper that builds on this one. The interval domain plays an important foundational role. However, we see intervals as generalised Dedekind cuts, which underly the construction of the real line, not as sets or pairs of real numbers. Our definitions of the arithmetic operations are more complicated than Moore's, because we work constructively. The final section compares ASD with other systems of constructive and computable topology and analysis. |
|
PDF (315 kb) DVI (114 kb) PostScript (compressed) (102 kb) A5 PS booklet (compressed) (95 kb) What are these? [12 Feb 2009] |
The slides that I used for my
presentation at Real Numbers and Computers
(Nancy, 10-12 July 2006) give a more complete account of this work.
The paper is incomplete.
We argue that Dedekind completeness and the Heine-Borel property should be seen as part of the "algebraic" structure of the real line, along with the usual arithmetic operations and relations. Dedekind cuts provide a uniform and natural way of formulating differentiation, integration and limits. They and these examples also generalise to intervals. Together with the arithmetic order, cuts enjoy proof-theoretic introduction and elimination rules similar to those for lambda abstraction and application. This system completely axiomatises computably continuous functions on the real line. We show how this calculus (of "single" points) can be translated formally into Interval Analysis, interpreting the arithmetic operations a la Moore, and compactness as optimisation under constraints. Notice that interval computation is the conclusion and not the starting point. |
This is www.PaulTaylor.EU/ASD/analysis.php and it was derived from ASD/analysis.tex which was last modified on 16 July 2009.