computably based locally compact

Definition

• 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
  1. 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);
  2. 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);
  3. 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;
  4. more generally, whether an open subspace includes a compact one, given their codes;
  5. codes for U and K such that L ⊂ U ⊂ K ⊂ V , given codes for L ⊂ V as above.
  6. 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.

Reference

• 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)