Topology on data types

We are following this text by Martín Escardó: https://www.cs.bham.ac.uk/~mhe/papers/entcs87.pdf

Idea

Semi-decidable (sub)sets behave like open sets:

• the empty set is semi-decidable,

• the whole set is semi-decidable,

• finite intersections are semi-decidable (perform the decision algorithms for each set one after the other. If an element is in the intersection then each will terminate in finite time, so the whole sequence will terminate in finite time.)

• arbitrary* unions are semi-decidable (perform the decision algorithms for each set in parallel and terminate as soon as one of the algorithms terminates. If an element is in the union then one of the algorithms will terminate in finite time and thus you know in finite time if the element is in the union.)

*at least countable

If we define open sets to be semi-decidable sets then computable partial functions are continuous functions.

Suppose f : X → Y is a computable partial function (it terminates in finite time with value f(x) if it is defined on x). Let V ⊆ Y be a semi-decidable set and let x ∈ X. If x ∈ f⁻¹(V), then f is defined on x and thus will terminate in finite time with value f(x). Then we apply the decision algorithm for V on f(x). This will terminate in finite time and say that f(x) is an element of V. Thus, chaining these two computations together, we have an algorithm for confirming in finite time that an element belongs to f⁻¹(V), so the pre-image is semi-decidable.

Continuous functions

We define the continuous functions to be the functions that are definable in the programming language that we use. In this case we use Haskell.

In Haskell we can define the element:

bot :: a

bot = bot

This represents a non-terminating computation and is an element of every data type.

We also define a data type corresponding to the Sierpinski space:

data S = T deriving (Show)

This data type has two elements: T and bot.

Open sets

Recall: in topology there is a one-to-one correspondence between open subsets of X and continuous functions from X to the Sierpinski space.

We translate this to define open sets on data types:

-- The type of open subsets of a

type Open a = a -> S

With this definition, the open sets are precisely the semi-decidable sets. For suppose you have a function f : a -> S for some data type a. Let x :: a. If x ∈ f⁻¹(T) then f will terminate with output T on x in finite time and thus we know that x is in the set. So f⁻¹(T) is semi-decidable.

Conversely, suppose U ⊆ X is a semi-decidable set. Then there exists an algorithm for confirming that an element lies in U that will terminate in finite time. Since Haskell is Turing complete, this algorithm can be represented in Haskell as a function from X to S.

Sanity check: there are three continuous functions from S to S (the same as the three continuous functions from Sierpinski to Sierpinski in topology).

-- Only terminates on T, not on bot

-- Characteristic function for {T}, so {T} is open

idS :: S -> S

idS x = x

-- Always terminates with T (even on bot)

-- Characteristic function for {T, bot}, so {T, bot} is open

projT :: S -> S

projT _ = T

-- Never terminates

-- Characteristic function for ∅, so ∅ is open

projBot :: S -> S

projBot _ = bot

{- Cannot define

invert :: S -> S

invert T = bot

invert bot = T -}

We cannot define a function that does not terminate on T but does terminate on bot. If we could, then we could solve the halting problem!

Any open subset that contains bot must necessarily contain the whole data type because if we have a function f :: a -> S that terminates on bot, then it cannot read the input (otherwise it would not terminate on bot), so it must be the function \_ -> T.

If f :: a -> b is continuous, then f⁻¹(V) is open for every open subset V of b.

Let V be an open subset of b. This means that we have a function g :: b -> S such that g v = T iff v ∈ V. Then for any x :: a we have: x ∈ f⁻¹(V) iff f(x) ∈ V iff g (f x) = T. So g . f is the characteristic map for f⁻¹(V) and it is continuous.

We make this into a definition in Haskell code.

preImage :: (a -> b) -> (Open b -> Open a)

preImage f g = g . f

Intersections

We use Sierpinski-valued conjunction to define intersections.

(/\) :: S -> S -> S

T /\ T = T

{-

The following hold automatically:

T /\ bot = bot

bot /\ T = bot

bot /\ bot = bot

-}

-- The intersection of two open sets is open

intersection :: Open a -> Open a -> Open a

u `intersection` v = \x -> u x /\ v x

Since binary intersections of open sets is open, any finite intersection of open sets is open.

Unions

In order to define unions of open sets we would need a disjunction operator (\/) :: S -> S -> S that satisfies:

T /\ T = T

T /\ bot = T

bot /\ T = T

bot /\ bot = bot

