Computable topology

Computable topology is a discipline in mathematics that studies the topological and algebraic structure of computation. Computable topology is not to be confused with algorithmic or computational topology, which studies the application of computation to topology.

As shown by Alan Turing and Alonzo Church, the λ-calculus is strong enough to describe all mechanically computable functions (see Church–Turing thesis). Lambda-calculus is thus effectively a programming language, from which other languages can be built. For this reason when considering the topology of computation it is common to focus on the topology of λ-calculus. Note that this is not necessarily a complete description of the topology of computation, since functions which are equivalent in the Church-Turing sense may still have different topologies.

The topology of λ-calculus is the Scott topology, and when restricted to continuous functions the type free λ-calculus amounts to a topological space reliant on the tree topology. Both the Scott and Tree topologies exhibit continuity with respect to the binary operators of application ( f applied to a = fa ) and abstraction ((λx.t(x))a = t(a)) with a modular equivalence relation based on a congruency. The λ-algebra describing the algebraic structure of the lambda-calculus is found to be an extension of the combinatory algebra, with an element introduced to accommodate abstraction.

Type free λ-calculus treats functions as rules and does not differentiate functions and the objects which they are applied to, meaning λ-calculus is type free. A by-product of type free λ-calculus is an effective computability equivalent to general recursion and Turing machines. The set of λ-terms can be considered a functional topology in which a function space can be embedded, meaning λ mappings within the space X are such that λ:X → X. Introduced November 1969, Dana Scott's untyped set theoretic model constructed a proper topology for any λ-calculus model whose function space is limited to continuous functions. The result of a Scott continuous λ-calculus topology is a function space built upon a programming semantic allowing fixed point combinatorics, such as the Y combinator, and data types. By 1971, λ-calculus was equipped to define any sequential computation and could be easily adapted to parallel computations. The reducibility of all computations to λ-calculus allows these λ-topological properties to become adopted by all programming languages.

...
Wikipedia