Computable topology explained

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.

Topology of lambda calculus

As shown by Alan Turing and Alonzo Church, the λ-calculus is strong enough to describe all mechanically computable functions (see Church–Turing thesis).^{[1] [2] [3]} 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.^[4] 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.^[5] 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.^{[6] [7]} By 1971, λ-calculus was equipped to define any sequential computation and could be easily adapted to parallel computations.^[8] The reducibility of all computations to λ-calculus allows these λ-topological properties to become adopted by all programming languages.

Computational algebra from λ-calculus algebra

Based on the operators within lambda calculus, application and abstraction, it is possible to develop an algebra whose group structure uses application and abstraction as binary operators. Application is defined as an operation between lambda terms producing a λ-term, e.g. the application of λ onto the lambda term a produces the lambda term λa. Abstraction incorporates undefined variables by denoting λx.t(x) as the function assigning the variable a to the lambda term with value t(a) via the operation ((λ x.t(x))a = t(a)). Lastly, an equivalence relation emerges which identifies λ-terms modulo convertible terms, an example being beta normal form.

Scott topology

The Scott topology is essential in understanding the topological structure of computation as expressed through the λ-calculus. Scott found that after constructing a function space using λ-calculus one obtains a Kolmogorov space, a

T _{o} topological space which exhibits pointwise convergence, in short the product topology.^[9] It is the ability of self homeomorphism as well as the ability to embed every space into such a space, denoted Scott continuous, as previously described which allows Scott's topology to be applicable to logic and recursive function theory. Scott approaches his derivation using a complete lattice, resulting in a topology dependent on the lattice structure. It is possible to generalise Scott's theory with the use of complete partial orders. For this reason a more general understanding of the computational topology is provided through complete partial orders. We will re-iterate to familiarize ourselves with the notation to be used during the discussion of Scott topology.

Complete partial orders are defined as follows:

First, given the partially ordered set D=(D,≤), a nonempty subset X ⊆ D is directed if ∀ x,y ∈ X ∃ z ∈ X where x≤ z & y ≤ z.

D is a complete partial order (cpo) if:

⋅ Every directed X ⊆D has a supremum, and:

∃ bottom element ⊥ ∈ D such that ∀ x ∈ D ⊥ ≤ x.

We are now able to define the Scott topology over a cpo (D, ≤).

O ⊆ D is open if:

1. for x ∈ O, and x ≤ y, then y ∈ O, i.e. O is an upper set.

1. for a directed set X ⊆ D, and supremum(X) ∈ O, then X ∩ O ≠ ∅.

Using the Scott topological definition of open it is apparent that all topological properties are met.

⋅∅ and D, i.e. the empty set and whole space, are open.

⋅Arbitrary unions of open sets are open:

Proof: Assume

U _{i} is open where i ∈ I, I being the index set. We define U = ∪. Take b as an element of the upper set of U, therefore a ≤ b for some a ∈ U It must be that a ∈ U _{i} for some i, likewise b ∈ upset(U _{i} ). U must therefore be upper as well since U _{i} ∈ U.

Likewise, if D is a directed set with a supremum in U, then by assumption sup(D) ∈

U _{i} where U _{i} is open. Thus there is a b ∈ D where b ∈ U _{i} \cap D \subseteq U \cap D . The union of open sets U _{i} is therefore open.

⋅Open sets under intersection are open:

Proof: Given two open sets, U and V, we define W = U∩V. If W = ∅ then W is open. If non-empty say b ∈ upset(W) (the upper set of W), then for some a ∈ W, a ≤ b. Since a ∈ U∩V, and b an element of the upper set of both U and V, then b ∈ W.

Finally, if D is a directed set with a supremum in W, then by assumption sup(D) ∈

U \cap V . So there is a ∈ U \cap D and b ∈ V \cap D . Since D is directed there is c ∈ D with a \le c, b\le c ; and since U and V are upper sets, c ∈ U \cap V as well.

Though not shown here, it is the case that the map

f: D → D ^{'} is continuous if and only if f(sup(X)) = sup(f(X)) for all directed X⊆D, where f(X) = and the second supremum in D ^{'} .

Before we begin explaining that application as common to λ-calculus is continuous within the Scott topology we require a certain understanding of the behavior of supremums over continuous functions as well as the conditions necessary for the product of spaces to be continuous namely

1. With