Such an operator must execute the computation of the left and the right hand side somehow in parallel. It is apparently possible to do in Haskell, but since we will not need unions that often, let us just suppose that we can extend the language with such a disjunction operation when we need it.

Given (\/), a countable union of open sets is open:

countable_union :: (Nat -> Open a) -> Open a

countable_union s = \x -> exists 0

    where exists i = s i x \/ exists (i+1)

Spaces

A space is just a subset of a data type. But we introduce the notion because we often want to talk about subsets of data types that are not definable in Haskell. For example, the space of natural numbers is the subset of non-divergent elements of the data type Nat. The Baire space is the subset of non-divergent elements of the data type Baire defined below.

-- We define Nat like this instead of recursively

-- for convenience

type Nat = Int

type Baire = Nat -> Nat

and the Cantor space is the subset of the Baire space, consisting of functions that take the value 0 or 1 on all non-divergent elements.

Relative continuity

If X and Y are subspaces of data types a and b then a function Φ : X → Y is (relatively) continous if there is at least one function f :: a -> b such that f restricted to X equals Φ. We do not care how f behaves outside X.

Let X be a subspace of data type a. Let U be a subset of X. U is open in X iff there is an open subset U' of a such that X ∩ U' = U. (Notice the similarity to subspaces of topological spaces.)

This follows from the definition of relative continuity: U is open in X iff there exists at least one function f :: a -> S such that f restricted to X equals the characteristic map of U. This means exactly that there exists an open subset U' of a such that X∩U' = U.

Discrete spaces

A subspace of a data type is discrete if the Sierpinski-valued equality map is continuous. For example, the space (not data type) of natural numbers is discrete:

equalN :: (Nat, Nat) -> S

equalN (m,n) = if m == n then T else bot

The Baire and Cantor spaces are not discrete because we cannot evaluate if two infinite sequences of natural numbers are equal in finite time.

In topology: we proved in the topology sessions that a topological space is discrete iff the diagonal (the set {(x,x) | x ∈ X}) is open. Translating this to our computational notion of openness we obtain exactly the definition above.

Sanity check: The natural numbers is a discrete space under the standard topology.

Hausdorff spaces

A subspace of a data type is Hausdorff if the Sierpinski-valued apartness map is continuous. For example, the Baire space (and therefore also the Cantor space) is Hausdorff:

apartBaire :: (Baire,Baire) -> S

apartBaire (s,t) = apart 0

  where apart i = if s i /= t i then T else apart (i+1)

In topology: we proved in the topology sessions that a topological space is discrete iff the diagonal is closed, i.e. its complement is open. Translating this to our computational notion of openness we obtain exactly the definition above.

Sanity check: the Cantor space is a Hausdorff space in ordinary topology, since it is a subspace of the real numbers, which is a Hausdorff space. (I assume the space of infinite sequences of natural numbers is also Hausdorff in ordinary topology..?)

Compact spaces

A subspace U of a data type a is compact if its universal quantification functional is continuous, i.e. if we can program a function

forallU :: (a -> S) -> S

such that forallU p = T iff p x = T for all x inline_formula not implemented U. Any finite set inline_formula not implementedof points is compact because we can program its universal quantification functional as follows:

forallX :: (a -> S) -> S

forallX p = p x1 /\ p x2 /\ ... /\ p xn

For any data type a, the space of all elements of a is compact because a predicate p :: a -> S returns T for all elements in a iff it returns T for bot. For one implication, suppose p bot = T. Then p cannot actually use the input to compute the output, because then p would never terminate since the input bot never terminates. So p must be the constant function that sends everything to T. On the other hand, if p x = T for every x :: a then in particular p bot = T.

Food for thought: is there any connection between the fact that any set containing bot is compact and the one-point compactification in ordinary topology, where you "add a point at infinity"?

A subset of the space of natural numbers is compact if and only if it is finite. For suppose that there is an infinite subset of the space of natural numbers that is compact. Since any infinite subset of natural numbers is in bijection to the natural numbers, this essentially means that the space of natural numbers is compact. Now, take any Turing machine and any input and construct the predicate p :: nat -> S that returns T on n if and only if the machine evaluated on the input has not halted at n steps. Then, since the natural numbers are compact, if the machine will never halt on the input, we will know that in finite time. Since we can determine for any Turing machine and any input that the machine will never halt, we have solved the halting problem.

Overt spaces

A subspace U of a data type a is overt if its existential quantification functional is continuous, i.e. if we can program a function

forsomeU :: (a -> S) -> S

