Computability in Locally Compact Spaces
This paper develops computation in Abstract Stone Duality.
Numerous results in computability theory, including Church’s thesis and various Choice principles, can be deduced from Kleene’s theorem that any RE predicate φ(x) is expressible as ∃ h.T(p,n,h), where T is decidable. Here we adapt these results to computation in any locally compact space (in particular, in R) by means of the effective bases of open and compact subspaces that were developed in the author’s earlier work.
Our Kleene theorem also provides a plan for a compiler from the Abstract Stone Duality calculus into constraint logic programming. The formal meets of the basis elements lead to a generalisation of unification, which is Cleary’s Logical Arithmetic in the case of the reals. Roundedness with respect to the way-below or cover relation indicates how to improve the precision of a value and how to perform universal quantification over a compact subspace.
Following Landin’s SECD machine, the stack consists of values like n that correspond to inputs, and has a contravariance property like the compact part of the basis. Intermediate and output values reside in the heap h, which, like the open part of the basis, is covariant, and indeed preserves meets.
Download the paper to print it
PDF, DVI, compressed PostScript or A5 booklet.
Table of contents
2. Bases for locally compact spaces
3. Examples of spaces
4. Binary trees as data structures
5. The Kleene normal form
6. Terms of ground type
8. General types
10. Choice principles
11. Implementing a compiler
12. Real arithmetic
This document was translated from LATEX by HEVEA.