{f _{i}} _{i} \subseteq [D → D ^{'} ] be a directed family of maps, then f(x) = \cup _{i} f _{i(x)} if well defined and continuous.

1. If F

\subseteq [D → D ^{'} ] is directed and cpo and [D → D ^{'} ] a cpo where sup.

We now show the continuity of application. Using the definition of application as follows:

Ap:

[D → D ^{'} ] x D → D ^{'} where Ap(f,x) = f(x).

Ap is continuous with respect to the Scott topology on the product (

[D → D ^{'} ] x D → D ^{'} ) :

Proof: λx.f(x) = f is continuous. Let h = λ f.f(x). For directed F

\subseteq [D → D ^{'} ]

h(sup(F)) = sup(F)(x)

= sup

= sup

= sup(h(F))

By definition of Scott continuity h has been shown continuous. All that is now required to prove is that application is continuous when it's separate arguments are continuous, i.e.

[D → D ^{'} ] and D → D ^{'} are continuous, in our case f and h.

Now abstracting our argument to show

f:D x D ^{'} → D ^{''} with g = λ x.f(x,x _{0)} and d =λ x ^{'} .f(x ^{'} _{0 ,x} ) as the arguments for D and D ^{'} respectively, then for a directed X ⊆ Dg(\sup(X)) = f(\sup(X), x ^{'} _{0} ))

= f(sup((x,

x ^{'} _{0} ) | x ∈ X}))

(since f is continuous and) is directed):

= sup

= sup(g(X))

g is therefore continuous. The same process can be taken to show d is continuous.

It has now been shown application is continuous under the Scott topology.

In order to demonstrate the Scott topology is a suitable fit for λ-calculus it is necessary to prove abstraction remains continuous over the Scott topology. Once completed it will have been shown that the mathematical foundation of λ-calculus is a well defined and suitable candidate functional paradigm for the Scott topology.

With

f \in [D x D ^{'} → D ^{''} ] we define \check{f} (x) =λ y ∈ D ^{'} f(x,y)We will show:

(i)

\check{f} is continuous, meaning \check{f} ∈ [D → [D ^{'} → D ^{''} ]

(ii) λ

f.\check{f}: [D x D ^{'} → D ^{''} ] → [D → [D ^{'} → D ^{''} ] is continuous.

Proof (i): Let X ⊆ D be directed, then

\check{f} (sup(X)) = λ y.f(sup(X),y)

= λ y.

\sup _{x} (f(x,y))

=

\sup _{x} (λy.f(x,y))

= sup(

\check{f} (X))

Proof (ii): Defining L = λ

f.\check{f} then for F \subseteq [D x D ^{'} → D ^{''} ] directed

L(sup(F)) = λ x λ y. (sup(F))(x,y))

= λ x λ y.

\sup _{y} f(x,y)

=

\sup _{y} λx λy.f(x,y)

= sup(L(F))

It has not been demonstrated how and why the λ-calculus defines the Scott topology.

Böhm trees and computational topology

Böhm trees, easily represented graphically, express the computational behavior of a lambda term. It is possible to predict the functionality of a given lambda expression from reference to its correlating Böhm tree. Böhm trees can be seen somewhat analogous to

R where the Böhm tree of a given set is similar to the continued fraction of a real number, and what is more, the Böhm tree corresponding to a sequence in normal form is finite, similar to the rational subset of the Reals.

Böhm trees are defined by a mapping of elements within a sequence of numbers with ordering (≤, lh) and a binary operator * to a set of symbols. The Böhm tree is then a relation among a set of symbols through a partial mapping ψ.

Informally Böhm trees may be conceptualized as follows:

Given: Σ =

\perp \cup

Notes and References

1. Church 1934:90 footnote in Davis 1952
2. Turing 1936–7 in Davis 1952:149
3. Barendregt, H.P., The Lambda Calculus Syntax and Semantics. North-Holland Publishing Company. 1981
4. Barendregt, H.P., The Lambda Calculus Syntax and Semantics. North-Holland Publishing Company. 1981.
5. D. S. Scott. Models for the λ-calculus. Informally distributed, 1969. Notes, December 1969, Oxford Univ.
6. Gordon, M.J.C., The Denotational Description of Programming Languages. Springer Verlag, Berlin. 1979.
7. Scott, D. S. and Strachey, C. Toward a Mathematical Semantics for Computer Languages, Proc. Symp. on Computers and Automata, Polytechnic Institute of Brooklyn, 21, pp. 19 46. 1971.
8. G. Berry, Sequential algorithms on concrete data structures, Theoretical Computer Science 20, 265 321 (1982).
9. D. S. Scott. "Continuous Lattices." Oxford University Computing Laboratory August, 1971.