such that forsomeU p = T iff p x = T for some x inline_formula not implemented U.

Overtness is a vacuous concept in classical mathematics, but not in constructive mathematics. You can read more about overtness here:

• https://ncatlab.org/nlab/show/overt+space

• https://mathoverflow.net/questions/165116/a-topological-concept-dual-to-compactness/165120#165120

Any r.e. set of natural numbers is overt in the language extended with the disjunction operator. If U is a r.e. subset of natural numbers, then we have a Turing machine that enumerates U. Since Haskell is Turing complete, we have a function f :: nat -> nat that enumerates U (U is in the image of f). Then we can construct the existential quanitification functional as follows:

forsomeU :: (nat -> S) -> S

forsomeU p = exists 0

	where exists i = p (f i) \/ exists (i+1)

An open subset of an overt space is overt. Suppose U is an overt subspace of data type a and V is an open subset of U, i.e. we have functions

forsomeU :: (a -> S) -> S

charV :: a -> S

such that forsomeU p = T iff p x = T for some x inline_formula not implemented U and charV x = T for all x inline_formula not implementedand charV x = bot for all x inline_formula not implemented. We can define the existential quantification functional as follows:

forsomeV :: (a -> S) -> S

forsomeV p = forsomeU $ p `intersection` charV

This function will return T if and only if there is some element in U that is mapped to T under both p and charV, i.e. if and only if there is some element in V that is mapped to T under p.

The Baire and Cantor spaces are overt in the language extended with the disjunction operator. Idea: if a predicate p :: Baire -> S returns T for some sequence, then it can only process a finite number of entries in the sequence before producing the output (otherwise it would never terminate). So we construct the existential quantification functional by checking the predicate on the (countable) set of sequences that are zero from some point on (for this we need the disjunction operator). Since p only processes a finite amount of input, this will eventually halt and then we know that p holds for some sequence.

Internal vs. external view of data

Before we can talk about compactness of the Cantor space we need to specify what we mean by an element of a data type. In the internal view we take the elements of a data type to be the equivalence classes of programs of that type. So the elements of a data type are the computable elements.

In the external view we allow non-computable elements of the data type. For example, in the external view, a sequence of natural numbers given by the user is seen as an element of the Baire data type. Such a sequence does not have to be computable.

Compactness of the Cantor space

Compactness of the Cantor space holds in the external view of data but not in the internal view.

We can view the Cantor space as an infinite binary tree, which we will call the Cantor tree, and an element of the Cantor space as an infinite path in this tree, by starting at the root and taking 0 to mean that we should go left and 1 to mean that we should go right.

Given any predicate p :: Baire -> S and sequence s in the Cantor space, if p halts on s, then it can only process a finite number of entries in s before producing the output. Let n be this number. This means that p will halt on any Cantor sequence that has the same n first entries as s. We can thus prune the Cantor tree from the n-th node in s seen as a path because p halts for all these infinite paths. We proceed to prune the tree like this for every Cantor sequence. If we have the external view of data, then the sequences range over all paths in the Cantor tree, so all paths in the resulting tree are finite. Therefore, by König's lemma, the tree is finite. We call the height of the pruned tree the uniform modulus of continuity. (This is a number that depends only on p, not on the input sequence.)

To check if p halts for all Cantor sequences, we thus only have to traverse the pruned tree. Since this is finite, we can do this in finite time. Hence the Cantor space is compact.

Note however: if we take the internal view of data, then we will not prune every path in the Cantor tree (since not every Cantor sequence is computable). The resulting tree is therefore not finite, so we cannot (necessarily?) traverse it in finite time.

Basic topology

We will now prove some basic results in topology. First we define a type for quantifiers.

type Quant a = (a -> S) -> S

A compact subspace of a Hausdorff space is closed. Let X be a subspace of data type a and let Q be a compact subspace of X, i.e. we have

apartX :: (a,a) -> S

-- for all x,y in X: apartX (x, y) = T iff x != y

forallQ :: Quant a

-- forallQ p = T iff p x = T for all x in Q

We can then construct the characteristic map of the complement of Q as follows:

complementQ :: Open a

complementQ x = forallQ (\y -> apartX (x, y))

since inline_formula not implemented if an only if inline_formula not implemented.

We can write a function that takes as input an apartness map and a universal quantification functional and returns the characteristic function of the complement:

compSubspOfHausClosed :: Quant a -> ((a, a) -> S) -> Open a

compSubspOfHausClosed forallQ apartX x = forallQ (\y -> apartX (x, y))

