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

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^AT_EX by H^EV^EA.