## Computability in Locally Compact Spaces## Paul Taylor |

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

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**

1. Introduction

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

7. Predicates

8. General types

9. Recursion

10. Choice principles

11. Implementing a compiler

12. Real arithmetic

References

This document was translated from L^{A}T_{E}X byH^{E}V^{E}A.