nLab effective topological space




topology (point-set topology, point-free topology)

see also differential topology, algebraic topology, functional analysis and topological homotopy theory


Basic concepts

Universal constructions

Extra stuff, structure, properties


Basic statements


Analysis Theorems

topological homotopy theory

Constructivism, Realizability, Computability



A kind of topological space about which one can reason “effectively”, hence constructively. Used in computable analysis, see at computable function (analysis).

  • formal topology Every effective topological space XX defines a formal space. If XX is ‘constructively complete’, then the formal points of XX coincide with its effective points; see Spreen10.
  • equilogical space


  • Dieter Spreen, On effective topological spaces, The Journal of Symbolic Logic, Vol. 63, No. 1, Mar., 1998 (JSTOR)

  • Dieter Spreen, Effectively Given Spaces, Domains, and Formal Topology, 2010 PDF

See the references at computable analysis.

Discussion in relation to equilogical spaces is in

  • Andrej Bauer, section 4.1.2 The Realizability Approach to

    Computable Analysis and Topology_, PhD thesis CMU (2000) (pdf)

With an eye twoards application in computable physics the definition also appears as def. 2.2 in

  • Klaus Weihrauch, Ning Zhong, Is wave propagation computable or can wave computers beat the Turing machine?, Proc. of the London Math. Soc. (3) 85 (2002) (web)

Last revised on March 9, 2014 at 09:38:01. See the history of this page for a list of all contributions to it.