A computably based locally compact space consists of a set of codes
for basic “points”, “open” and “compact” subspaces, together with an interpretation of
these codes in a locally compact sober space. We require of the space that every open
subspace be a union of basic ones. We also want to be able to compute
codes (that we shall just call 0 and 1) for the empty set and the entire space, considered
as open and compact subspaces (if, that is, the entire space is in fact compact);
codes for the union and intersection of two open subspaces, and for the union of two
compact ones, given their codes (we write + and ⋆ instead of ∪ and ∩ for these binary
operations, to emphasise that they act on codes, rather than on the subspaces that the
codes name);
whether a particular representable point belongs to a particular basic open subspace,
given their codes; but we only need a positive answer to this question if there is one, as
failure of the property is indicated by non-termination;
more generally, whether an open subspace includes a compact one, given their codes;
codes for U and K such that L ⊂ U ⊂ K ⊂ V , given codes for L ⊂ V as above.
In fact, we shall require the basic compact and open subspaces to come in pairs, with
U_n ⊂ K_n as in [JS96], where the superscript n names the pair, and we also need part
v. to yield such a pair as the interpolant.
Taylor, Paul , Computably based locally compact spaces.[J] Log. Methods Comput. Sci. 2, No. 1, Paper 1, 70 p., electronic only (2006).
[JS96] Jung, Achim and Sünderhauf, Philipp On the duality of compact vs. open.[A] Andima, Susan (ed.) et al., Papers on general topology and applications. Papers presented at the 11th summer conference at the University of Southern Maine, Gorham, ME, USA, August 10--13, 1995. New York, NY: The New York Academy of Sciences. Ann. N. Y. Acad. Sci. 806, 214-230 (1996)