Dually, an overt subspace of a discrete space is open. Given functions

existsO :: Quant a

-- existsO p = T iff there is some x in O such that p x = T

equalX :: (a, a) -> S

-- for all x,y in X: equalX (x, y) = T iff x == y

we can define the characteristic map of O as follows:

charO :: Open a

charO x = existsO (\y -> equalX (x, y))

since inline_formula not implemented if and only if inline_formula not implemented.

We can also write this as a higher order function:

overtSubspOfDiscrOpen :: Quant a -> ((a, a) -> S) -> Open a

overtSubspOfDiscrOpen existsO equalX x = existsO (\y -> equalX (x, y))

If we have the disjunction operator then a closed subspace of a compact space is compact. Given the functions

forallX :: Quant a

-- forallX p = T iff p x = T for all x in X

complementF :: Open a

-- for all x in X: complementF x = T iff x not in F.

we can define

forallF :: Quant a

forallF p = forallX (\x -> complementF x \/ p x)

since p halts on every element of F iff for every element in X, p either halts on it, or it is in the complement of F.

Dually, an open subspace of an overt space is overt. We can define the following higher order function:

openSubspOfOvertOvert :: Quant a -> Open a -> Quant a

openSubspOfOvertOvert existsU charV p = existsU $ p `intersection` charV

since p halts on some element in V iff p halts on some element in U that is also in V.

The image of a compact set is compact. We can construct the following program:

imageOfCompIsComp :: (a -> b) -> Quant a -> Quant b

imageOfCompIsComp f forallQ p = forallQ (p . f)

It follows that in the external view of data: any image under a continuous function of the Cantor space in the natural numbers is finite (since it is compact and any compact subset of the natural numbers is finite.

The image of an overt subspace is overt. We can construct the following program:

imageOfOvertIsOvert :: (a -> b) -> Quant a -> Quant b

imageOfOvertIsOvert f existsQ p = existsQ (p . f)

The product of two compact spaces is compact. We can construct the following program:

prodOfCompIsComp :: Quant a -> Quant b -> Quant (a,b)

prodOfCompIsComp forallQ forallR p = forallQ (\x -> forallR (\y -> p (x,y)))

Dually, the product of two overt spaces is overt. We can construct the following program:

prodOfOvertIsOvert :: Quant a -> Quant b -> Quant (a,b)

prodOfOvertIsOvert existsQ existsR p = existsQ (\x -> existsR (\y -> p (x,y)))

The product of two discrete spaces is discrete. We can construct the following program:

prodOfDiscrIsDiscr :: ((a,a) -> S) -> ((b,b) -> S) -> ((a,b),(a,b)) -> S

prodOfDiscrIsDiscr equalA equalB ((x,y),(x',y')) = equalA (x,x') /\ equalB (y,y')

Dually, if we have the parallel disjunction operator, the product of two Hausdorff spaces is Hausdorff. We can construct the following program:

prodOfHausdIsHausd :: ((a,a) -> S) -> ((b,b) -> S) -> ((a,b),(a,b)) -> S

prodOfHausdIsHausd apartA apartB ((x,y),(x',y')) = apartA (x,x') \/ apartB (y,y')

If Q is compact and V is open then the set N(Q,V):={f :: a -> b | f Q ⊆ V} is open. We can construct the following program:

charNQV :: Quant a -> Open b -> Open (a -> b)

charNQV forallQ charV f = forallQ (charV . f)

If a set of open sets is compac then its intersection is open. We can construct the following program:

charInterQ :: Quant (Open a) -> Open a

charInterQ forallQ x = forallQ (\charX -> charX x)

If a set of open sets is overt then its union is open. We can construct the following program:

charUnionQ :: Quant (Open a) -> Open a

charUnionQ existsQ x = existsQ (\charX -> charX x)

If X is overt and Y is Hausdorff then the subspace X inline_formula not implemented Y of functions a -> b is Hausdorff. We can construct the following program:

apartXtoY :: Quant a -> ((b,b) -> S) -> (a -> b, a -> b) -> S

apartXtoY existsX apartY (f,g) = existsX (\x -> apartY (f x , g x))

If X is compact and Y is discrete then the subspace X inline_formula not implemented Y of functions a -> b is discrete. We can construct the following program:

equalXtoY :: Quant a -> ((b,b) -> S) -> (a -> b, a -> b) -> S

equalXtoY forallX equalY (f,g) = forallX (\x -> equalY (f x , g x))